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 D1EC2BB9C for ; Wed, 16 Nov 2005 04:28:26 +0100 (CET) Received: from zproxy.gmail.com (zproxy.gmail.com [64.233.162.193]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id jAG3SPKT013883 for ; Wed, 16 Nov 2005 04:28:26 +0100 Received: by zproxy.gmail.com with SMTP id v1so1686256nzb for ; Tue, 15 Nov 2005 19:28:25 -0800 (PST) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:reply-to:user-agent:x-accept-language:mime-version:to:cc:subject:references:in-reply-to:content-type:content-transfer-encoding:from; b=tSxZ14prxcZ40Xh4dqOdap6thFiTVWZaorezCuLUxrJYcE7nmXLS/qULltA6Fdcb3Cfh1AmHKfdYwq1HGGTR8FkwGSFyomWn2KLdhI7X1dR629KlIcoQECyJ4mktHKByUYXSVHl9ueagebUSv+M6A0vF645TTpHyul+whA8TnBc= Received: by 10.36.135.17 with SMTP id i17mr3563697nzd; Tue, 15 Nov 2005 19:28:25 -0800 (PST) Received: from ?192.168.1.2? ( [68.33.49.160]) by mx.gmail.com with ESMTP id m1sm535896nzf.2005.11.15.19.28.25; Tue, 15 Nov 2005 19:28:25 -0800 (PST) Message-ID: <437AA762.5060909@cs.jhu.edu> Date: Tue, 15 Nov 2005 22:28:34 -0500 Reply-To: swaroop@cs.jhu.edu User-Agent: Mozilla Thunderbird 1.0.6 (Windows/20050716) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Jacques Garrigue Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Recursive types References: <20050506044107.1698.70519.Mailman@yquem.inria.fr> <437A64C1.3000807@cs.jhu.edu> <20051116.084030.02302710.garrigue@math.nagoya-u.ac.jp> In-Reply-To: <20051116.084030.02302710.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit From: Swaroop Sridhar X-Miltered: at nez-perce with ID 437AA75A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 recursive:01 checker:01 nodes:01 mutable:01 unification:01 integers:01 unification:01 syntax:01 tvar:01 tvar:01 mutable:01 rec:01 'a-: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=RCVD_BY_IP autolearn=disabled version=3.0.3 Jacques Garrigue wrote: > No, types are just implemented as (cyclic) graphs. > All functions in the type checker have to be careful about not going > into infinite loops. There are various techniques for that, either > keeping a list/set of visited nodes, or using some mutable fields. 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? Considering a language with integers, records and type variables. Let record types be unified by structural unification. My representation of type is (please forgive my sloppy syntax at times): type KindUnion = Integer | Tvar | Record type 'a option = None | Some 'a type TYPE = { id: int; (* unique ID *) kind: kindUnion; (* type of this type: integer/ tvar/ record *) components: mutable vector of TYPE (* vector of types containing legs of a record *) typeArgs: mutable vector of TYPE (* vector of types containing type-arguments / type-parameters of a record *) (* example type ('a, 'b) rec = { a: 'a->'b; b: int} typeArgs components *) link: mutable (TYPE option) (* to link unified types *) unf: mutable (TYPE option) (* This is a marker used by the unifier. Initially, this field is set to `None' for all types. If we are attempting to unify t1 and t2, the unifier will mark t1-> unf = Some t2, and t2-> unf = Some t1 so that we detect them next time when we recurse *) } I also assume that a function repr is defined that will traverse the links so that (repr t) will provide the "final" type. So, now the Unifier algorithm can be written as (in some hypothetical algorithmic language): 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. (* The unifier will set unf field on the way in and will clear it on its way out. So, first test if we have a recursive case *) if(t1.unf != None and t2.unf != None) if(t1.unf == t2.unf) return true endif if(t2.unf == t1.unf) return true else return false endif endif 4. (* set the unf fields *) if(t1.unf == None and t2.unf != None) t1.unf := Some t2 else if(t2.unf == None and t1.unf != None) t2.unf := Some t1 else t1.unf = Some t2 t2.unf = Some t1 endif endif 5. 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 for each i in 0 to t1.components.size() Unify (t1.components[i], t2.components[i]) if Unification fails, return false for each i in 0 to t1.typeArgs.size() Unify (t1.typeArgs[i], t2.typeArgs[i]) if Unification fails, return false return true case (_, _) -> return false 6. t1.unf = None t2.unf= None 7. Stop Is this algorithm correct? If not, how should it be fixed? > 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} Thanks again, Swaroop.