Differences

This shows you the differences between two versions of the page.

--- rl:primitives [2019/01/09 17:27] – sprowell
+++ rl:primitives [2020/11/21 23:04] (current) – [Boolean Literals] sprowell
@@ Line 1: / Line 1: @@
 ====== Primitives ======
-RL admits some special terms that receive special treatment.
+RL admits some terms that receive special treatment.
-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.
+===== The Root of the Type System =====
-There is a special term ''ANY'' that, as a //pattern//, matches any //subject//.  There is also a 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 //not// ''NONE'' or ''ANY''.
+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."
-^ pattern  ^ subject                            ^^^
+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''.
-^          ^ ''ANY''  ^ //t//         ^ ''NONE''  ^
-| ''ANY''  | match    | match         | match     |
+Note the unusual name.  This is the only unquoted symbol that starts with a caret (''^'').
-| //u//    | no match | //u// ~ //t// | no match  |
-| ''NONE'' | no match | no match      | no match  |
+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''.