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. Whenever an unquoted symbol without an explicit type is parsed, it is checked to see if it is a known root type. If so, it is converted to that type. Thus INTEGER by itself parses as the root type INTEGER: ^ROOT, while 'INTEGER' is explicitly a quoted symbol, and parses as INTEGER: SYMBOL. In a similar vein, note the Boolean literals, described below.

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 refer to ANY as the wildcard, and it may also be abbreviated by a single underscore _. There is also a root term NONE that, as a pattern, does not match any subject except itself. 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 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. As with root terms, if the symbol is intended and not the Boolean literal, it must be quoted or an explicit type given, as with 'TRUE' and FALSE: SYMBOL.

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.