Re: [Caml-list] Coinductive semantics

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

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 theory of final coalgebras is NOT
> just a dual of the theory of initial algebras.

Agree, assuming you mean 'The' theory to refer to
"the historically accumulated body of literature in
this domain of discourse".

Quite clearly the dual of "the theory" of initial
algebras is "a theory" of final algebras, that's beyond
dispute. so your claim seems to be quite simply that
this dual theory is not the same as "the theory" of
final coalgebras.

What you seem to miss is that I know that, and it is the
whole point of my comments. Read again: I said

"it is silly ... "

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.

You are of course free to disagree on that, since it isn't
a mathematical statement, but one about research direction.
Some people DO disagree -- they think functional programming
is enough. They may be right! I don't know (but I do not
believe it).

I am saying that "we" programmers want something which
provides better integration of the two models than C.
Ocaml is better. I don't write C much these days :)

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.

The integration in Charity IS supported this way --
but Charity isn't strong (expressive) enough.

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

My answer is that you would be completely missing
the point. I can run BOTH of I and O on my OS,
which is U. But I have to use weak ad hoc primitives
under U to connect programs written in I and O together.
Such as writing and reading files of binary data --
not very typesafe or efficient and requiring lots of
ugly housekeeping.

My REAL programming language is actually U, not I or O:
they're just subcomponents of U, and U is UGLY!!!

So having separate I and O is bad. I want ONE language U
which is general purpose and scales to ALL levels.

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

Thus .. the idea of working in I or O is silly.
That was my claim. The only system worth working in is U:
the system that integrates both models seamlessly.
We just don't know what U is yet .. but we should be
looking for it!

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net