Type Theory

[chharvey]

Types are conceptually thought of as sets of Solid Language Values.

• A type union is thought of as a set union (containing values “in” either set).
• A type intersection is thought of as a set intersection (containing values “in” both sets).
• When a type ‹S› is a subtype of a type ‹T›, it’s conceptually understood that the values “in” ‹S› are also “in” ‹T›.
• Types that are equal are thought of as “containing” the same values.

The concepts above are merely conceptual aids for the programmer. The word “in” is in scare quotes, because types are not actually implemented as sets “containing” values — this would be impossible to achieve. (For example, the int type would need to contain 2¹⁶ values, and the String type would need to contain literally an infinite number of values.) Rather, as an implementation, it’s more appropriate to define an algorithm that determines whether a given value ‹x› is assignable to a given type ‹T›. When it is, we say ‹x› is “of type” ‹T›, and ‹x› is conceptually understood as “contained in” ‹T›.

The following abstract algorithms must be defined:

• [x] Check whether a value x is of type T, or assignable to type T. (If T is a class and x is an object, saying x is “of type” T is equivalent to saying x is an instance of T.)
  • [x] Check whether a type S is a subtype of type T, i.e. all the values of type S are also of type T.
  • [x] Check whether types T and U are equal, i.e. they are subtypes of each other.
  • [ ] Check whether types T and U are disjoint, i.e. they do not have any overlap, i.e. no value is of type T and of type U.
  • [x] Create a type intersection T & U containing the values that are assignable to both T and U.
  • [x] Create a type union T | U containing any value that is assignable to either T or U.
  • [x] Define an empty type / bottom type, call it never (TBD), to which no value or expression is assignable.
  • [x] Define a universal type / top type, call it unknown, to which any value or expression is assignable.
  • [x] Define an Object type, obj, to which any value is assignable.

For this version, unknown is equivalent to obj, since every expression has a value. In future versions, not every expression will have a value, and so there will be a type void, to which no values but to which some expressions are assignable. Therefore expressions assignable to void would be assignable to unknown but not to obj.

Type Laws

The following is a list of facts about types in general. The metavariables ‹T›, ‹A›, ‹B›, ‹C›, and ‹D› denote placeholders for Solid Language Types and do not refer to real variables or real types. For brevity, angle quotes will be omitted. In the notation below, let <: be an unofficial symbol denoting “is subtype of”, and let && and || denote “and” and “or” respectively.

For any type ‹T›,

1. T & unknown equals T. (Identity Element, Intersection)
2. T | never equals T. (Identity Element, Union)
3. T & never equals never. (Absorption Element, Intersection)
4. T | unknown equals unknown. (Absorption Element, Union)
5. never is always a subtype of T.
6. T is always a subtype of unknown.

For any types ‹A› and ‹B›,

1. A & B equals B & A. (intersection is commutative)
2. A | B equals B | A. (union is commutative)

For any types ‹A› and ‹B›,

1. A & B is a subtype of each of A and B.
2. A and B are each subtypes of A | B.
3. (It follows that A & B is always a subtype of A | B.)
4. A <: B if and only if A & B equals A.
5. A <: B if and only if A | B equals B.

For any types ‹A›, ‹B›, and ‹C›,

1. (A & B) & C equals A & (B & C). (intersection is associative)
2. (A | B) | C equals A | (B | C). (union is associative)
3. A | (B & C) equals (A | B) & (A | C). (union is distributive over intersection)
4. A & (B | C) equals (A & B) | (A & C). (intersection is distributive over union)

For any types ‹A›, ‹B›, and ‹C›,

1. A <: A. (subtype is reflexive)
2. If A <: B && B <: A, then A equals B. (subtype is anti-symmetric)
3. If A <: B && B <: C, then A <: C. (subtype is transitive)

For any types ‹A›, ‹B›, ‹C›, and ‹D›,

1. A <: C && A <: D if and only if A <: C & D. (subtype is left-factorable under conjunction and left-distributive over intersection)
2. If A <: C || A <: D then A <: C | D, but not the converse. (subtype is left-factorable under disjunction)
3. A <: C && B <: C if and only if A | B <: C (subtype is right-antifactorable under conjunction and right-antidistributive over union)
4. If A <: C || B <: C then A & B <: C, but not the converse. (subtype is right-antifactorable under disjunction)