## Old computer science and technical books worth searching for

There have been several threads recently about buying old computer science books, so I thought I'd make it into its own topic. What obscure books are out there that are worth searching for?

One that I've found interesting is "Lucid: The Dataflow Programming Language." There's also a followp, "Multidimensional Programming" (which haven't seen).

Occam books are also eye-opening.

And I have a copy of "Programming in Parlog" (a parallel Prolog variant) which I have yet to read.

## Comment viewing options

### The one I don't have

Been eyeing a PL book at the used bookstore. Any recommendations of whether The GÃ¶del Programming Language is worth the effort?

### Some favourites

• The Architecture of Concurrent Programs, Per Brinch Hansen. He presents Concurrent Pascal (based on Monitors in a way completely unlike Java) and several very simple real operating systems written in it. Very Wirth style: simplicity of implementation is everything. I picked this up on a recommendation by Ralph Johnson on Wiki.
• ACM Turing Award Lectures: The First Twenty Years (in print). Many great ones are online too (e.g. Knuth, Floyd, Backus, Karp).
• Selected Papers on Computer Science, Donald Knuth. Many of these articles are quite informal and show Knuth's hacker-side.
I've been on the lookout for Project Oberon by Niklaus Wirth and The Implementation of Functional Programming Languages by Simon Peyton Jones for years. They're books that I've borrowed in the past and want to get back to.

News Flash! :-) Right now I'm beside myself because I just discovered the archive of Stanford CS technical reports going back to the 1960s! I knew about MIT's AI-lab archive, Dijkstra's "EWD"s, and CMU's AI repository but not about this. Are there more free archives from the "golden era" around too?

### Recursive Programming Techniques by W. H. Burge

RPT by Burge is very good. I rediscovered it recently and was surprised to see how many of the modern FP techniques are in this book from 1975.

I think the stuff on generating functions corresponding to various data structures will still yield good ideas, if I ever get around to understanding it (if it is obvious to you that the generating function for recursively specified non-null lists is x/(1-x), I suppose you might be disappointed). Perhaps there is some connection with the way Conor McBride and company take derivatives of types ...

Anyway, it is a good book, but downright fascinating in the context of its time.

Its ISBN is 0-201-14450-6, by the way.

Oh, and also I would re-iterate what Luke Gorrie said about Knuth's Selected Papers.

### I think the stuff on generati

I think the stuff on generating functions corresponding to various data structures will still yield good ideas, if I ever get around to understanding it (if it is obvious to you that the generating function for recursively specified non-null lists is x/(1-x), I suppose you might be disappointed). Perhaps there is some connection with the way Conor McBride and company take derivatives of types ...

There is a connection, though I am fuzzy on it. The recent work by McBride et al. on container types makes use of functors which are close to André Joyal's analytic functors, and the latter somehow generalize generating functions from the theory of species to the setting of categories.

This is an area which is growing in importance, and promises to make working with types only a little harder than doing arithmetic on numbers. See, for example,

M.P. Fiore.Â  Isomorphisms of generic recursive polynomial types. Â  In 31st Symposium on Principles of Programming Languages (POPL 2004), pages 77-88.Â  ACM Press, 2004.
(Yes, isos are everywhere!)

### OK, then ...

I see that you are familiar with this notion of generating function. My next question: do you (a) know it from the Burge book or did you (b) see it elsewhere ... or is it (c) just *that* obvious to someone with the right background? Casing on your choice for answer (and assuming no match error): (a) do you agree that Burge was pretty well ahead of his time? (I rarely see this book cited, oddly enough.) (b) can you tell me where else you saw material on gen. funs.? (i.e., besides perhaps connections in Joyal and Fiore, which I will pursue) (c) uh, gee, I guess you *are* the bright boy then :) .

### (b)

It is certainly not obvious. But if you remember from high school that the sum of:
x + x^2 + x^3 + ...
is x/(1-x) (for |x| < 1), and you read this series as a type expression, it is not impossible to guess—though what the |x| < 1 condition should mean for types leaves me baffled.

