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: 2005-11-16 (23:00) From: Swaroop Sridhar Subject: Re: [Caml-list] Recursive types
```Jacques Garrigue wrote:
> There is a problem with your algorithm ...
> The approach in ocaml is simpler: link at each type node, so that
> already unified types will look equal.

Let me have another take at the algorithm :

Unify (first:TYPE, second: TYPE)
will return true on Unification false if not.

1. Start
2. let t1 = repr first
let t2 = repr second

3. match (t1.kind, t2.kind) with

case (Integer, Integer) ->
return true

case (Tvar, _ )  ->
return true

case (_, Tvar) ->
return true

case (Record, Record) ->

if the record lengths don't match
return false

for each i in 0 to t1.components.size()
Unify (t1.components[i], t2.components[i])
if Unification fails,
return false
endif

for each i in 0 to t1.typeArgs.size()
Unify (t1.typeArgs[i], t2.typeArgs[i])
if Unification fails,
return false
endif

return true

case (_, _)  ->
return false

4. Stop

Is this correct/ similar to what Ocaml does?

> Note in this case: the definition of llist is nominal, so this type is
> only iso-recursive, which is much easier to handle.

We might have syntactic restrictions (ex: one of ML's restriction that
recursion can occur only across variant constructor boundaries, etc) so
that arbitrary recursion is disallowed. However, from an implementation
standpoint, I *think* that the above implementation of the unifier is
easier to do even in the case of iso-recursive types. Is this true?

I thought of introducing explicit fold/unfold operations into the
algorithm, but it seemed to do more work. If I am wrong, can you please
suggest modifications to the above algorithm that works (better) only
for iso-recursive types.

Thanks,
Swaroop.

```