Recursive types in OCaml/OLabl-1.06

Recursive types in OCaml/OLabl-1.06

[Wolfram Kahl]

After porting my project from OLabl-1.05 to OLabl-1.06,
I have been bitten by the change of policy wrt. recursive
types, too. I have solved my problems, and I enjoy the
new features --- many thanks to all involved for this
nice system!

Nevertheless I have some ideas about recursive types.

Xavier Leroy wrote:
> The point I'm trying to make here is that pretty much all the time, 
> recursive types can be avoided and clarity of the code can be improved
> by using the right concrete types (sums or records) to hide the
> recursion, rather than using generic sum or product types such as
> "option" and "*", then obtain the desired recursive structure by using
> recursive type expressions.

I agree that this is essentially true,
but I shall argue that the use of generic sum or product types such as
"option" and "*" also has its advantages, which lie mainly in the
domain of code reuse,
and I shall propone a variant that might be able to give us
the best of both worlds ;-)


I need recursive types essentially for being able to
establish bidirectional links between different kinds
of mutable records (NOT objects -- motivated mainly by the absence
of typecase expressions), but it happens
that there is also a variant inside the path of the
recursion, so I dealt with the problem at the point.


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
@}

(This message can be used as an input file for FunnelWeb;
the passage above then defines the contents of the
FunnelWeb ``O''utput file @{rectest1.mli@}.)

Actually this concrete example is not at all interesting for me,
but I think that for illustrating my point, nothing is gained
by a more realistic variant example.

Testing this in OLabl-1.06 (all those tests give exactly
the same results with OCaml-1.06),
the command @{olablc -c rectest1.mli@} reports:

@$@<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@}.

So in order to get a viable solution that
still reasonably fits into my other facilities for
handling values of type @{option@}
(this is the code reuse argument --- if my variant
is more complicated, I do not want to duplicate
all the code I have for handling it ---
even though I could easily do it with FunnelWeb :-),
I am forced to write:

@O@<rectest3.mli@>==@{@-
type x = NoneX | SomeX of x
val x_of_option : x option -> x
val option_of_x : x -> x option
@}

This is accepted, and I have to use the
adaptation functions all over the place.

This is essentially the solution that has been
recommended before, and I use it, too
(though not (yet) for @{option@}).

======================================================

As a new alternative which I think should be viable,
I would be happy if I could make the first variant
more explicit, resorting to the possibility of
``reexported variant types'':

@O@<rectest4.mli@>==@{@-
type x = x option = None | Some of x
@}

But again, @{olablc -c rectest4.mli@} gives:

@$@<rectest4 output@>@Z==@{@-
File "rectest4.mli", line 1, characters 4-36:
The type abbreviation x is cyclic
@}

Has this possibility already been considered
in that context? Would accepting this break
something else? Are ``reexported variant types''
allowed to instantiate type variables anyway?
Should they be allowed to do so?

=========================================================

By the way, when I define a polymorphic (mutable record)
type inside a big recursive type definition,
and use different instances of this type inside
the same recursive type definition,
I get an error along the lines of (since I already have adapted
my code, I cannot reproduce it right now):

``<<Instance3>> should be an instance of <<Instance1>>=<<Instance2>>''

which I conclude has something to do with lacking
support for polymorphic recursion.
However, I do not find any documentation for this
anywhere in the manual --- is this on purpose?
(The equality <<Instance1>>=<<Instance2>> is actually
only an assumption on the part of the compiler
which would, in the situation I encountered,
turn out to be invalid later.)

(The use of the keyword @{lazy@} and the
module @{Lazy@} are also not documented...)


Best regards,

Wolfram

Re: Recursive types in OCaml/OLabl-1.06

[Jacques GARRIGUE]

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>