Skip to main content

Zef Value Types

Not all type systems are equal. One perspective on types is to distinguish between representation types and logic types.

Representation Types

In languages like C, one important part of a variable's type is to tell the compiler how to represent the data and how to read it. Given the address of a variable, the representation type and its declaration contains the context how to make sense out of the bit sequence starting at that location.

Logic Type

How to concretely interpret a sequence of bits is not the only role of a type and this aspect moves to the background in languages with more advanced type systems. Examples are Idris, Haskell, OCaml and Typescript.

Here Types can be seen much more as sets: specifically sets of things that fulfill certain constraints. Using types allows for a concise syntax that is

  1. easy and powerful to combine (unions, intersections, negations, differences)
  2. humanly readable - especially in composite form

Structural Typing

The Zef Type System itself is structural: the types themselves obey value semantics are not considered to have an identity.

Let's look at an example of defining a composite type on the fly:

PositiveInt = Int & Is[lambda x: x>0]    # & denotes intersection  

Is is a wrapper function that takes an arbitrary predicate function (of one argument) and returns a ValueType. This type declaratively denotes the set of all things for which the predicate function returns True.

Overview of Zef Types

!ZefDoc - Zef Value Types 2022-10-16 08.28.16.excalidraw
related: ZefDoc - Ref Types vs UIDs

Typing in Native Python

Zef's type system is semantically similar the path that Python started going down recently. This also applies to the semantics of subtyping.


In normal Python Dict can be understood to represent the set of all instances of dictionaries.
Using the square brackets [...] after a type specifies additional constraints, i.e. the resulting expression refers to a subset of elements as compared to the original expression without the [...]. Some examples:

List            # the set of all lists in Python, e.g. [1. 'hello', True]  
List[int] # lists that contain only ints

Dict # all dictionaries
Dict[str, int] # all dicts for which all keys are strings and all values are ints

Constructing Types

Combining Existing Types
# suppose T1 and T2 are ValueTypes  

T3 = Union[T1][T2]
T3 = T1 | T2 # shorthand

T4 = Intersection[T1][T2]
T4 = T1 & T2 # shorthand

T5 = Complement[T1] # logical complement: everything but this
T5 = ~T1 # shorthand
Wrapping a Predicate Function
Evens = Is[lambda x: x%2==0]  
Pattern Operator
# T6 denotes the set of all dictionaries for which *all* of the following hold:  
# 1. `x` is a key and the associated val is an Int
# 2. `y` is a key
T6 = Pattern[{
'x': Int,
'y': Any

{'x': 42, 'y': 'hello'} | is_a[T6] # True
{'x': 42} | is_a[T6] # False: no 'y' key
{'x': hi, 'y': 'hello'} | is_a[T6] # 'x' val wrong type

# ok to have more
{'x': 42, 'y': 'hello', 'z': True} | is_a[T6] # True

We can also use the Pattern operator for Lists

T7 = Pattern[(Int, Int, String)]  
(4, 5, 'hello') | is_a[T7] # True
(4, 5, 'hello', 'hi') | is_a[T7] # True: can be longer


Graph Pattern Matching

RP[Z, RT.ReleaseYear, {1996, 1997}]  

# Z indicates the position of the "subject": which thing are we talking about?


Builtin Types