Standard operators

Arithmetic operators

Addition has the signature Int + Int -> Int and is a total operator. It is required to be associative and commutative. Given c := a + b, the postcondition when the signs of a and b are the same is that .

Specifically, suppose an implementation stored integers in a 4-bit two’s complement register that can represent -8 through 7 inclusive. If processing 5 + 5, rather than returning -6 the compliant action is to signal a representation failure.

The unary prefix operator + a has the signature + Int -> Int. It is an identity operation, required to be equivalent to 0 + a.

Subtraction has the signature Int - Int -> Int. It is required that a - b is equivalent to a + -b, and must uphold the restrictions placed on addition.

The unary prefix operator - a has the signature - Int -> Int. It is required to be equivalent to 0 - a.

Note that two’s complement representations have an asymmetric representation of negative numbers. In our 4-bit example, the implementation may not claim that - (-8) = -8; again the compliant action is to signal a representation failure.

Multiplication has the signature Int * Int -> Int. It is required to be associative and commutative. As with addition, multiplication must not return incorrect values on overflow.

Floor division and modulo have the signatures Int // Int -> Int and Int % Int -> Int respectively. Floor division a // b is defined as .

The following equations relate floor division and modulo:

In these equations, it is guaranteed must have the same sign as . For example, when determining whether a number is odd or even, x % 2 will always return 0 or 1, even when x is negative.

Both operators are partial, being undefined when the divisor is 0 and thus raising Div_By_Zero.

All binary integer operators have assignment variants:

a += b
expands to a := a + b
a -= b
expands to a := a - b
a *= b
expands to a := a * b
a //= b
expands to a := a // b
a %= b
expands to a := a % b

Static analysis: issue warnings for these operations

no-ops
a += 0, a *= 1, a //= 1
constant results
a *= 0, a -= a, a += -a, a %= 1
constant or bottom results
a //= a, a %= a
always bottom
a // 0, a % 0

Concatenation operators

String concatenation has the signature Str ++ Str -> Str. The concatenation c := a ++ b holds that c is equivalent to constructing a string from the concatenation of the sequences of codepoints of a and b. Associativity must be guaranteed such that (a ++ b) ++ c == a ++ (b ++ c). Identity must be guaranteed such that "" ++ x == x ++ "" == x.

Fixers: recognize + as potentially meaning concatenation and replace with ++.

List concatenation has the signature List[T] ++ List[T] -> List[T] and is a total operation. Associativity must be guaranteed such that (a ++ b) ++ c == a ++ (b ++ c).

The concatenation identity guarantees that [] ++ x == x ++ [] == x.

Relational operators

The standard relations are defined for integers having the signature Int op Int -> Bool, defining a total ordering over integers.

Equality is, for all comparable types, a total operation.

Equality and inequality are defined for strings. Two strings are equal when the sequences of codepoints are equal.

As a generic type, two List variables can only be compared if a common element type can be resolved. Equality is only defined if the common element type itself supports equality.

Two lists are defined as equal when lengths are equal and all corresponding elements are equal.

Map equality has the signature Eq K, V ::: Map[K, V] == Map[K, V] -> Bool. It has an equivalence to map difference, such that a == b iff a -- b == {:} and b -- a == {:}.

Set equality has the signature Eq T ::: Set[T] == Set[T] -> Bool

Union equality is defined for a given union type only when all variants are defined for equality. It is defined such that two tagged values are equal iff they have the same tag and their variants are equal.

Membership is defined for maps and sets, and is a total operator. It is read as “elem in container.”

For maps, Eq K ::: K in Map[K, V] -> Bool returns true iff the key is in the map.

For sets, Eq T ::: T in Set[T] -> Bool returns true iff the element is in the set.

Set operators

The set operators union, intersection and difference have the signature Eq T ::: Set[T] op Set[T] -> Set[T] and are total operations.

The union of two sets c := a || b constructs a new Set c such that it includes every element that is a member of a or b. The empty set {} is the identity of union. The union operator must be commutative and associative.

The intersection of two sets c := a && b constructs a new Set c such that it includes every element that is a member of a and b. Any set intersected with the empty set must return the empty set. The intersect operator must be commutative and associative.

The difference of two sets c := a -- b constructs a new Set c such that it includes every element that is a member of a but that is not a member of b. The empty set on the right-hand side is the identity of difference. Set difference is asymmetric.

Set relations are defined by building on difference and the empty set. The empty set is only equal to itself, it is an improper subset of all sets, and all sets are an improper superset of the empty set.

Set equality is defined such that a == b iff a -- b == {} and b -- a == {}.

Map union has the signature Eq K, V ::: Map[K, V] || Map[K, V] -> Map[K, V] and is a partial operator. It constructs a new map that combines keys and values from both arguments. If the same key is specified in both and the corresponding values are different, it raises Key_Conflict. It is commutative and associative.

If the Key_Conflict isn’t handled, the compiler should notify the user of the merge builtin.

