Polymorphism
------------

ML and Haskell have a feature called polymorphic types (parametric polymorphism).

This is different from the notion of polymorphism used in O-O languages, which
is based on subclassing (subtypes).

Example 1. Simplest example: the identity function

- val f = fn x => x;     (or fun f x = x;)
val f = fn : 'a -> 'a

Any particular use of f can have any instance of the polymorphic type 'a -> 'a.
We can write this polymorphic type as

    ∀α.α → α.

How do we type fn x => x?

1. Assign a type variable, say U, as the type of the bound variable x. Think
of this as the hypothetical type of the parameter x.

2. Computer the type of the body of the function.  In this case the body
is the expression x, whose type is U.

3. The type of the function is U -> U (a function type from the argument
type U to the body type U).

4. No equational constraints were generated, so U is unconstrained.  It
could therefore be any type.  Therefore we can "quantify" or generalize
U to produce the polymorphic type ∀α.α → α.  We replace U with a
bound type variable α and universally quantify α.

The SML system prints this polymorphic type as 'a -> 'a.

--------------
Example 2: Applying a polymorphic function.

How do we type check (f 3)?
The type of f inferred from its definition is:

    f : ∀α.α → α

This means that a given use of f (an "applied occurrence" of f) can
take on any "instance" of the polymorphic type. We represent a
potential instance by replacing α with a type variable U whose
value is to be determined.

    f : U → U

The type of the argument is known:

    3 : int

By the typing rule for application, the type of the argument 3
and the domain type of f must agree, giving us the equation:

    U = int

Then the range type of (this occurrence of f) is also int, so
the type of f 3 is int:

    f 3 : int


--------------
Example 3: A function with pattern argument.

    fun g (x,y) = (y,x)

We assign type variables representing the unknown types of the
argument variables x and y:

    x : U,  y : V

Then the type of the pair (x,y) is determined by the rule


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


where C is a type environment assigning types to free variables
that might occur in e1 and e2.

In our case, we are assuming the context 

    C = x : U,  y : V

    (x,y) : U * V

And this will be the domain type of the function g. The range
type is the type of the body (y,x) in the same context C.

    (y,x) : V * U

So the type of g is

    g : U * V → V * U

Since there are no further constraints, U and V could take on
any types as their meanings, so we generalize to 

    g : ∀ α. ∀ β. α * β → β * α 

or

    g : ∀ α, β. α * β → β * α 

In the application

    g(true,3)

g's type would be instantiated to

    g : bool * int → int * bool

=>  g(true,3) : int * bool

Which agrees with the value of g(true,3), which is (3,true).


--------------
Example 4: A recursive, polymorphic function on lists.

    fun length nil = 0
      | length (x::xs) = 1 + length xs


The list type constructor is defined as a datatype:

    datatype 'a list = nil | :: of 'a * 'a list

This defines list, but also the data constructors nil and ::.
Their types are polymorphic:

    nil : ∀ α. α list

    ::  : ∀ α. α * α list → α list

To type the definition of list, we type the two equations
(rules) independently and then unify their types.

    length nil = 0

The argument pattern nil gets an instance of the polymorphic
type of nil:

    nil : U list

This is the domain type of length. The range type is the type
of the rhs: 0.  

    0 : int

So the type of this rule is

   Rule 1: U list → int

The second rule has a cons pattern as the argument, we type it
as follows, starting with the argument pattern ::(x,xs).

   x : V                       -- unknown types of x, xs

   xs : W

   :: : Z * Z list → Z list    -- instance of polytype of ::

   (x,xs) : V * W              -- product rule

   ::(x,xs)

      V * W == Z * Z list      -- domain of :: has to match type of (x,xs)
  ==>  V == Z                  -- solving for V, the type of x
  ==>  W == Z list             -- solving for W, the type of xs

   ::(x,xs) : Z list           -- application rule

   with resulting context

     C0 = x: Z, xs : Z list

   describing the bound pattern variables x, xs

