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

• sum(List[Int]) -> Int
• sum(Set[Int]) -> Int

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:

• product(List[Int]) -> Int
• product(Set[Int]) -> Int

#### Division and modulo functions


Mode Definition Functions
Floor $\lfloor \frac{n}{d} \rfloor$ floor_div, floor_mod, floor_divmod
Ceiling $\lceil \frac{n}{d} \rceil$ ceil_div, ceil_mod, ceil_divmod
Truncated $\trunc{} \frac{n}{d}$ trunc_div, trunc_mod, trunc_divmod
Euclidean $\sign{} e \lfloor \frac{n}{\abs{d} } \rfloor$ euc_div, euc_mod, euc_divmod

The following helper functions are required:

Helper Meaning Definition In C Semantics
$\sign{} x$ Sign of $x$ $\sign{} x$ $(x > 0) - (x < 0)$
$\nzero{} x$ $x \neq 0$ $\abs{\sign{}x}$ $x \neq 0$
$\isneg{} x$ $x < 0$ $\nzero{} (x - \abs{x})$ $x < 0$
$\dsigns{} (a, b)$ Signs differ $\nzero{} (\sign{} a - \sign{} b)$ $\sign{} a \neq \sign{} b$
$\esigns{} (a, b)$ Signs are equal $1 - \dsigns{}(a, b)$ $\sign{} a = \sign{} b$

Reference implementations of the various division and modulo modes are below. $f(n, d)$ is the base floor division or floor modulo function.

Mode Division from floor div Modulo from floor mod
Floor $f(n, d)$ $f(n, d)$
Ceiling $-f(-n, d)$ $f(n, d) - \nzero{}f(n, d) \cdot b$
Truncated $f(\abs{n}, \abs{d}) \cdot \sign{} n \cdot \sign{} d$ $\nzero{} f(n, d) \cdot (f(n, d) - (\dsigns{}(a, b) \cdot b)$
Euclidean $\sign{} d \cdot f(n, \abs{b})$ $f(n, d) + \isneg{} f(n, d) \cdot \abs{d}$

Below, $t(n, d)$ 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
Floor $t(n + \dsigns{}(n, d) \cdot (\sign{} d - d), d)$ $t(n, d) + \nzero{} t(n, d) \cdot \dsigns{}(n, d) \cdot d$
Ceiling $-t(n + \esigns{}(n, d) \cdot (d - \sign{} d), -d)$ $t(n, d) - \nzero{} t(n, d) \cdot \esigns{}(n, d) \cdot d$
Truncated $t(n, d)$ $t(n, d)$
Euclidian $\sign{} d \cdot t(n + \isneg{} n \cdot (1 - \abs{d}), \abs{d})$ $t(n, d) + \isneg{} t(n, d) * \abs{d}$

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.

### Containers

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

• len(List[T]) -> Integer returns the length of a list
• Eq T ::: len(Set[T]) -> Integer returns the cardinality of a set
• Eq K ::: len(Map[K, V]) -> Integer returns the cardinality of a map

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:

• Eq T ::: sort(List[T]) -> List[T]
• Eq T ::: sort(Set[T]) -> List[T]
• Eq K ::: sort(Map[K, V]) -> List[(key: K, val: V)]

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:

• Eq T ::: min(List[T]) -> T
• Eq T ::: min(Set[T]) -> T
• Eq T ::: max(List[T]) -> T
• Eq T ::: max(Set[T]) -> T

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.

#### Ordering

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:

• Integers are ordered as per the relational operators.

• Strings are naïvely ordered lexically by codepoint.

• Lists are ordered lexically by their contents.

• Lists are orderable iff their elements are orderable.

• Sets are ordered lexically by their sorted elements.

• Maps are ordered as though the items are sorted into lists of ordered pairs of (key, value), and then compared lexically.

• Maps are orderable when both key and value types are orderable.

• Unions are ordered first by tag symbol and then by variant.

• Unions are orderable if all variant types are orderable.

• Records are compared lexically by attributes in canonically sorted order.

• Note that records must be the same type to compare, and two records with different attributes have no common supertype.

• Records are orderable if all attributes are orderable.

• Functions are not orderable, nor is any value that contains or could contain a function.

Rationale:

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.

### Relational

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