[comp.lang.misc] Polymorphic Type Systems: some unsolved problems

kdmoen@watcgl.UUCP (07/24/87)

I've been researching strongly typed, polymorphic languages for my thesis.
Although the problems of defining such polymorphic functions as 'identity'
(which maps a value of any type onto itself) and 'sort' (which sorts
an array of any length and any base type) are well understood,
it seems to me that there are many interesting and well defined
polymorphic functions which cannot be easily expressed in currently
existing polymorphic type systems.

Here is a partial list of difficult to define polymorphic functions.
I would greatly appreciate additions to this list, or sample code
that shows how to define any of these functions in your favourite
strongly typed, polymorphic programming language.

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.

2) Define a function similar to the 'printf' function in the C
   library, except that it is fully type checked.

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.

4) Define a function called 'curry' which maps functions onto functions.
   Curry maps functions with 0 or 1 arguments onto themselves,
   and maps functions with 2 or more arguments onto Curried versions
   of these functions.  For example, it maps a function of type
   "(T1, T2) -> R" onto a function of type "T1 -> T2 -> R". Similarly, it maps
   "(T1, T2, T3) -> R" onto "T1 -> T2 -> T3 -> R", etc.

5) Define a function called 'uncurry' which is more or less the inverse
   of curry.

6) Suppose that 'array N of T' is the type of a one dimensional array
   of N elements of type T.  Define a polymorphic function that
   can accept an argument with one of the following types:
      T
      array N1 of T
      array N1 of (array N2 of T)
      array N1 of (array N2 of (array N3 of T))
      ...etc, ad infinitum

7) Define a single function that can accept an argument whose type
   is either T1 or T2.
-- 
Doug Moen
University of Waterloo Computer Graphics Lab
UUCP:     {ihnp4,watmath}!watcgl!kdmoen
INTERNET: kdmoen@cgl.waterloo.edu

pase@ogcvax.UUCP (Douglas M. Pase) (07/30/87)

In article <watcgl.1506> kdmoen@watcgl.UUCP (Doug Moen) writes:
> [...] it seems to me that there are many interesting and well defined
>polymorphic functions which cannot be easily expressed in currently
>existing polymorphic type systems.

I use a strongly typed variant of ML *we* call SML, which appears
to be otherwise unrelated to *Standard* ML.

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

>
>2) Define a function similar to the 'printf' function in the C
>   library, except that it is fully type checked.

This is harder, since it depends on the I/O system defined by the language
(SML has none).  In general it is very difficult (if at all possible) to
define a function which is able to accept a list of args, whose length and
types are both arbitrary.  The big problem I see is when do you stop looking
for more args?  If the length is fixed, count the args you've got.  If the
type is fixed, use a marker of a different type to signal the end.

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

>
>4) Define a function called 'curry' which maps functions onto functions.
>   Curry maps functions with 0 or 1 arguments onto themselves,
>   and maps functions with 2 or more arguments onto Curried versions
>   of these functions.  For example, it maps a function of type
>   "(T1, T2) -> R" onto a function of type "T1 -> T2 -> R". Similarly, it maps
>   "(T1, T2, T3) -> R" onto "T1 -> T2 -> T3 -> R", etc.
>

This one actually borders on the difficult.  SML does not support arbitrarily
long "pairs" the way it supports lists.  Lists must have all elements of the
same type, but are unbounded in length.  Pairs may contain many different types
of expressions, but are fixed in length.  Thus a "curry2" or a "curry3" may
easily be written, but a "curryN" is not within its bounds.  LML, which is also
a variant of ML supports a disjoint union (it momentarily escapes me if this
is the proper term) of types (e.g. int+real+...) and is therefore able to
create a "curryN" function.  However, because tuples only come in one size
also (i.e. pairs), there is some ambiguity if a type Tn is itself a pair.

>5) Define a function called 'uncurry' which is more or less the inverse
>   of curry.
>

Similar to #4, SML could define an "uncurry2", etc., but I do not see how
either SML or LML could support an "uncurryN".  Neither am I sure it is
impossible.

>6) Suppose that 'array N of T' is the type of a one dimensional array...

Neither SML nor LML support arrays so I cannot provide assistance.

>7) Define a single function that can accept an argument whose type
>   is either T1 or T2.

SML is not capable of this.  In LML (if I remember my syntax):

	let f x = case (x)
		int :  3 ;
		real : 4 ;
		;;

	f : (int+real) -> int

(The beauty of the disjoint union!)


I have received numerous requests for information/articles/references/authors
for LML (Lazy ML) and ML, but alas, I have none.  My information came from
classes offered here, so I can't offer much in the way of assistance.  (I 
suppose you could write and ask for the class notes for CSE 511, 512 and 515,
but I don't guarantee results.)  So if any of you advanced students of
functional programming or closet type-theorists do have such knowledge,
please share it with the rest of us.
--
Doug Pase   --   ...ucbvax!tektronix!ogcvax!pase  or  pase@Oregon-Grad.csnet

lambert@cwi.nl (Lambert Meertens) (08/05/87)

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