Types in Tenet

Tenet doesn’t try to apply a single paradigm to all “things” that can be modeled by the language. For instance, in object-oriented languages, it’s common to claim that “everything is an object.” Instead, Tenet has a few broad categories of “things” that serve various purposes.

In Tenet, a value is defined by some properties:

The most important kind of “value” that these rules proscribe is a function value. The problem with function values is that the equality of two function values is a non-trivial attribute and, per Rice’s theorem, determining this in general is equivalent to solving the halting problem.

And the practical implementation is that any value can be placed in any variable, or stored within a record or collection.

Tenet has no null or undefined special values. Rather than shoe-horning various kinds of missing values into a generic null, it’s preferable to plainly state that the data is #missing, #corrupted, #blank, #lost or whatever meaningful label applies.

Another category is a block that:

These look like function values in other languages, but can’t be assigned to variables. That is, they aren’t first-class function values. The advantage is that blocks can guarantee that control flow in the block must always work: they are always used while the function is running, so it’s always meaningful to break out of a loop.

And we’d also dispute how “first-class” function values actually are when there’s no good definition of equality for them.

Three final categories are:

stator
The guts of an object: a stator defines some local state, it can respond to methods and update its state, but it's not allocated on the heap. A stator is also a hierarchical finite state machine.
capability
A mechanism to control side-effects, capabilities can be passed explicitly or implicitly to mark which functions can do things like perform IO or spawn threads. These are very similar to the effects algebra, but capabilities work a bit more smoothly with blocks.
object
Objects tie stators and capabilities and values together. As the description of stator suggests, objects are simply stators allocated on the heap. These are managed by an object capability, e.g. in a GC implementation, it may be the global GC. The object capability can also grant other capabilities to objects, allowing passing capabilities around while keeping track of their lifetime. While objects are allocated on the heap, they also have a value semantic as a unique ID of the object. The value semantic can't be overridden: equality of objects is always based on identity.

Value Types

Atomic Types

Container Types

Lists have a type [T], or List[T] in full. They are a homogeneous finite sequence of values of type T. A list value literal is written as [a, b, c, d], and the empty list is [].

Sets have a type Set[T]. They are a homogeneous finite set of values of type T. A set value literal is written as set\[a, b, c, d], and the empty set is set\[].

Note: the backslash is used to indicate the word set is not a regular variable name.

Maps have a type [K: V], or Map[K: V] in full. They are a finite mapping from keys of type K to values of type V. A map literal is written as [a: b, c: d], and the empty map is [:].

let numbers : [Int]     = [1, 2, 3]
let colors : Set[Color] = set\[#red, #blue]
let scores : [Str: Int] = ["alice": 95, "bob": 87]

Algebraic Types

Records

A record is a fixed collection of named fields with potentially different types. Record types are closed — two records are compatible only if they have exactly the same field names and compatible field types.

type Point = (x: Int, y: Int)
let p = (x: 3, y: 4)

Tagged Unions

A union is a discriminated sum type. Every member is a tagged value tag ~ variant and an expression #tag is shorthand for tag ~ (), meaning the variant is the unit record value.

type Result(T) =
    ok ~ T
  | #err

type Optional(T) = just ~ T | #nothing

Unions are order-independent within Tenet semantics.

Non-value Types

Block Argument Types

We can declare a block argument type in a type statement:

type Callback = { when: Time, msg: Str => Result(Str) }

These can’t be used in any value type expression. In particular, you can’t have a list of callbacks.

More commonly, though, block argument types can be directly shown as part of the function signature.

fun foreach-users(users: [User]) func: { user: User, number: Int => () } {
  let mut num = 0;
  for user in users {
    func(user: user, number: (num += 1));  
  }
}

do {
  foreach-users([user-1, user-2, user-3]) { user, number =>
    print-line("User number \(number) has name \(user.name).")
  }
}

Block types describe the argument names and types and the return type. Blocks aren’t normal values; they can’t be assigned to variables, but can only be constructed when passed to a function invocation.

Type Expressions

Type expressions appear in type definitions, function signatures, and annotations. In general, Tenet tries to make types homoiconic, that is, types usually look like the values they represent.

Special Types

Bottom (⊥)

The empty type, used internally during type inference.

Top (⊤)

This is used internally. In inference, we often need to find a common supertype of multiple types, and if this isn’t available, Top is a marker to indicate this.

Future / Deferred

The following are not part of the current version: