Math builtins

The sign function finds the sign of a value, has the signature sign(Int) -> Int and is a total function.

The abs function finds an absolute value and has the signature abs(Int) -> Int and is a total function. As with unary minus, implementations using fixed two’s complement integer representations must ensure that they raise a signal if the absolute of the smallest negative value can’t be represented with a positive value.

The sum function sums the values in a list or set of integers. It is a total function. It returns 0 for empty containers. It has two overloads:

The product function calculates the product of values in a list or set of integers. It is a total function. It returns 1 for empty containers. It has two overloads:

Division and modulo functions

Host lanaguages have differing standards for division and modulo. The native mode in Tenet is floor division as it is both widely used and mathematically sound. However, other modes of division are useful, but tricky to implement. All modes guarantee that .

Mode Definition Functions
Floor floor_div, floor_mod, floor_divmod
Ceiling ceil_div, ceil_mod, ceil_divmod
Truncated trunc_div, trunc_mod, trunc_divmod
Euclidean euc_div, euc_mod, euc_divmod

The following helper functions are required:

Helper Meaning Definition In C Semantics
Sign of
Signs differ
Signs are equal

Reference implementations of the various division and modulo modes are below. is the base floor division or floor modulo function.

Mode Division from floor div Modulo from floor mod

Below, is the base truncated division or truncated modulo. Note that some host languages use truncated division but floor modulo.

Mode From truncated div From truncated mod

Each divmod function calculates division and modulo simultaneously and has the signature divmod(Int, Int) -> {div: Int, mod: Int}. It is equivalent to the expression {div: a // b, mod: a % b}. It is undefined when b is 0 and raises Div_By_Zero.


The len builtin is a total function, and returns the length of the container. It has the overloads:

The sort builtin is a total function, and returns a new list in sorted order according to the canonical ordering of the container elements. An invariant is that len(sort(x)) == len(x). It has the overloads:

The reverse builtin has the signature reverse(List[T]) -> List[T], is a total function, and returns a new list in reverse order. An invariant is that reverse(reverse(x)) == x.

The min and max builtins are partial functions; they are undefined when the container is empty and raise Empty. Otherwise return the least or greatest elements of the container, sorted by canonical ordering. They have the following overloads:

Possible feature: partial_sort for lists.

Sorting that encounters functions could return a partial ordering. Sorting such a list must preserve the original order of elements. Thus, in sorting a list [c~fun_a, a~fun_c, a~fun_b], the algorithm would return [a~fun_c,a~fun_b, c~fun_a] as the tag symbols are sorted first, and the variants present a singleton FUNCTION collation value.

The keys function has the signature Eq K ::: keys(Map[K, V]) -> Set[K] and is a total function. It returns the keys of a map and has the invariants len(keys(x)) == len(x) and x && keys(x) == x.

The values function has the signature Eq K ::: values(Map[K, V]) -> List[V] and is a total function. It returns the values of a map in order of their keys, using canonical ordering.

The merge function has the signature Eq K ::: merge(Map[K, V], Map[K, V]) -> Map[K, V] and is a total function. It is equivalent to:

func merge(a: [K: V], b: [K: V]) -> [K: V] {
    return (a -- keys(b)) || b

The inverse function has the signature Eq K, V ::: inverse(Map[K, V]) -> Map[V, K] and is a partial function. It attempts to create a inverse mapping of values to keys. If two values map to the same key, it raises Key_Conflict.


This version of Tenet is obscures the underlying implementation of sets by requiring sorting to extract a set to a list. The details of the canonical ordering are:


Two functions are equal iff they have the same signature (type) and for all inputs they return the same outputs. This may be decidable given the way Tenet functions are limited, but if we later add functions that aren’t comparable, we’d have two kinds of functions which would be worse.

And it’s not worth it, at this time, to add a second “identity” based equality just for functions. They are more of an opaque type.

Lexical ordering of a collation is partial and application specific. To guarantee it is canonical would require bundling the collation table with the build artifiacts.


The set relational builtins have the signature Eq T ::: is_op(Set[T], Set[T]) -> Bool and are total functions.

The proper superset comparison holds that is_super(a, b) iff a -- b != {} and b -- a == {}.

The proper subset comparison holds that is_sub(a, b) iff a -- b == {} and b -- a != {}.

The improper superset comparison holds that is_sup_eq(a, b) iff is_super(a, b) or a == b

The improper subset comparison is defined as is_sub_eq(a, b) iff is_sub(a, b) or a == b