🚀 go-pugleaf

-- 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)