Type Expressions

Type expressions are used both in type definitions, in function signatures, and in annotated assignments.

Terminology note: in Tenet, a function takes “arguments” while a type takes “parameters.”

Builtin types

The builtin types come in three flavors: atoms, containers and algebraic types. These are the building blocks of user-defined types.

Atom types

The atom types are simple names:

type My_Int := Int
type My_Str := Str
type My_Bool := Bool

func my_function(x: Int, msg: Str) -> Int {
    ...
}

There are restrictions on the use of Bool as detailed in Boolean.

Future: restricted types will add parameters to Int and Str, e.g. Int[min: 0, max: 2^32 - 1].

Container Types

The container types are defined using homoiconic constructors that mimic the literal constructors:

type List_of_Ints := [Int]       ;; meaning List[Int]
type Set_of_Str := {Str}         ;; meaning Set[Str]
type Map_of_List := {Str: [Int]} ;; meaning Map[Str, List[Int]]

let my_ints := [1, 2, 3]
let my_set := {4, 5, 6}
let my_map := {"key": [7, 8, 9]}

Note that [Int, Str] is not allowed, but [#apple | #banana | #cherry] is.

Algebraic Types

Tenet has three algebraic types: unions, records and functions.

Enums are a special case of unions, strictly #tag_name is the same as tag_name ~ ().

As with containers, algebraic types are expressed using a homoiconic form that mimics the literal forms. The following blocks demonstrate:

;; Means Record[]
type Unit := ()
let unit := ()

;; Means Union[ok: Int, fail: Unit]
type Pass_Fail := ok ~ Int | #fail
let pass := ok ~ 3

;; Means Map[Enum[apple, banana, cherry], Str]
type Map_of_Enums := {#apple | #banana | #cherry: Str}
let map_of_enums := {#apple: "red delicious", #banana: "yellow fruit"}

;; Means Record[hour: Int, minute: Int, second: Int]
type Time := (hour: Int, minute: Int, second: Int)
let time := (hour: 7, minute: 35, second: 23)

type Callback := Func(when: Time, msg: Str) -> Pass_Fail
;; This function's type is inferred as Func(when: Time, msg: Str) -> #fail
;; Functions are covariant on their return type, so it is a Callback.
func callback(when: Time, msg: Str) {
    return #fail
}

Union types

All user-defined unions are tagged unions.

Tagged union types are expressed as a union, the | operator, of tagged types, through the ~ operator. All types the | operator is applied to must be tagged types. A tagged type by itself is promoted to a union. Unions declared in other types can not be combined with the | operator.

type Valid := a ~ Int | #b
type Also_Valid := c ~ Str
type Invalid := Int | Str | #b
type Also_Invalid := Valid | Also_Valid

Tenet unions are order-independent within Tenet semantics. For purposes of encoding:

Syntactically, the | operator is commutative and associative. Unions of unions may be declared through parentheses.

type Union_of_Unions :=
   a ~ (
      b ~ B            |
      c ~ (d ~ D | #e) |
      f ~ F
   ) | g ~ G
let uou_vals = [a~b~1, a~c~d~"two", a~c~#e, a~f~3, g~[4]]

type Simply_Flat := (#a | #b) | (#c | #d) | #e
type Same_As     := #a | #b | #c | #d | #e

let flat_vals = [#a, #b, #c, #d, #e]