Transcript Type Checking

CS321 Functional Programming 2
Type Checking
Polymorphism in Haskell is implicit.
ie the system can derive the types of all objects.
This is different to the philosophy of languages like Pascal
where all typing is explicit.
The aim in this part of the course is to examine in more detail
how the type of any object (function, or expression) can be
derived.
© JAS 2005
3-1
CS321 Functional Programming 2
The basis for a type checking algorithm was worked out by
Robin Milner (who used to be here at Swansea) in the mid
1970s.
Much of the theoretical background to the type checking
algorithm cames from work on the typed λ-calculus, in
particular work done by Roger Hindley (who is still here at
Swansea).
People refer to the type checking algorithm as the Milner or
Hindley-Milner type checking algorithm.
© JAS 2005
3-2
CS321 Functional Programming 2
Consider the following function in Haskell:len lis = if lis == []
then 0
else 1 + len (tail lis)
if
[]
0, 1
tail
+
lis
(==)
len
::
::
::
::
::
::
::
::
Bool -> a -> a -> a
[b]
Int
[c] -> [c]
Int -> Int -> Int
d
e -> e -> Bool
f
© JAS 2005
3-3
CS321 Functional Programming 2
len lis = if
(==)
e->e->Bool
Bool
then 0
Int
else (+)
lis
d
[]
[b]
1 len (tail lis)
[c]->[c] d
f
[c]
Int->Int->Int Int
g
Int
Bool->Int->Int->Int
d
Int
len::[c]->Int with e=d=[b];d=[c];f=[c]->g; g=Int
© JAS 2005
3-4
CS321 Functional Programming 2
Consider another example:-
oops fn lis = if lis == []
then []
else (fn(head lis)):fn (tail lis)
if
:: bool->a->a->a
(==) :: b->b->bool
[]1 :: [c]
[]2 :: [d]
(:) :: e->[e]->[e]
head :: [f]->f
tail :: [g]->[g]
fn
:: h
lis :: i
© JAS 2005
3-5
CS321 Functional Programming 2
oops fn lis =
if (==)
lis []
b->b->Bool i [c]
then []
[d]
else (:) (fn(head
lis)) (fn (tail
lis))
[f]->f i
h
f
[g]->[g] i
h
[g]
b=i=[c];i=[f]; i=[g]; h=f->j; h=[g]->k
f=[g]=i=[f]
3-6
© JAS 2005
CS321 Functional Programming 2
A Type Checking Algorithm
We have derived type equivalences.
This is essentially an example of term unification.
This idea can be defined without reference to types.
Let us assume that we are given a collection Ops of operators
and a collection Vars of variables.
The family Terms of terms is then defined:Terms ::=Vars | (Ops, [Terms,...., Terms])
Thus an "unsugared'' version of the expression:1 + x * y is:- (+,[(1,[]),(*,[x,y])])
© JAS 2005
3-7
CS321 Functional Programming 2
Any function that assigns terms to variables is called a
substitution.
Every such function may be extended to act upon terms.
If σ is a substitution then Σ is a function Terms -> Terms defined:Σ(v) = σ(v) forall v є Vars
Σ(o,[t1,..tn]) = (o,[Σ(t1),..Σ(tn)]) forall є Ops
Suppose σ assigns "x+y'' to "x'' and "0'' to "y'' then
Σ(1+x*y) = 1+(x+y)*0
© JAS 2005
3-8
CS321 Functional Programming 2
Two substitutions σ and t may be combined:τ;σ(v) = (Σ . τ)(v) = Σ(τ(v)) forall v є Vars
A unifier for any two terms, t and t', is any substition σ such
that Σ(t) = Σ(t').
The most general unifier of two terms is the unifier σ0 of
these terms such that for any other unifier σ1 there exists a
unification τ such that σ1 = σ0; τ.
It can be proved that for any pair of unifiable terms a most
general unifier (unique up to renaming of variables) exists.
Term unification is the process of finding the most general
unifier.
© JAS 2005
3-9
CS321 Functional Programming 2
How do we find the most general unifier, mgu, of two terms, t and t‘?
Need to consider both variables and operators.
If t is a variable that does not occur in t' then mgu(t,t') is the
substitution [t'/t] of term t' for t.
The reverse is true if t' is a variable that does not exist in t.
If t is a variable that does occur in t' there is no unifier unless t=t'.
For operators then it is clear that for two terms no unifier can exist
unless the operators are equal.
If the operators are equal then a unifier can exist iff the argument lists
are equal in length and the arguments are pairwise unifiable by the
same substitution.
© JAS 2005
3-10
CS321 Functional Programming 2
Consider the two terms:(o,[t1,....,tn])
(o,[t'1,....,t'n])
and let the following substitutions exist
σ1 = mgu(t1,t'1)
σ2 = mgu(Σ1t2,Σ1t'2)
σ3 = mgu(Σ2(Σ1t3),Σ2(Σ1t'3))
..........
σn = mgu(Σn-1(Σ2(Σ1tn)),Σn-1(Σ2(Σ1t'n)))
then
mgu(t,t‘) = σ1; σ2;......;σn
© JAS 2005
3-11
CS321 Functional Programming 2
To write a program to perform the type checking we would
need a type to represent a type expression:
type Tvname = String
data Texp = Tvar Tvname
| Tcons String [Texp]
arrow :: Texp -> Texp -> Texp
arrow t1 t2 = Tcons "arrow" [t1,t2]
int :: Texp
int = Tcons "int" []
cross :: Texp -> Texp -> Texp
cross t1 t2 = Tcons "cross" [t1,t2]
list :: Texp -> Texp
list t = Tcons "list" [t]
© JAS 2005
3-12
CS321 Functional Programming 2
A subsitution function maps type variable names to type expressions
type Subst = Tvname -> Texp
We can extend this to apply to type expressions
sub_type :: Subst -> Texp -> Texp
sub_type phi (Tvar tvn) = phi tvn
sub_type phi (Tcons tcn ts) =
Tcons tcn (map (sub_type phi) ts)
Composition of substitutions is possible
scomp :: Subst -> Subst -> Subst
scomp sub2 sub1 tvn = sub_type sub2 (sub1 tvn)
© JAS 2005
3-13
CS321 Functional Programming 2
We define an identity substitution
id_subst :: Subst
id_subst tvn = Tvar tvn
such that
sub_type id_subst t = t
A delta substitution is one that affects only one variable and
all other substitutions can be built from the identity
substitution by composition on the left with delta
substitutions.
delta :: Tvname -> Texp -> Subst
delta tvn t tvn' = if tvn == tvn'
then t
else Tvar tvn'
© JAS 2005
3-14
CS321 Functional Programming 2
Assume a data type to allows to return success (a Subst) or failure
data Reply a = OK a | FAILURE
A unification function will be applied to pairs of Type expressions
unify :: Subst->(Texp,Texp)->Reply Subst
unify phi ((Tvar tvn),t)=
unify phi ((Tcons tcn ts),(Tvar tvn))=
unify phi ((Tcons tcn ts),(Tcons tcn' ts')) =
© JAS 2005
3-15
CS321 Functional Programming 2
Applying type checking to Haskell
Need to extend from simple function abstractions and
applications to include (for example)
Pattern Matching
for each case the type of the pattern(s) must be consistent
Guards
each guard must be of type Bool
Type Classes
© JAS 2005
3-16
CS321 Functional Programming 2
Type Checking Classes – An Example
member :: Eq a => [a] -> a -> Bool
member []
y = False
member (x:xs) y = (x == y) || member xs y
e :: Ord b => [[b]]
member
e
[a]=[[b]];
[a]->a->Bool [[b]]
(Eq[b],Ord b)
[b] -> Bool
Recall instance Eq => Eq [a]…
class Eq a => Ord a…
(Eq b, Ord b)
Ord b
Ord b => [b] -> Bool
© JAS 2005
3-17
CS321 Functional Programming 2
member
[id]
Eq a => [a]->a->Bool [a->a]
[a->a] not an instance of Eq
© JAS 2005
3-18