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

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.

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

These laws relate type relational operators and the unifying operators: