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)
tcheck(env, id) = lookup_var(env,id)
tcheck(env, fn (id:t) => e) = t -> tcheck(add_var(env,id,t),e)
tcheck(env, e1(e2)) = t2
when tcheck(env, e1) = t1 -> t2
and tcheck(env, e2) = t3
and same_types(t1,t3)
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)
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)
tcheck(env, (e1,e2,...,en)) = (t1 * t2 * ... * tn)
when tcheck(env, ei) = ti (for 1 <= i <= n)
tcheck(env, #i e) = ti
when tcheck(env, e) = (t1 * t2 * ... * tn)
and (1 <= i <= n)
tcheck(env, {lab1=e1,lab2=e2,...,labn=en}) = sort_labels({lab1:t1,...,labn:tn})
when tcheck(env, ei) = ti
and lab1,...,labn are distinct
tcheck(env, #lab e) = ti
when tcheck(env,e) = {lab1:t1,...,labi:ti,...,labn:tn}
and same_labels(lab,labi)
tcheck(env, Id) = nullary_constructor_result_type(Id)
tcheck(env, Id(e)) = constructor_result_type(Id)
when tcheck(env, e) = t
and same_types(t, constructor_arg_type(Id))
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.)
tcheck(env, let d in e end) = t
when declcheck(env,d) = env'
and tcheck(env',e) = t
declcheck(env, val p = e) = env'
when tcheck(env,e) = t
and patcheck(env,t,p) = env'
(and p is exhaustive for t)
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)
patcheck(env, t, p) = union_env(env,env')
when vars(p) are unique
and patenv(t, p) = env'
patenv(t, _) = empty_env
patenv(t, id) = add_var(id,t,empty_env)
patenv(t, c) = empty_env
when tcheck(empty_env,c) = t2
and same_type(t,t2)
patenv((t1 * ... * tn), (p1,...,pn)) = union_envs(env1,...,envn)
when patenv(ti,pi) = envi
patenv({lab1:t1,...,labn:tn}, {lab1=p1,...,labn=pn}) = union_envs(env1,...,envn)
when patenv(ti,pi) = envi
patenv(t, Id) = empty_env
when nullary_constructor_result_type(Id) = t2
and same_type(t,t2)
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
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.