🚀 go-pugleaf

In <1992Jul21.130843.16294@sci.kun.nl> daniel@cs.kun.nl (Daniel Tuijnman)
writes, as a follow-up to my posting,

that CIP is a `wide-spectrum' programming language, capable of
expressing abstract, non-executable specifications, as well as concrete
programs (both imperative and functional).

>Within functional programming, both methods do have the same power. We
>challenge you to present us a BMF law which cannot be expressed as a CIP
>transformation rule.

I suppose you can encode BMF in CIP, but that was not my point, and
hence you thought that I was ``not serious''. I stated that, in my
opinion, BMF is much conciser, and simpler to learn, than CIP. On the
other hand, there is not yet a system for automatic reasoning in BMF.
There is such a system for CIP, although I recall the demonstration of
it at CWI, where attempts to transform the program `1+1' to the more
efficient program `2' ended in a core dump, after some 15 minutes of
trying the thing to work.
Making things concise and simple is the _aim_ of BMF. For instance,
using category theory has reduced the number of different laws
dramatically. Being able to do everything is the aim of CIP. But that
has lead to an enormous system, which is hard to master.

>>>[In CIP] One first specifies an algebraic data type -- 
>>>without the BMF constraint of polynomial types -- and then has several 
>>>layers of expression constructs for making programs over these data types. 
>>
>>If you can give an example of a datatype which uses non-polynomial
>>constructors, I would be very interested! All datatypes occurring in
>>current programming languages, however, are polynomial.
>
>You're right about the latter.

In fact I wasn't, as Jeremy Gibbons (jeremy@cs.aukuni.ac.nz) pointed out
to me in a mail. For instance, the type of finitely branching trees is not.
It is the least fixed point of the functor

   \lambda X . A + (X*)

where X* means lists of X. There is a list functor (*) in there, which
is not polynomial. This can be circumvented, however, by viewing this as
a many-sorted algebra, and defining lists and finitely branching trees
together.
Another example of a non-polynomial type is the type of functions from A
to B, A -> B. 
The restriction made in BMF is that some nice properties do not hold for
such types, which do hold for polynomially-generated types. But you're
not going to change that in CIP, I think. (That would be truly
amazing!)

>But for instance bags (multisets) or (finite)
>sets are not expressible as a polynomial datatype, since additionally
>laws are needed to express commutativity and idempotency...  but this
>has not been a topic of research within BMF.
>[Maarten Fokkinga's work] ... But then, to actually
>implement these datatypes with laws in an everyday programming language,
>you still need some kind of representation theorem in order to obtain an
>isomorphism between the datatype with laws and a (subset of a) purely
>polynomial datatype.

\begin{plug}
Read my latest technical report, ``Congruences and Quotients in
Categories of Algebras'' for this. It gives a simple way to model
equations in BMF, and gives the connections with ``everyday programming
languages''.
\end{plug}
Can you point out (preferably in mail) what representation theorem you
mean? I'm not quite sure about this, so maybe it's still in my paper as
well.