Re: [Caml-list] Recursive types

[Swaroop Sridhar <swaroop@cs.jhu.edu>]

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, _ )  ->
            t1.link = Some t2
            return true

    case (_, Tvar) ->
            t2.link = Some t1
            return true

    case (Record, Record) ->

            if the record lengths don't match
               return false

  	   t1.link = t2  (***** linked speculatively *****)

            for each i in 0 to t1.components.size()
               Unify (t1.components[i], t2.components[i])
               if Unification fails,
			t1.link = None
			unlink all types that were linked until now
			return false
	      endif

            for each i in 0 to t1.typeArgs.size()
               Unify (t1.typeArgs[i], t2.typeArgs[i])
               if Unification fails,
			unlink all types that were linked until now
			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.