Moses Types

This document describes the type system for Moses: a brief overview, the rules for types, and the rules for subtypes.

Overview

Moses has a different type system from Haskell; it has subtyping and parametric types (for example, lists of int and lists of string), but does not have parametric polymorphism (type variables).

In addition, to make types stand out, Moses adopts the convention of writing type names in upper case in the concrete syntax. Moses has the basic types INT, REAL, STRING, and BOOL, as well as tuples, such as (INT, BOOL) or (BOOL, STRING, INT). It also has homogenous lists, such as [INT] or [(STRING, BOOL)]. There are also function types, such as INT -> STRING. Finally, it has two special types, ANY and NONE.

A value belonging to the ANY type is a value that is a member of the universal set—if you have an ANY value, it could be anything. Thus all types are subtypes of the ANY type. An ANY value is so underspecified that we can’t do anything useful with it (because Moses has no operator to safely cast ANY to a more well-specified type). But the ANY type does have a few uses. For example, a function that ignores its argument and returns 42 is best described as having type ANY -> INT since it doesn’t care what its argument is. Think, “a useless ANY value”.

The NONE type contains no values at all. Like “a member of the empty set”, everything is tautologically true of such a value.

Because no NONE values actually exist, every NONE that does exist (all zero of them) can be used as anything you want. Thus, NONE is a subtype of all types because a mythical NONE value can do anything. But NONEs do have their uses—for example, the empty list has type [NONE] because, being empty, it doesn’t actually contain any NONEs. Similarly, the error function has type STRING -> NONE because it prints the error-message string and terminates the program—because the function never returns it can make the false promise that it will return something miraculous. Think, “a mythical NONE value”.

Natural-deduction rules

We describe the typing rules using natural deduction, where each rules looks like the following:

          premise
      —————————————————  (name)
         conclusion

We read the rule like so: “If the premise is true, then the conclusion is true”. If the premise is missing, then the rule is an axiom: the conclusion is always true. With this format, we can have multiple premises, all of which must be true for the conclusion to be true. We can also have multiple conclusions, any of which can be true as long as the premise is true.

We provide each rule with a name (written in parentheses to the right of the rule), so that we can refer to the name when talking about the type system in office hours or on Piazza.

Subtype rules

The subtype rules for Moses are as follows.

Every type is a subtype of itself.

      —————————————————  (ST-Identity)
            t ⊑ t

NONE is a subtype of every type.

      —————————————————  (ST-None)
          NONE ⊑ t

ANY is a supertype of every type.

      —————————————————  (ST-Any)
           t ⊑ ANY

INT is a subtype of REAL.

      —————————————————  (ST-Number)
          INT ⊑ REAL

For a list, if $t1$ is a subtype of $t2$, then a list of $t1$s is a subtype of a list of $t2$s.

            t1 ⊑ t2
      —————————————————  (ST-List)
          [t1] ⊑ [t2]

For a tuple, if tuple $x$ and $y$ have the same number of elements, and if each of the elements of tuple $x$ is a subtype of its corresponding element of type $y$, then $x$’s type is a subtype of $y$’s type.

          m == n        ∀ i : ty1i ⊑ ty2i
      ——————————————————————————————————————  (ST-Tuple)
       (ty1a, ..., ty1m) ⊑ (ty2a, ..., ty2n)

For a function, if the input of function $g$ is a subtype of the input of function $f$, and if the output of function $f$ is a subtype of the output of function $g$, then $f$’s type is a subtype of $g$’s type.

       ty3 ⊑ ty1       ty2 ⊑ ty4
      ————————————————————————————  (ST-Function)
         ty1 → ty2 ⊑ ty3 → ty4

Common supertypes and common subtypes

Types form a lattice, with the most general type (ANY) at the top and the most specific type (NONE) at the bottom.

For any two Moses types $t_1$ and $t_2$, we can compute:

  • The common supertype of $t_1$ and $t_2$, denoted $t_1 \sqcup t_2$, which is the most specific type $t$ that is a supertype of both $t_1$ and $t_2$.
  • The common subtype of $t_1$ and $t_2$, denoted $t_1 \sqcap t_2$, which is the most general type $t$ that is a subtype of both $t_1$ and $t_2$.

