Basic Typing
------------

First, let's define a simple language, essentially a small subset 
of ML (or Haskell for that matter).  The language comprises expressions, 
declarations, and types.

expressions -- expressions denoting (computing) values
  described by a BNF grammar

   n ::= 0, 1, 2, 3, ...  (numbers)
   b ::= true, false      (booleans)
   var ::= x, y, x1, y1, u, v, w, ...  (variables)
   exp ::= n | b | var
         | (exp1, exp2)     (pairs)
         | fn var => exp    (functions)
         | exp1 exp2        (function application)
         | if exp1 then exp2 else exp3   (conditional)
         | let decl in exp  (let expression)

   E.g. :  3, true, x, plus(2,y), fn x => mult(2,x)
           if eq(x,3) then 2 else 3
           (fn x = x+1) (plus(3,1))

declarations -- define names

   decl ::= val var = exp


types  -- a language of simple expressions (type expressions)

   ty ::= int | bool | ... 
        | ty1 -> ty2  |  ty1 * ty2  |  ...

type environments (contexts, static environments)
   -- finite mapping from variables to types (a dictionary)
   -- tyenv for short

Typing:
  exp --> ty
  dec --> tyenv

This only works for "closed expressions and declarations".
In general, we need to provide type environments (contexts)
to tell us the types of variables.

  exp * tyenv --> ty
  decl * tyenv--> tyenv


Typing Rules
------------
The typing rules tell us how to derive typing "judgements" of
the form 

    C ⊦ exp : ty

where C is a "context" or type environment assigning types to
a (finite) set of variables that may occur in exp.  E.g.

     x : int ⊦ x + 1 : int

There are typing rules for each form of expression and for 
declarations.

------------------------------ 
Constants:

Rules: TyConst

   C ⊦ n : int   (n an int constant, any context C)
   C ⊦ b : bool  (b a bool constant, any context C)

3 : int

true : bool

------------------------------ 
Variables

Rule: TyVar

   -----------------
      C ⊦ x : C(x)

E.g.

   C, x :int ⊦ x : int   (any context C)


------------------------------
Applications

Rule: TyApp

       C ⊦ e1 : t1 -> t2    C ⊦ e2 : t1
    -------------------------------------
	     C ⊦ e1 e2 : t2

E.g.

       C ⊦ even : int -> bool    C ⊦ 2 : int
    ----------------------------------------- [TyApp]
  	         C ⊦ even 2 : bool

  where C = even : int -> bool
    

------------------------------
Pairs

Rule: TyProd

       C ⊦ e1 : t1    C ⊦ e2 : t2
    ------------------------------
         C ⊦ (e1, e2) : t1 * t2

E.g.

        ⊦ 1 : int     ⊦ 2 : int
    ------------------------------ [TyPair]
          ⊦ (1, 2) : int * int


E.g. (using TyVar, TyPair, TyApp)

                                        C ⊦ 1 : int    C ⊦ 2 : int
                                      ------------------------------
       C ⊦ + : int * int -> int           C  ⊦ (1, 2) : int * int
    ------------------------------------------------------------------
                         C ⊦ +(1,2) : int

  where C = + : int * int -> int   (+ is a variable)


------------------------------
Functions

Rule: TyAbs

	 C, x: t1 ⊦ e : t2
    -----------------------------
       C ⊦ fn x => e : t1 -> t2

E.g.

	  x: int ⊦ x : int
    -----------------------------
       ⊦ fn x => x : int -> int


	  x: bool ⊦ x : bool
    -------------------------------
       ⊦ fn x => x : bool -> bool


	  x: X ⊦ x : X
    --------------------------  (X a type metavariable)
       ⊦ fn x => x : X -> X


    
                                        C1 ⊦ x : int    C1 ⊦ 2 : int
                                      ------------------------------
       C1 ⊦ + : int * int -> int           C1  ⊦ (x, 2) : int * int
    ------------------------------------------------------------------
                           C1 ⊦ +(x,2) : int
                  ------------------------------------
                     C0 ⊦ fn x => +(x,2) : int -> int

  where C0 = + : int * int -> int
  and   C1 = C0, x : int


------------------------------
Conditional Expr

Rule: TyCond

       C ⊦ e1 : bool    C ⊦ e2 : t    C ⊦ e3 : t
    ----------------------------------------------
            C ⊦ if e1 then e2 else e3 : t

E.g.

       ⊦ true : bool     ⊦ 3 : int     ⊦ 7 : t
    --------------------------------------------
             ⊦ if true then 3 else 7 : int


------------------------------
Declarations

New judgement form:

    C ⊦ decl : C

Rule: TyDecl

	   C ⊦ e : t
    --------------------------
      C ⊦ val x = e : (x : t)

E.g.

            ⊦ 3 : int
    --------------------------
      ⊦ val x = 3 : (x : int)

     
            C0 ⊦ fn x => x + 2 : int -> int
    ------------------------------------------------
      C0 ⊦ val f = fn x => x + 2 : (f : int -> int)

  where C0 = + : int * int -> int


------------------------------
Let exprs

Rule: TyLet  (simple version)

      C ⊦ decl : C'     C,C' ⊦ e : t
    ----------------------------------
          C ⊦ let decl in e : t

  where C,C' is the "concatenation" of the two contexts

