Programming languages I have known and loved
Robin Cockett
University of Calgary
Abstract:
It all started with Tatsuya Hagino's PhD thesis (1986) in which he
showed how category theory could be used directly as a programming
language. Computation in Tatsuya's system was delivered by rewriting
categorical combinators -- similarly to Curien's categorical abstract
machine (CAM). The downside was that you had to write programs in
categorical combinators which was downright impossible ...
Dwight Spencer and I showed how one could translate from a more useable
term logic into the categorical combinators. This became the
programming language Charity. The computational power of Charity was
delivered by the inductive and coinductive data declarations.
Furthermore, in order to enhance the expressive power we allowed
definitions of "combinators".
The resulting setting was not Cartesian closed: so, one had to program
in a purely first-order manner. This, it turned out, was a bit of a
problem because one could not write efficient programs! To overcome
this defect we increased the power of coinductive definitions to allow
"higher-order coinductive" data. In this way the computational power
of Charity was still delivered by data declarations but one could
declare the exponential type as a coinductive data type if you wanted
to write higher-order programs.
Charity development stopped in about 1996. It was a sequential
programming language and the world had meanwhile become very
concurrent! Thus, I was determined to produce a categorical
concurrent language. This led to the development of CaMPL which stands
for "Categorical Message Passing Language". In CaMPL one can write
write concurrent programs (and parallel programs) with typed
communication channels. For example, one can write airline booking
systems.
Notably, in (a strongly typed version of) CaMPL one cannot write
programs which have deadlocks or livelocks ... however, the language
seems to be quite expressive. I shall introduce you to the ideas of
CAMPL which are strongly influenced by Charity ... and what I had
learnt from its development.