From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 BEF2DBCAE for ; Thu, 30 Jun 2005 11:51:25 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j5U9pPhN012578 for ; Thu, 30 Jun 2005 11:51:25 +0200 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA14219 for ; Thu, 30 Jun 2005 11:51:25 +0200 (MET DST) Received: from justus.rz.uni-saarland.de (justus.rz.uni-saarland.de [134.96.7.31]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j5U9pO2r000414 for ; Thu, 30 Jun 2005 11:51:24 +0200 Received: from cs.uni-sb.de (cs.uni-sb.de [134.96.254.254]) by justus.rz.uni-saarland.de (8.12.10/8.12.10) with ESMTP id j5U9pNr55572981 for ; Thu, 30 Jun 2005 11:51:23 +0200 (CEST) Received: from mail.cs.uni-sb.de (mail.cs.uni-sb.de [134.96.254.200]) by cs.uni-sb.de (8.13.4/2005033000) with ESMTP id j5U9pMtX019838 for ; Thu, 30 Jun 2005 11:51:23 +0200 (CEST) Received: from ps.uni-sb.de (grizzly.ps.uni-sb.de [134.96.186.68]) by mail.cs.uni-sb.de (8.13.4/2005060800) with ESMTP id j5U9pMRW002771 for ; Thu, 30 Jun 2005 11:51:22 +0200 (CEST) X-Authentication-Warning: mail.cs.uni-sb.de: Host grizzly.ps.uni-sb.de [134.96.186.68] claimed to be ps.uni-sb.de Received: from [134.96.186.172] (groove.ps.uni-sb.de [134.96.186.172]) by ps.uni-sb.de (8.12.10/8.12.10) with ESMTP id j5U9pKJU004964; Thu, 30 Jun 2005 11:51:20 +0200 Message-ID: <42C3C098.6040303@ps.uni-sb.de> Date: Thu, 30 Jun 2005 11:51:20 +0200 From: Andreas Rossberg User-Agent: Mozilla Thunderbird 1.0.2 (X11/20050317) X-Accept-Language: en-us, en MIME-Version: 1.0 To: "O'Caml Mailing List" Subject: Re: [Caml-list] Type abstraction and (polymorphic) equality References: <20050629.023111.15476874.debian00@tiscali.be> <42C2E3AA.8090502@yahoo.fr> In-Reply-To: <42C2E3AA.8090502@yahoo.fr> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-1.5.1 (justus.rz.uni-saarland.de [134.96.7.31]); Thu, 30 Jun 2005 11:51:23 +0200 (CEST) X-AntiVirus: checked by AntiVir Milter 1.0.6; AVE 6.31.0.7; VDF 6.31.0.126 X-Miltered: at concorde with ID 42C3C09D.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 42C3C09C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; rossberg:01 rossberg:01 caml-list:01 abstraction:01 recursives:01 dfas:01 compiler:01 polymorphism:01 recursives:01 recursion:01 recursion:01 existential:01 criterium:01 wrote:01 uni-sb:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: sejourne_kevin wrote: > > A generic equality should be one that work with recursives. Not so easy. In order to be a proper equivalence test for cyclic data structures it essentially had to test graph equivalence, which is the same as testing equivalence of DFAs. So it would be a completely different algorithm, with significant complexity in space and time. > When the compiler generate code he have the complete type, no ? No, not in the presence of polymorphism. > so he > can know if a type is recursives or not, so he can select the slow but > recursives compliant version are the actual. Recursion on the type level does not necessarily imply recursion on the value level. Just consider lists, they are rarely cyclic. On the other hand, there may be recursion even where it is not visible in types, e.g. when you have implicit forms of existential quantification, like for abstract types, (non-recursive) object types, function types (closures). So this is not a useful criterium. In Alice ML, where we have recently added such a co-recursive equivalence operation, we opted for turning it into a separate operation, to avoid these issues. -- Andreas Rossberg, rossberg@ps.uni-sb.de Let's get rid of those possible thingies! -- TB