Alas, I am not bright enough to connect such disparate topics on my own, and I know about generating functions and datatypes because have seen them mentioned before in the same context. The first place I saw generating functions mentioned was probably Baez and Dolan's HDA3, and I subsequently leafed through Combinatorial Species and Tree-like Structures by Bergeron et al. Since then I have seen mention of it here and there in the categorical CS literature. Sadly, Joyal's article on analytic functors is entirely in French, so I was a bit stymied there.

BTW, I found this book online, which looks pretty neat and accessible, though, not surprisingly, it doesn't seem to mention datatypes:

generatingfunctionology by Herbert S. Wilf
Cute name, eh?

### neat!

This paper:

∂ for data by Abbott, Altenkirch, Ghani, and McBride

has a nice explanation of the intuition of differentiating data types. It uses constructive set theory instead of category theory, which makes it a little more accessible than some of their other papers, for me anyway. Although I started getting confused when it talked about shapes and positions. (Maybe I need to read some of Jay's papers.)

Their idea uses Huet's zipper structures (unfortunately only available in JFP). A zipper is a data structure representing a context with a single hole. (Huet's paper shows some nice applications of zippers to data structure traversals.)

From the introduction on page 2: if we represent a binary tree with a hole in it like so:

data Tree' = Left Tree | Right Tree
data Zipper = [Tree']

where Tree' represents (a) which direction you have to go at each step in the traversal of the tree to find the hole and (b) the rest of the tree not on the path of the traversal, then we can fill the hole with:

plug :: Zipper -> Tree -> Tree
plug [] t = t
plug ((Left rrest) : z) t = Node (plug z t) rrest
plut ((Right lrest) : z) t = Node lrest (plug z t)

So here's the cool part: in general an n-ary tree will have some type T = μX.F X, where for binary trees F X = 1 + X2, for ternary trees F X = 1 + X3, and so on. The type of the zipper structure is then Z = List(F' T), where for binary trees F' X = 2 × X, for ternary trees F' X = 3 × X, and so on.

Apparently they derive the rules from calculus for differentiating general polynomials, as well as the chain rule, and then a couple other rules for initial algebras and final coalgebras. They claim the connection is not just coincidental, but my calculus is rusty, and my type theory near nonexistent. So I'm still trying to slog through it. :)

### Wild guess

fruehr:if it is obvious to you that the generating function for recursively specified non-null lists is x/(1-x)

and

Frank:if you remember from high school that the sum of:
x + x^2 + x^3 + ...is x/(1-x) (for |x| < 1)

Uh, I think x + x^2 + x^3 + ... looks more like formula for non-unit tuples, ain't it? Ah, probably the type of these tuples is isomorphic to the type of non-null lists...

Frank:though what the |x| < 1 condition should mean for types leaves me baffled
Indeed, may interpretation would be:
assuming lists are defined by x = c + d * x, with natural (and > 0) c and d, |x| < 1 means that c < d-1.
Which I interpret as... eh... What do these c and d mean, by the way? A number of different constructors of each degree?
Well, naive algebra is not working, I have to read that paper...

### A bit of calculus

Is The Derivative of a Regular Type is its Type of One-Hole Contexts relevant? Was it ever mentioned on LtU?

As I wrote down the rules corresponding to the empty type, the unit type, sums and products, I was astonished to find that Leibniz had beaten me to them by several centuries: they were exactly the rules of differentiation I had learned as a child.

### Generating Functions From Outer Space

The |x| < 1 condition is a red herring in this case. It is quite standard to work with generating functions in the context of the ring of formal power series k[[x]] with coefficients in a field k. (You can generalize the heck out of this definition.) A formal power series is a polynomial except for the fact that we don't require the elements of its coefficient sequence to become zero after a certain point. We define addition in this ring in the obvious way and multiplication by convolution of the coefficient sequences, just like you would in a polynomial ring.

In the present context, it makes sense to view a formal power series such as 1 + x + x^2 + ... as a polymorphic type, parameterized by its element type, x. You interpret 1 as the empty type, + as union and multiplication as Cartesian multiplication. Thus the above power series reads 'This type is empty, or equal to x, or equal to a pair of x's, or ...' I'm pretty sure Frank, etc understand this, so this is merely clarification for those of you who might still be a bit confused.

