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 9A551BC0A for ; Thu, 5 Apr 2007 10:17:53 +0200 (CEST) Received: from an-out-0708.google.com (an-out-0708.google.com [209.85.132.247]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l358HqQZ016576 for ; Thu, 5 Apr 2007 10:17:53 +0200 Received: by an-out-0708.google.com with SMTP id c24so578647ana for ; Thu, 05 Apr 2007 01:17:52 -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=enEITQ41IYGwW4VjN6xH7ScZJGDQ3uhwErTvnOWHZqXRWreQqZ00pLgwBQgNQEPDwfJkM2/WJ5Hz04gAqNHru91tzi/ognDdDRRvwRS81pkqqYG3d0pY2+wb7TGn2pAUJJ6uexwjzXAEZMWBXNEo7i2el/rJPsq8ikJpLbJeoiA= 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=HFSS7zrQJ17GG7VnbYF9sng9MDs88YPcz19ZjW1o9rycD++bD4t+UQQHj9L0J6SoCG9Q/zPJeh3kmpyKhXRq+avRKbFVPnm1WInCgS2sOV6BqjmdGeaFVA7mLXxzjsneCc7iLoVhQqv7D1LaA04x8xbGP7P5EQYUHaIg8YGkpzo= Received: by 10.100.121.12 with SMTP id t12mr1128959anc.1175761072257; Thu, 05 Apr 2007 01:17:52 -0700 (PDT) Received: by 10.100.168.16 with HTTP; Thu, 5 Apr 2007 01:17:52 -0700 (PDT) Message-ID: <6f9f8f4a0704050117o41bb58f2x96e50a323a2d9737@mail.gmail.com> Date: Thu, 5 Apr 2007 10:17:52 +0200 From: "Loup Vaillant" To: "Brian Hurt" Subject: Re: [Caml-list] Polymorphic recursion Cc: caml-list@yquem.inria.fr In-Reply-To: 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> X-j-chkmail-Score: MSGID : 4614B0B0.001 on discorde : j-chkmail score : X : 0/20 1 0.000 -> 1 X-Miltered: at discorde with ID 4614B0B0.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; recursion:01 okasaki's:01 functionnal:01 ocaml:01 seq:01 seq:01 okasaki:01 iirc:01 okasaki:01 trivial:01 invariants:01 2007,:98 polymorphic:01 polymorphic:01 wrote:01 2007/4/5, Brian Hurt : > > > On Tue, 3 Apr 2007, Loup Vaillant wrote: > > > I was reading Okasaki's book, "Purely functionnal data structures", > > and discovered that ML (and Ocaml) doesn't support non uniforms > > function definitions. > > > > So, even if: > > > > (**) > > type 'a seq = Unit | Seq of ('a * ('a * 'a)seq);; > > (**) > > This way lies GADTs, which are a really neat idea, but even the > Haskeller's aren't 100% sure how to implement correctly yet. > > In any case, there's a fairly simple work around which does work in the > current type system, which Okasaki describes IIRC. Basically, you just > do: > > type 'a tuple = Tuple of 'a tuple * 'a tuple | Leaf of 'a;; > > type 'a mono_seq = Unit | Set of 'a tuple * 'a seq;; > > which is a bit of a pain, but works. (note: I have renamed "mono_seq" for disambiguation) This workaround doesn't work exactly as intended: as Okasaki pointed at, the binary tree "tuple" is not guaranteed to be balanced. Therefore, even if we can build a trivial injection of type (* seq -> mono_seq *), it will not be a surjection as well. We have lost an invariant, and are forced to maintain it programmatically. This kind of workaround is well known: we call it abstract type. What I find cool with polymorphic types is that more invariants can be checked directly by the type system. It has two advantages: -> It is less error prone when writing the module attached to the type. -> Sometimes, a programmer outside the module can even do pattern matching on this type and still be guaranteed she will not produce a single wrong value. For these reasons,I wanted a way to exploit polymorphic type. You all provided three. I don't mind the syntactic burden, provided someone come up a syntactic shortcut. Loup