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

Operator Example Meaning
~ tag ~ a construct a tagged value with tag tag and variant a
# #tag construct a tagged value with tag tag and variant ()
. a.attr look up attr in the record 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, positive
++ a ++ b concatenation
- 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
func func() {} 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) -> 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.

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

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 Record 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*
Record Record* Record* selects
Slots Record* 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 Record 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*
Record Record* 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: