From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id C750CBB81 for ; Thu, 12 Jan 2006 03:11:10 +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 k0C2BATB028519 for ; Thu, 12 Jan 2006 03:11:10 +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 DAA07491 for ; Thu, 12 Jan 2006 03:11:09 +0100 (MET) Received: from smtp3.adl2.internode.on.net (smtp3.adl2.internode.on.net [203.16.214.203]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k0C2B7DR013684 for ; Thu, 12 Jan 2006 03:11:08 +0100 Received: from rosella (ppp33-253.lns1.syd6.internode.on.net [59.167.33.253]) by smtp3.adl2.internode.on.net (8.13.5/8.13.5) with ESMTP id k0C2ArBK003721; Thu, 12 Jan 2006 12:41:00 +1030 (CST) (envelope-from skaller@users.sourceforge.net) Subject: Re: [Caml-list] Coinductive semantics From: skaller To: Andrej.Bauer@andrej.com Cc: caml-list@inria.fr In-Reply-To: <43C51C33.2000206@andrej.com> References: <43BD6418.4090407@barettadeit.com> <43BE6CAB.2030503@andrej.com> <43C3963D.5030601@tsc.uc3m.es> <1136981974.8962.100.camel@rosella> <43C51C33.2000206@andrej.com> Content-Type: text/plain Date: Thu, 12 Jan 2006 13:10:53 +1100 Message-Id: <1137031853.3681.138.camel@rosella> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 43C5BABE.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 43C5BABB.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 coinductive:01 semantics:01 andrej:01 unifying:01 ocaml:01 ocaml:01 model:01 binary:01 'the':98 wrote:01 wrote:01 sourceforge:01 expressive:01 supported:01 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 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 theory of final coalgebras is NOT > just a dual of the theory of initial algebras. Agree, assuming you mean 'The' theory to refer to "the historically accumulated body of literature in this domain of discourse". Quite clearly the dual of "the theory" of initial algebras is "a theory" of final algebras, that's beyond dispute. so your claim seems to be quite simply that this dual theory is not the same as "the theory" of final coalgebras. What you seem to miss is that I know that, and it is the whole point of my comments. Read again: I said "it is silly ... " 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. You are of course free to disagree on that, since it isn't a mathematical statement, but one about research direction. Some people DO disagree -- they think functional programming is enough. They may be right! I don't know (but I do not believe it). I am saying that "we" programmers want something which provides better integration of the two models than C. Ocaml is better. I don't write C much these days :) 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. The integration in Charity IS supported this way -- but Charity isn't strong (expressive) enough. 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". My answer is that you would be completely missing the point. I can run BOTH of I and O on my OS, which is U. But I have to use weak ad hoc primitives under U to connect programs written in I and O together. Such as writing and reading files of binary data -- not very typesafe or efficient and requiring lots of ugly housekeeping. My REAL programming language is actually U, not I or O: they're just subcomponents of U, and U is UGLY!!! So having separate I and O is bad. I want ONE language U which is general purpose and scales to ALL levels. Category theory more or less promises this! It is the first system where you can use itself to talk about constructions in itself. Thus .. the idea of working in I or O is silly. That was my claim. The only system worth working in is U: the system that integrates both models seamlessly. We just don't know what U is yet .. but we should be looking for it! -- John Skaller Felix, successor to C++: http://felix.sf.net