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=2.8 required=5.0 tests=DNS_FROM_RFC_POST,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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 1995BBC37 for ; Wed, 30 Sep 2009 00:41:36 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjkBAFgqwkpKfU4Yimdsb2JhbACRRYh5PwEBAQoJDAcRBaotgTSQIwEDAgWEGQU X-IronPort-AV: E=Sophos;i="4.44,475,1249250400"; d="scan'208";a="35267613" Received: from ey-out-2122.google.com ([74.125.78.24]) by mail3-smtp-sop.national.inria.fr with ESMTP; 30 Sep 2009 00:41:03 +0200 Received: by ey-out-2122.google.com with SMTP id 9so333961eyd.7 for ; Tue, 29 Sep 2009 15:41:03 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from :user-agent:mime-version:to:cc:subject:references:in-reply-to :content-type:content-transfer-encoding; bh=+bhYqRL2zKq8+LIvbyVL9MDE3sv/SxZ/iRi/OFX+eDQ=; b=wJ7sySEIvAwEHapOsIdjxTR1I+9jmaPvqtBOBO4wx0H2qgz3zmrZAw+5T8gBxFz+DB Wg/Eek5xClOmSOy3cdkjjpwVwIQQejlvgwMpQDfhD+6wqPEckvikLc4ZvN7dold1YjoL bCWrlceaxIbDWOqB8Yy2zmiPPv5hKRiL7FRRY= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:cc:subject :references:in-reply-to:content-type:content-transfer-encoding; b=KvWY3xNcCHMm5LX/yt/f0f0fsc4DhRR1LPvC4C/WL9DPbtQVqUInMb+6oCdoaavUaj y24xYjifCg/Yy6kVQMnUMKaT+Qna5/2LD6Wx66SXaacNiTg+pnSGfsKFKo7ylcj6khCy gTi24wl3AdJOb/f2f2J3vQ3OSf8B9A5Y8cP0o= Received: by 10.210.6.21 with SMTP id 21mr5250959ebf.58.1254264063141; Tue, 29 Sep 2009 15:41:03 -0700 (PDT) Received: from ?192.168.1.64? (host86-141-47-239.range86-141.btcentralplus.com [86.141.47.239]) by mx.google.com with ESMTPS id 7sm373670eyb.28.2009.09.29.15.41.02 (version=TLSv1/SSLv3 cipher=RC4-MD5); Tue, 29 Sep 2009 15:41:02 -0700 (PDT) Message-ID: <4AC28D3F.20709@gmail.com> Date: Tue, 29 Sep 2009 23:42:07 +0100 From: Jeremy Yallop User-Agent: Mozilla-Thunderbird 2.0.0.22 (X11/20090701) MIME-Version: 1.0 To: Damien Guichard Cc: "caml-list@inria.fr" Subject: Re: [Caml-list] ANN: pa_polyrec: syntax for polymorphic recursion References: <4AC12336.1040703@gmail.com> <200909291620091407574@orange.fr> In-Reply-To: <200909291620091407574@orange.fr> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; syntax:01 recursion:01 damien:01 damien:01 guichard:01 expressivity:01 recursion:01 ocaml:01 variants:01 ocaml:01 compiler:01 compiler:01 undetected:01 runtime:01 parser:01 Thanks for the comments, Damien. Damien Guichard wrote: > Problems are : > 1. functions are harder to type > 2. type errors are quite hard to interpret and to locate > (although *pa-polyrec* certainly helps in this department) > 3. benchmarks show you pay a certain (small) price for the added type > expressivity I think that the arguments you make against polymorphic recursion could also be made against other features of OCaml, such as structurally-typed objects and polymorphic variants: they make type errors more complex and can be less efficient than the alternatives. Still, I'm glad that OCaml has those features because they make it possible to write programs that would otherwise be impossible. I'm glad you raised these points, though, because they highlight the fact that there is a tradeoff involved. If you use nested data types and polymorphic recursion then you may have to work harder to satisfy the compiler. However, in return the compiler will guarantee the absence of certain errors that would otherwise remain undetected until runtime, and perhaps forever. > May be polymorphic recursion is actually a tool for the working ML programmer. > Yet i am still waiting to see the exemple that is more than a nice trick for the ML hacker. Here is one example: the following paper shows how to use OCaml extended with GADTs to give a precise type to the output of a parser generator: Towards efficient, typed LR parsers François Pottier and Yann Régis-Gianas ACM Workshop on ML, 2006 http://gallium.inria.fr/~fpottier/publis/fpottier-regis-gianas-typed-lr.pdf The run and gotoE procedures, which form a central part of the implementation described in that paper, are inherently polymorphic-recursive, just like most other non-trivial functions over GADTs. OCaml doesn't have GADTs, of course, but Oleg recently described a technique that can be used to translate many programs that use GADTs into OCaml: http://caml.inria.fr/pub/ml-archives/caml-list/2009/07/2984f23799f442d0579faacbf4e6e904.en.html Polymorphic recursion is an important element of that technique. > In my opinion, when wants the added type expressivity he actually wants > dependant types. That may be true, but since OCaml doesn't support dependent types I think that it's useful to know what can be accomplished without them. There is an ancillary benefit to pa_polyrec (besides polymorphic recursion): it provides a clear way of ensuring that a function is polymorphic, giving a solution to the problem described in this blog post by Stephen Weeks: http://ocaml.janestreet.com/?q=node/29 For example, suppose that you have a function let f = fun x -> 13 :: x and you want to tell the compiler that it has type 'a list -> 'a list, for any type 'a. (Since it actually does *not* have that type, we want the compiler to complain.) This is surprisingly difficult to write straightforwardly in OCaml! You can't write the following let f : 'a list -> 'a list = fun x -> 13 :: x since OCaml will simply unify the variable 'a with the element type of the list, and type-checking will succeed. That blog post shows how to use an uninhabited type to guarantee polymorphism: you can write something like the following type a let f = fun x -> 13 :: x let (_ : a list -> a list) = f and the compiler will duly complain that 'a' and 'int' cannot be unified. This is certainly a useful trick; still, it would be nice to be able to ascribe the polymorphic signature directly. Using pa_polyrec one can write let rec f : 'a. 'a list -> 'a list = fun x -> 13 :: x and the compiler will complain that the type of the right hand side is insufficiently general. (Of course, it would be better to be able to omit the 'rec'; perhaps a future release will permit that.)