Reference

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

(Somewhat out of date compared to the spec.)

Expressions

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

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) -> Record[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[Record[arg=A...]]
unzip(List[Record[arg=A...]]) -> Record[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, ...]
• Record[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, ...]

Slots

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

Antiunion

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.

Overloads

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.

Type union

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

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 $A \odot B$ means A is incompatible with B.

These laws relate type relational operators and the unifying operators:

$$\begin{aligned} A = B \implies& A = B = A \cup B = A \cap B \\ A \supset B \implies& A \cup B = A \\ \wedge& A \cap B = B \\ A \subset B \implies& A \cap B = A \\ \wedge& A \cup B = B \\ A \odot B \implies& A \cup B \supset A \\ \wedge& A \cup B \supset B \\ \wedge& A \cap B \subset A \\ \wedge& A \cap B \subset B \end{aligned}$$