Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Coinductive semantics
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2006-01-12 (14:02)
From: Andrej Bauer <Andrej.Bauer@a...>
Subject: Re: [Caml-list] Coinductive semantics
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. May I ask what experience you have with present research
directions in inital algebra and final coalgebras?

skaller wrote:
> 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 claim "it is silly to have separate development of these things
[initial algebras and final coalgebras]" is true, but it is FALSE that
there is such a separate development.

> 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.

The people who work in research in initial algebras and final coalgebras
for computer science usually are quite familiar with both directions
(naturally, if you're trying to do something serious, you're going to
put more emphasis on one particular thing). They are well aware of the
duality that you are aware or, and quite likely are aware of a number of
things that you have never heard about. One of them is that final
coalgebras and initial algebras are two different ballgames. They
require different ideas, proofs and techniques.

You make it sound as if all these people forgot to apply a trivial
duality principle. They did not.

You make it sound as if "these people" are divided into two disjoint
sets, one doing initial algebra and another doing final coalgebra. This,
too is completely false. Typical conferences in this area, and even
typical papers, consider both algebras and coalgebras. People DO strive
to give unified accounts of both subjects (via category theory, mainly).

I do not know where you got the idea that serious researchers harbor
simplistic convictions such as:

> Some people DO disagree -- they think functional programming
> is enough.

This is an opinion that only a programmer who knows very little about
the theory of programming languages would propose. It is at the level of
 a discussion that two drunk engineers would have over a beer.

> 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.

Oh yes, you are familiar with theoretical models on which ocaml is based
then? Are you then familiar with, say, realizability models? Do you know
that every polynomial functor has both an initial algebra and a final
coalgebra in any realizability model? Or are you just saying stuff that
sounds good?

If you have specific criticisms about the design of programming
languages, that is a different issue. But so far you are just
criticising an entire research community. Not everyone in that community
does design and implementation of programming languages.

> 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".

You think initial algebras are somehow fundamentally linked to
functional languages and final coalgebras to stateful langauges. This
again shows poor understanding.

The forementioned realizability models demonstrate that initial algebras
and final coaglebras coexist in any realizability model over _any_
Turing complete programming language, whether functional, stateful or
parallel, non-deterministic, etc. It is a matter of _design_ (not
theory) on how to give access to algebras and coalgebras to programmers.

> Category theory more or less promises this! It is the
> first system where you can use itself to talk about
> constructions in itself.

What do you mean precisely by "can use itself to talk about
constructions in itself"?

I apologize for saying in such a straightforward way that you have got
no clue what you are talking about. But until you say something that
does not display total ignorance of what researchers (not programmers)
know or are doing about these matters, I shall think your opinion is
worthless--and harmful because you are badmouthing people you know
nothing about.

Andrej Bauer