In SML:
-------

parameterized types are defined as follows:

    type (<typeParameters>) <typeName> = <typeExpression>
    type ('a, 'b) pairList = ('a * 'b) list;

We can also define datatype declarations for parameterized data types.

Define Btree:

- datatype ('a,'b) Btree = LEAF of 'a 
=                        | NODE of 'b * ('a,'b) Btree * ('a,'b) Btree;
datatype ('a,'b) Btree
  = LEAF of 'a | NODE of 'b * ('a,'b) Btree * ('a,'b) Btree

- type intBTree = (int, int) Btree;
type intBTree = (int,int) Btree

The type intBTree is structurally identical to the iTree type defined below:

- datatype iTree = LEAF of int | NODE of int * iTree * iTree;
datatype iTree = LEAF of int | NODE of int * iTree * iTree


Example functions and their types
----------------------------------

- fun leftmost(LEAF(x)) = x
=     | leftmost(NODE(y, l, r)) = leftmost(l);
val leftmost = fn : ('a,'b) Btree -> 'a

Computes the leftmost element of a Btree. The return type would be the same
as the type of the argument of the LEAF constructor, and hence the
type ('a,'b) Btree -> 'a for the function.

- fun discriminants(LEAF(x)) = nil
=   | discriminants(NODE(y, l, r)) = 
=       let
=          val l1 = discriminants(l)
=          val l2 = discriminants(r)
=       in 
=          l1 @ (y::l2)
=       end;
val discriminants = fn : ('a,'b) Btree -> 'b list

Note: "@" is the operator in SML for concatenating two lists to produce
a new list. 

The above function operates by traversing the list recursively, and collecting
the discriminant values in all nodes of the tree into a single list. The
traversal order is left-to-right, i.e., an inorder traversal of the tree.

The return value is a list of elements, each of which has the same type 
as the first argument of NODE, i.e., type 'b. Hence the function has
the type ('a,'b) Btree -> 'b list

- fun append(x::xs, y) = x::append(xs, y)
=   | append(nil, y) = y;
val append = fn : 'a list * 'a list -> 'a list

This function concatenates two lists. (Performs the same function 
as the "@" operator). It does not care about the type of elements
in the list -- it does not even look at their values. Thus, the
function is polymorphic w.r.t. to the type of elements in the list.
However, we have to ensure that all elements of a list 
have the same type. Since elements from both argument lists
appear in the output list, this means that the element
types in both argument lists must be the same. 
This is captured by the type  'a list * 'a list -> 'a list

If we make a slight modification to append, so that in the
second rule, it discards y rather than returing y. 

- fun f(x::xs, y) = x::f(xs, y)
=   | f(nil, y)   = nil;
val f = fn : 'a list * 'b -> 'a list

In this case, the function would completely ignores the second argument.
Hence the second argument type does not matter at all, leading to the
type: 'a list * 'b -> 'a list

SML Operators that restrict polymorphism: 
          Arithmetic, relational, boolean, string, type conversion operators


SML Operators that allow polymorphism
          tuple, projection, list, equality ("=" and "<>")


Type equivalence
-------------------

1. Structural equivalence: two types are equivalent if they 
        are defined by identical type expressions.
   -- Issues: what components are counted? array range? record labels?
      Typically: array ranges are not considered as part of the type,
                 but record labels are considered part of the type.

2. Name equivalence: two types are equal if they have the same name.

3. Declaration equivalence: two types are equivalent if their 
     declarations lead back to the same original type expression
     by a series of redeclarations. 

Structural equivalence is the lest restrictive notion of type equivalence
among the above three, while name equivalence is the most restrictive.
Declaration equivalence is in between these two notions.

Pure name equivalence is not very useful:
    TYPE t1 = ARRAY [1..10] of INTEGER;
    TYPE t2 = t1;

  t1 and t2 are not equivalent. In
     v1: ARRAY [1..10] OF INTEGER;
     v2: ARRAY [1..10] OF INTEGER;  
  v1 and v2 have different types!

Using the notion of structural equivalence, t1 and t2 are equivalent;
v1 and v2 have equivalent types.

Using declaration equivalence, t1 and t2 are equivalent, but the
types of v1 and v2 are treated to be distinct.