is a type expression.
is a type-variable, then
is a type-expression.
1
2
are type-expressions then
1
2
is a type-expression.
is a type-expression.
is a type expression.
is a type-variable, then
is a type-expression.
1
2
are type-expressions then
1
2
is a type-expression.
is a type-expression.
is a type-expression, and 
is a map
from type-variables to type expressions, then () is extended to operate on type-expressions
(1 2) = (1) (2)
() =
1 = (2) for some , we say that 1 is an instance of 2.
We can define an equivalence relation on type expressions.
1 and
2 are equivalent if there exist
and ' for which
1 =
( 2)
and also
2 =
'( 1)
Or in other words, two type-expressions are equivalent if each is an instance of the other.
1,2 are unifiable, then there exists a most
general unifier = mgu(1,2), with the
property that
(1) = (2)
if '(1) = '(2) then there exists " such that
' = " o where
o is functional product.
The most general unifier is unique up to equivalence.
1
2) 
)
= (2)
if the most general unifier
= mgu(1,
)
exists.
=
for any type-variable . (We can
interpret this by saying that can be unified
with 
,
so that the previous rule could be applied).
((1
2) )
= otherwise
1 and
1 have no variables in common (if not,
we simply rename them).
operation defined above is well-defined.
1,
mgu(2,
3)) =
mgu(mgu(2,
2),3)
0, we have a type expression
that unifies with every
expression, then = for some
type-variable .
Suppose = ,
a type-constant. Then does not unify
with for
any type-variable .
Suppose =
1
2
Then does not unify with 0
So the only possiblity is that = ,
a type-variable.
1 and
2 have the property that for any
,
= mgu(1, )
iff
', '
= mgu(2, )
1 and 2
are equivalent.
1
1 = , a
type-constant.
Then
=
mgu(1, 1)
exists, so that
mgu(2, 1)
also exists. Therefore 2 =
or 2 = , for some
type-variable . In the latter case,
mgu( , ) exists, where
=
for some type variable . But this does not unify
with 1, a contradiction. Therefore
2 =
1 = , a
type-variable.
Then every expression unifies with
1, and so every expression unifies with
2
Hence by the lemma above, 2 = , is a type-variable, and so 1
and 2
are equivalent.
1
of height h
,
= mgu(1, )
iff
', '
= mgu(2, )
1 and 2
are equivalent.
Consider 1 of height h + 1,
and 2, supposing that
,
= mgu(1, )
iff
', '
= mgu(2, )
1 must have the form
11
12, and since
1 unifies with itself, it unifies
with 2. So 2
is either (a) a type-variable, or (b) it has the form
21
22.
But, if it were a type-variable, it would unify with
0, which 1
doesn't, so we are left with possibility (b).
Now suppose ' unifies with
21. Then, for any type variable
it is clear that
'
unifies with
11
12
hence, by our supposition,
'
unifies with
21
22
so that ' unifies with 21.
Conversely, any " which unifies with
21 also unifies with
11. Hence by the inductive hypothesis,
11 is equivalent to
21.
Similarly 12 is equivalent to
22. Hence 1 is
equivalent to 2, establishing our result.
K =
S =
(
)
( )
1) =
(
)
1
=
(( )
1) =
Now consider
1
2
3 ) =
((
)
( )
)
1
2
3 )
We may suppose that the variables of
1,
2 and
3
are distinct.
There are 2 cases.
),
1) exists.
In this case,
1 =
11
12
13
for some
11,
12,
13. Moreover
1
2
3 ) =
(((11
12)
11
13)
2
3 )
There are 2 sub-cases:
= mgu(
11
12 ,
2) exists.
In this sub-case,
2 =
21
22
where
(11) =
(21) =
'11
(12) =
(22) =
'12
(13) =
'13
Moreover
1
2
3 ) =
('11
'13)
3
There are two sub-sub-cases
' = mgu(
'11 ,
3) exists. In this sub-sub-case
1
2
3 ) =
'('13) =
'((13))
= "13
We'll also write
'((12))
= "12 and
'((11))
= "11
Now 11 and
3 have a common instance in
"11, so that
"' =
mgu(11, 3)
exists. Now consider
(1
3)
(2
3 )
=
((11
12
13)
3)
(2
3 )
=
(
"'12
"'13)
(2
3 )
Where
"'11 =
"'(11)
,
"'12 =
"'(12)
,
"'13 =
"'(13)
Proceeding, we obtain
(1
3)
(2
3 )
=
(
"'12
"'13)
(
(21
22 )
3 )
But 21 and 3
also have a common instance in "11
so that
"" =
mgu(21, 3)
exists. Hence
(1
3)
(2
3 )
=
(
"'12
"'13)
""22
Where
""22 =
""(22).
Since
"11
is a common instance of
11, 3
there exists
- for which
-('''
(11))
=
'( (11))
-('''
(12))
=
'( (12))
=
"12
-('''
(13))
=
'( (12))
=
"13
(for we we are free to choose - so that
the function product
- o '''
agrees with
' o
for those variables of 12,
13 that do not
occur in 11).
Likewise, since "11 is a common instance of
3 and 21
there exists
x
for which
x(""
(21))
=
'( (21))
= "11
x(""
(22))
=
'( (22))
= "12
for we can choose x so that the
function product
x o ""
agrees with the function product
' o
for those variables of 22 that do not occur
in 21.
Thus "12 is an instance of
"'12 and ""22.
Hence there exists
+ =
mgu(
"'12, ""22),
and moreover "12 is an instance of
+('12)
= +12, say, that is, for
some y,
"12
=
y
(+12),
"13
=
y
(+13)
where again we may choose y so that
y o
+o "'
agrees with
' o
for those variables of 13 that do not
occur in 12.
Now +12 is an instance of
12 and 22.
Hence there exists # for which
#('12) =
+12
#(
(11))
=
+("'
(11))
= +11
# as we have chosen maps before to
agree appropriately on variables not occurring in
12.
That is
#
('11)
=
+
("'11)
+11 is a common
instance of 3 and
'11. Therefore, as above, there exists
z for which
z('
((1)))
=
+("'
(1))
z('
((13)))
=
+("'
(13)
On the other hand
y(+
("'(13)))
=
'
((13))
""13 and
"13 are instances of each other, and
so the equivalence classes are equal.
Thus the result is true in this sub-sub-case.
'11 ,
3) does not exist. In this sub-sub-case
1
2
3 ) =
Now consider
(1
3)
(2
3 )
=
((11
12
13)
3)
(2
3 )
Now suppose
"' = mgu( 11 ,
3) does exist.
=
"'(
12
13)
(2
3 )
=
"'(
12
13)
(
(21
22)
3 )
Likewise, suppose
"" = mgu( 21 ,
3) does exist.
"'(
12
13)
""(22)
=
("'(12)
"'(13))
""(22)
Finally, suppose
+ =
mgu
("'(12),
""(22))
exists. Then +12 is a common
instance of 12 and
22. Therefore there exists
# for which
#(
(12))
=
+("'
(12))
= +11,
#(
(11))
=
+("'
(11))
= +11
Thus 11 and
11 have a common instance, a contradiction
to the basic assumption of sub-sub-case 1.1.2. Hence either of the most
general unifiers we have subsequently supposed to exist in this
sub-sub-case does not exist. In either of these circumstances
(1
3)
(2
3 )
= 
= mgu(
11
12 ,
2) does not exist.
In this sub-case we can, as above, construct
+ and # leading
to the conclusion that, if
(1
3)
(2
3 )
then
11
12
and 2 does exist
),
1) does not exist. In this case
(S
1
2
3 )
=
1
(11
12), for any 11, 12
(not the same as the previous quantities of this name)
then
(1
3)
(2
3 )
=
(2
3 )
=
=
(S
1
2
3 )
1 =
(11
12)
where 12
(121
122) (for if it had this form,
we would be in Case 1)
In this case (1
3) is an instance
of 12, which will give
when applied to (2
3 )
= ( )
( ).
d0) d1 =
d0 d1
There are 3 cases
a type-constant.
d0) d1
= d1
=
= d0 d1
a
type-variable.
d0) d1
=
( )
) d1
=
While
d0 d1 =
01
02
Here
d0 = d0
so the required equation is immediate.
D
d = d1 d
d0 =
d1
Then for any
function type 1 2,
1 2
= 1 2.
However, for any non-function
type , = bottom.
Suppose
11 12) = (21 22)
for all .
11 12)
11 = 12 = (21
22) 11 = (22)
where
= mgu(11,21). Thus 12 is an instance of 22. Likewise 22 is
an
instance of 12. Hence 12 is equivalent to 22.
Moreover, any that unifies with
11 necessarily unifies with
12, and conversely. So, by Lemma TA3 above,
we have that 11 is equivalent to
12.
=
that is
)
( )
( 
)
( )
=
( )
( )
=
x) must have the type-value
, since if x had the type
(1
2)
we would require that a term unify with a proper sub-term, which is
impossible.
In particular both Curry's and Turing's fixpoint combinators involve
self-application, so both map to in the type-algebra.
However the following lemma shows that the existence of a
well-typed fixpoint operator is not ruled out.
)
)
=
(1
2)
1
2.
Consider
=
((( )
)
)
((1
2)
1
2)
=
1
2
On the other hand
(Ytype )
=
((1
2)
1
2)
1
2
=
1
2
has any other form, then
=
=
(Ytype )
Thus establishing our result.
let variable = expr1
in expr2
end
as being a sugared form of
variable . expr2)
expr1
expression. Consider for example the following POP2000 fragment
let m = map
in
length (m sin list1) + length (m hd list2)
end
Here map has the polymorphic type
(->) -> (List ) ->
(List ), but the first occurrence of m
has the instance
(float -> float) -> (List float) -> (List float)
while the second has type
((List ) -> ) -> (List (List )) -> (List )
but if we consider the corresponding form:
(( m.
length (m sin list1) + length (m hd list2)
) map)
we have a problem that m is not, according to the usual rules, allowed
to have different instances of a polymorphic type. We can
(( m1.
length (m1 sin list1) + length (m2 hd list2)
) map map)