From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id F0E55BD74 for ; Fri, 19 Aug 2005 09:54:25 +0200 (CEST) Received: from haka.fmf.uni-lj.si (haka.fmf.uni-lj.si [193.2.67.18]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j7J7sNQD030661 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Fri, 19 Aug 2005 09:54:25 +0200 Received: from bsn-77-186-71.dsl.siol.net ([193.77.186.71] helo=[192.168.1.109]) by haka.fmf.uni-lj.si with esmtpa (Exim 4.50) id 1E61hW-0007eB-2a; Fri, 19 Aug 2005 09:54:19 +0200 Message-ID: <43058F36.8020803@andrej.com> Date: Fri, 19 Aug 2005 09:50:14 +0200 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Debian Thunderbird 1.0.2 (X11/20050331) X-Accept-Language: en-us, en MIME-Version: 1.0 To: skaller Cc: caml-list@yquem.inria.fr References: <161F0D30A699A84A8B7435B62BCE33B30360E19F@APS-MSG-01.southpacific.corp.microsoft.com> <200508161734.38909.jon@ffconsultancy.com> <20050816181604.GA21719@furbychan.cocan.org> <200508162242.50803.jon@ffconsultancy.com> <1124261702.6858.21.camel@localhost.localdomain> <430444BC.9090903@andrej.com> <1124387475.8402.32.camel@localhost.localdomain> In-Reply-To: <1124387475.8402.32.camel@localhost.localdomain> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 193.77.186.71 X-SA-Exim-Mail-From: Andrej.Bauer@andrej.com Subject: Re: [Caml-list] Snd question X-SA-Exim-Version: 4.2 (built Thu, 03 Mar 2005 10:44:12 +0100) X-SA-Exim-Scanned: Yes (on haka.fmf.uni-lj.si) X-Miltered: at concorde with ID 4305902F.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; andrej:01 andrej:01 caml-list:01 functors:01 functors:01 recursion:01 coq:01 coq:01 ...:98 ...:98 wrote:01 theorem:01 defined:01 polynomial:02 polynomial:02 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 I was hoping skaller wouldn't object to a simple terminological point. Oh well :-) skaller wrote: > EG: 1 is a list, if L is a list then T * L is a list. It follows > T is a list, T * T is a list .. etc, and so a list is given > by the polynomial > > 1 + T + T * T + T * T * T + ... You are confusing the interesting observation that lists can be given both as an inductive type and a polynomial with the definition of polynomial functors. Polynomial functors are defined without mention of inductive types (contrary to your _definition_). Since we are discussing a _definition_, it is irrelevant that there are inductive types which can also be expressed as polynomial functors. If you do not believe me, I can give you a reference. > "Such types are well > understood and have accompanying induction and recursion principles from > which various operations (map, fold, etc.) can be built systematically." > > and I wonder why no production languages actually do that... I believe the coq proof assistant (http://coq.inria.fr/) knows how to do this, and quite possibly the Isabelle theorem prover, too. One could presumably rip out this part of coq and put it in a programming language. Best regards, Andrej