CS312:  Type-Checking
Quick Reference


Constants:

tcheck(env, c) = int (when c is an integer)
tcheck(env, c) = real (when c is a real)
tcheck(env, c) = string (when c is a string)
tcheck(env, c) = char (when c is a char)

Variables:

 
tcheck(env, id) = lookup_var(env,id)

Anonymous Functions:

tcheck(env, fn (id:t) => e) = t -> tcheck(add_var(env,id,t),e)

Function Applications:

tcheck(env, e1(e2)) = t2
  when tcheck(env, e1) = t1 -> t2
   and tcheck(env, e2) = t3
   and same_types(t1,t3)

Unary Operations:

tcheck(env, u e) = unary_op_result_type(t1,u)
  when tcheck(env, e) = t1
   and unary_op_arg_type(t1,u) = t2
   and same_types(t1,t2)

Binary Operations:

tcheck(env, e1 b e2) = binary_op_result_type(b,t1)
  when tcheck(env, e1) = t1
   and tcheck(env, e2) = t2
   and binary_op_arg_type(b,t1) = t3
   and same_types((t1 * t2), t3)

Tuples:

tcheck(env, (e1,e2,...,en)) = (t1 * t2 * ... * tn)
  when tcheck(env, ei) = ti (for 1 <= i <= n)

Tuple Projections:

tcheck(env, #i e) = ti
  when tcheck(env, e) = (t1 * t2 * ... * tn) 
   and (1 <= i <= n)

Records:

tcheck(env, {lab1=e1,lab2=e2,...,labn=en}) = sort_labels({lab1:t1,...,labn:tn})
  when tcheck(env, ei) = ti
   and lab1,...,labn are distinct

Record Projections:

tcheck(env, #lab e) = ti
  when tcheck(env,e) = {lab1:t1,...,labi:ti,...,labn:tn}
   and same_labels(lab,labi)

Simple Datatype Constructors:

tcheck(env, Id) = nullary_constructor_result_type(Id)

Value-Carrying Datatype Constructors:

tcheck(env, Id(e)) = constructor_result_type(Id)
  when tcheck(env, e) = t
   and same_types(t, constructor_arg_type(Id))

Case Expressions:

tcheck(env, case e of p1 => e1 | p2 => e2 | ... | pn => en) = t1
  when tcheck(env, e) = t
   and patcheck(env,t,p1) = env1
   and tcheck(env1,e1) = t1
   and patcheck(env,t,p2) = env2
   and tcheck(env2,e2) = t2
     ...
   and patcheck(env,t,pn) = envn
   and tcheck(envn,en) = tn
   and same_types([t1,t2,...,tn])
   (and p1,...,pn are exhaustive for t and do not overlap.)

Let Expressions:

tcheck(env, let d in e end) = t
  when declcheck(env,d) = env'
   and tcheck(env',e) = t

Val Declarations:

declcheck(env, val p = e) = env'
  when tcheck(env,e) = t
   and patcheck(env,t,p) = env'
   (and p is exhaustive for t)

Fun Declarations:

declcheck(env, fun id1(id2:t1):t2 = e) = env''
  when env' = add_var(id2,t1,add_var(id1,t1->t2,env))
   and env'' = add_var(id1,t1->t2,env)
   and tcheck(env', e) = t3
   and same_type(t2,t3)

Pattern Checking:

patcheck(env, t, p) = union_env(env,env')
  when vars(p) are unique
   and patenv(t, p) = env'

Wildcards:

patenv(t, _) = empty_env

Variable Patterns:

patenv(t, id) = add_var(id,t,empty_env)

Constant Patterns:

patenv(t, c) = empty_env
  when tcheck(empty_env,c) = t2
   and same_type(t,t2)

Tuple Patterns:

patenv((t1 * ... * tn), (p1,...,pn)) = union_envs(env1,...,envn)
  when patenv(ti,pi) = envi

Record Patterns:

patenv({lab1:t1,...,labn:tn}, {lab1=p1,...,labn=pn}) = union_envs(env1,...,envn)
  when patenv(ti,pi) = envi

Simple Constructor Patterns:

patenv(t, Id) = empty_env
  when nullary_constructor_result_type(Id) = t2
   and same_type(t,t2)

Value-Carrying Constructor Patterns:

patenv(t, Id(p)) = env
  when constructor_result_type(Id) = t2
   and same_type(t,t2)
   and constructor_arg_type(Id) = t3
   and patenv(t3,p) = env

Notes:

Throughout, env is a type-environment (a mapping from variables to types.)  The function lookup_var tries to find the variable in the environment and returns its type.  If the variable is not found, then we have a type error (unbound variable.)  empty_env is the empty environment, add_var(id,t,env) is the same as env, except that lookup_var(id,env) always returns t.  union_envs(env1,env2) is the (disjoint) union of the two mappings env1 and env2.

We assume some global functions, such as constructor_result_type, constructor_arg_type, etc. that provide information about the types of data constructors and their arguments.  Similarly, we assume functions to give us the argument and result types for unary and binary operations.  Note that the result type of a binary operation (such as +) may depend upon the types of its arguments.  For instance, when e1 and e2 are ints, e1+e2 has type int, but when e1 and e2 are reals, then e1+e2 has type real.

tcheck takes an environment and an expression and returns a type.

declcheck takes an environment and declaration and returns a new environment.

patcheck takes an environment, type, and pattern and returns a new environment.

patenv takes a type and a pattern and returns a new environment.

This simple treatment does not deal with type inference, but it turns out to be relatively straightforward to do so.  In addition, this treatment does not deal with polymorphism, but again, this is relatively simple to add to the type-checker.  Finally, we aren't specifying how to check that a list of patterns is exhaustive and does not overlap.  This turns out to be fairly tricky to implement.