English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
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 <swaroop@c...>
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, _ )  ->
            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

            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

        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.