Now we type the rhs of the second rule, using context C0

   xs : Z list

   length : R → S             -- unknown function type of length

   length xs : S              -- application rule
 ==> R == Z list              -- solving for R

   + : int * int → int        -- from the primitive typing environment

   1 : int

   (1, length xs) : int * S   -- pairing rule

   +(1, length xs) : int
 ==> S == int		      -- solving for S

 ==> length : Z list -> int

   Rule 2:  Z list -> int

Now we unify the types of Rule 1, Rule 2 and the inferred type of the
recursive call of length:

   Rule 1 : U list -> int
   Rule 2 : Z list -> int
   length : Z list -> int

 ==> U == Z                   -- solving for U (could have been Z == U)

 and the type of the defined function length is

   length : Z list -> int

 Since nothing constrains Z, it can take on any type, so we generalize
 the type to get

   length : ∀ α. α list -> int


------------------
Example 5: local polymorphic functions

    let fun id x = x
     in (id 3, id true)
    end

Here we type check the definition of id as before, including 
generalizing to get a polymorphic type:

    id : ∀α. α → α 

Then in the body the two occurrences of id get the instances

    id : int -> int

    id : bool -> bool

so  (id 3, id true) : int * bool


Example 6. Nested functions:

(1)

    fun f1 x =
        let fun g y = (x,y)
         in (#2(g 3) + 1, not (#2(g true)))
        end 

(2) 

    fun f2 x =
        let fun g y = (x,y)
         in (#1(g 3) + 1, not (#1(g true)))
        end 


Typing f1

      x : U   -- argument of f1

  typing g, in context C0 = x: U

      y : V

      (x,y) : U * V

      g : V → U * V

  generalizing (both U and V?)

      g : ∀α,β. α → β * α 
      
  typing body of let

    #2(g 3) + 1 : int         where g : int -> W * int
    not(#2(g true)) : bool    where g : bool -> T * bool
    
    (#2(g 3) + 1, not (#2(g true))) : int * bool

    let ... end : int * bool

    f1 : U -> int * bool

    f1 : ∀α. α → int * bool


But the typing of f2 would seem to go exactly the same,
except for the steps:

    #1(g 3) + 1 : int         where g : W -> int * W
    not(#1(g true)) : bool    where g : T -> bool * T
    (#1(g 3) + 1, not (#1(g true))) : int * bool

    ...
    f2 : ∀α. α → int * bool

But what happens when we apply f2?
    
    f2 5

x gets bound to 5, x is an integer, and so g true = (5,true),
so #1(g true) = 5, so not(#1(g true)) is a type error, which
should have been detected!

Problem: we were too indescriminate when generalizing type
of g.

      g : V → U * V    in context C0 = x : U

We could generalize V, but we should not have generalized U,
which is the type of x bound in a surrounding context.

We should have had, for the generalized type of g:

     g : ∀α. α → U * α

Then the typing of the let-body would still work:

    #2(g 3) + 1 : int         where g : int -> U * int
    not(#2(g true)) : bool    where g : bool -> U * bool
    
    (#2(g 3) + 1, not (#2(g true))) : int * bool

But the corresponding typing of the f2 let-body would not
work:

    #1(g 3) + 1 : int         where g : int -> int * int

  ==> U = int       -- solving for U, globally affecting
                       the type of g, not just this particular
                       occurence of g

    not(#1(g true)) : ERROR!    where g : bool -> int * bool


This leads to the following "let rule" for typing local
let-bindings (t1 and t2 represent type expressions):

     C ⊦ e1 : t1       C, x : Gen(C,ty1) ⊦ e2 : t2
   --------------------------------------------------
	    C ⊦ let x = e1 in e2 : t2

where for any context C and type t, Gen(C,t) is the polymorphic
type produced by generalizing any unification type variables (like
U,V, etc. above) that occur in ty, but do NOT occur in the context C.