(First post, by the way.)

### Another "arithmetic & types" idea (but remember Burge!)

Well, thanks to Frank and everyone else for the references; I will mention two more which exploit the (really stronger than) "analogy" between arithmetic and type-theoretic sum, product and exponentiation, namely Ralf Hinze's work on generalized tries (Generalizing generalized tries and Memo functions, polytypically!): here the laws of exponentials are used to derive structures for memoization. (To be fair, Ralf cites a paper by Connelly and Morris on this, and they apparently credit Wadsworth, though it seems Ralf has pushed the idea furthest.)

OK, I hereby offer a free Haskell t-shirt to the first person to come up with a useful type-theoretic interpretation of the long division algorithm :) .

Anyway ... I would still recommend the Burge text to everyone searching for "Old computer science and technical books worth searching for". Hmm, in fact, it seems that Burge uses the same kinds of techniques as McBride and co. (derivatives of types, roughly, though he doesn't call it that) to derive programs for generating permutations, combinations and partitions (see section 3.11, "Combinatorial configurations"). And there is a lot of other material, too: combinators, closures, the SECD machine, efficient compilation of lambda terms, graph representations, coroutines and streams, parsing techniques, polyphase and cascade merge sorting, etc. All expressed in what amounts to a sort of pre-Haskell/pre-Scheme hybrid.

Again, pretty good for a book written in 1975!

### Long division

OK, I hereby offer a free Haskell t-shirt to the first person to come up with a useful type-theoretic interpretation of the long division algorithm :) .

Heh, I might take you up on this! My work is closely related to this area, and I think it might not be long before I could give some reasonable interpretations of division.