The rules for $\sqcup$ and $\sqcap$ can be derived from the subtyping rules, but it is often helpful to spell them out. Here they are:

ANY

      ANY ⊔ ty = ANY
      ANY ⊓ ty = ty

NONE

      NONE ⊔ ty = ty
      NONE ⊓ ty = NONE

Numbers

      INT ⊔ REAL = REAL
      INT ⊓ REAL = INT

Lists

      [ty1] ⊔ [ty2] = [ty1 ⊔ ty2]
      [ty1] ⊓ [ty2] = [ty1 ⊓ ty2]

Tuples

      (ty1a, ..., ty1n) ⊔ (ty2a, ..., ty2n) = (ty1a ⊔ ty2a, ..., ty1n ⊔ ty2n)
      (ty1a, ..., ty1n) ⊓ (ty2a, ..., ty2n) = (ty1a ⊓ ty2a, ..., ty1n ⊓ ty2n)

Functions

      (ty1 → ty2) ⊔ (ty3 → ty4) = (ty1 ⊓ ty3) → (ty2 ⊔ ty4)
      (ty1 → ty2) ⊓ (ty3 → ty4) = (ty1 ⊔ ty3) → (ty2 ⊓ ty4)

Everything else

⊔ and ⊓ are idempotent:

      ty ⊔ ty = ty
      ty ⊓ ty = ty

⊔ and ⊓ are commutative:

      ty1 ⊔ ty2 = ty2 ⊔ ty1
      ty1 ⊓ ty2 = ty2 ⊓ ty1

If none of the above rules described so far apply, then:

      ty1 ⊔ ty2 = ANY
      ty1 ⊓ ty2 = NONE

Type rules

The type rules for Moses are as follows.

Constants

Integer constants have type INT.


              n ∈ ℤ
          —————————————————  (T-INT)
            Γ ⊢ n : INT

Real constants have type REAL.


              r ∈ ℝ
          —————————————————  (T-REAL)
            Γ ⊢ r : REAL

String constants have type STRING.


              s ∈ String
          —————————————————  (T-STRING)
           Γ ⊢ S : STRING

Boolean constants have type BOOL.


          b ∈ {True, False}
          —————————————————  (T-BOOL)
            Γ ⊢ b : BOOL

The empty list ([] or “nil”) has type [NONE].


          —————————————————  (T-Nil)
           Γ ⊢ [] : [NONE]

Other data types

If a variable’s type is defined, then we lookup the type in the environment.


              v ∈ dom(Γ)
          ————————————————— (T-Lookup)
            Γ ⊢ v : Γ(v)

The type of a tuple is a tuple of the types of its elements.


                    Γ ⊢ ei : ti
          ———————————————————————————————— (T-Tuple)
            Γ ⊢ (v1, …, vn) : (t1, …, tn)

For a lambda expression, we first type-check the body of the expression, in an environment that is extended to include the declaration of the expression’s variable. The resulting type is a function from the variable type to the body’s type.


                    Γ, v:ty ⊢ e : t
          ———————————————————————————————— (T-Lambda)
            Γ ⊢ λ v :: ty . e : (ty → t)

Operations on data

For an arithmetic operation, (addition, subtraction, multiplication, or division), each operand must have a numeric type (either INT or REAL), and the type of the expression is the common supertype of the types of the operands.


              Γ ⊢ e1 : ty1    Γ ⊢ e2 : ty2
                  ty1, ty2 ∈ {INT, REAL}
          ————————————————————————————————————— (T-Math)
                 Γ ⊢ e1 + e2 : ty1 ⊔ ty2
                 Γ ⊢ e1 - e2 : ty1 ⊔ ty2
                 Γ ⊢ e1 * e2 : ty1 ⊔ ty2
                 Γ ⊢ e1 / e2 : ty1 ⊔ ty2

For string concatenation, each operand must have type STRING, and the type of the entire expression is a STRING.


            Γ ⊢ e1 : STRING    Γ ⊢ e2 : STRING
          ———————————————————————————————————————— (T-Concat)
                  Γ ⊢ e1 ++ e2 : STRING

