This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Recursive types
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: -- (:) From: Jacques Garrigue Subject: Re: [Caml-list] Recursive types
```From: Swaroop Sridhar <swaroop.sridhar@gmail.com>

> Thanks for the clarification. In order to ensure that I understand you
> correctly, can you please look into the following unification algorithm
> and see if it is reasonably correct?

There is a problem with your algorithm:
the way you check the unf field is buggy (you dereference both sides),
but this seems a trivial a trivial error.
More importantly, even corrected it will fail when unifying a loop of
length 3 with a loop of length 2:
t1 = (int * (int * 'a) as 'a)
t2 = (int * (int * (int * 'b)) as 'b)
when you reach the inner 'b, you have already unrolled t1, so it also
has its unf field set, but not to t2...

The approach in ocaml is simpler: link at each type node, so that
already unified types will look equal. As a result, after unification
you have only a loop of length 1.

> > A few years ago, infinite loops were a commonly reported bug :-)
>
> hurt oneself with a type being parameterized itself. I also read that
> the type system needs to deal with this in order to support objects.
> Aren't recursive types necessary even to do a simple linked list like:
>
> type llist = {contents: int; link : mutable llist}

Note in this case: the definition of llist is nominal, so this type is
only iso-recursive, which is much easier to handle.
The difficulties only appears with
type llist = < contents: int; link : llist >

Jacques Garrigue

```