To get an exact correspondence between types and algebras, one needs to restrict to algebras which, syntactically, are close to linear theories. In such a setting, the exponential actually behaves much like division, although it splits into two operators called residuals, which will be familiar to anyone who has seen the Lambek calculus. I think this is enough to `divide' monomials; if I can figure out how to handle arbitrary polynomials, then the expansion of a natural number (expressed in some base) as a power series suggests a framework for doing long division...

I will, of course, have to insist on a black shirt. :) Did you ever find a place that makes those?

Frank, I'm replying to you since you seem to have a good idea of the correspondence between generating functions and type definitions. We have (and correct me if I am wrong) the following correspondence:

1 empty type

+ disjoint union

* Cartesian product

The question arises of how to deal with coefficients. I cannot think of a natural way to interpret anything but (nonnegative) integer coefficients so let's go with that: Distributivity implies nx = (1 + ... + 1)x = x + ... + x, so we are FORCED to interpret nx as the disjoint union of n copies of x. But it is a well-known fact from the theory of ordinary generating functions that any formal power series (with integer coefficients) with a nonzero constant term has an inverse, e.g. (1 + 2x + 4x^2 + 8x^3 + ...)(1 - 2x) = 1. With the above correspondence in mind, this is clearly absurd since the Cartesian product of two countable, nonempty sets is nonempty; we don't even need the axiom of choice for this countable case. Cartesian products distribute over disjoint unions up to isomorphism (count the cardinalities to see this) so what's the problem? I haven't read any papers or books on generating functions in this context so I'm a bit confused.

### Non-correspondence

First of all, I actually know very little about generating functions, though they are on my list of things to look into. (In particular, I didn't know that theorem about inverses you mention.)

The long answer is that the "correspondence" between arithmetic (say, for rings) and types is not well developed yet, so using it naively is likely to yield contradictions like the one you demonstrate.

Let me point out a few places where your reasoning seems specious.

First, as I said, the correspondence holds best for non-commutative linear theories, where one should read the equality symbol as "canonically isomorphic". (By "best", I mean that this restriction on theories appears to be sufficient, but not necessary to establish a correspondence.) So if your argument depends on up-to-iso properties such as commutativity of product or distributivity of products over sums (note that it involves duplication of a variable), it is likely to yield nonsense.

Second, your example of an inverse (1 - 2x) involves subtraction, and I don't know an interpretation for that; set minus is too strict because ti depends on set equality. The coexponential behaves a bit like subtraction, but any category with both exponentials and coexponentials is trivial (collapses to a poset)—in particular, the category Set has exponentials, so it can't have coexponentials. (Of course, one expects even more strongly than subtraction that coexponentials should interpret logarithms, so they are probably not the right choice here anyway.)

Third, I don't know even if every ring can be assigned a type-theoretical meaning, but if so, I doubt it will be as an object of Set, and probably not even as one in a topos, at least if you interpret "equality" as "canonically iso". I think what is actually required is some kind of asymmetric *-autonomous category because this has the right linearity properties.

(Given these considerations, it is probably not a good thing for authors to use the term "polynomial functor". This class of functors is often used to describe the ones which generate ML-like datatypes, but in fact the correspondence with polynomials is pretty weak.)

### Non-correspondence, part deux

"First of all, I actually know very little about generating functions, though they are on my list of things to look into. (In particular, I didn't know that theorem about inverses you mention.)"

The book by Wilf you mentioned is a good starting point. In particular, I am confident it mentions the theorem I mentioned. In fact it's pretty easy to see why it's true; let me try to work it out here.

Theorem. Let k[[x]] be the ring of formal power series with coefficients in a field k. Let f be an element of k[[x]]. Then f is invertible if and only if f has a nonzero constant term.

Proof. Necessity is obvious since if f has a zero constant term then fg will have a zero constant term for any g in k[[x]]. Conversely, suppose that f has a nonzero constant term. Write f = a_0 + a_1 x + ... a_n x^n + ... where a_i is in k. We seek a formal power series g in k[[x]] such that fg = 1. If we write g = b_0 + b_1 x + ... + b_n x^n + ... then we have fg = (a_0 b_0) + (a_0 b_1 + a_1 b_0) x + (a_0 b_2 + a_2 b_0 + a_1 b_1) x^2 + .... We want a_0 b_0 = 1, a_0 b_1 + a_1 b_0 = 0, a_0 b_2 + a_2 b_0 + a_1 b_1 = 0, ... and since a_0 is nonzero we may take b_0 = 1/a_0 (since k is a field). The nth equation is to be solved for b_n and since the coefficient of b_n in this equation is a_0 (which is nonzero) and the earlier coefficients are already determined (by induction on n), we can indeed solve for b (since k is a field).

I just realized that I misquoted this theorem earlier since I said it works when you take coefficients in any ring. In fact it only works for a formal power series whose constant coefficient is a unit in the coefficient ring. (This is the natural generalization of the above theorem.)

"The long answer is that the "correspondence" between arithmetic (say, for rings) and types is not well developed yet, so using it naively is likely to yield contradictions like the one you demonstrate."

I agree; I was intentionally being rather cavalier in my manipulations to see where the correspondence would "naively" lead us.

"First, as I said, the correspondence holds best for non-commutative linear theories, where one should read the equality symbol as "canonically isomorphic". (By "best", I mean that this restriction on theories appears to be sufficient, but not necessary to establish a correspondence.) So if your argument depends on up-to-iso properties such as commutativity of product or distributivity of products over sums (note that it involves duplication of a variable), it is likely to yield nonsense."

That makes sense to me; thanks for pointing that out.

"Second, your example of an inverse (1 - 2x) involves subtraction, and I don't know an interpretation for that; set minus is too strict because ti depends on set equality."

Indeed, this is a huge problem. However, we are quickly imposing requirements that rapidly diminish the number of useful theorems in the theory of generating functions that could be used to investigate type theory. At best we'd like a partial correspondence between analytic and formal power series since this allows us to use e.g. complex analysis to tackle combinatorial (or in our case, type theory) problems. However, we obviously cannot have that in the present context. Barring that, we'd at least like a coefficient ring (or commutative rig -- see work by Baez) with "enough" units. We don't have that here either; the empty type is quite obviously the only unit with respect to the Cartesian product.

All this really makes me question the usefulness of this approach. I'd love to be proven wrong, however, since I absolutely love generating functions.

### Old and new computer science

BTW, when I read the words "old computer science" I cannot help but recall Donald Rumsfeld's remarks about "old" and "new" Europe.

old Europe : old CS : FP :: new Europe : new CS : OOP?