For a relational operation, (equality, inequality, etc.), the operands must both be numeric types (INT or REAL) or both be STRINGs, and the type of the expression is BOOL.


                  Γ ⊢ e1 : ty1    Γ ⊢ e2 : ty2
          ty1, ty2 ∈ {INT, REAL}  v  ty1, ty2 = STRING
          —————————————————————————————————————————————— (T-Compare)
                      Γ ⊢ e1 == e2 : BOOL
                      Γ ⊢ e1 /= e2 : BOOL
                      Γ ⊢ e1 < e2  : BOOL
                      Γ ⊢ e1 > e2  : BOOL
                      Γ ⊢ e1 <= e2 : BOOL
                      Γ ⊢ e1 >= e2 : BOOL

For list-append, the types of the operands must be LISTs, and the type of the entire expression is the common supertype of the types of the operands.


              Γ ⊢ e1 : [ty1]    Γ ⊢ e2 : [ty2]
          ———————————————————————————————————————— (T-Append)
                Γ ⊢ e1 @ e2 : [ty1] ⊔ [ty2]

For a cons expression, we compute the type of the new head (ty1) and the type of the existing list (whose type must be a list of some kind: [ty2]). The type of the entire expression is the common supertype of [ty1] and [ty2].


              Γ ⊢ v0 : ty1       Γ ⊢ [v1, … vn] : [ty2]
          ———————————————————————————————————————————————— (T-Cons)
                Γ ⊢ [v0, v1, … vn] : [ty1] ⊔ [ty2]

Control-flow expressions

For a let expression with a single variable (not pattern-matching with a tuple), we first type check the assigned expression. Then we typecheck the body of the let in an environment extended to include the declaration of the introduced variable. The type of the entire expression is the type of the body.


             Γ ⊢ eDef : ty1      Γ, v:ty1 ⊢ eBody : ty2
          ———————————————————————————————————————————————— (T-Let)
                  Γ ⊢ let v = eDef in eBody : ty2

For a let expression with a pattern-matching tuple, we first type check the assigned expression, which must be a tuple type. Then we typecheck the body of the let in an environment extended to include the declarations of each variable with its corresponding type. The type of the entire expression is the type of the body.


        Γ ⊢ eDef : (ty1, …, tyn)    Γ, (vi:tyi) ⊢ eBody : ty
      —————————————————————————————————————————————————————————— (T-Let-Match)
            Γ ⊢ let (v1, …, vn) = eDef in eBody : ty

For an if expression, the condition must be of type BOOL. The type of the entire expression is the common supertype of the types of two branches.


                          Γ ⊢ eCond : BOOL
                Γ ⊢ eT : ty1           Γ ⊢ eF : ty2
          ———————————————————————————————————————————————— (T-If)
              Γ ⊢ if eCond then eT else eF : ty1 ⊔ ty2

For a case expression, we:

  1. Compute the type of the argument (whose type must be a list of some kind: [tyA]).
  2. Compute the type of the result for the empty case (ty1).
  3. Compute the type of the result for the non-empty case (ty2).

The type of the entire expression is common supertype of ty1 and ty2.


                              Γ ⊢ eArg : [tyA]
              Γ ⊢ eNil : ty1        Γ, vH:tyA, vT:[tyA] ⊢ eCons : ty2
        ————————————————————————————————————————————————————————————————— (T-Case)
            Γ ⊢ case eArg of [] -> eNil | vH:vT -> eCons : ty1 ⊔ ty2

For a function application, we:

  1. Compute the type of the first expression, which must be a function type (ty1 → ty2).
  2. Compute the type of the second expression (the argument), which must be a subtype of ty1.

The type of the entire expression is the result-type of the function.


            Γ ⊢ e1 : (ty1 → ty2)    Γ ⊢ e2 : ty1'    Γ ⊢ ty1' ⊑ ty1
        ————————————————————————————————————————————————————————————————— (T-Apply)
                              Γ ⊢ e1 e2 : ty2

For a recursive let expression, we want the least fixpoint of the typing rules, applied to the expression that defines the variable’s value, starting at NONE. We denote this value as: μ ty1 . Γ ⊢ eDef : ty1. Then, we compute the type of the body, in an environment extended with the variable mapped to ty1. The type of the entire expression is the type of the body.


            μ ty1 . Γ ⊢ eDef : ty1      Γ, v:ty1 ⊢ eBody : ty2
          ————————————————————————————————————————————————————— (T-LetRec)
                Γ ⊢ letrec v = eDef in eBody : ty2