From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.0 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id AD3BABC0A for ; Wed, 4 Apr 2007 18:52:50 +0200 (CEST) Received: from ug-out-1314.google.com (ug-out-1314.google.com [66.249.92.168]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l34GqofZ015984 for ; Wed, 4 Apr 2007 18:52:50 +0200 Received: by ug-out-1314.google.com with SMTP id q2so809978uge for ; Wed, 04 Apr 2007 09:52:49 -0700 (PDT) DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=S1sqQ4iw326vzzX+976NTyetG3XjgBcV7FChCtKSMXBGbyYYdCPAuUWGsowPSet9aYX/CyHK2k3Bz8e55eDKLjXRhL97E9KZ5kiH58p2s6OhmJdfHUUCUqkGbr0eeYPoj0FETl8cjciBbwPrRuwey1BitGWLvdua116dYsO6twA= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=QhTi/b3AW3a/OrprsmVuItIXXG2III9rgXMh7x47Bm/1TusaKk8jEyT8IexXpda/6v9z/SOg+tyEwoEpOBBMOy+GqYZDkqAnIIgDJ8rv2WZYdqiYulx0S8RgnhBeIZfuextMimQIQTRlTqE77AEqfBQSoZgypRuUW1fHGVgJZ9c= Received: by 10.114.209.1 with SMTP id h1mr307624wag.1175705158978; Wed, 04 Apr 2007 09:45:58 -0700 (PDT) Received: by 10.114.66.7 with HTTP; Wed, 4 Apr 2007 09:45:58 -0700 (PDT) Message-ID: Date: Wed, 4 Apr 2007 18:45:58 +0200 From: "Roland Zumkeller" To: "Alain Frisch" Subject: Re: [Caml-list] Polymorphic recursion Cc: caml-list@yquem.inria.fr In-Reply-To: <4613C22E.5060206@inria.fr> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <6f9f8f4a0704030959l8ebb155g8532e3ee6d31c66d@mail.gmail.com> <4613C0AA.8010405@inria.fr> <4613C22E.5060206@inria.fr> X-j-chkmail-Score: MSGID : 4613D7E2.000 on discorde : j-chkmail score : X : 0/20 1 0.000 -> 1 X-Miltered: at discorde with ID 4613D7E2.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; recursion:01 frisch:01 frisch:01 structurally:01 seq:01 val:01 seq:01 val:01 annotations:01 lix:01 equality:01 polymorphic:01 wrote:01 wrote:01 rec:01 On 04/04/07, Alain Frisch wrote: > Alain Frisch wrote: > > but since there is no value of type ('a * 'a as 'a) > > Sorry, there are actually values in this type, but they are all > structurally equal to the result of "let rec x = (x,x) in x". Yes, but "('a * 'a as 'a) seq" has more than one value (modulo structural equality), so it works to *some* extent: # let rec x = (x,x);; val x : 'a * 'a as 'a = # size (Seq (x,Unit));; - : int = 1 # size (Seq (x, Seq (x,Unit)));; - : int = 3 However, you are right in pointing out that this limited use won't be helpful for most applications, so I'd suggest: # let rec size = function | Unit -> 0 | Seq (_, b) -> 1 + 2 * size (Obj.magic b);; val size : 'a seq -> int = The function can be checked in richer type systems with annotations (e.g. Coq's), so we know that Obj.magic is not dangerous here. Roland -- http://www.lix.polytechnique.fr/~zumkeller/