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 nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 7B95DBB9C for ; Wed, 16 Nov 2005 09:35:48 +0100 (CET) Received: from rabbit.math.nagoya-u.ac.jp (rabbit.math.nagoya-u.ac.jp [133.6.130.5]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id jAG8Zk45005586 for ; Wed, 16 Nov 2005 09:35:47 +0100 Received: from localhost (millas [172.16.30.29]) by rabbit.math.nagoya-u.ac.jp (8.12.11/3.7W) with ESMTP id jAG8ZbJ0005418; Wed, 16 Nov 2005 17:35:37 +0900 (JST) Date: Wed, 16 Nov 2005 17:38:02 +0900 (JST) Message-Id: <20051116.173802.68165704.garrigue@math.nagoya-u.ac.jp> To: swaroop@cs.jhu.edu, swaroop.sridhar@gmail.com Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Recursive types From: Jacques Garrigue In-Reply-To: <437AA762.5060909@cs.jhu.edu> References: <437A64C1.3000807@cs.jhu.edu> <20051116.084030.02302710.garrigue@math.nagoya-u.ac.jp> <437AA762.5060909@cs.jhu.edu> X-Mailer: Mew version 4.0.69 on Emacs 22.0.50 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 437AEF62.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 recursive:01 unification:01 trivial:01 trivial:01 unifying:01 ocaml:01 node:01 unification:01 bug:01 recursive:01 mutable:01 simpler:01 corrected:01 int: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 From: Swaroop Sridhar > 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 :-) > > I read a couple of postings about this issue. I understand that one can > 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