Primitives

RL admits some terms that receive special treatment.

The Root of the Type System

Every term has an associated type. This potentially infinite regress is broken by the special term ^ROOT, which is the root of the type system and is its own type. Any term whose type is ^ROOT is referred to as a root term or root type. Since types are just terms in RL, either usage is fine; it is also fine for the type theorists out there to refer to ^ROOT as “bottom.”

Many of the “usual” types are really just symbols whose declared type is ^ROOT, such as INTEGER: ^ROOT, which is the usual type for integers: 5: INTEGER.

Note the unusual name. This is the only unquoted symbol that starts with a caret (^).

Parsing is complicated by the existence of symbol root types. Without any additional context, INTEGER would be interpreted as INTEGER: SYMBOL, but parsing requires that we instead interpret INTEGER as INTEGER: ^ROOT for things to work correctly. This is true for all the primitive root types: INTEGER, FLOAT, BITSTRING, STRING, and BOOLEAN, and for the special patterns ANY and NONE.

Defined Root Terms

The following root terms are known to the parser.

ANY BITSTRING BOOLEAN FLOAT
INTEGER MAP NONE PRODUCT
PROPERTIES ^ROOT SPECIAL_FORM

The Wildcard and Nothing

There is a special root term ANY that, as a pattern, matches any subject. We may refer to ANY as the wildcard, and it may also be abbreviated _. There is also a root term NONE that, as a pattern, does not match any subject. We can summarize this as follows, where t and u are arbitrary terms that are neither NONE nor ANY.

pattern subject
ANY t NONE
ANY match match match
u no match u ~ t no match
NONE no match no match no match

The special term ANY is intended to be the only term that breaks the pattern matching “substitution rule.” If pattern p matches term u with bindings b, then it must be the case that b(p) is equal to u, up to isomorphism. That cannot work for ANY since it contains no variables to be bound.

Boolean Literals

The Boolean literals TRUE and FALSE are parsed as TRUE: BOOLEAN and FALSE: BOOLEAN.

The Map Type

The type of a mapping such as a lambda is given as a static map INTEGER → INTEGER. Because this type is itself a term, it also has to have a type and it does not make sense for that type to be ^ROOT. Instead, the type of a static map is MAP, which is a root type. This gives the full type: (INTEGER → INTEGER): MAP: ^ROOT.

The Product Type

The type of a product of two types is given as a static product INTEGER * FLOAT. Because this type is itself a term, it also has to have a type and it does not make sense for that type to be ^ROOT. Instead, the type of a static product is PRODUCT, which is a root type. This gives the full type: (INTEGER * FLOAT): PRODUCT: ^ROOT.

Sequence Types

Sequences are

Special Form Type

The type of all special forms is the root type SPECIAL_FORM.