From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 16330BB81 for ; Thu, 12 Jan 2006 22:54:30 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k0CLsTn3010664 for ; Thu, 12 Jan 2006 22:54:29 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id WAA26739 for ; Thu, 12 Jan 2006 22:54:28 +0100 (MET) Received: from smtp3.adl2.internode.on.net (smtp3.adl2.internode.on.net [203.16.214.203]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0CLsQKf002658 for ; Thu, 12 Jan 2006 22:54:27 +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 k0CLs8SW035428; Fri, 13 Jan 2006 08:24:19 +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: <43C661AF.2080404@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> <1137031853.3681.138.camel@rosella> <43C661AF.2080404@andrej.com> Content-Type: text/plain Date: Fri, 13 Jan 2006 08:54:08 +1100 Message-Id: <1137102848.3681.268.camel@rosella> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 43C6D015.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43C6D012.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 algebra:01 unbalanced:01 structs:01 lacks:01 ocaml:01 ocaml:01 semantics:01 mismatch:01 extensional:01 polymorphism:01 theorems:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.9 required=5.0 tests=SOME_BREAKTHROUGH autolearn=disabled version=3.0.3 On Thu, 2006-01-12 at 15:03 +0100, Andrej Bauer wrote: > 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. I know. > May I ask what experience you have with present research > directions in inital algebra and final coalgebras? Very little, apart from reading occasional papers I don't understand :) But I don't think I'm being silly, I think you just misunderstood my point. Even ordinary people are capable of reasoning, and academics often can't see the wood for the trees. In this case it seems simple -- to me anyhow. The ideas are dual, the theories should be symmetrical, if they're not then its the theories that are out of whack and need to be fixed. Just as, for example, C++ is unbalanced, because it has good support for products (structs) but lacks proper sums. So again, when you said: "The theory of final coalgebras is NOT just a dual of the theory of initial algebras." I consider you wrong, because your statement is about history -- and mine is an axiom. Mine isn't about the current state of the art -- its about where it should be going KNOWING that the theories are necessarily symmetrical. We can speculate about why products are understood better than sums, why there's been more research into functional than stateful programming: the history of mathematics is fascinating. It's kind of like the discussion of 'void'. Your argument at that time just showed my inability to express myself ;( You said Ocaml was an expression language and so unit was the right type for a statement -- and so missed the point that one could -- and I WAS -- arguing that Ocaml is not a functional language, and if we're arguing about changes to make it better, you cannot sensibly turn around and argue statements can't be void *because* it uses a syntactic form appropriate for a language semantics it doesn't have in the first place: given the mismatch another way to fix the problem is to change it so it some syntactic forms are considered statements, and then your argument evaporates. It's quite possible to do that, I have done it in Felix, and I have seen it done in other languages developed by world renowned experts (including many examples from Reynolds, and Jays FISh: FISh used 'command' as the type of a statement, rather than 'void', so there's an additional argument about whether void -- which has a functional interpretation -- can be used instead: recall I conceded it was a hack, but appeared to work in practice anyhow, at least in a language like Felix with extensional polymorphism) The problem here is communication of subtle things like intent and viewpoint. As in this case, where what YOU mean by 'the theory' seems to me to be different to what I mean -- I can't believe we could disagree on the underlying mathematics -- you'd be right every time on that I'm sure. But it isn't just a matter of the actual formal facts, but their context. Please read again the interchange: >> 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. >The theory of final coalgebras is NOT >just a dual of the theory of initial algebras. >While it is true that final coalgebras and initial algebras are dual >concepts, it is far from truth that we may translate results about one >to results about others by applying simple duality. First, you agree the ideas are dual .. and that's a formal mathematical statement that the very definitions are obtainable from each other by a mechanical application of the duality principle -- provided the definitions are stated formally enough of course. And then you say the theories are not -- yet theories are nothing more than the bodies of theorems derived from a given set of axioms and particular inference rules: here the rules are invariant so it follows immediately the theories ARE in fact NECESSARILY dual, and indeed derivable from each other by mechanical application of the duality. I do not require a PhD to do basic logical reasoning -- and it turns out I just paraphrased Maclane anyhow :) You go on to explain that the systems are not studied in self-dual categories .. which is the wood for the trees problem. It isn't relevant, except historically, and I myself made a comment (which I paraphrase having deleted the email) that this may lead to theorems in an unfamiliar setting, which could be a difficulty. In citing the case of dualising Birkhoff being hard work you have just confirmed this -- but your conclusion that my claim is false is quite unjustified -- and that's because you seems to have incorrectly assumed my arguments applied only within a single setting -- which I did not. [I'm saying they SHOULD apply in a single setting .. and citing the fact this isn't the case as the actual problem!] To take a simpler example, I simply say in some category X with products, and perhaps some extra structure, you can dualise any set of theorems to obtain another theory. I didn't say about the same category!!! Obviously!! Since the dual categories have sums not products. But it is certainly a dual theory by construction. The same clearly applies to initial and final algebras, and ALL other dual concepts -- that's the whole POINT of duality. So perhaps you can now see what I was really saying? That the PROBLEM isn't the mathematical theories are not dual -- they are, necessarily. The problem is that before duality was considered bodies of theories arose from different considerations that were not in fact dual i the literature, and that at least for the purpose of studying programming languages the lack of symmetry is ITSELF the real problem. There's no way to construct a good programming language that isn't fully symmetrical -- that's my opinion. It is based on intuition, its only an opinion, and I might be convinced otherwise: as I mentioned some people -- perhaps many here -- believe purely functional programming is the answer. I do not. So I'm left believing you can't read my English as I intend -- probably because I just can't express my ideas succinctly. You say something I said is 'completely false' when in fact the claim is a belief about where research should be heading to get what I want -- a decent programming language. Therefore, it isn't a statement of the kind for which you can reasonably say it is false: it isn't an argument in the mathematical sense where mathematical reasoning could be wrong, nor is it a fact of nature to be disputed, but an opinion about what research is needed to achieve my goals. You would be free to counter-claim by saying my belief was misguided, and appreciated if you explained why -- since as you say that's actually YOUR area of research. For example, having said that symmetry WOULD be obtained if studies were restricted to self-dual categories, perhaps you'd care to explain why doing that is NOT a good idea, for the purpose of eventually obtaining a decent programming language?? That's a genuine question -- what I learned started off with distributive categories (ones with all finite sums and products and a distributive law), and they ARE self-dual, are they not? The whole Sydney School uses them as the basis of studying programming. (You can understand my viewpoint then, having studied at Sydney .. :) Are such categories too weak? Does this mean we must pick instead just ONE of the theories or the other? Would one be better for a programming language and why? [This may well be the case because programming languages are not independent of human psychology] Finally -- I wish to show why your claim about self-dual categories is misguided: "The duality principle also applies to statements involving several categories and functors between them." --- Saunders MacLane, Categories for the Working Mathematician, Page 32. Wood for trees: it doesn't make any difference whether the categories are self dual or not. The 'theories' are constructed in complex *systems* and again my point is that the systems within which initial and final algebras are studies may well have been different, perhaps for historical reasons, and perhaps by demand of some particular application -- my claim is that is NOT the case for study of programming languages: if the systems aren't symmetrical, and you take as an axiom they should be, it FOLLOWS that scientists interested in programming languages should be trying to find a symmetrical system. So as far as I can see it is all very simple: everything follows from the one Platonistic belief that programming languages should be symmetrical, and they should scale to all levels of application -- from systems programming to building GUIs, networks and databases. At least more symmetrical than we have now! And my own experience confirms this -- Ocaml is MUCH better than C++ because it provides good support for both products and sums, C++ does not. Symmetry matters. It is a key guiding principle, and responsible for most of the major breakthroughs in theoretical physics. We surely need something similar in programming theory. -- John Skaller Felix, successor to C++: http://felix.sf.net