Re: [Caml-list] Coinductive semantics

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

On Fri, 2006-01-13 at 11:23 +0100, Hendrik Tews wrote:
> Dear skaller,

> This is completely wrong. If you dualize an initial algebra you
> get a final coalgebra, _but in Set^op, (ie, dualized Set)_.

Indeed.

> Nobody is interested in final coalgebras in Set^op. 

Why not? This is really the key point of misunderstanding
I think. I'm not disputing your claim, I'm asking why not?
Perhaps they should be?

The dual of a vector space is a space of functionals,
and is independently useful and interesting. Why doesn't
this apply to programming languages as well?

Andrej actually answered that here:

"Whenever C is useful for modelling programming languages, 
C^op is useless"

"The symmetries that you want are not there, provably."

Why? Why is C^op useless for all possible C that are
useful for modelling programming languages?

For example an answer like "The distributive law 
is required in C and never holds in C^op" would be
an answer (not claiming it is the case just trying
to illustrate the kind of answer I would like to see).

> Take for instance the (set-) functor F(X) = (X x nat) + 1, where
> x is product, + is disjoint union, 1 is a one-element set. The
> initial algebras for it are the finite lists over nat. The final
> coalgebra for it are sequences over nat, that is finite and
> infinite list over nat. Do you see the difference? This
> difference makes coalgebras interesting.

Yet somehow Charity has both and supports both symmetrically
and seamlessly, more or less as I would desire.

So perhaps what I need (as a programmer) isn't what I asked
for (the client has genuine needs but doesn't know what they
are.. the client asks for X, but really needs Y .. the
expert gives them Y anyhow :)

>    dual -- they are, necessarily. The problem is that before
>    duality was considered bodies of theories arose from different
>    considerations that were not in fact dual i the literature, 
> 
> Sorry, you make yourself a fool here.

Why (are you sorry about a fault that is clearly mine)? 

The court jester or fool was an important contributor
to social cohesion. Some fool like me who risks looking
stupid .. and look at all the good information now
coming out! I'm sure I'm not the only one to appreciate it.
Most people wouldn't risk looking stupid  .. I did.
I'm willing to stick my neck out. 

But I do take exception to being accused of trying
to 'badmouth' a group of people who I have great
respect for -- mathematicians and especially category
theorists. Even if I were to say research direction
was on the wrong track, right or wrong I wouldn't
be trying to badmouth anyone (I'll reserve that
for John Howard and George Bush :)

>  Go out, read the papers on
> the Co-Birkhoff theorem! 

That's a pretty big ask of someone who isn't a
category theorist isn't it? Most mathematicians
can't understand category theory .. and I'm just
an ordinary programmer :)

> Then you'll see that duality was always
> considered by all authors on that subject. 

Hmm .. correct me if I'm wrong, but weren't initial algebras
studied well before final coalgebras? Perhaps even before
category theory existed? I would have thought there were
quite a few term calculi around, such as formal polynomials,
lambda calculus, etc .. and it seems to me the study of
coalgebras is newer. 


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