Variant typing and recursive types

Andrew Kennedy was asking on this list for the availability of
non-defined variants and recursive types for ML (ML2000 in

I would just like to recall here that Objective Label, which is an
extension of Objective Caml, provides such variants. For instance in
O'Labl one can write

# let rec map f = function `nil -> `nil | `cons(a,l) -> `cons(f a, map f l);;
val map : ('a -> 'b) -> 'c[< cons('a * 'c) nil] -> 'd[> cons('b * 'd) nil]

(reminder: let rec is SML's fun, and the following line is the
compiler's anser)

As you can see, the system infers both variants and recursive
types. The result is structurally polymorphic: 'c[< cons('a * 'c) nil]
means that we may get something smaller than mu x.[cons ('a * x) nil] as
input, and be expecting something bigger then mu x.[cons ('b * x) nil]
as output.

How to type it is not new: Remy already gave a solution in his POPL'91
paper "Typing records and variants in an extension of ML".

Compiling it is also solved in a very simple way: just hash variant
constructors to a single word. You have a very small probability of
getting conflicting hash values for different tags, but the type
system statically takes it. It looks like one would loose in
efficiency for case statements, but interestingly this is not true for
cases with less than 10 branches on most architectures.

As for the other example,
	fun query f n = f ([], f, n)
you may of course use again a variant if you don't want to define a

# let query f n = f (`protect([],f,n));;
val query : ([> protect('b list * 'a * 'c)] -> 'd as 'a) -> 'c -> 'd

However, let us bet that you expect some more interesting structure
for f, and it would be better to use O'Caml's object system.

# let rec query o n = o#f ([], o, n)
val query : (< f : 'b list * 'a * 'c -> 'd; .. > as 'a) -> 'c -> 'd

Remark also that while providing polymorphic variants O'Labl does not
provide polymorphic records, not even not-defined records a` la SML.
O'Caml records have to be pre-defined. However, for polymorphism
issues, the object system is more powerful than a polymorphic record
system, and for the problem of named parameter-passing Bob Harper was
pointing out, O'Labl provides a much more powerful mechanism, based on
labels and optional arguments, which makes compatible currying and
out-of-order application.

More information:


Jacques Garrigue	Kyoto University      garrigue@kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>