[Camllist] extensible records again
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20040323 (19:09) 
From:  skaller <skaller@u...> 
Subject:  Re: [Camllist] extensible records again 
On Mon, 20040322 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: 061296600850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net  To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners