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

- Negation has the signature
`not Bool -> Bool`

and`not a`

returns . - Conjunction has the signature
`Bool and Bool -> Bool`

and`a and b`

returns . - Disjunction has the signature
`Bool or Bool -> Bool`

and`a or b`

returns . - Exclusive disjunction has the signature
`Bool xor Bool -> Bool`

and`a xor b`

returns . - Equivalence has the signature
`Bool eqv Bool -> Bool`

and`a eqv b`

returns .

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:

`a != b`

iff`not (a == b)`

`a <= b`

iff`not (a > b)`

`a >= b`

iff`not (a < b)`

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

is the actual syntax indicating a partial application. - The original function has some arbitrary number of arguments and types.
- And
`argB`

and`argC`

represents an arbitrary subset of the original arguments. - Ordering does not matter.

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:

- Grouping expressions
- Function application
- Literal record construction

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
```