Re: Recursive types in OCaml/OLabl-1.06

[Jacques GARRIGUE <garrigue@kurims.kyoto-u.ac.jp>]

From: Wolfram Kahl <kahl@diogenes.informatik.unibw-muenchen.de>

> Recapitulating an argument that already has been
> discussed to a certain degree in the last few days,
> I would like to write something like:
> 
> @O@<rectest1.mli@>==@{@-
> type x = x option
> @}

[ lots of material erased: cf. the original message ]
 
> @$@<rectest1 output@>@Z==@{@-
> File "rectest1.mli", line 1, characters 4-17:
> The type abbreviation x is cyclic
> @}
> 
> Obviously it is not a good idea to write
> 
> @O@<rectest2.mli@>==@{@-
> type x = None | Some of x
> @}
> 
> which is accepted, but gives bad name clashes
> with the original constructors of @{option@}.

I'm sorry to give an O'Labl specific answer in the caml-list, but this
program is supposed to be an O'Labl one.

In fact, using O'Labl there is another solution to this problem.
You can define your own option type using polymorphic variants:

	type 'a opt = [None Some('a)]

And since the rule for O'Labl is that a cyclic abbreviation should go
through an object OR a polymorphic variant,

	type nat = nat opt

will be accepted, and is exactly equivalent to,

	type nat = [None Some(nat)]

Since these are polymorphic variants, there is no problem of name clash:
you may define the same tag in as many types as you want.

Last, if you care about speed, remember that as long as you have only
a small number of variant tags by type, polymorphic variants are just
as efficient as standard ones when you use the native code compiler.

Another remark, related with this discussion, is that O'Labl 1.05 was
already more restrictive than O'Caml 1.05 about recursive types. In
particular ('a option as 'a) was not a valid type to infer.

Here is an O'Labl 1.05 example:

# type nat = nat option;;
type nat = nat option
# fun x -> (x = Some x);;
This expression has type 'a option but is here used with type 'a
# fun (x : nat) -> (x = Some x);;
- : nat -> bool = <fun>

As you can see, such recursive types may be used, but not inferred.
The second and third line would have been equivalently OK with O'Caml.
This may seem not very clean, since you need a type annotation in
order to type the function, and I suppose this is why it is not
allowed in O'Caml 1.06.

Regards,

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