# Reference

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

## Expressions

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, ...]

### Slots

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.

### 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.

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

These laws relate type relational operators and the unifying operators: