Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!mnetor!uunet!seismo!mcvax!lambert
From: lambert@cwi.nl (Lambert Meertens)
Newsgroups: comp.lang.misc
Subject: Re: Polymorphic Type Systems: some unsolved problems
Message-ID: <29@piring.cwi.nl>
Date: Wed, 5-Aug-87 16:43:55 EDT
Article-I.D.: piring.29
Posted: Wed Aug  5 16:43:55 1987
Date-Received: Sat, 8-Aug-87 08:51:24 EDT
References: <watcgl.1506> <1365@ogcvax.UUCP>
Organization: CWI, Amsterdam
Lines: 130

In article <1365@ogcvax.UUCP> pase@ogcvax.UUCP (Douglas M. Pase) writes:
] In article <watcgl.1506> kdmoen@watcgl.UUCP (Doug Moen) writes:
] >1) Write a single function 'twice' such that
] >      twice(f, x) = f(f(x))
] >   for any function f and value x for which this makes sense.
] 
]         let twice = \f. \x. f (f x) ;
] 
]         twice : (*a -> *a) -> *a -> *a

If f : *a -> {*a}, f composed with f makes sense and has type *a -> {{*a}},
but this is not covered by the type given for twice.  (The notation {T}
means Set_of(T).)

What you want is something like

         twice : (*a -> *F(*a)) -> (*a -> *F(*F(*a))),

in which *F is a "higher-order" type: a type former rather than just a
(poly)type.  Unification on such animals is much tougher, which gives a
pragmatic but rather compelling reason not to include them in polymorphic
typing systems.  Just try to determine the type of twice(twice) by
simulating a unification algorithm (with renaming of type variables, of
course).

I don't think this is entirely impossible if a type-former variable like
*F can be refined by notation like T1=>T2, in which T1 and T2 are polytypes
that can contain doubly starred type variables (bound to this type
function).  For example, **x => {**x} would be a function that applied to
*a gives the type {*a}.

You can first unify the type of twice to (a marked version of) its argument
type:

         (*a -> *F(*a)) -> (*a -> *F(*F(*a))),

              *a'       ->      *F'(*a').

We find *a' = *a -> *F(*a), and substituting that in *F'(a') leads to the
problem of unifying

          *a -> *F(*F(*a))

with

          *F'(*a -> *F(*a)).

This is solved by *F' = (**a -> **F(**a)) => (**a -> **F(**F(**a))).
We have to determine *F'(*F'(*a')); taking a shortcut since we have
*F'(*a') already, we have to determine

          *F'(*a -> *F(*F(*a))).

This can be done by handling *F' as an ordinary function type with
refreshed variables (replace **a with *a" and **F by *F"):

        (*a" -> *F"(*a")) => (*a" -> *F"(*F"(*a")))

Unification of the argument type with *a -> *F(*F(*a)) gives

        *a" = *a,

        *F" = **a => *F(*F(**a)).

So now the result (the type of twice(twice) we wanted to determine) is

        *a -> *F"(*F"(*a)),

in which the apllication (twice:-) of *F" is straightforward, giving

        *a -> *F(*F(*F(*F(*a)))).

This simple-minded approach works fine in this case, but undoubtedly not
always.  I don't know what the exact limitations are.  What happens for
example on recursively defined functions?

] >3) Define a function 'apply' such that
] >      apply(f, arglist)
] >   calls the function 'f' with 'arglist' as an argument list,
] >   for any function f, and any argument list that can legal be
] >   passed to it.
] 
] I find it hard to fathom exactly what is wanted here.  My own guess results
] in the trivial function
] 
]         let apply = \ f . f ;
] 
]         apply : *a 
] 
] This works, because apply is an implicit operator in the language.

Apply as defined here is the identity function and so should have type
*a -> *a.  This is however a Curry'd version of the function asked for.  If
instead of an arglist (which, by the way, is an existing Dutch word meaning
"guile") we have a simple arg, a solution is

        let apply =  \ (f, a) . f(a) ;

        apply : ((*a -> *b) X *a) -> *b.

So what you want to express is something like

        let apply =  \ (f, a1, ... , an) . f(a1, ... , an) ;

        apply : (((*a1 X ... X *an) -> *b) X *a1 X ... X *an) -> *b.

If there were something like a cons-onto for tuples and a corresponding
type former, you could imagine something like

        let apply =  \ (f ,: a) . f(a) ;

        apply : ((*a -> *b) X: *a) -> *b.

For the unification algorithm this is not particularly difficult.
You need something like a disjoint-union discrimination and a polymorphic
type for all non-tuple types (or a type for the "empty" tuple) to use
something like this for the printf problem and other similar problems.

In the end, there is no limit to all things you could ask for; for example
a function to reverse tuples:

        revtup : (*a1 X ... X *an) -> (*an X ... X *a1),

or a function to repeat the i-th component i times

        repcom : (*a1 X *a2 X ... X *an) -> (*a1 X *a2 X *a2 X ...
                                                        *an X ... X *an).
-- 

Lambert Meertens, CWI, Amsterdam; lambert@cwi.nl