Re: [Caml-list] extensible records again

[skaller <skaller@users.sourceforge.net>]

On Mon, 2004-03-22 at 16:54, Michael Vanier wrote:

> > The main downside is that to make covariant subtyping
> > you need to use fixpoints, which is fine for a single
> > parameter but unworkable for a more complex term
> > structure.
> 
> Forgive my ignorance, but what do you mean by this?

At the moment you can do this:

type x = [`A | `B ]
type y = [a | `C ]

so that y is a subtype (extension) of x.

You can even match:

match aY with
| #x as xv -> xv
| _ -> failwith "Not an x"

to reduce aY to an x.

This works fine as written because y is a 'flat'
extension of x: the type constructors are invariant
in their arguments (vacuously in the example, since
none of the constructors have any arguments).

But now consider a recursive type:

type x = [`A of x | `B]
type y = [ `A of y | `B | `C of y]

Jacques Garrigue showed me a solution using fixpoints
where the you don't want to write out all the terms
of x in y again:

type 't x1 = [`A of 't | `B]
type 't x2 = [`C of 't] (* the extension *)

type 't y1 = ['t x1 | 't x2] (* combine the parts *)
type x = 't x1 as 't (* fixate *)
type y = 't y1 as 't

A real world example: terms of some language
may included 'syntactic sugar' which can be removed
recursively by rewriting rules/term reductions.
For example Felix uses an extended type term which
allows lambda abstractions in types.

We'd like to indicate *statically* that a term
has been reduced. The difficulty is that there
seems to be an almost combinatorial explosion
in how much you have to write in the number
of parameters. In the above example there is only 
one, indicated by 't.

In Felix, I want to partition expressions, types,
patterns, statements, and a few other kinds of terms
into one or more classes and use some combinations
of these: but all these terms are mutually recursive:
statements can contain expressions and types and patterns,
patterns have 'when' expressions, types may contain
"typeof(expression)" as a type, and statements can
be considered as expressions..

So I end up with a rather large number of parameters
on each of the fine grained components I want to combine:
something like:

type 'expr 'typ 'pat 'stat expr1 = ....
...
type 'expr 'typ 'pat 'stat typ1 = ...
...

In the 'flat' case I don't have to write out the
parameters. And if I forget the covariant refinement
and just use the supertype everywhere, losing the 
benefit of extra static type checking, I can just
declare all these terms once and make them all
mutually recursive.

I want to have my cake and eat it too :D
I want to write:

type x = [`A of x | `B ]
type y = [a | `C ]

and have it 'know' that the `A in type y takes
an y argument, not an x. Perhaps this can be done as so:

type x = [`A of +x | `B ]

where the '+' indicates that the argument is covariant.

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net



-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners