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
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 operands 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 STRINGs, 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:
- Compute the type of the argument (whose type must be a list of some kind:
[tyA]). - Compute the type of the result for the empty case (
ty1). - 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:
- Compute the type of the first expression, which must be a function type (
ty1 → ty2). - 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