Re: [Caml-list] Coinductive semantics

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

On Thu, 2006-01-12 at 15:03 +0100, Andrej Bauer wrote:
> 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.

I know.

>  May I ask what experience you have with present research
> directions in inital algebra and final coalgebras?

Very little, apart from reading occasional papers I don't understand :)

But I don't think I'm being silly, I think you just misunderstood
my point. Even ordinary people are capable of reasoning, and
academics often can't see the wood for the trees.

In this case it seems simple -- to me anyhow. The ideas
are dual, the theories should be symmetrical, if they're
not then its the theories that are out of whack and need
to be fixed.

Just as, for example, C++ is unbalanced, because it
has good support for products (structs) but lacks
proper sums.

So again, when you said:

"The theory of final coalgebras is NOT
just a dual of the theory of initial algebras."

I consider you wrong, because your statement is about
history -- and mine is an axiom. Mine isn't about the
current state of the art -- its about where it should
be going KNOWING that the theories are necessarily
symmetrical.

We can speculate about why products are understood better
than sums, why there's been more research into functional
than stateful programming: the history of mathematics
is fascinating.

It's kind of like the discussion of 'void'. Your argument
at that time just showed my inability to express myself ;(
You said Ocaml was an expression language and so unit
was the right type for a statement -- and so missed the point
that one could -- and I WAS -- arguing that Ocaml is not
a functional language, and if we're arguing about changes
to make it better, you cannot sensibly turn around and
argue statements can't be void *because* it uses a syntactic
form appropriate for a language semantics it doesn't have
in the first place: given the mismatch another way to fix
the problem is to change it so it some syntactic forms
are considered statements, and then your argument evaporates.
It's quite possible to do that, I have done it in Felix,
and I have seen it done in other languages developed by
world renowned experts (including many examples from
Reynolds, and Jays FISh: FISh used 'command' as the type
of a statement, rather than 'void', so there's an additional
argument about whether void -- which has a functional
interpretation -- can be used instead: recall I conceded
it was a hack, but appeared to work in practice anyhow,
at least in a language like Felix with extensional polymorphism)

The problem here is communication of subtle things like
intent and viewpoint. As in this case, where what
YOU mean by 'the theory' seems to me to be different
to what I mean -- I can't believe we could disagree
on the underlying mathematics -- you'd be right every
time on that I'm sure. But it isn't just a matter
of the actual formal facts, but their context.

Please read again the interchange:

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

>While it is true that final coalgebras and initial algebras are dual
>concepts, it is far from truth that we may translate results about one
>to results about others by applying simple duality. 

First, you agree the ideas are dual .. and that's a formal
mathematical statement that the very definitions are obtainable
from each other by a mechanical application of the duality
principle -- provided the definitions are stated formally
enough of course.

And then you say the theories are not -- yet theories are nothing
more than the bodies of theorems derived from a given set
of axioms and particular inference rules: here the rules are
invariant so it follows immediately the theories ARE in fact
NECESSARILY dual, and indeed derivable from each other by
mechanical application of the duality. I do not require
a PhD to do basic logical reasoning -- and it turns out
I just paraphrased Maclane anyhow :)

You go on to explain that the systems are not studied
in self-dual categories .. which is the wood for the trees
problem. It isn't relevant, except historically, and I
myself made a comment (which I paraphrase having deleted
the email) that this may lead to theorems in an unfamiliar
setting, which could be a difficulty. In citing the case
of dualising Birkhoff being hard work you have just confirmed
this -- but your conclusion that my claim is false is quite
unjustified -- and that's because you seems to have incorrectly
assumed my arguments applied only within a single setting --
which I did not. [I'm saying they SHOULD apply in a single
setting .. and citing the fact this isn't the case
as the actual problem!]

To take a simpler example, I simply say in some category X
with products, and perhaps some extra structure,
you can dualise any set of theorems to obtain another theory.
I didn't say about the same category!!! Obviously!! Since
the dual categories have sums not products. But it is certainly
a dual theory by construction.

The same clearly applies to initial and final algebras,
and ALL other dual concepts -- that's the whole POINT of duality.

So perhaps you can now see what I was really saying?
That the PROBLEM isn't the mathematical theories are not
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, 
and that at least for the purpose of studying programming languages 
the lack of symmetry is ITSELF the real problem. There's no way
to construct a good programming language that isn't fully
symmetrical -- that's my opinion. It is based on intuition,
its only an opinion, and I might be convinced otherwise:
as I mentioned some people -- perhaps many here -- believe
purely functional programming is the answer. I do not.

So I'm left believing you can't read my English as I intend --
probably because I just can't express my ideas succinctly.
You say something I said is 'completely false' when in 
fact the claim is a belief about where research should
be heading to get what I want -- a decent programming language.
Therefore, it isn't a statement of the kind for which
you can reasonably say it is false: it isn't an argument
in the mathematical sense where mathematical reasoning
could be wrong, nor is it a fact of nature to be disputed,
but an opinion about what research is needed to achieve my goals.

You would be free to counter-claim by saying my belief was 
misguided, and appreciated if you explained why -- since
as you say that's actually YOUR area of research.

For example, having said that symmetry WOULD be obtained
if studies were restricted to self-dual categories,
perhaps you'd care to explain why doing that is NOT a
good idea, for the purpose of eventually obtaining
a decent programming language??

That's a genuine question -- what I learned started
off with distributive categories (ones with all
finite sums and products and a distributive law),
and they ARE self-dual, are they not? The whole Sydney
School uses them as the basis of studying programming.
(You can understand my viewpoint then, having studied
at Sydney .. :) 

Are such categories too weak? Does this mean we
must pick instead just ONE of the theories or the
other? Would one be better for a programming language
and why? [This may well be the case because programming
languages are not independent of human psychology]

Finally -- I wish to show why your claim about self-dual
categories is misguided:

"The duality principle also applies to statements involving
several categories and functors between them." --- Saunders
MacLane, Categories for the Working Mathematician, Page 32.

Wood for trees: it doesn't make any difference whether
the categories are self dual or not. The 'theories' are
constructed in complex *systems* and again my point is that
the systems within which initial and final algebras are
studies may well have been different, perhaps for
historical reasons, and perhaps by demand of some particular
application -- my claim is that is NOT the case for
study of programming languages: if the systems aren't
symmetrical, and you take as an axiom they should be,
it FOLLOWS that scientists interested in programming languages
should be trying to find a symmetrical system.

So as far as I can see it is all very simple: everything
follows from the one Platonistic belief that programming
languages should be symmetrical, and they should scale
to all levels of application -- from systems programming
to building GUIs, networks and databases. At least more
symmetrical than we have now! And my own experience
confirms this -- Ocaml is MUCH better than C++ because
it provides good support for both products and sums,
C++ does not.

Symmetry matters. It is a key guiding principle,
and responsible for most of the major breakthroughs
in theoretical physics. We surely need something similar
in programming theory.

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