## Standard Types

Values in Tenet are semantically immutable. While Tenet code must not be able to alter values, Tenet makes no guarantees that the host language will be unable to do so. In, particular, in languages where encapsulation is by a naming convention, the use of such advisories conforms to this specification.

Values may not be cyclic; equivalently, value constructors must use copy semantics. The implementation may use any kind of graph or pointers to represent values, provided the interface presents them as acyclic.

### Integers

The Integer type is an unbounded enumeration of integer numbers. Tenet integers are signed and have no minimum or maximum. The Integer type contains no infinity or “not a number”. While Integer is an enumeration, as an atom it is not a subtype of Union.

If an integer value can’t be expressed in the host representation, a representation failure is signalled.

The Integer type is named Int. An integer literal is a decimal number; the sign is a separate operator.

### Strings

Tenet strings are immutable, finite sequences of Unicode codepoints. The String type is named Str.

No normalization of codepoints should be done to strings.

Any Tenet operation that makes a guarantee that relies on constant time indexing of strings is a bug in the spec.

The empty string is defined as "". A string literal is contained within double quotes and may contain any ASCII characters 0x09, 0x20, 0x21, 0x23 through 0x7f, and the following escape sequences:

Sequence Meaning Code
\a BEL 0x07
\b BS 0x08
\f FF 0x0c
\n LF 0x0a
\r CR 0x0d
\t TAB 0x09
\v VT 0x0b
\\ \ 0x5c
\' ' 0x26
\" " 0x22
\xXX Hex codepoint
\uXXXX Hex codepoint
\UXXXXXXXX Hex codepoint

#### Encoding

Ideally, a Tenet string is revealed to the target language using its native strings. If a target language only offers byte strings, it is recommended that UTF-8 be used to convert to and from native strings.

The target language may use any encoding internally, provided it faithfully reports the string as a sequence of codepoints.

Any string constructed from host data must be a valid sequence of codepoints, if not, a decoding failure must be reported.

#### Future functionality

Tenet does not have a substring or string index operator as user expectations are invariably that string indexing is constant complexity. Some kind of reasonable parsing language could be adopted that allowed a string to be parsed with linear complexity.

Case folding and conversion will require collations, which in turn will require dependency management.

### Lists

The List type is an exponential type as a list value can represent a function of a non-negative integer to some value. Tenet lists are homogenous finite sequences of Tenet values.

A list constructor is a comma delimited list of values within square brackets, e.g. [elem1, elem2, elem3]. The empty list value [] has the type List[⊥] and is a member of all list types. It is the identity of list concatenation.

List concatenation must be associative. Lists do not have missing values.

List types are expressed as List[T] or simply [T]. The type inferred by a list constructor is the common supertype of all elements.

#### Iteration

Lists may be iterated over using a for loop. If the list body updates an ordered accumulator, iteration must be performed in index order.

Optiization: Loop iteration may be done out of order if accumulation can be proven to be order invariant.

for item in some_list {
...
}


Within the body of the loop, item is set to each consecutive value. The iterator item does not persist outside the loop, however.

Future: Allow assignment to item?

### Sets

The Set type is an exponential type as a set value can represent a function of some type to boolean. Tenet sets are homogenous finite sets of Tenet values. All types defined for == may be used as set elements; specifically, function types may not be used in sets.

A set constructor is curly braces surrounding comma-separated elements, e.g. {elem1, elem2, elem3}. The Set type is written as Set[T] or simply {T}. The empty set value {} has the type Set[⊥] and is a subset of all set types. It is the identity of set union.

### Maps

The Map type is an exponential type as a map value can represent a unary function mapping keys to values. Tenet maps are finite maps of a single homogeneous key type to a single homogenous value type.

The Map constructor is curly braces around colon pairs of keys and values, e.g. {key1: val1, key2: val2}. The Map type is written as Map[Key, Value] or simply {Key: Value}.

The empty map is denoted {:} has the type Map[⊥, ⊥] and is a member of all map types.

A key type must support equality; thus neither functions nor values that contain function values may be used as keys.

The value type may be any type, however, some operations require that values support equality.

The map itself is based on the relational algebra, treating a map as a binary relation and enforcing a candidate key constraint on the key attribute.

### Unions

The Union is a discriminated union and is the Tenet sum type. A Union type maps tags to variant types. The members of a union type are called tagged values and consist of a tag and variant separated by the ~ token.

The syntax tag~variant is not a binary expression, because tag is not an arbitrary expression.

Rather, ~ is a parametric constructor whwere tag is the parameter, in essence, tag~ is a unary prefix operator that takes a single argument for the variant. And other_tag~ is another unary prefix operator.

A parametric operator is one in which changing the parameter is, effectively, describing a new operator with a new signature. The parameter must be a literal value, there is no syntax or mechanism to set parameters dynamically.

Future metaprogramming facilities may relax this rule.

A tagged value constructor has the signature tag ~ V -> tag ~ V and is syntactically a unary prefix operator, where the portion tag ~ is considered the operator. It is a total operator, and any variant V is acceptable.

