types are sets

the single idea that unlocks the whole type system.

the usual mental model

In most languages, a type is something your compiler enforces:

def greet(name: str) -> None: ...    # compile/check-time rule

The type exists in a different layer from the values. You can't say "is 42 a positive-int-less-than-100 between odd numbers?" because your type system doesn't let you express that kind of thing.

the zef mental model

42 | is_a(Int)           # True
'hi' | is_a(Int)          # False
42 | is_a(Any)           # True — Any is the universe

"Is this value a member of that set?" That's it. No static analysis phase. No generics infrastructure. Just sets.

set operations on types

Once you think of types as sets, the usual operators make sense:

IntOrString = Int | String            # union ∪
BoundedInt  = Int & (Z < 100)         # intersection ∩
NotString   = ~String                 # complement

Test them:

5 | is_a(IntOrString)               # True
'hi' | is_a(IntOrString)            # True
3.14 | is_a(IntOrString)            # False

50 | is_a(BoundedInt)               # True
999 | is_a(BoundedInt)              # False

refinement types — constraints as types

The Z placeholder lets you build predicates that are types:

Positive      = Int & (Z > 0)
Adult         = Int & (Z >= 18) & (Z < 120)
NonEmptyStr   = String & (Z | length > 0)
LongRunningID = String & (Z | length == 22)

Now you can filter, test, pattern-match with them:

ages = [15, 17, 20, 150, 99]
ages | filter(Adult) | collect    # [20, 99]

21 | match([
    (Adult,       'welcome in'),
    (Int,         'sorry kid'),
    (Any,         'what?'),
]) | collect

Z-expressions that return types

Here's the wild one. You can write a predicate as a normal-looking Python expression with Z, and it literally becomes a type:

InsideUnitSphere = (Z[0]**2 + Z[1]**2 + Z[2]**2 <= 1)

[0.2, 0.5, 0.8] | is_a(InsideUnitSphere)   # True

points | filter(InsideUnitSphere) | collect

That's a 1-line, in-lined, runtime-checkable, composable, first-class type.

container types

Collection types can be refined by element type:

[1, 2, 3] | is_a(Array)                # True
[1, 2, 3] | is_a(Array[Int])           # True
[1, 3.14] | is_a(Array[Int])            # False
[1, 3.14] | is_a(Array[Int | Float])   # True

And tuple-shaped:

IntAndString = Tuple[Int, String]
[1, '🌿'] | is_a(IntAndString)      # True
[1, 2] | is_a(IntAndString)         # False

And dict-shaped:

IntKeyedStr = Dict[Int, String]
{1: 'a', 2: 'b'} | is_a(IntKeyedStr)     # True
{1: 'a', 2: 2} | is_a(IntKeyedStr)       # False

refined entity types

The most expressive form. Put constraints on entity fields:

Adult = ET.Person[
    'name': String,
    'age':  Int & (Z > 18),
    ...                          # allow other fields
]

jack  = ET.Person(name='Jack', age=21)
alice = ET.Person(name='Alice', age=10)

jack  | is_a(Adult)       # True
alice | is_a(Adult)       # False

"what is the type of 42?"

In Zef, this question has many correct answers. A value of 42 is a member of all these sets:

Any
Int
Int32
Int & (Z > 0)
Int & (Z == 42)
{42, 100, 1000}

There's no anointed "the" type. If you really need one answer, Zef provides two:

42 | layout_type | collect       # Int32
42 | primary_type | collect      # Int
UInt8(42) | layout_type | collect # UInt8
UInt8(42) | primary_type | collect # Int  — same category

recap

• A type is a set of values.
• Membership is checked at runtime with is_a(T).
• Use |, &, ~ to combine types.
• Use Z to turn any predicate into a type.
• Use Array[T], Dict[K, V], Tuple[A, B] for containers.
• Use ET.Name[...] for refined entity types.
• Use layout_type or primary_type if you really need one answer.

Email = String & ('@' | Z.contains)   # rough approximation
Age   = Int & (Z >= 0) & (Z <= 150)
User  = Dict['email': Email, 'age': Age, ...]

Next up: entities — ET, UIDs, and those cute 🍃 prefixes. →