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 47212BB81 for ; Thu, 12 Jan 2006 15:02:52 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0CE2pU7010560 for ; Thu, 12 Jan 2006 15:02:51 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id PAA17824 for ; Thu, 12 Jan 2006 15:02:50 +0100 (MET) Received: from haka.fmf.uni-lj.si (haka.fmf.uni-lj.si [193.2.67.18]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k0CE2nse019684 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Thu, 12 Jan 2006 15:02:50 +0100 Received: from theo.dagstuhl.de ([192.76.146.31] helo=[192.168.11.178]) by haka.fmf.uni-lj.si with esmtpa (Exim 4.50) id 1Ex32I-0003vl-Ry; Thu, 12 Jan 2006 15:02:48 +0100 Message-ID: <43C661AF.2080404@andrej.com> Date: Thu, 12 Jan 2006 15:03:27 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Debian Thunderbird 1.0.7 (X11/20051017) X-Accept-Language: en-us, en MIME-Version: 1.0 To: skaller Cc: caml-list@inria.fr References: <43BD6418.4090407@barettadeit.com> <43BE6CAB.2030503@andrej.com> <43C3963D.5030601@tsc.uc3m.es> <1136981974.8962.100.camel@rosella> <43C51C33.2000206@andrej.com> <1137031853.3681.138.camel@rosella> In-Reply-To: <1137031853.3681.138.camel@rosella> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 192.76.146.31 X-SA-Exim-Mail-From: Andrej.Bauer@andrej.com Subject: Re: [Caml-list] Coinductive semantics 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 43C6618B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 43C66189.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; andrej:01 andrej:01 caml-list:01 coinductive:01 semantics:01 algebra:01 unifying:01 trivial:01 algebra:01 ocaml:01 model:01 ocaml:01 functor:01 model:01 strive:98 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 Dear skaller, with all due respect, you are being silly here. I am quite familiar with research in initial algebras and final coalgebras. I am a researcher myself. May I ask what experience you have with present research directions in inital algebra and final coalgebras? skaller wrote: > On Wed, 2006-01-11 at 15:54 +0100, Andrej Bauer wrote: >> skaller wrote: >> > And of course, separate development of these things is fairly >> > silly, since as the 'co' indicates the two ideas are formally >> > dual. >> >> This is claim is completely false. > > Which claim? The claim "it is silly to have separate development of these things [initial algebras and final coalgebras]" is true, but it is FALSE that there is such a separate development. > which is a comment about research direction. I am saying > that from now on researches in the field of theoretical > computing should be focusing on development of the theories > together -- on unifying them. The people who work in research in initial algebras and final coalgebras for computer science usually are quite familiar with both directions (naturally, if you're trying to do something serious, you're going to put more emphasis on one particular thing). They are well aware of the duality that you are aware or, and quite likely are aware of a number of things that you have never heard about. One of them is that final coalgebras and initial algebras are two different ballgames. They require different ideas, proofs and techniques. You make it sound as if all these people forgot to apply a trivial duality principle. They did not. You make it sound as if "these people" are divided into two disjoint sets, one doing initial algebra and another doing final coalgebra. This, too is completely false. Typical conferences in this area, and even typical papers, consider both algebras and coalgebras. People DO strive to give unified accounts of both subjects (via category theory, mainly). I do not know where you got the idea that serious researchers harbor simplistic convictions such as: > Some people DO disagree -- they think functional programming > is enough. This is an opinion that only a programmer who knows very little about the theory of programming languages would propose. It is at the level of a discussion that two drunk engineers would have over a beer. > But Ocaml is far from ideal .. the integration remains > weak and ad hoc. The integration is NOT SUPPORTED BY > A THEORETICAL MODEL with good properties. Oh yes, you are familiar with theoretical models on which ocaml is based then? Are you then familiar with, say, realizability models? Do you know that every polynomial functor has both an initial algebra and a final coalgebra in any realizability model? Or are you just saying stuff that sounds good? If you have specific criticisms about the design of programming languages, that is a different issue. But so far you are just criticising an entire research community. Not everyone in that community does design and implementation of programming languages. > Maybe I can say this: suppose we have a purely > functional language I and a purely stateful language O > (whatever that means .. :) I ask, which should I use > to write code? And you may say "whichever is best > for the task". You think initial algebras are somehow fundamentally linked to functional languages and final coalgebras to stateful langauges. This again shows poor understanding. The forementioned realizability models demonstrate that initial algebras and final coaglebras coexist in any realizability model over _any_ Turing complete programming language, whether functional, stateful or parallel, non-deterministic, etc. It is a matter of _design_ (not theory) on how to give access to algebras and coalgebras to programmers. > Category theory more or less promises this! It is the > first system where you can use itself to talk about > constructions in itself. What do you mean precisely by "can use itself to talk about constructions in itself"? I apologize for saying in such a straightforward way that you have got no clue what you are talking about. But until you say something that does not display total ignorance of what researchers (not programmers) know or are doing about these matters, I shall think your opinion is worthless--and harmful because you are badmouthing people you know nothing about. Andrej Bauer