E.g. 

      C0 ⊦ val f = fn x => x + 2: C1     C0,C1 ⊦ f 3 : int
    -------------------------------------------------------
          C0 ⊦ let val f = fn x => x + 2 in f 3 : int

  where C0 = + : int * int -> int
  and   C1 = f : int -> int


What are we missing?

  - recursive functions
  - polymorphic variables (polymorphism)


----------------------------------------------------------------------
A Typing Algorithm:

type var = string

datatype exp
  = Num of int
  | Bool of bool
  | Var of var          (* x *)
  | Pair of exp * exp   (* (exp1, exp2) *)
  | Fun of var * exp    (* fn var => exp *)
  | App of exp * exp    (* e1 e2 -- function application *)
  | If of exp * exp * exp  (* if exp1 then exp2 else exp3 *)
  | Let of decl * exp   (* let decl in exp *)

and decl
  = Decl of var * exp

datatype ty
  = INT | BOOL | FUN of ty * ty | Prod of ty * ty

type context = (var * ty) list

exception Unbound 
exception TypeError

(* getTy : var * context -> ty *)
fun getTy (var, nil: context) = raise Unbound
  | getTy (var, (var',ty)::c) = 
    if var = var' then ty else getTy (var, c)

(* expTy : exp * context -> ty *)
fun expTy (Num n, c) = INT
  | expTy (Bool b, c) = BOOL
  | expTy (Pair(e1,e2), c) =
    PROD(expTy(e1,c), expTy(e2,c))
  | expTy (App(rator,rand), c) =
      (case expTy(rator,c)
         of FUN(t1,t2) =>
	    let val randTy = expTy(rand,c)
             in if randTy = t1 then t2
	        else raise TypeError
            end
          | _ => raise TypeError)
  | expTy (Fun(x, e), c) =
      let val t = expTy(e, (x,U)::c)
       in FUN(U, t)
      end
  | expTy(Let(d,e), c) =
      let val c' = declTy(d,c)
       in expTy(e, c'@c)
      end

and declTy (Decl(x,e), c) =
    [(x, expTy(e,c))]


----------------------------------------------------------------------
Introducing type variables, with unification
----------------------------------------------------------------------

datatype ty
  = INT | BOOL
  | FUN of ty * ty
  | PROD of ty * ty
  | TVAR of string   (* or int, or ... *)

(* type substitutions - represented as association list *)
type tysubst = (string * ty) list  

(* emptyTysub : tysubst *)
val emptyTysub: tysub = nil

(* subTy : tysubst * ty -> ty *)
fun subTy (s, INT) = INT
  | subTy (s, BOOL) = INT
  | subTy (s, PROD(t1,t2)) = PROD(subTy(s,t1), subTy(s,t2))
  | subTy (s, FUN(t1,t2)) = FUN(subTy(s,t1), subTy(s,t2))
  | subTy (s, TVAR name) = lookup(name, s)

(* composeSub : tysubst * tysubst -> tysubst *)
fun composeSub (snew, sold) =
    let val sold' = map (fn (n,ty) => (n, subTy(snew,ty)) sold
     in snew @ sold'
    end

(* subContext : tysubst * context -> context *)
fun subContext(s,c) = 
    map (fn (n,t) => (n, subTy(s,t))) context

(* expTy : exp * context -> ty * tysubst *)
fun expTy (Num n, c) = (INT, emptyTysubst)
  | expTy (Bool b, c) = (BOOL, emptyTysubst)
  | expTy (Pair(e1,e2), c) =
      let val (t1, s1) = expTy(e1,c)
          val (t2, s2) = expTy(e2,subContext(s1,c))
       in (PROD(subTy(s2,t1), t2), composeSub(s2,s1))
      end
  | expTy (App(e1,e2), c) = 
      let val (t1,s1) = expTy(e1,c)
          val (t2,s2) = expTy(e2,subContext(s1,c))
          val tv = newTyvar()
       in case unify (subTy(s2,t1), Fun(t2,tv))
            of SOME s3 =>
	        (subTy(s3,tv), composeSub(s3,composeSub(s2,s1)))
             | NONE => raise TypeError
      end
  | expTy (Fun(x, e), c) =
      let val tv = newTyVar()
          val (t,s) = expTy(e, (x,tv)::c)
       in (FUN(subTy(s,tv), t), s)
      end
  | expTy (If(e1,e2,e3), c) =
      let val (t1,s1) = expTy(e1,c)
       in case unify(t1, BOOL)
            of NONE => raise TypeError
             | SOME s2 =>
    	         let val s2' = composeSub(s2,s1)
                    val c2 = subContext(s2',c)
		      val (t2,s3) = expTy(e2,c2)
		      val s3' = composeSub(s3,s2')
		      val c3 = subContext(s3,c2)
		      val (t3,s4) = expTy(e3,c3)
		      val s4' = composeSub(s3',s4)
		   in case unify(t2,t3)
		        of NONE => raise TypeError
                       | SOME s5 =>
		           (subTy(s5,t2), composeSub(s5,s4'))
                end			   
      end
  | expTy(Let(d,e), c) =
      let val (c',s) = declTy(d,c)
       in expTy(e, c'@(subContext(s,c)))
      end

(* declTy : decl * context -> context * tysubst *)
and declTy (Decl(x,e), c) =
      let val (t,s) = expTy(e,c))
       in ([(x, t)], s)
      end