Coinductive semantics
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  skaller <skaller@u...> 
Subject:  Re: [Camllist] Coinductive semantics 
On Wed, 20060111 at 09:34 +0100, Hendrik Tews wrote: > "Francisco J. Valverde Albacete" <fva@tsc.uc3m.es> 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 > objectorientation. 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 coalgebraic 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 <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net