An enum value constructor has the signature #enum -> enum ~ () and is exactly equivalent to enum ~ {} constructing a tagged value with an empty record variant. It is syntactically a nullary operator, and the whole expression #enum is the operator. It is a total operator.

The type expression tag ~ Variant refers to a union with a cardinality of one times the cardinality of Variant. A Union type consists of tag types joined with |, for example:

 tag ~ Variant | other_tag ~ Other_Variant


Conceptually, this has the cardinality of the cardinality of Variant + Other_Variant.

Often, Union types don’t need to be declared. Consider the function:

func odd_or_even(num: Integer) {
if num % 2 == 0 {
return even~"xxx"
} else {
return odd~num
}
}


Type inference can deduce that the return type is even~String | odd~Integer.

#### Enumerations

Enumerations fall naturally out of Union. An enum value is simply a tag whose variant is the unit record.

The #tag constructor is logically equivalent to tag ~ (). The type expression #tag is also equivalent to tag ~ ().

### Records

The Record is the Tenet product type. A Record type maps slots to their individual types. The Record type is closed meaning that two record types whose slots don’t match exactly are entirely disjoint. The Open Record type constraint does not behave this way.

A record literal is zero or more slot pairs separated by commas and surrounded by parentheses:

(slot: val, slot2: other_val)


As a convenience, the value may be omitted and is then assumed to be a variable with the same name as the slot.

let apple := "red"
let rec := (apple:, num: 3)
;; rec == (apple: "red", num: 3)


A record type has an equivalent syntax, (slot: Type, slot2: Other_Type), or a bracketed syntax Rec[slot: Type, slot2: Other_Type]. The cardinality of such a type is, conceptually, the cardinality of Type * Other_Type.

The empty record () is the unit value, and beyond the fact that there’s only one of it, it has no special properties. Its type is similarly ().

#### Common supertypes

Two Record types have a common supertype only if their attributes are identical, and all attributes have a common supertype.

### Functions

The Tenet Function type describes the signatures of user-defined functions and is an exponential type.

A function type looks like a function definition:

type Example_Type := Func (arg: Type, other_arg: Other_Type) -> Return_Type

func example(arg: Type, other_arg: Other_Type) -> Return_Type {
...
}


Unlike a function definition, a function type must specify all types. Arguments are not ordered in any way.

A function defition creates and assigns a function value to the name. The above is identical to using an anonymous function value:

let some_function := func(arg: Type, other_arg: Other_Type) -> Return_Type {
...
}


Functions in Tenet are not unary, there are multiple named arguments and a single return value. Functions are not curried.

Partial application constructs a new function value; the two are equivalent:

let part_func := some_function(other_arg: 5, ...)
func part_func(arg: Type) -> Return_Type {
return some_function(other_arg: 5, arg::)
}


The partial application some_function(...) is identical to some_function and may indicate a refactoring error.

The invocation some_function(x:=arg, y:=other_arg, ...) is equivalent to the expression:

func(x: Type, y:Other_Type) -> ReturnType {
return some_function(arg: x, other_arg: y)
}


The lazy expression #(a + b) constructs a function value equivalent to func(a, b) { return a + b }. This works in Tenet because arguments are unordered; note that positional syntax can’t be used on a function defined through invocation.

### Tree type

This type is a proposition and not fully specified.

The Tree and Path types enable the implementation of graphs and traversals. A type Tree[T] is a directed acyclic graph of T, while a Path[T] is a series of accessors that, when applied to a value, yields an element of that value.

A Tree value is constructed with the @ operator:

let nums : Tree[Int] := 1 @ {
2 @ {
3,
4 @ 5
}, 6 @ {7, 8}
}


The @ operator joins a root with a set of children and has the signature T @ Set[Or[T, Tree[T]]] -> Tree[T].

Note here that the Tree type doesn’t enforce what values are used in

Trees may be traversed using the walk statement using either a depth-first or breadth-first traversal. The prune command disregards children of the present node.

;; Depth-first traversal.
let sum := 0
walk node in tree {
sum += node
}

let sum := 0
walk node over tree {
if node > 5 {
prune ;; do not visit children of this node
}
sum += node
}


#### Keyed edges

Trees whose edges have no value are fine assuming the intended use is to walk the tree. It also makes clear what the nodes are and keeps types simple.

It seems the most practical uses of trees are for nodes that have some payload associated with them. And a user typically won’t expect to have to inspect all edges to traverse the tree.

But this would look like:

type Stat := #file | #dir

let tree : Stat @ Str := #dir @ {
"foo.txt": #file,
"dir": #dir @ {
"bar.txt": #file,
"empty_dir": #dir
}
}


The homoiconic form of the type becomes node @ edge. It’s potentially a bit tricky that a root node does not have a leading key. A walk command becomes tricky: if we present only the node, we ignore the keys. We could also provide the present path, either using the Path type or as simply a list of keys.