These are some tables for (mostly my) reference of operators, keywords, etc.


While some of the details of builtins are still in flux, Tenet has these operators:

Operator Example Meaning
~ tag ~ a construct a tagged value with tag tag and variant a
. a.attr look up attr in the tuple a
? a ? tag assert a has tag tag and get the variant
* a * b multiplication
// a // b floor division
% a % b modulo
+ a + b, +a addition or concatenation, positive
- a - b, -a subtraction and negation
== a == b equality
!= a != b inequality
> a > b greater than
< a < b less than
>= a >= b greater than or equal to
<= a <= b less than or equal to
in a in b member of
not in a not in b not a member of
not not a boolean negation
and a and b boolean conjunction
or a or b boolean disjunction
xor a xor b boolean exclusive disjunction
eqv a eqv b boolean equivalence
imp a imp b boolean implication
-> () -> a lambda expression
| a | b guard expression
union a union b set or map union (possibly)
inter a inter b set or map intersection (possibly)
diff a diff b set or map difference (possibly)

Internal functions implementing operators

Proposed type signatures for internal functions.

UnMinus(Int) -> Int
UnPlus(Int) -> Int
UnNot(Bool) -> Bool
BinTimes(Int, Int) -> Int
BinFloorDivide(Int, Int) -> Int
BinDivide(Int, Int) -> Bottom
BinModulo(Int, Int) -> Int
BinPlus(Int, Int) -> Int
       (Str, Str) -> Str
BinMinus(Int, Int) -> Int
BinEquals(E, E) -> Bool, E is Equatable
BinNotEqual -- same
BinLessThan(Int, Int) -> Bool
BinLessEqual := same
BinGreaterThan := same
BinGreaterEqual := same
BinIn(Str, Str) -> Bool
     (E, Set[E]) -> Bool, E is Equatable
     (K, Map[K, _]) -> Bool, K is Equatable
BinNotIn := same
BinUnion(Set[E], Set[E]) -> Set[E], E is Equatable
        (Map[K, V], Map[K, V]) -> Map[K, V]], K is Equatable
BinIntersect := same
BinDiff(Func[Set[E], Set[E]) -> Set[E]
       (Map[K, V], Map[K, V]) -> Map[K, V]
       (Map[K, V], Set[K])-> Map[K, V]
BinAnd(Bool, Bool) -> Bool
BinOr(Bool, Bool) -> Bool
BinXor(Bool, Bool) -> Bool
BinEqv(Bool, Bool) -> Bool
BinImp(Bool, Bool) -> Bool

Special functions

GetIndex := Overloads[Func[Int, List[E]] -> E,
                      Func[K, Map[K, V]] -> V]
GetSlot(slot, Slots[slot: S]) -> S
GetVariant(tag, Union[tag ~ V]) -> V
SetSlot(slot, Slots[slot: S], S) -> Slots[slot: S]
SetIndex := Overloads[Func[Int, List[E], E] -> List[E],
                      Func[K, Map[K, V], V] -> Map[K, V]]
SetVariant(tag, Union[tag ~ V], V) -> Union[tag ~ V]

ForLoop(Func[__iter__:I, __accum__:A] -> Union[cont~A, stop~A], List[I], A) -> A
WhileLoop(Func[__accum__:A] -> Union[cont~A, stop~A], A) -> A
GuardExpr(T, T) -> T
Failure() -> T

Builtin functions

abs(Int) -> Int
chr := Int -> Str
count := Overloads[Func[List[E], E] -> Int, Func[Set[E], E] -> Int]
divmod(Int, Int) -> Tuple[div: Int, mod: Int]
index := Overloads[Func[Str, Str] -> Int, Func[List[E], E] -> Int]
len := Overloads[Func[Str] -> Int, Func[List[Top]] -> Int, Func[Set[Top]] -> Int]
lower(Str) -> Str
min := Overloads[List[Int] -> Int, Set[Int] -> Int]
max := same
sum := same
ord(Str) -> Int
range(Int, Int, Int) -> List[Int]
upper(Str) -> Str
zip(arg=List[A]...) -> List[Tuple[arg=A...]]
unzip(List[Tuple[arg=A...]]) -> Tuple[arg=List[A]]

Type assertions

Broadly, type assertions are either concrete or special. An assertion is concrete if its head is concrete and all parameters are concrete.

The concrete assertion heads are:

  • Integer
  • String
  • List[E]
  • Set[E] where E is equatable
  • Map[K, V] where K is equatable
  • Union[tag: V, ...]
  • Tuple[slot: A, ...]
  • Function[arg: E, ...] -> R

A type is equatable if there exists a well-defined equality for it. No Function type is equatable, and a parametric type is equatable iff all parameters are equatable.

Special assertions are not user-visible, and if type inference infers a special assertion, it has failed. The special assertions are:

  • Slots[slot: A, ...]
  • Antiunion[tag: V, ...]
  • Overloads[A, B, C, ...]


A slots type represents all possible tuples that have at least the attributes represented. Slots are used to make assertions about the result of getting or assigning an attribute of a tuple.


An antiunion is used to determine the type of the subject of a switch over possible values of a union within the default case. So Antiunion[foo: Top, bar: Top] asserts the type is any type that does not have the tags foo or bar.


Certain primitives may be overloaded. An Overloads assertion is an implicit union of disjoint types. Thus, + has the signature Overloads[Function[left: Integer, right: Integer] -> Integer, Function[left: String, right: String] -> String]

Type operations

We need some rules to handle type inference, and these are built on internal type primitives.

Type intersection

Here, blanks are Bottom as it’s the notional subtype of all types.

↓ inter → Integer String List Map Set Union Antiunion Tuple Slots Function Overload
Integer Integer selects
String String selects
List List* selects
Map Map* selects
Set Set* selects
Union Union* Union* selects
Antiunion Union* Antiunion* selects*
Tuple Tuple* Tuple* selects
Slots Tuple* Slots* selects*
Function Function* selects
Overload selects selects selects selects selects selects selects* selects selects* selects Overload*

Type union

Here, blanks are Top as it’s the notional supertype of all types.

↓ union → Integer String List Map Set Union Antiunion Tuple Slots Function Overload
Integer Integer absorbs
String String absorbs
List List* absorbs
Map Map* absorbs
Set Set* absorbs
Union Union* Antiunion* absorbs
Antiunion Antiunion* Antiunion* absorbs*
Tuple Tuple* Slots* absorbs
Slots Slots* Slots* absorbs*
Function Function* absorbs
Overload absorbs absorbs absorbs absorbs absorbs absorbs absorbs* absorbs absorbs* absorbs Overload*

Laws of relational operators and unifying operators.

Types behave much like sets and I generally use the analogous set operators to represent type operators, except means A is incompatible with B.

These laws relate type relational operators and the unifying operators: