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 4151CBCA2 for ; Thu, 18 Aug 2005 10:20:19 +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 j7I8KI3Z012820 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Thu, 18 Aug 2005 10:20:19 +0200 Received: from localhost ([127.0.0.1] ident=andrej) by haka.fmf.uni-lj.si with esmtp (Exim 4.50) id 1E5fdF-0003IW-Hn; Thu, 18 Aug 2005 10:20:13 +0200 Message-ID: <430444BC.9090903@andrej.com> Date: Thu, 18 Aug 2005 10:20:12 +0200 From: Andrej Bauer User-Agent: Debian Thunderbird 1.0.2 (X11/20050331) X-Accept-Language: en-us, en MIME-Version: 1.0 To: caml-list@yquem.inria.fr Cc: skaller Subject: Re: [Caml-list] Snd question 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> In-Reply-To: <1124261702.6858.21.camel@localhost.localdomain> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 127.0.0.1 X-SA-Exim-Mail-From: Andrej.Bauer@andrej.com X-SA-Exim-Scanned: No (on haka.fmf.uni-lj.si); SAEximRunCond expanded to false X-Miltered: at concorde with ID 430444C2.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; andrej:01 andrej:01 caml-list:01 minor:01 functor:01 functor:01 recursion:01 wrote:01 constants:01 polymorphic:01 arbitrary:01 equation:02 functorial:02 finite:02 hoc: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 skaller wrote: > Jay's Functorial ML describes how to do this properly: > map, fold, etc, can be applied to any > polynomial type (a type built out of sums, products, > and induction). This is polyadic = functorially polymorphic, > not ad hoc. Just a minor terminological remark: A polynomial functor (functor in the sense of category theory) is a functor built from sums, products, arrow types and type constants, where the lhs of an arrow must be constant, e.g. P(x) = a * x + (b -> x) + c Contrary to what skaller says, no inductive types are allowed in a polynomial functor. Side remark: the fully general definition of a polynomial functor allows an arbitrary dependend sum, not just a finite one, so we get the general form P(x) = sum_{y : a} (b(y) -> x), where b is a type dependent on a. An inductive type is the initial solution to a fixed-point equation, t = F(t) for some functor F. In case F is a polynomial functor, the inductive type t is called a w-type, or a well-founded type. Such types are well understood and have accompanying induction and recursion principles from which various operations (map, fold, etc.) can be built systematically. Best regards, Andrej