ghosr@sersun0.essex.ac.uk (Ghosh-Roy R) (01/22/91)
-- Read the PhD thesis "M. Gerritsen, Type Assignment Functions" 1988.
-- University of Twente
-- She built a type inference algorithm where the occurrences of variables
-- not necessarily have the same type.
-- Instead she uses `conjuction types': *a & *b .
-- (\x.x o x) has the type ((*b->*c)&(*a->*b))->*a->*c which sais that x
-- must be
-- instantiatable as *a->*b and as *b->*c .
-- Application of (\x.x o x) to hd yields the equations:
-- *a->*b = List *d->*d (and so: *a=List *d, *b=*d)
-- *b->*c = List *e->*e (and so: *b=List *e, *c=*e)
-- The two occurrences of x have types List *d->*d and List *e->*e
-- respectively.
-- Solving the equations yields:
-- *a=List (List *e)
-- *b=List *e
-- *c=*e
-- *d=List *e
-- and so
-- (\x.x o x) hd::*a->*c = List (List *e)->*e
--
-- In this type inference system there is no more need for an explicit
-- let-construct.
The intersection systems were probably developed for the same reason!
-- All Milner-typable expressions are also typable in this scheme, but
-- some
-- non Milner-typable expressions too.
-- Try `twice twice k' where
-- twice f x = f (f x)
-- k x y = x
--
-- Mark Ramaer
I have a copy of the paper `Type Deduction Systems For Functional Languages'
authored by Mirjam Gerritsen and Gerrit F van der Hoeven; this paper was
submitted to TAPSOFT-87.
In all, 5 (ABCDE) systems were described using Conjunction-Types. The types
assigned to
Twice Twice : (('b->'c) ^ ('a->'b)) -> ('d->'e).
(\x.xx) Twice : (('b->'c) ^ ('a->'b)) -> ('d->'e).
Let us now define a function say,
f x = [x], i.e., f : 'a -> 'a-list
Try `Twice Twice f' and one gets stuck since the type variables 'd or 'e
are completely independent from the domain variables. I believe that the
unification procedure for Conjunction-Types described in the paper needs
to be modified. Otherwise the system is the same as the intersection
systems without the `\omega' rule.
In GR system, the type assigned to
Twice Twice : (('a->'b) ^ ('b->'c) ^ ('c->'d) ^ ('d->'e)) -> ('a->'e).
(\x.xx) Twice : (('a->'b) ^ ('b->'c) ^ ('c->'d) ^ ('d->'e)) -> ('a->'e).
Apply f to (Twice Twice) and you get ('a -> 'a-list-list-list-list) as
expected.
Try `Twice Twice Twice k' if you wish.
Rana
(0206) 87 22 97 (0206) 82 42 63 National
+ 44 206 87 22 97 + 44 206 82 42 63 InterNational
Room No.: 4B.526, Department of Computer Science, University of Essex
Wivenhoe Park, Colchester Essex CO4 3SQ, England, UK (ghosr@essex.ac.uk)