Special or missing types

This section is to avoid confusion by explicitly identifying types that are either not available to users, or simply not part of the Tenet type system at all.

There are four kinds of types in Tenet:

Type constraints declare possible types that could apply, and the inference engine must solve the network of constraints to specify single types for all global and local names.

Null

There is no null, undefined, missing or other such value, or any type in Tenet that contains such a value.

Users may trivially define enums #null, #undefined, #missing, but these are regular values with semantics consistent with all other enums.

Users may also define an Option or Maybe type as #nothing | just ~ Type. These are described under Unions.

In languages with null or undefined values, these must be prohibited as inputs to generated functions, and never returned as outputs.

A compiler may exploit nulls to compactly represent values internally. For instance, a list homomorphic to the form [#nothing | just ~ Type] might internally be represented as an array of Type, translating nulls to #nothing and other values to just~value.

Comparable constraint

The comparable constraint is used by builtin functions. It is depicted in this specification as Eq T ::: T where T on the right-hand side is typically a more complex type expression.

It means that T is not a function type, nor does any parameter directly or indirect contain a function type.

Sets and map keys must be comparable.

Undiscriminated union constraint

A union constraint Or[T1, T2, ..., TN] indicates that the real type could be one of its parameters. It is used in type inference and is not accessible to users.

The constraint Or[T] is equivalent to T. The constraint Or[] is the definition of Bottom.

An overloaded builtin function’s type is expressed as a union constraint. For example, the len builtin has the signature:

Or[
    Func(val: Str[T1]) -> Int,
    Func(val: List[T2]) -> Int,
    Func(val: Set[T3]) -> Int,
    Func(val: Map[T4, T5]) -> Int
]

Bottom

Bottom is a type constraint. It is theoretically the empty type that is a subtype of all types. It is represented here as UP TACK . It is also equivalent to Or[].

Bottom does not have any values, which implies:

  1. As an argument type, it indicates a function can’t be called. This simply means no function can be declared that accepts bottom as any value.

  2. As a return type, it indicates a function must fail. Tenet is a total language, so this is disallowed.

  3. As a type parameter, it indicates a container is empty. The empty list is an example of parameterizing a type over Bottom. For example:

[1, 2, 3] ++ []

In type inference, we have [Integer] ++ [], but the signature of ++ is [T] ++ [T] -> [T]. To solve this, the common T that is a supertype of both Integer and is Integer.

Another example, the list indexing operator has the signature [T][Integer] -> T, and when T is ⊥, we see that it is returning Bottom and must therefore fail. The compiler must thus disallow the expression [][x].

Because host languages rarely support Bottom, Tenet doesn’t make it an exportable type. These statements are thus valid within a module:

let x := []
func y() {
    return []
}

However, neither can be exported. The name x has the type List[] and y has the type Func() -> List[]. These can be made exportable by specifying a type signature:

let x : [Int] := []
func y() -> [Int] {
    return []
}

Boolean

Boolean is a non-exportable type, referred to in this documentation as Bool. Boolean is a bound enumeration of true and false. As a non-exportable type, boolean values have specific restrictions:

Symbols

The section on Identifiers describes the rules around identifiers used in various domains.

Symbols are an internal type used by unions, records, and local variables. Essentially, any identifier in the source is a symbol.

No “Symbol” type is accessible to users. The rules for identifiers are consistent when distinguishing between variables, values and types. Further, when a canonical ordering is implemented, Unions and Records are ordered according to these rules.

Open Record

The Record type is closed, meaning that there is no type relationship between Records with differing slots. Thus (a: Int, b: Int) is entirely disjoint to (a: Int, b: Int, c: Int).

In contrast, the Open Record constraint is a type constraint that does have such a relation. An Open Record is represented as either (slot1: Type1, slot2: Type2, slotN: TypeN, ...) where the ellipsis is a literal, or Open[slot1: Type1, slot2: Type2, slotN: TypeN].

There are several uses for Open Record in type inference.

Slot access

The expression record.slot is a slot access parametric operation with the signature (slot: T, ...).slot -> T. The type expression (slot: T, ...) indicates that any Record type that has a slot named slot is a valid type for record.

Destructuring

The left-hand side of an assignment let (slot1, slot2, slotN) := value has the type (slot1: T1, slot2:T2, slotN: TN, ...). Consider the transformation:

;; Destructuring
let (slot1, slot2) := value

The constraint (slot1: T1, slot2:T2, ...) is inferred from the left-hand side of the destructuring assignment.

;; Transformed destructuring
slot1 := value.slot1
slot2 := value.slot2

In the transformed version,the types (slot1: T1, ...) and (slot2: T2, ...) describe the constraints inferred from the right-hand sides of the transformed assignments. As value must satisfy both constraints, the overall constraint is the intersection of those two constraints. As described in type algebra, this evaluates to (slot1: T1, slot2:T2, ...).