Coinductive semantics

Coinductive semantics

[Alessandro Baretta]

http://pauillac.inria.fr/~xleroy/publi/coindsem.pdf

This beautiful paper describes a logic system comprising coinductive inference 
rules. Neither Google nor Wikipedia nor Mathworld have given me a formal 
definition of "coinduction", to support my intuition. Is there anyone around who 
can help?

Alex

-- 
*********************************************************************
http://www.barettadeit.com/
Baretta DE&IT
A division of Baretta SRL

tel. +39 02 370 111 55
fax. +39 02 370 111 54

Our technology:

The Application System/Xcaml (AS/Xcaml)
<http://www.asxcaml.org/>

The FreerP Project
<http://www.freerp.org/>

Re: [Caml-list] Coinductive semantics

[David Baelde]

In short,

An inductive type is the least fixpoint of some equations. The
coinductive type is the greatest fixpoint. For "t = nil | cons of
e*t", the elements of the inductive type are the lists, but the
coinductive type also contains the infinite lists.

Now for induction and coinduction, not so easy to tell... The
induction is the process building inductive types, the coinduction
builds coinductive types. In theory, the induction always terminates
and build a finite object. The coinduction should be seen as a lazy
process, since it potentially builds an infinite object: running it
builds the beginning of the object, then the process freezes and waits
for you to inspect the object deep enough.

Hope this helps... at least that's a try.
--
David

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

Alessandro Baretta wrote:
> Is there anyone around who  can help?

Induction is about initial algebras. It says that an initial algebra
does not have any non-trivial SUB-algebras. General induction principle
for the initial algebra A with operations f_1, ..., f_n (some of which
may be 0-ary operations, i.e., constants) goes as follows:

INDUCTION PRINCIPLE:
Suppose S is a subset of A which is closed under operations f_i, meaning
that if x_1, ..., x_{k_i} are in S then also f_i(x_1, ..., x_{k_i}) is
in S (here k is the arity of operation f_i). Then S = A.

If we apply this to the case when we have one constant f_0=Empty and one
binary operation f_1=Tree, we get as A all finite binary trees and the
induction principle:

INDUCTION PRINCIPLE FOR FINITE BINARY TREES:
Suppose S is a set of finite binary trees such that the empty tree is in
S, and whenever x and y are in S then also tree Tree(x,y) is in S. Then
S is the set of all finite binary trees.

Now coinduction is about final coalgebras. It says that a final
coalgebra does not have any non-trivial QUOTIENT coaglebras. This is
usually expressed as follows: if F is the final coalgebra for operations
f_1, ..., f_n, and E is an equivalence relation on F which respects the
operations, then E is the identity relation (because if it were not, we
could form a nontrivial quotient coaglebra F/E). The actual coinduction
principle may be stated for an arbitrary relation R (think of E as the
equivalence relation generated by R):

COINDUCTION PRINCIPLE:
Suppose R is a relation on the final coalgebra F which respects the
operations, i.e., if x_1 R y_1, ...., x_{k_i} R y_{k_i} then
f_i(x_1, ..., x_{k_i}) R f_i(y_1, ..., y_{k_i}) for all x's, y's and
f_i's. Then R(x,y) implies x = y.

An R satisfying the above condition generates the trivial equivalence
relation (equality) and so the quotient F/R is just F.

We take again as example the final coalgebra F with one constant
f_0=Empty and one binary operation f_1=Tree. This is the set of finite
and infinite binary trees.

COINDUCTION FOR (FINITE AND INFINITE) BINARY TREES:
Suppose R is a relation on trees such that:
(1) Empty R Empty
(2) if x R y and x' R y' then Tree(x,y) R Tree(x',y').
Then x R y implies x = y.

It takes some practice to get used to coinduction and to figure out how
to prove properties of final coalgebras with it. If this was too terse,
let me know (and tell me which bits to expand upon).

Andrej

Re: [Caml-list] Coinductive semantics

[Francisco J. Valverde Albacete]

Hi

