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 B233EBB81 for ; Wed, 11 Jan 2006 13:19:45 +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 k0BCJj2f019901 for ; Wed, 11 Jan 2006 13:19:45 +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 NAA26017 for ; Wed, 11 Jan 2006 13:19:44 +0100 (MET) Received: from ash25e.internode.on.net (ash25e.internode.on.net [203.16.214.182]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0BCJgwb014957 for ; Wed, 11 Jan 2006 13:19:43 +0100 Received: from rosella (ppp33-253.lns1.syd6.internode.on.net [59.167.33.253]) by ash25e.internode.on.net (8.13.5/8.13.5) with ESMTP id k0BCJZ01062592; Wed, 11 Jan 2006 22:49:36 +1030 (CST) (envelope-from skaller@users.sourceforge.net) Subject: Re: [Caml-list] Coinductive semantics From: skaller To: Hendrik Tews Cc: caml-list@inria.fr In-Reply-To: References: <43BD6418.4090407@barettadeit.com> <43BE6CAB.2030503@andrej.com> <43C3963D.5030601@tsc.uc3m.es> Content-Type: text/plain Date: Wed, 11 Jan 2006 23:19:34 +1100 Message-Id: <1136981974.8962.100.camel@rosella> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 43C4F7E1.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43C4F7DE.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 coinductive:01 semantics:01 hendrik:01 tews:01 valverde:01 algebra:01 constructors:01 datatypes:01 descriptors:01 datatypes:01 semantics:01 coalgebraic:01 bisimulation: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=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 On Wed, 2006-01-11 at 09:34 +0100, Hendrik Tews wrote: > "Francisco J. Valverde Albacete" writes: > > although I may be out on a limb here, I recall reading *somewhere* :( > that while initial algebras where good models for stateless abstract > data types (and (structural) induction the way to work over terms in > the free algebra defined by constructors modulo the laws of the ADT), > final algebras where good models for *stateful* datatypes (and > coinduction the way to work over the finer "state descriptors" modulo > the laws of state equivalence), hence they *might* be better models > for *objects* (as stateful datatypes) than initial algebras. > > That's precisely what many people in the field of coalgebras > believe. There are many papers on coalgebras as semantics for > object-orientation. There are coalgebraic specification languages > with an OO touch, etc. And of course, separate development of these things is fairly silly, since as the 'co' indicates the two ideas are formally dual. If I recall the theory connecting them is called the really ugly name "Bisimulation Theory". Basically every theorem of functional programming is automatically a theorem of stateful programming, and the theorem can be found by simply applying the duality principle. The algorithm is purely mechanical and well known, however in practice many theorems are not specified in a formal language, and so some work is required to find the co-algebraic dual, and even more to try to figure out what it means in the unfamiliar domain. The bottom line here is that purely functional programming is necessarily an entirely stupid idea -- obviously we want a programming model that allows BOTH functional and stateful programming, and allows a programmer to easily engineer code so it can use both models together seamlessly. That's the Holy Grail. Of course subsidiary techniques are known for doing this, for example Monadic programming in Haskell, but I doubt anyone would consider this mechanism general enough to constitute a proper integration of the two dual models. There is one language that integrates both models seamlessly, and that's Charity. It has the nice property that all programs terminate -- however it isn't as expressive as other languages (it isn't Turing complete .. obviously). The paper I read on this (I'd love to find it again) shows how to derive much of the Eiffel semantics -- such as preconditions etc .. directly from dualising functional programming ideas. This paper was written for ordinary programmers like me, not theorists. The most interesting thing was that inheritance wasn't covered.. we all know inheritance is screwed by the covariance problem and this should just drop out of dualising some basic functional programming ideas. In particular, it is probably the guideline for engineering a solution involving both OO and functional models (tells the programmer when to switch models). Ok .. now a real category theorist can please correct all my mistakes? -- John Skaller Felix, successor to C++: http://felix.sf.net