(worked-typing-examples.txt)

Manual type checking/inference examples
---------------------------------------

I present below a systematic manual procedure for carrying out manual
typechecking. There are two main points to pay attention to. One is
that each step should be labeled by the particular subexpression or
declaration that is being analyzed, and the second is that at each
point one maintains a "context" or "type environment" that maps bound
expression variables to their approximate types, which are type
expressions that contain "unification variables" representing unknown
types. This procedure as shown in the worked examples goes beyond the
typechecker in typecheck2.zip in that it allows multi-rule (clausal)
function definitions with pattern formal arguments (e.g. the append
function in example 1). Thus it is close to what is actually required
for full SML definitions and expressions.

In the type environment, each variable binding is labeled with
either F or L. An F binding indicates a lambda-bound variable,
i.e. a function formal parameter (including argument pattern
variables on the left-hand-side of a function definition). Types
of lambda bindings cannot be generalized.

An L binding involves a let-bound variable, which may have a 
polymorphic type if the some of the variables in the type of
its definition rhs can be generalized.

Function names in fun declarations are treated as F bindings while
typing the definition of the function, because all occurrences of
the function in its own definition must have the same type. Once
the typing of the function is complete, the type of the function
may be generalized and the function variable binding becomes an
L binding.

We add bindings to the type environment whenever we enter scopes
(e.g. bodies of let expressions or function expressions (or RHS of
function declarations). We update the types in the type environment
whenever we unify constraint equations, i.e. we apply the substitution
produced by unification to the context and other appropriate types to
eliminate all occurrences of the type variables that were solved for
in that unification.

----------------------------------------------------------------------
Examples
----------------------------------------------------------------------

1. Typecheck

    fun append (nil, ys) = ys
      | append (x::xs, ys) = x :: append(xs,ys)

We type each rule separately, and the type assigned to append must
agree. We ensure this using the type of append derived from the
first rule in the initial environment for typing the second rule.

[@ append function header, rule 1]
env: F append : A
[@ nil pattern]
  nil: B list    -- instance of 'a list, the polymorphic type of nil
env: F append: A; F ys : YS
[@ (nil, ys) pattern]
  (nil, ys) : B list * YS
[@ append function header]
  append : (B list * YS) -> Z
    A = (B list * YS) -> Z
  append (nil, ys) : Z
env: F append: (B list * YS) -> Z; F ys : YS
[@ rhs, rule 1]
  ys : YS  -- lookup ys in type env

    Unify LHS and RHS types:
      Z = YS
    env: F append : (B list * YS) -> YS
      (drop ys binding because we are leaving its scope)


[@ append function header, rule 2]
env: F append : (B list * YS) -> YS; F x : X; F xs : XS; F ys : YS'
  (add F bindings for argument pattern variables)
[@ argument pattern x::xs]
:: : C * C list -> C list   -- instance of :: : 'a * 'a list -> 'a list
(x,xs) : X * XS     -- pair rule
x::xs : X list      -- apply rule
  C = X
  XS = X list
env: F append : (B list * YS) -> YS; F x : X; F xs : X list; F ys : YS'
[@ argument pattern (x::xs,ys)]
(x::xs,ys) : X list * YS'
[@ append function header]
append(x::xs,ys) : YS'
  B = X
  YS = YS'
env: F append : (X list * YS') -> YS'; F x : X; F xs : X list; F ys : YS'

[@ rule 1 RHS]
:: : D * D list -> D list
(xs,ys) : X list * YS'
append(xs,ys) : YS'
x :: append(xs,ys) : X list
  D = X
  YS' = X list
env: F append : (X list * X list) -> X list; F x : X; F xs : X list; F ys : X list

[@ defn of append, implicitly a top level let (or val rec)]
F append : X list * X list -> X list
Generalize:
L append : 'a list * 'a list -> 'a list
----------------------------------------

2. Typecheck

    fun f x =
        let fun g y = x
         in g true + 1
        end

[@ f function header (LHS)]
env: F f : F; F x : X    -- new type variables F, X

[@ (f x)]
f x : U         -new U
  F = X -> Y
env: F f : X -> U; F x : X

[@ g function header]
env: F f : X -> U; F x : X; F g : G; F y : Y   -- new G, Y
[@ (g y)]
g y : Z        -- new Z
  G = Y -> Z
env: F f : X -> U; F x : X; F g : Y -> Z; F y : Y

[@ g RHS: x]
x : X
[@ g defn - unify LHS and RHS types]
  Z = X
drop y binding
env: F f : X -> U; F x : X; F g : Y -> X

generalize type of g, changing to L binding
env: F f : X -> U; F x : X; L g : ∀'a. 'a -> X

[@ let body (g true + 1)]
+ : int * int -> int     -- ignoring overloading
true : bool
g : V -> X    -- new V, instance of polytype of g
g true : X
  V = bool    -- V not in type environment, so type env not affected
+(g true, x) : int
  X = int
env: F f : int -> U; F x : int; L g : ∀'a. 'a -> int

[@ RHS f defn]
let fun g ... end : int
env: F f : int -> U; F x : int
[@ f defn, unify LHS and RHS types]
  U = int
env: F f : int -> int

generalize type of f (no effect, since no unification
variables to generalize) and switch to L binding:

env: L f : int -> int
-------------------------

3. Typecheck

    fun f x = 
        let fun h y =
                let fun g z = z :: y
                 in g x
                end
         in h x
        end

[@ f function header]
env: F f : F; F x : X
f x : W
  F = X -> W     -- application rule
env: F f : X -> W; F x : X

[@ h function header]
env: F f : X -> W; F x : X; F h : H; F y : Y 
h y : U
  H = Y -> U
env: F f : X -> W; F x : X; F h : Y -> U; F y : Y 

[@ g function header]
F f : X -> W; F x : X; F h : Y -> U; F y : Y; F g : G; F z : Z 
g z : V
  G = Z -> V

[@ g RHS]
env: F f : X -> W; F x : X; F h : Y -> U; F y : Y; F g : Z -> V; F z : Z 
:: : A * A list -> A list
z :: y : Z list
  A = Z
  Y = Z list

[@ g binding, equating types of g header and g RHS]
env: F f : X -> W; F x : X; F h : Z list -> U; F y : Z list; F g : Z -> V; F z : Z 
g z = z :: y   ->
  V = Z list

[@ inner let body: no generalization because x: Z nonlocal at g binding.
 Note that g binding switches from F to L]
env: F f : X -> W; F x : X; F h : Z list -> U; F y : Z list; L g : Z -> Z list
g x : X list
  Z = X
env: F f : X -> W; F x : X; F h : X list -> U; F y : X list; L g : X -> X list

[@ h RHS]
env: F f : X -> W; F x : X; F h : X list -> U; F y : X list
let fun g ... end : X list

[@ h binding: equating types of h header and h RHS]
  U = X list
env: F f : X -> W; F x : X; F h : X list -> X list
generalize type of h (no generalization because X nonlocal)
env: F f : X -> W; F x : X; L h : X list -> X list

[@ outer let body]
env: F f : X -> W; F x : X, L h : X list -> X list
h x : ?
  X = X list

Unsolvable because of occurence check in unification: X occurs in X
list. Thus a type error!