although I may be out on a limb here, I recall reading *somewhere* :( 
that while initial algebras where good models for stateless abstract 
data types (and (structural) induction the way to work over terms in the 
free algebra defined by constructors modulo the laws of the ADT), final 
algebras where good models for *stateful* datatypes (and coinduction the 
way to work over the finer "state descriptors" modulo the laws of state 
equivalence), hence they *might* be better models for *objects* (as 
stateful datatypes) than initial algebras.

Has anybody read anything proving or disproving this?

Regards,

    Francisco Valverde - DTSC
    Univ. Carlos III de Madrid


Andrej Bauer wrote:

>Alessandro Baretta wrote:
>  
>
>>Is there anyone around who  can help?
>>    
>>
>
>Induction is about initial algebras. It says that an initial algebra
>does not have any non-trivial SUB-algebras. General induction principle
>for the initial algebra A with operations f_1, ..., f_n (some of which
>may be 0-ary operations, i.e., constants) goes as follows:
>
>INDUCTION PRINCIPLE:
>Suppose S is a subset of A which is closed under operations f_i, meaning
>that if x_1, ..., x_{k_i} are in S then also f_i(x_1, ..., x_{k_i}) is
>in S (here k is the arity of operation f_i). Then S = A.
>
>If we apply this to the case when we have one constant f_0=Empty and one
>binary operation f_1=Tree, we get as A all finite binary trees and the
>induction principle:
>
>INDUCTION PRINCIPLE FOR FINITE BINARY TREES:
>Suppose S is a set of finite binary trees such that the empty tree is in
>S, and whenever x and y are in S then also tree Tree(x,y) is in S. Then
>S is the set of all finite binary trees.
>
>Now coinduction is about final coalgebras. It says that a final
>coalgebra does not have any non-trivial QUOTIENT coaglebras. This is
>usually expressed as follows: if F is the final coalgebra for operations
>f_1, ..., f_n, and E is an equivalence relation on F which respects the
>operations, then E is the identity relation (because if it were not, we
>could form a nontrivial quotient coaglebra F/E). The actual coinduction
>principle may be stated for an arbitrary relation R (think of E as the
>equivalence relation generated by R):
>
>COINDUCTION PRINCIPLE:
>Suppose R is a relation on the final coalgebra F which respects the
>operations, i.e., if x_1 R y_1, ...., x_{k_i} R y_{k_i} then
>f_i(x_1, ..., x_{k_i}) R f_i(y_1, ..., y_{k_i}) for all x's, y's and
>f_i's. Then R(x,y) implies x = y.
>
>An R satisfying the above condition generates the trivial equivalence
>relation (equality) and so the quotient F/R is just F.
>
>We take again as example the final coalgebra F with one constant
>f_0=Empty and one binary operation f_1=Tree. This is the set of finite
>and infinite binary trees.
>
>COINDUCTION FOR (FINITE AND INFINITE) BINARY TREES:
>Suppose R is a relation on trees such that:
>(1) Empty R Empty
>(2) if x R y and x' R y' then Tree(x,y) R Tree(x',y').
>Then x R y implies x = y.
>
>It takes some practice to get used to coinduction and to figure out how
>to prove properties of final coalgebras with it. If this was too terse,
>let me know (and tell me which bits to expand upon).
>
>Andrej
>
>_______________________________________________
>Caml-list mailing list. Subscription management:
>http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
>Archives: http://caml.inria.fr
>Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>Bug reports: http://caml.inria.fr/bin/caml-bugs
>  
>

Re: [Caml-list] Coinductive semantics

[Hendrik Tews]

"Francisco J. Valverde Albacete" <fva@tsc.uc3m.es> writes:

   although I may be out on a limb here, I recall reading *somewhere* :(
   that while initial algebras where good models for stateless abstract
   data types (and (structural) induction the way to work over terms in
   the free algebra defined by constructors modulo the laws of the ADT),
   final algebras where good models for *stateful* datatypes (and
   coinduction the way to work over the finer "state descriptors" modulo
   the laws of state equivalence), hence they *might* be better models
   for *objects* (as stateful datatypes) than initial algebras.
   
That's precisely what many people in the field of coalgebras
believe. There are many papers on coalgebras as semantics for
object-orientation. There are coalgebraic specification languages
with an OO touch, etc.

Hendrik Tews

Re: [Caml-list] Coinductive semantics

[skaller]

On Wed, 2006-01-11 at 09:34 +0100, Hendrik Tews wrote:
> "Francisco J. Valverde Albacete" <fva@tsc.uc3m.es> writes:
> 
>    although I may be out on a limb here, I recall reading *somewhere* :(
>    that while initial algebras where good models for stateless abstract
>    data types (and (structural) induction the way to work over terms in
>    the free algebra defined by constructors modulo the laws of the ADT),
>    final algebras where good models for *stateful* datatypes (and
>    coinduction the way to work over the finer "state descriptors" modulo
>    the laws of state equivalence), hence they *might* be better models
>    for *objects* (as stateful datatypes) than initial algebras.
>    
> That's precisely what many people in the field of coalgebras
> believe. There are many papers on coalgebras as semantics for
> object-orientation. There are coalgebraic specification languages
> with an OO touch, etc.

And of course, separate development of these things is fairly
silly, since as the 'co' indicates the two ideas are formally
dual. If I recall the theory connecting them is called
the really ugly name "Bisimulation Theory". Basically every theorem
of functional programming is automatically a theorem of
stateful programming, and the theorem can be found by simply
applying the duality principle. The algorithm is purely
mechanical and well known, however in practice many theorems
are not specified in a formal language, and so some work is
required to find the co-algebraic dual, and even more to
try to figure out what it means in the unfamiliar domain.

The bottom line here is that purely functional programming is
necessarily an entirely stupid idea -- obviously we want
a programming model that allows BOTH functional and stateful
programming, and allows a programmer to easily engineer code
so it can use both models together seamlessly. 

That's the Holy Grail.

Of course subsidiary techniques are known for doing this,
for example Monadic programming in Haskell, but I doubt
anyone would consider this mechanism general enough
to constitute a proper integration of the two dual models.

There is one language that integrates both models seamlessly,
and that's Charity. It has the nice property that all programs
terminate -- however it isn't as expressive as other languages
(it isn't Turing complete .. obviously).

The paper I read on this (I'd love to find it again) shows how
to derive much of the Eiffel semantics -- such as preconditions
etc .. directly from dualising functional programming ideas.
This paper was written for ordinary programmers like me,
not theorists. The most interesting thing was that inheritance
wasn't covered.. we all know inheritance is screwed by the
covariance problem and this should just drop out of dualising
some basic functional programming ideas. In particular, it is
probably the guideline for engineering a solution involving
both OO and functional models (tells the programmer when
to switch models).

Ok .. now a real category theorist can please correct
all my mistakes?

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

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

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

While it is true that final coalgebras and inital algebras are dual
concepts, it is far from truth that we may translate results about one
to results about others by applying simple duality. This would only be
the case if we studied algebras and coalgebras in self-dual categories,
which usually we do not (only very special kinds of categories are
self-dual).

For example, the famous Birkhoff theorem about universal algebras says
something about initial algebras. It took a Ph.D. (by Jesse Hughes) to
figure out what the dual of Birkhoff's theorem might be. And believe me
this was not because either Jesse or his advisor failed to "apply a
simple duality principle".

Andrej

Re: [Caml-list] Coinductive semantics

[skaller]

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

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

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

Re: [Caml-list] Coinductive semantics

[skaller]

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

Re: [Caml-list] Coinductive semantics

[Hendrik Tews]

Dear skaller,

please read some of the relevant paper, for instance the tutorial
on (Co)Algebras and (Co)Induction.

   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.
   
Please read the relevant definitions. Coalgebras are the duals of
algebras _but_ coalgebra morphisms are not the duals of algebra
morphisms. Otherwise the theory of coalgebras would be void.
Because most interesting properties/definitions are connected
with the morphisms you get that the theory of algebras is _not_
dual to the theory of coalgebras.

   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.
   
   The same clearly applies to initial and final algebras,
   and ALL other dual concepts -- that's the whole POINT of duality.
   
This is completely wrong. If you dualize an initial algebra you
get a final coalgebra, _but in Set^op, (ie, dualized Set)_.
Nobody is interested in final coalgebras in Set^op. People are
interested in finial coalgebras in _Set_, which are the same as
initial algebras in Set^op.

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.

   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. Go out, read the papers on
the Co-Birkhoff theorem! Then you'll see that duality was always
considered by all authors on that subject. The point is that when
you dualize the Birkhoff theorem you don't get a theorem on
coalgebras!

Bye,

Hendrik

PS. Sorry if I missed some of your points, I did not read all of
your prose.

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

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

Re: [Caml-list] Coinductive semantics

[skaller]

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

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

Alessandro Baretta wrote:
> I am very much ashamed of myself for discovering that I simply I have no clue as 
> to what the terms "algebra" and "co-algebra" mean, formally. I take the first to 
> be an algebraic structure with a single set and any number of operations--within 
> this definition the notion of initial algebra can be interpreted without 
> difficulty

Yes, that's what algebras are, except that you may also impose equations
that operations are supposed to satisfy (such as associativity).

> --but what in the world is the second? I can't think of anything 
> different, really: a set and some operations. Even the definition of final 
> co-algebras can be easily interpreted in this definition.

As my advisor once explained: algebras are about putting things
together--take two numbers and "put them together" with an operation,
take an element and a list and put them together to form a new list.
Coalgebras are about taking things apart--take a stream and decompose it
into the head and the tail, take a binary tree and decompose it into its
left and right subtrees, take a Markov process and "decompose" it into
its first transition and the rest of the process, etc. So, in this sense
coalgebras still are sets with operations, you are perfectly right.
Perhaps we could say that algebras have constructors and coalgebras have
"deconstructors".

What may be confusing is that a final coalgebra is also an algebra. For
example, the coalgebraic structure of (finite and infinite) binary trees
may be described by the operation

  take_apart : tree -> (unit | tree * tree)

which takes a tree and returns either (), signifying the tree cannot be
taken apart (the empty tree), or a pair (l,r) where l and r are the left
and the right subtrees, respectively. By Lambek's Lemma take_apart is an
isomorphism. Its inverse (still acting on infinite and finite trees)

  put_together : (unit | tree * tree) -> tree

is best seen as a pair of constructors: put_together () gives a tree
without any subtrees (the empty tree), whereas put_together (l,r) is the
tree whose left and right subtrees are l and r, respectively.

Exercise for skaller ;-): using basic duality, derive the fact that
every initial algebra is also a colagebra, and give an example. How does
this allow us to relate an initial algebra (finite trees) and the
corresponding final coalgebra (infinite and finite trees)?

> So, is it true that algebras and co-algebras are the same beasts, except that 
> when referring to algebras we implicitly declare interest in inductive 
> properties of initial structures, and when referring to co-algebras we imply 
> interest in the co-inductive properties of final structures?

Both algebras and coalgebras are sets with operations. The difference is
in what these operations are doing (constructors vs. deconstructors) and
what properties they have (induction vs. coinduction).

Andrej

Re: [Caml-list] Coinductive semantics

[Hendrik Tews]

skaller <skaller@users.sourceforge.net> writes:

   > 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?
   
Coalgebras in Set^op are for all intents and purposes identical
to algebras in Set. If you want to study them, study them as
algebras in Set. You will see nothing new if you look at these
objects as coalgebras in Set^op. That's what duality means.

Looking at an object through a mirror you see precisely what you
can see looking at the object itself.

   >  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 :)
   
Well, you could try. I guess, that already the introductions
contain enough information for what you are interested in: the
duality of the Birkhoff and the Co-Birkhoff theorem. In any case,
if you don't even try, your speculations about the contents of
these papers remain wild guesses.

   > 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 mean duality was considered by Gumm, Kurz, Hughes, Goldblatt
and all other people that worked on the Co-Birkhoff theorem even
before they started to work on it.

Hendrik

Re: [Caml-list] Coinductive semantics

[skaller]

On Wed, 2006-01-18 at 13:58 +0100, Hendrik Tews wrote:
> skaller <skaller@users.sourceforge.net> writes:
> 
>    > 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?
>    
> Coalgebras in Set^op are for all intents and purposes identical
> to algebras in Set. If you want to study them, study them as
> algebras in Set. You will see nothing new if you look at these
> objects as coalgebras in Set^op. That's what duality means.
> 
> Looking at an object through a mirror you see precisely what you
> can see looking at the object itself.

Perhaps my analysis is naive. But consider a simpler case
of products and sums. They're dual concepts, are they not?

In Ocaml we have representations of both, each can be used
with reasonable utility -- there is a degree of symmetry,
associated with the duality. It feels good!

Contrast to C, which has products, but the union construction
isn't a sum. And the many other 'popular' languages with 
this weakness.

Sometimes it seems looking in the mirror is good. 
It's what we want. We don't want something new!

>    >  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 :)
>    
> Well, you could try. I guess, that already the introductions
> contain enough information for what you are interested in: the
> duality of the Birkhoff and the Co-Birkhoff theorem. In any case,
> if you don't even try, your speculations about the contents of
> these papers remain wild guesses.

I often do try.. but seemed like a good idea to read Adameck first:

http://www.tac.mta.ca/tac/volumes/14/8/14-08abs.html

Still this is quite heavy going for me.

Incidentally .. if you look in Wikipedia for 'coalgebra' you may
be a bit disappointed.

http://en.wikipedia.org/wiki/Coalgebra


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

Re: [Caml-list] Coinductive semantics

[William Lovas]

On Thu, Jan 19, 2006 at 01:22:37AM +1100, skaller wrote:
> On Wed, 2006-01-18 at 13:58 +0100, Hendrik Tews wrote:
> > Looking at an object through a mirror you see precisely what you
> > can see looking at the object itself.
> 
> Perhaps my analysis is naive. But consider a simpler case
> of products and sums. They're dual concepts, are they not?

A thought: products and sums are duals, classically, but not
intuitionistically.  Since O'Caml lacks classical control constructs like
callcc, there's no redundancy having both products and sums: neither is
representable solely using the other.

Also, O'Caml's datatypes are much more than just sums: they also include
recursive types, polymorphism, pattern matching, and a degree of
abstraction.

cheers,
William

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

William Lovas wrote:
> A thought: products and sums are duals, classically, but not
> intuitionistically.

This is false. Products and sums are dual concepts, both classically and
intuitionistically.

> Since O'Caml lacks classical control constructs like
> callcc, there's no redundancy having both products and sums: neither is
> representable solely using the other.

The above statement is rather vague and I am tempted to ignore it. If I
try to interpet it the best I can, it looks as if William is confusing
sums and products with unions and intersections (and is thus thinking
that complements might help in representing sums as products, using laws
of Boolean algebra).

Intersection of sets is a special case of products. Unions is a special
case of coproducts. In any Boolean algebra (hence also in the Boolean
algebra of subsets), unions and intersections may indeed be expressed in
terms of each other, using complements:

 A union B = complement (complement A intersection complement B)

where A, B are elements of a Boolean algebra. But in a general category
there is not such relationship between products and coproducts.

(By the way, unions and intersections are dual concepts even if there is
no complementation available, such as in intuitionistic set theory.)

> Also, O'Caml's datatypes are much more than just sums: they also include
> recursive types, polymorphism, pattern matching, and a degree of
> abstraction.

So? What is the point here?

In a programming language equipped with products and natural numbers,
and irrespective of what else is there, sums of (inhabited) types may be
encoded by products, as every programmer knows (at some level). For
example, to encode the following sum, which expresses the fact that
programmers are interesting characters and mathematicians may experience
instabilities,

  type person = Programmer of char | Mathematician of float

we assign constants

  let programmer = 0
  let mathematician = 1

pick two dummy values

  let dummy_c = '\0'
  let dummy_f = 0.0

and encode values of type person as values of the product type

  type person' = int * char * float

A value Programer(c) is represented by the triple (programmer, c,
dummy_f) and a Mathematician(x) is represented by (mathematician,
dummy_c, f). In a less strictly typed language (e.g. assembler), we may
avoid the redundancy and encode the sum with the product type

  type person'' = int * t

where t is a type large enough to hold both char and float. This is
precisely how people who use "lesser" languages work with sums, and
precisely how sums are represented in compiled ocaml code (modulo
optimizations). Of course, it does not provide a water-tight duality
between products and sums at the level of datatypes, but a certain
realizability construction gets you to a category (built on top of
datatypes) in which the above trick is precisely how sums are
constructed--all that is added as an aftertaught is the definition of
the subobject of person' consisting of those triples whcich represent
valid values of the corresponding sum type.

Andrej

Re: [Caml-list] Coinductive semantics

[William Lovas]

On Fri, Jan 20, 2006 at 10:57:39AM +0100, Andrej Bauer wrote:
> William Lovas wrote:
> > A thought: products and sums are duals, classically, but not
> > intuitionistically.
> 
> This is false. Products and sums are dual concepts, both classically and
> intuitionistically.

Perhaps you can explain this in more detail; my training is in type theory,
not category theory, and i had deMorgan duals in mind.

> > Since O'Caml lacks classical control constructs like
> > callcc, there's no redundancy having both products and sums: neither is
> > representable solely using the other.
> 
> The above statement is rather vague and I am tempted to ignore it. If I
> try to interpet it the best I can, it looks as if William is confusing
> sums and products with unions and intersections (and is thus thinking
> that complements might help in representing sums as products, using laws
> of Boolean algebra).

It is well-known that control constructs like callcc correspond via
Curry-Howard to classical axioms like Peirce's law.  I was referring to
the fact that in the presence of such control operators, one can devise a
sound and complete encoding of products in terms of sums or sums in terms
of products.  For example, section 7 of Tom Murphy's 2005 CSL paper
"Distributed Control Flow with Classical Modal Logic" showed how to define
sums in terms of products using deMorgan duality and letcc.

Maybe what i mean when i say "product" and "sum" is something different
from what you mean?  I *have* been thinking about deMorgan duality using
negation as you mentioned, but it's unrelated to union and intersection
types.

> > Also, O'Caml's datatypes are much more than just sums: they also include
> > recursive types, polymorphism, pattern matching, and a degree of
> > abstraction.
> 
> So? What is the point here?

The point is that even if sums were encodable using products, the inclusion
of datatypes in O'Caml would not be redundant as skaller suggests, since
they bring with them access to several other important features whose
behavior would not otherwise be expressible.

>   type person = Programmer of char | Mathematician of float
> [...]
>   type person' = int * char * float
> [...]
>   type person'' = int * t

These encodings do not have the same force as the original type; they are
complete, but unsound -- every value of person has a corresponding value in
person', but not every value of person' has a corresponding person value
(like (3, 'c', 0.0), for example).  To do this sort of encoding correctly,
wouldn't you need dependent types in the language?  So you could write
something like:

    type person''' = Sigma x:bool. if x then char else float

with

    Programmer(c) =def= (true, c)
    Mathematician(x) =def= (false, x)

> where t is a type large enough to hold both char and float. This is
> precisely how people who use "lesser" languages work with sums, and
> precisely how sums are represented in compiled ocaml code (modulo
> optimizations). Of course, it does not provide a water-tight duality
> between products and sums at the level of datatypes, but a certain
> realizability construction gets you to a category (built on top of
> datatypes) in which the above trick is precisely how sums are
> constructed--all that is added as an aftertaught is the definition of
> the subobject of person' consisting of those triples whcich represent
> valid values of the corresponding sum type.

Perhaps this afterthought subobject is similar to what i'm referring to
above, but i don't know enough category theory to be certain.

cheers,
William

Re: [Caml-list] Coinductive semantics

[skaller]

On Fri, 2006-01-20 at 13:59 -0500, William Lovas wrote:
> On Fri, Jan 20, 2006 at 10:57:39AM +0100, Andrej Bauer wrote:
> > William Lovas wrote:

> These encodings do not have the same force as the original type; they are
> complete,

How would you decode an Andrej sum without a conditional 
control transfer? 

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

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

skaller wrote:
> How would you decode an Andrej sum without a conditional 
> control transfer? 

The control is a consequence of the fact that natural numbers are an
inital algebra (I am pretending that "int" denotes natural numbers). In
a programming language the initiality of natural numbers manifests
itself as an operation "rec" with which we may define function by simple
recursion, i.e, given x : 'a and f : int -> 'a, the expression "rec x f"
has they type int -> 'a and satisfies:

  rec x f 0 = x
  rec x f (n+1) = f (rec x f n)

Since I suggested that we use 0 and 1 as tags for variants, we could
define a deconstructor "match" for sums (i.e. the conditional control
transfer for the sum type) using rec as follows:

  match g h (t, x, y) = rec (g x) (fun _ -> h y) t

The above match has the property that

 match g h (0, x, y) = g x
 match g h (1, x, y) = h y

There are a few details about eager/lazy evaluation of rec which I will
let you sort out (in case rec is "too eager", we use thunking).

Andrej

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

William Lovas wrote:
>> This is false. Products and sums are dual concepts, both classically and
>> intuitionistically.
> 
> Perhaps you can explain this in more detail; my training is in type theory,
> not category theory, and i had deMorgan duals in mind.

Concepts X and Y are dual if X's in a category C are the same thing as
Y's in the opposite category C^op. There is no classical logic involved
when you ask "are products and coproducts dual"--it is apparent that
they are if you look at their definitions in terms of categorical limits
and colimits.

The type-theory training explains (to me) what you had in mind. In type
theory, types and propositions are the same thing, so it makes sense to
talk about deMorgan rules that involve types. Presumably one could do
that in categories as well: consider a category that is equipped with an
involution * such that

  X + Y = (X* x Y*)*

This would be an analogue of deMorgan rules and it would give you
coproducts out of products. But it's a rather special thing and I don't
know how to even express the above equation without first postulating
that coproducts exist. There are several other ways of getting
coproducts out of other things that exist in a category.

> Maybe what i mean when i say "product" and "sum" is something different
> from what you mean?

I mean categorical products and coproducts.

> These encodings do not have the same force as the original type; they are
> complete, but unsound -- every value of person has a corresponding value in
> person', but not every value of person' has a corresponding person value
> (like (3, 'c', 0.0), for example).  To do this sort of encoding correctly,
> wouldn't you need dependent types in the language?  So you could write
> something like:
> 
>     type person''' = Sigma x:bool. if x then char else float
> 
> with
> 
>     Programmer(c) =def= (true, c)
>     Mathematician(x) =def= (false, x)
> 
> Perhaps this afterthought subobject is similar to what i'm referring to
> above, but i don't know enough category theory to be certain.

Not quite, in terms of dependent type theory the aftertaught would be
something like defining a coproduct u+t as a setoid with underlying type
int * u * t and "equality" relation ~

    (a,x,y) ~ (b,x',y') <==>  (a=b=0 and x=x') or (a=b=1 and y=y')

I am not too well-versed in type theory, so you'll have to translate
that into "real" type-theoretic lingo.

As I said, there are many ways to get coproducts. Above you mention one
which uses dependent sums and the type of booleans, which is the
simplest instance of a sum, namely bool = unit + unit.

Another well known construction of coproducts comes from the polymorphic
lambda calculus, where the coproduct u + t is represented by the type

  (u -> 'a) -> (t -> 'a) -> 'a

To see this, use the exponential laws:

  (u -> 'a) -> (t -> 'a) -> 'a =
  (u -> 'a) * (t -> 'a) -> 'a =
  ((u + t) -> 'a) -> 'a .

Nevertheless, none of the above is an argument in favor of eliminating
coproducts from a programming language. In general, the argument "we may
eliminate concept X because it can be reconstructed using other concepts
already present" must be used with caution, lest one ends up programming
directly in assembler.

We are way off topic for this mailing list here, aren't we?

Andrej

Re: [Caml-list] Coinductive semantics

[skaller]

On Sat, 2006-01-21 at 19:36 +0100, Andrej Bauer wrote:
> skaller wrote:
> > How would you decode an Andrej sum without a conditional 
> > control transfer? 
> 
> The control is a consequence of the fact that natural numbers are an
> inital algebra

Hmm ..

>   rec x f 0 = x
>   rec x f (n+1) = f (rec x f n)

Yeah. Of course, natural numbers subsume bool: the switch
is right there already. Thanks!

FYI in Felix 0,1,2 .. etc are types given by n = 1 + 1 + .. + 1.
Not quite natural numbers (since + isn't strictly associative).
For any sum t a variant has notation like

	case 5 of t

in particular the components of bool = 2 are names
false = case 1 of 2 and true = case 2 of 2. The underlying
representation is a tagged pointer, with the pointer optimised
away if no variant has a (non-unit) argument. Since the
tag is an int, the run time representation of a unit sum
is just an int.

I also have arrays t ^ n = t * t * t * .. * t.

In principle, the j'th component is found by indexing
function:

	prj: t ^ n * n -> t

Unlike 'normal' array indexing .. this is entirely safe.
BTW I learned this trick from Pascal, which never needs
array bounds checks -- you have to check conversion 
int ==> n of the index instead.

What I don't know how to do is extend the collection of
fixed length array types, kind of like

	(lim n-> inf) Sum (t ^ n)

Of course I know how to *implement* this infinite sum.
(Which in practice isn't infinite of course)

The problem is that I have to somehow convert from
a run time dynamic type (the array bound is a type!)
to an integer with a 'super switch'. Rougly the
projection for the above limit is 

	typematch .. with ..
	...
	| 5 => let j = check 5 i in a.[j]
	...

in other words its an infinite switch over all the fixed
length array types. Clearly for this particular case
the implementation is just to do an dynamic array bounds
check the way Ocaml does.

But this is very unsatisfying, and in particular provides
no way to optimise away gratuitous checks at compile time.
In other words, you can't compose these things.

I'm not sure my rant really explains what I'm looking for:
basically I don't know enough theory to turn the purely
algebraic finite array types -- fairly useless in practice --
into variable length arrays required in practice.
[By variable I mean the length is an immutable dynamic type,
not that you can change the length of the array]

It would be really nice -- in BOTH Felix and Ocaml --
to have safe arrays. Unlike lists, functions like
combine and split then make sense.

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

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

skaller wrote:
> basically I don't know enough theory to turn the purely
> algebraic finite array types -- fairly useless in practice --
> into variable length arrays required in practice.
> [By variable I mean the length is an immutable dynamic type,
> not that you can change the length of the array]

If I understand you correctly, you have types [0], [1], [2], [3], ...,
one for each natural number 0, 1, 2, ... (to avoid confusion I want to
distinguish notationally between number n and type [n] here, even if
Felix does not do it). Let me call [n] "the type of indices of arrays of
length n". We may think of [n] as the set {0,1,2,...,n-1}.

You know how to deal with the type [n]->t, which is an array of length n
containing t's. Now you would like to "make n variable (dynamic)". This
sounds like a dependent type to me, i.e, you want not just a bunch of
types [0], [1], [2], ... but rather a _type constructor_ [-], which maps
from int to types. You may define it in dependent type theory (I am
going to use set-theretic notation so that I don't confuse everyone):

  [n] = {k : int | 0 <= k and k < n}

In set theory, this is interpreted as follows: an index of an array of
length n is an integer k. This integer must be between 0 and n.

In type theory, this is interpreted as follows: an index of an array of
length n is a _pair_ (k,p) where k is an integer and p is a proof of the
fact k is between 0 and n.

The type of arrays you're talking about is a dependent sum

  't array = sum (n:int) [n]->'t

An element of this type (according to type theory) consists of a pair
(n,a) where n is an integer and a is a map [n]->'t, i.e., an array of
length n. Elements of such an array are indexed by pairs (k,p).

If everyone believed in type theory, compilers would be easy to write.
Every time a programmer wanted to address an element of an array, he
would provide not just the index k but also the proof p that k is a
valid index. Compiler would just have to check that p is a valid proof
(easy when p is a formal proof). But programmers don't want to do that.

If we care about soundness and safety, we are left with two
possibilities: either the compiler or the run-time environment must
supply the missing proof p. For the run-time environment this is easy,
because k and n are always instantiated to particular constants and we
may simply check that 0<=k<n. But for the compiler, it is an impossible
task, since k and n may be arbitrarily complex expressions. The compiler
would have to be able to solve undecidable problems in order to
determine whether an index is valid. You're hitting the theoretical
limit of static type checking.

There may be special cases where compiler can determine whether the
index is ok. For example, if the index is a linear function of a bunch
of integer variables, which is typical of array computations as long as
you're _not_ simulating a matrix as a one-dimensional table or some
such, then you're in the realm of Presburger arithmetic (integers, +, -,
<, =, and multiplication by _constants_ only) which has a decision
procedure (double exponential time, if I remember it right). I am sure
people have looked into this sort of thing. Good luck!

Andrej

Re: [Caml-list] Coinductive semantics

[skaller]

On Sun, 2006-01-22 at 13:23 +0100, Andrej Bauer wrote:
> skaller wrote:

> If everyone believed in type theory, compilers would be easy to write.

LOL!

> Every time a programmer wanted to address an element of an array, he
> would provide not just the index k but also the proof p that k is a
> valid index. Compiler would just have to check that p is a valid proof
> (easy when p is a formal proof). But programmers don't want to do that.

Actually some of us would like to do it .. however this is moving
past my real problem.

I'm willing to accept that the typing may end up being unsound
in the sense the compiler cannot prove what it needs to:
this is actually easy to fix, by simply inserting a runtime
check.

Also, in this particular case (arrays) the run time representation
is already known (literally it is the same as a variant,
where the discriminant tag is the array length). This is very
nice, since you can actually match on it against particular
constant lengths.

My problem is more categorical: given your explanation that
this is a dependent typing thing, how do I represent
such typing in the compiler?

If the type of the *value* of the array bound is a unitsum,
what is the type of the store containing that value?

In particular if I have a match:

	match somearray_of_float with
	| (case 1 of NAT) data => ... // 0 elements
	| (case 2 of NAT) data => ... // 1 elements
	| (case ?n of NAT) data =>    // n-1 elements

what is NAT? At present my type system only has terms like:

	type t = [
	| `tuple of t list
	| `sum of t list
	| `unitsum of int
	...

so they're all just constants. How do I modify the type system
to allow for a variable? Do I have to actually put executable
terms into the type terms? That would account for construction,
what about destructors (pattern matches)?

Clearly the match has to get out a run time representation
of the length .. but it isn't an integer: I mean, the encoding
at run time is certainly an integer .. but what is the 
type ascribed to this value? I called it NAT above ..
what, categorically, is NAT?

BTW: I think all this analysis could apply to Ocaml too.


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

Re: [Caml-list] Coinductive semantics

[Kenn Knowles]

On Sun, Jan 22, 2006 at 01:23:49PM +0100, Andrej Bauer wrote:
> There may be special cases where compiler can determine whether the
> index is ok. 
> [...]
> I am sure
> people have looked into this sort of thing. Good luck!

Yes.  One might be interested in Dependent ML, or the references at the bottom
of the page.

http://www.cs.bu.edu/~hwxi/DML/DML.html

- Kenn

Re: [Caml-list] Coinductive semantics

[Andrej Bauer]

Kenn Knowles wrote:
> Yes.  One might be interested in Dependent ML, or the references at the bottom
> of the page.
> 
> http://www.cs.bu.edu/~hwxi/DML/DML.html

Oh my, I forgot about Hongwei's work (we were both grad students at CMU
for a while). His Ph.D. thesis (available at above url) is highly
relevant to what skaller is asking. It answers all questions better than
I can.

Andrej