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 D6ADCBB9C for ; Wed, 16 Nov 2005 09:52:51 +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 jAG8qmem007166 for ; Wed, 16 Nov 2005 09:52:51 +0100 Received: from localhost (millas [172.16.30.29]) by rabbit.math.nagoya-u.ac.jp (8.12.11/3.7W) with ESMTP id jAG8qlWE007320; Wed, 16 Nov 2005 17:52:47 +0900 (JST) Date: Wed, 16 Nov 2005 17:55:12 +0900 (JST) Message-Id: <20051116.175512.27779356.garrigue@math.nagoya-u.ac.jp> To: keiko@kurims.kyoto-u.ac.jp Cc: Alain.Frisch@inria.fr, caml-list@yquem.inria.fr Subject: Re: [Caml-list] Recursive types From: Jacques Garrigue In-Reply-To: <20051116.164048.68541720.keiko@kurims.kyoto-u.ac.jp> References: <20051116.112005.68539737.keiko@kurims.kyoto-u.ac.jp> <437AD616.7060006@inria.fr> <20051116.164048.68541720.keiko@kurims.kyoto-u.ac.jp> 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 437AF360.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 recursive:01 checker:01 unification:01 unification:01 memoizing:01 expansions:01 annotation:01 abbreviation:01 unifying:01 abbreviation:01 jacques:01 jacques:01 algorithm:01 algorithm: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: Keiko Nakata > I think that it is not easy to know when to apply eta-expansion, > namely, to replace a type name with its underlying definition. > > For instance, to check equivalence betweeen the types t and s below: > type t = < m : t * t > > type 'a tuple = 'a * 'a > type s = < m : s tuple > > > the algorithm should memorize that t * t and s tuple are equivalent, > and then expands s tupl into s * s > so as to check between t * t and s * s? No need to memorize equivalences: s tuple expands at its head to s * s. The type checker guarantees that it is always safe to expand the head of a type (i.e., definitions are well-founded.) But you're right that abbreviations complicate the unification algorithm a lot. In order for unification to succeed above, t must expand to (< m: 'a * 'a> as 'a), and s too. But to print nicely types we must keep the abbreviations. This is done by memoizing expansions inside the abbreviations themselves. I.e., the expansion of t is actually: (< m : t[t='a] * t[t='a] > as 'a) and that of s is (< m : s[s='b] tuple[s='b]> as 'b) where [t='a] is an internal annotation to the abbreviation. So when unifying, you can actually check the underlying type of an abbreviation. But maintaining these abbreviations is rather involved... Fo instance abbreviations must be propagated: type u = and w = u * u will expand to () Jacques Garrigue