Re: [Caml-list] Coinductive semantics

[skaller <skaller@users.sourceforge.net>]

On Wed, 2006-01-11 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
> 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 <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net