Re: [Caml-list] Coinductive semantics

[Andrej Bauer <Andrej.Bauer@andrej.com>]

Your main observation seems to be this: algebras in a category C are
dual to coalgebras in the opposite category C^op. Leaving further
insults aside, let me explain why this observation does not help much.

In order to have a category C which is a useful model of computation,
the category C must have certain properties (such as being cartesian
closed so that we can interpret lambda calculus in it). Also, one cannot
use _two_ categories C and D and model some features in C, others in D,
and hope to get a coherent picture which tells how the features interact
with each other.

Whenever C is useful for modelling programming languages, C^op is
useless. While it is true that whatever you prove about algebras in C
corresponds to something about coalgebras in C^op, this tells you
absolutely nothing about coalgebras in C. Since C is what we care about,
we then need to study coalgebras in C separately.

The symmetries that you want are not there, provably.

Believe me, what you are suggesting is trivial and researchers know
precisely to what amount it works.

Andrej