Glossary

[]
Tuple-brackets. An empty-tuple is also known as: no, nil, unit, an empty-list.
[ a ,, b ]
A pair.
[ a, b, c ]
Equivalent to [ a ,, [ b ,, [ c ,, [] ] ] ].
[ a, b ,, c ]
Equivalent to [ a ,, [ b ,, c ] ].
()
Term-brackets
{}
Type-brackets
->
lambda
=>
lambda-yes
|->
lambda-no
|=>
lambda-maybe
nil
A value, typically used to denote the absence of another value, such as a pair.
pair
A compound value, containing a head value and a tail value.
tuple
A tail-nested arrangement of zero or more pair values terminated by a nil value.
list
A tail-nested arrangement of zero or more pair values terminated by a nil value.
list
TODO
Any
A type which contains all the recursively-discernable values.
All
A type which contains all values.
Pair
A type-constructor. (Pair A B) denotes the type containing pair values whose heads have type A and tails have type B.
Maybe
A type-constructor. (Maybe A) denotes the type containing
List
A type-constructor.
discernable-value
A value that can be used with the ifNil, ifBool, ifInt, isStr, ifPair functions.
Discernable
A type that contains all the values in Nil, Bool, Int, Str and (Pair All All).
DiscernableRecursive
A type that contains all the values in Nil, Bool, Int, Str and (Pair Any Any).
Bool
A type that contains only the 'true' and 'false' values.
Int
A type that contains all whole numbers.
Str
A type that contains all string values.
Data
A type that contains all the values in Nil, Bool, Int, Str and (Pair Data Data).
literal
Values of type Nil, Int, Str can be denoted using literal syntax ([], 123, "ABC").
value
A sufficiently reduced term.
data
TODO
term
A graph-node which may or may not be reduced to a value.
type-term
A graph-node which has or will reduce to a type-value.
type-value
A term which reduced to a type-value. Denotes a set of values.
type
Ambiguously used for both type-terms and type-values.
Type
The type containing all types.
term-brackets
(), used for precedence, and to move from a type-context to a term-context.
type-brackets
{}, used for precedence, and to move from a term-context to a type-context.
term-context
A context in which operators and juxtaposition denote term-level operations, and literals denote term-level values.
type-context
A context in which operators and juxtaposition denote type-level operations, and literals denote singleton-types.
no-tuple
A tuple of length 0. Another name for nil.
yes-tuple
A tuple of length 1.
lambda
A nameless pattern-matching function. Pattern-match failure is considered a term-error, and so will cause a panic.
lambda-yes
A lambda that wraps its result in a yes-tuple.
lambda-no
A lambda that returns a no-tuple on pattern-match failure.
lambda-maybe
A lambda that returns a no-tuple on pattern-match failure, and wraps its result in a yes-tuple on pattern-match success.
type-error
TODO
term-error
TODO
panic
A term-error at runtime causes a panic which halts the program.
synthesized-type
For compound terms, the type calculated for a term, based on its sub-terms. For term-variables, the type looked-up in the environment. For pattern-variables, the context-type is used. For literals, the singleton-type containing only that literal-value.
context-type
The type for a term calculated from its parent's context-type, and the synthesized types of zero or more of its siblings.
type-inhabitation
A type is inhabited if it contains at least one term.
relative-complement
TODO
Void
The type that contains no terms.
singleton-type
A type that contains exactly one value.
Unit
The type which contains only the unit value.
unit
Another name for nil
strong-form
TODO
weak-form
TODO
TorP
Term or Pattern, terminology used internally
TorT
Term or Type, terminology used internally