From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id C477CBB9C for ; Thu, 17 Nov 2005 00:00:29 +0100 (CET) Received: from blaze.cs.jhu.edu (blaze.cs.jhu.edu [128.220.13.50]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jAGN0S5H027764 for ; Thu, 17 Nov 2005 00:00:29 +0100 Received: from [128.220.220.231] (wheat.cs.jhu.edu [128.220.220.231]) by blaze.cs.jhu.edu (8.12.9/8.12.9) with ESMTP id jAGN0HRl014330; Wed, 16 Nov 2005 18:00:17 -0500 (EST) Message-ID: <437BBA00.3090505@cs.jhu.edu> Date: Wed, 16 Nov 2005 18:00:16 -0500 From: Swaroop Sridhar User-Agent: Mozilla Thunderbird 1.0.7-1.1.fc4 (X11/20050929) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Jacques Garrigue , caml-list@yquem.inria.fr Subject: Re: [Caml-list] Recursive types References: <437A64C1.3000807@cs.jhu.edu> <20051116.084030.02302710.garrigue@math.nagoya-u.ac.jp> <437AA762.5060909@cs.jhu.edu> <20051116.173802.68165704.garrigue@math.nagoya-u.ac.jp> In-Reply-To: <20051116.173802.68165704.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 437BBA0C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 recursive:01 ocaml:01 node:01 unify:01 unification:01 tvar:01 tvar:01 unify:01 unification:01 ocaml:01 ml's:01 recursion:01 recursion:01 unifier:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 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.