Map intersection has the signature Eq K, V ::: Map[K, V] && Map[K, V] -> Map[K, V] and is a total operator. It constructs a new map that contains key/value pairs that are common to both arguments. That is, keys must match and the corresponging values must match. It is commutative and associative.

Map-set intersection has the signatures Eq K ::: Map[K, V] && Set[K] -> Map[K, V] and Eq K: Set[K] && Map[K, V] -> Map[K, V] and is a total operator. It constructs a new map that contains key/value pairs from the map but only whose keys are in the set. It is commutative. (And associative?)

Map difference has the signature Eq K, V ::: Map[K, V] -- Map[K, V] -> Map[K, V] and is a total operator based on the relational antijoin operator. It constructs a new map that contains all key/value pairs from the left-hand side without pairs from the right-hand side that match both key and value.

Map-set difference has the signature Eq K, V ::: Map[K, V] -- Set[K] -> Map[K, V] and is a total operator. It constructs a new map that contains all key/value pairs from the left-hand side without pairs whose keys are in the right-hand side.

Logical operators

All boolean operators are total operations. They are:

Use of Bool == Bool should be flagged as an error and fixers should replace it with eqv.

For Boolean returning operations, implementations must guarantee that:

Parametric operators

Record slot access

A record’s slots may be accessed by the . slot postfix parametric operator. This is a total operation that returns the value associated with the slot.

A slot of a record may be updated through assignment to the . slot operator. This is a total operation. The postcondition of x.slot := y is that x.slot == y.

let x := ( count: 3, name: "Fred" )
let x.count += 1
let x == ( count: 4, name: "Fred" )

Union variant access

A tagged value deconstrutor has the signature (tag ~ V | ...) ? tag -> V and is syntactically a unary postfix operator, where the portion ? tag is considered the operator. It is a partial operator, as it is only defined for the given tag. If the tag doesn’t match, Wrong_Tag is raised.

Enum values can also be deconstructed, but the variant will always be ().

The variant of a union may be assigned to using the ? tag deconstructor. This is a partial operation, as it is only defined for the given tag. If the tag doesn’t match, Wrong_Tag is raised. The postcondition of x ? tag := y is that x ? tag == y.

let x := tag ~ ( slot: 5, data: 4 )
let x ? tag . slot := 3
x == tag ~ ( slot: 3, data: 4 )

Indexing operators

List indexing has the signature List[T][Integer] -> T. Indexing is a partial operation, x[j] enforces the precondition that 0 <= j < len(x). If not met, list indexing raises Out_Of_Bounds.

Map indexing has the signature Eq K ::: Map[K, V][K] -> V and is a partial operator. It retrieves a value for a given key. It raises Missing_Key if the key is not in the map.

List slicing has the signature List[T][Integer .. Integer] -> List[T]. Slicing is a partial operation; the slice x[i .. j] enforces the precondition 0 <= i <= j <= len(x), raising Out_Of_Bounds if not met. Ranges in Tenet are closed .. open so the slice will contain the all elements starting at index i and stopping (thus not including) index j.

Note that empty slices are valid, so x[0 .. 0] is valid as is x[len(x) .. len(x)].

Many languages will returning any elements they can from a slice. To be able to enforce a simple postcondition with assignment and have consistency between access and assignment, Tenet enforces preconditions on the slice as well. Negative indices are not allowed and do not read from the end of the list. Negative indices can be achieved with e.g. j % len(x).

Lensing

Operators on lists have assignment forms that conduct simulated mutations, that is, a new list is constructed as if the mutation had taken place.

Assigning to a specific index has a postcondition that after x[i] := v it must be that x[i] == v and is decomposed as:

let x[i] := v
let x := !setindex(x, i, v)
;; Equivalent to:
let x := x[.. i] ++ [v] ++ x[i + 1 ..]

If the index is out of bounds it can’t guarantee the postcondition and must thus raise Out_Of_Bounds.

The type of v must be assignable to the element type of x.

Assigning to a slice x[i .. j] := v, or splicing, the precondition is 0 <= i <= j <= len(x).

When it’s also true that len(v) == j - i, the postcondition is x[i .. j] == v

The more general postcondition is essentially the concatenation:

x[.. i] == x_[..i]
x[i .. i + len(y)] == y
x[i + len(y) ..] == x_[j..]

And this is because splicing is decomposed as:

let x[i .. j] := v
let x := !setslice(x, i, j, v)
;; Equivalent to:
let x := x[.. i] ++ v ++ x[j ..]

Concatenation may be used in assignment form, and decomposes as:

let x ++= y
let x := x ++ y

Map index assignment has the signature Eq K ::: Map[K, V][K] := V and is a total operator. The assignment m[k] := v has the postcondition that m[k] == v.

Function application

Within an expression, a function’s arguments are applied to the function itself using, primarily, a keyword-based syntax. Arguments may be specified in any order, and all arguments must be specified.

