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:
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.
| || || ||
| || || ||
| || ||
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
|u||no match||u ~ t||no match|
| ||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.
The Boolean literals
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
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.
Special Form Type
The type of all special forms is the root type