Re: Where are higher-rank and existential types used?

13 Sep 2003

      In article <9jc531-5jc.ln1@proper.ptq.dyndns.org>,
 Ken Shan <ken@digitas.harvard.edu> wrote:
...
Norman Ramsey and I are looking for examples of where higher-rank
polymorphism and existential types are useful.  Can anyone think of
uses besides the following?
I use HRP a fair amount. My most common use is in functions that convert 
structures to use different monads:

  remonadBigStruct :: (forall a. m1 a -> m2 a) ->
    BigStruct m1 -> BigStruct m2;

I use existential types very occasionally:

1.
when using types to represent compiled code, as in SQL:

  newtype Value t = MkValue String;

Here the idea is that a "Value Int16" contains an SQL expression that 
will return a column of signed 16-bit values when used in a SELECT 
statement. Really I'm using the Haskell type-system as a stand-in for 
the essentially unrelated SQL type system.

I build up Values in a special monad. But the function that turns that 
into an SQL statement needs a list of Values that may be of different 
types:

  getSQLSelect :: (Monad m) =>
   SelectMonad m [Any Value] -> m String;

  data Any f = forall a. MkAny (f a);

2.
Existential types also turn up in my implementation of the Scheme letrec 
function.

This sort of thing is not normally allowed in Scheme:

  (letrec (
    (a (cons 'x b))
    (b (cons 'y a))
    )
    ...body...
  )

But Haskell is a lazy language, and I wanted to use that to extend 
letrec to allow lazy recursive construction of circular lists and the 
like, using mfix. But this is complicated by the fact that there may be 
any number of declarations in the head of the letrec form. I need some 
structure to be the argument type for my mfix.

The existential type at the heart of my implementation is this:

    data MutualBindings f a v = forall t. (ExtractableFunctor t) =>
     MkMutualBindings (t (f a)) (forall r. f r -> f (t v -> r));

The idea is that I want to represent n functions, each of which has n 
dependencies, for any n. "t" here is one of my fixed-length list types, 
depending on n:

    data ZeroList a = MkZeroList;
    data NextList t a = MkNextList a (t a);

MutualBindings is used to represent the binding declarations in the head 
of the letrec form. In the example above, these would be

  (a (cons 'x b))
  (b (cons 'y a))

Here there are two binding declarations, so n = 2, and the 
MutualBindings that gets built will use (NextList (NextList ZeroList)) 
for t. The first argument of the MutualBindings is therefore two 
expressions, corresponding to the Scheme expressions "(cons 'x b)" and 
"(cons 'y a)". The second part is an "abstracter" function that converts 
any expression on r into an expression on a function to r that takes a 
pair of variables, by abstracting on the Scheme symbols "a" and "b".

The important thing is that I've made the type existential on "t" to say 
that I want the two ts the same, but I don't care which "t" it is. So if 
I have two expressions, then the abstracter must work on two symbols. If 
I have five expressions, then it must work on five symbols. And all I 
need to know about it is that it's an ExtractableFunctor, i.e. I have 
fmap and the function

  fExtract :: t (f a) -> f (t a);

If my "a" type is in fact (IO SchemeObject) or somesuch, I can then use 
mfix to perform the letrec.

Try it out at
<http://hscheme.sourceforge.net/interpret.php>

 (define xyxy (letrec
   ((a (cons 'x b)) (b (cons 'y a)))
   a))

 (list-head xyxy 30)

-- 
Ashley Yakeley, Seattle WA