return keyword_style(arg1: value1, arg2: value2, arg3: value3)
return keyword_style(arg3: value3, arg2: value2, arg1: value1)

As syntactic sugar, up to the first three arguments may be called using a traditional positional syntax.

return positional_style(value1, value2)
return positional_style(value1, value2, arg3: value3)

Positional arguments must be specified in the order they are defined, and this order must match the best known signature. For example:

func two_args(arg1: Int, arg2: Str) -> Str {
   ...
}
let val := two_args(5, "foo")  ;; Okay, matches the defined ordering.
func takes_func(funarg: Func(arg2: Str, arg1: Int) -> Str) {
   return funarg("foo", 5) ;; Okay, uses the ordering of the local variable.
}

The function itself can be an arbitrary expression that resolves to a function value.

return some_tuple.function(arg2: value2, arg1: value1)
return function_one(value1)(value2)

As another syntactic sugar, in the keyword style, if a name in scope matches an argument name, it may be abbreviated.

let some_val := keyword_style(arg1:, arg2:, arg3:)
let same_val := keyword_style(arg1: arg1, arg2: arg2, arg3: arg3)

All user-defined functions in Tenet are total. A function may represent an error through a tagged union; if this is uncommon, variant access may be used to assume an ok or other correct value. Otherwise, a switch may inspect various return codes.

let result := function(value1, value2) ? ok
switch function(value1, value2) {
case ok ~ result:
   ;; same value for result as above.
case err ~ code:
   ...
}

Partial application

A function value may be partially applied to construct a new function value.

In general:

func original(argA: TypeA, argB: TypeB, argC: TypeC, argD: TypeD) -> Return_Type {
    return body()
}
let partial := original(argB: valB, argC: valC, ...)

Notes:

The value of partial is logically equivalent to:

func partial(argA: TypeA, argD: TypeD) -> Return_Type {
    return original(argA:, argB: valB, argC: valC, argD:)
}

A partial application may not specify arguments that don’t exist on the original function value. A partial application may specify no arguments, in which case it is the original value. A partial application may specify all arguments, in which case partial() applies the function. Partial application may be applied repeatedly. While implementations may choose any appropriate representation for a partial application, it should be treated as equivalent to any other function value.

A practical example:

func times(x: Int, y: Int) {
    return x * y
}
let double := times(x: 2, ...)
func also_double(y: Int) {
    return times(x:2, y:)
}

Renaming within partial application

Within a partial application, arguments may be renamed. Working from the prior case:

let renamed := original(new_argB := argB, new_argC := argC, ...)
;; Same as:
function renamed(argA: TypeA, new_argB: TypeB, new_argC: TypeC, argD: TypeD)
-> Return_Type {
    return original(argA:, argB: new_argB, argC: new_argC, argD:)
}

Grouping constructs

Parentheses have overloaded meaning in Tenet:

The rules to distinguish these are demonstrated:

(expr)       ;; grouping
expr(expr)   ;; function application
(slot: expr) ;; record construction
()           ;; unit record

Guard expressions

The | operator guards partial operations by creating a construct equivalent to a try / catch.

In general, these are equivalent:

let result := val1 op1 (val2 op2 val3 | val4)
try {
    let temp := val2 op2 val3
} catch any {
    let temp := val4
}
let result := val1 op1 temp

Except that catch any is not valid. In particular, partial operations outside the guard are not protected. If a guarded expression is used within another, the innermost guard will catch the raised exception.

Anonymous functions

An anonymous function is a way to immediately construct a function value with a syntax similar to a function definition. The general form is similar to the function declaration:

let anon_func := func(arg1: Type1, arg2: Type2) -> Return_Type { return body() }

An anonymous function may not be generic. An anonymous function may omit types as a function definition would. Linters should complain about a simple assignment to a name and recommend replacing it with a function definition.

Lazy expressions

A briefer form of an anonymous function is a lazy expression. The general form is:

let lazy_expr := #(name op name)

Within a lazy expression, any unknown names are implicitly arguments.

let local_name := 55
let lazy_expr := #(arg + local_name)

This is logically equivalent to an anonymous function, except that positional syntax can not be used with a lazy expression.

let local_name := 55
let lazy_expr := func(arg) {
    return arg + local_name
}

Evaluation order

Tenet makes the least possible guarantees about the order of evaluation of expressions.

Expressions do not make assignments visible within the scope, but evaluation may fail.

Within a guarded expression such as example(a: 1 / x, b: list[3]) | 66, the nature of the failure is suppressed, so the order is not relevant.

However, a try block with different catch clauses is sensitive to order of evaluation.

This order is a postorder traversal of the expression’s abstract syntax tree.

let x := 0
let y := [1, 2]
try {
    let a := example(a: example(a: 1/x, b: y[3]), b: y[3])
} catch Out_Of_Bounds {
    let a := 33
} catch Div_By_Zero {
    let a := 66
}
;; div_by_zero caught first
return a == 66