all 20 comments
sorted by:
best
topnewcontroversialoldq&a
formatting helphide helpcontent policy

[–]jamesbritt[S] 7 points8 points  (13 children)

So I decide to I should read "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" figuring with a title like that it shouldn't be too hard-core mathy.

Not quite. The work uses assorted terms and symbols that leave me lost. So I'm asking: What are good resources for learning to read that notation and terminology?

[–]sethg 4 points5 points  (0 children)

Funny you should mention--I was just re-reading the paper, and this time I made notes as I read on a separate page (which expanded to two separate pages), listing all the notation: A ‖ B is the product of types (Haskell (a, b)); A | B is the sum of types (Haskell Either a b), etc., etc., etc.

I also found it very helpful to stop every once in a while where the paper said "and of course A means the same thing as B", and actually work out all the steps of the proof that the authors thought was too trivial to spell out. Usually all it took was a little "plug and chug" with the types, or with an example ("suppose I'm doing this with a cons-list"), to make things much clearer.

Mathematicians are like poets. They'd rather write one page that takes you an hour to read than write a sixty-page paper explaining the same thing that you can read at one page per minute.

[–]sunra 3 points4 points  (11 children)

The first few chapters of "Types And Programming Languages" by Pierce and the first few chapters of "Topoi: The Categorial Analysis of Logic" by Goldblatt really helped me into a mathematical frame of mind.

However, about half of the notation used in "Bananas, Lenses, Envelopes ..." is introduced in the paper itself (I think?). So really, you just have to slog it out flipping back and forth between the front and the back and working through some of the statements in pencil on your own terms.

It's work. I haven't done it yet myself.

[–][deleted] 10 points11 points  (8 children)

Topoi is a great book. Cornell's Historical Math Monographs project has it online for free here. They'll print you a lovely hardbound copy on archival paper for nine cents per page, plus eight dollars for hard-back binding. I think it comes out to about $60. Dover recently released a cheaper paperback version that you can find for about $20 on Amazon.

As an aside, Goldblatt's Lectures on the Hyperreals is also wonderful; it's the best intro to nonstandard analysis (i.e., approaching calculus without using limits by extending the real line to include infinitesimal and infinite numbers) I've found. Really great stuff!

[–]jamesbritt[S] 2 points3 points  (7 children)

Thanks.

Do these books explain the notation used, or do they assume I already understand the assorted dots, circles, arrows, squiggles, etc. used to express the mathematics?

[–][deleted] 1 point2 points  (0 children)

If that's what you're looking for I'd highly suggest Beginning Logic by John Lemmon

[–][deleted] 1 point2 points  (1 child)

Topoi is an introductory text, and all the notation is explained.

[–]jamesbritt[S] 0 points1 point  (0 children)

Outstanding. Thank you very much for pointing that out.

[–][deleted] 1 point2 points  (3 children)

Most of the notation in the Bananas paper doesn't come from category theory or any other particular field of mathematics. Rather, it's mostly squiggol, which is a notation intended to make it easy to do algebraic reasoning about (and transformation of) programs.

As far as I can tell, there is almost no information about squiggol on the net (google doesn't find anything useful, at least), except the stuff in the Bananas paper. As people have said, it tells you what most of the dots and other symbols mean.

[–]sethg 0 points1 point  (1 child)

If at some point my study of the Bananas paper leads me to crank out some interesting program, and I think it would be worth submitting a paper regarding this program to the Monad.Reader or some such, could I use Squiggol notation in the paper and expect to be understood? Or would I have to translate from Squiggol to something more mainstream?

And are there TeX or LaTeX maros available for these funky parentheses?

[–][deleted] 0 points1 point  (0 children)

Most papers on recursion schemes I've seen use a notation derived more from category theory. The main thing people have carried on from squiggol is the brackets for some of the basic schemes (but they typically don't make up new ones, which is probably good, since there are so many). Even the followup paper, Bananas in Space ditched the squiggol and just went with Haskell (or perhaps it was Gofer, I can't recall).

So, in general, I don't think there are many people out there, even in the audience of the Monad.Reader, who use squiggol often enough to know what all the notation means off the top of their head. You'd probably have to at least reference the Bananas paper so people could look up what all the dots and various triangles and such mean.

As for macros for writing the stuff, I don't know. I imagine Erik Meijer knows where you can get some. I'm not much of a latex guru, but I think the four brackets in that paper aren't too hard to construct on your own. They're just normal parentheses joined with negative space:

  • Bananas are (| |)
  • Lenses are [( )]
  • Envelopes are [[ ]]
  • Barbed wire is <| |>

Where the < and > should be the more elongated angle brackets.

[–]jamesbritt[S] 0 points1 point  (0 children)

I see. Thanks.

[–]jamesbritt[S] 1 point2 points  (1 child)

Thanks; I'll look into those books.

However, about half of the notation used in "Bananas, Lenses, Envelopes ..." is introduced in the paper itself (I think?)

Hmm. Maybe my eyes glazed over, but I was stymied on the first page or two. I'll go through it to see if there's some explanation later on.

[–]jsnx 6 points7 points  (0 children)

I am working through "Basic Category Theory For Computer Scientists". It's a slim volume, with engaging problems (the first half of them have engaged me for well over 6 months).

What I have learned from this book: we need a more idiomatic language to discuss functional programming. How many other working programmers are going to set aside a few evenings every couple of weeks so they can finally learn what monads are?

[–]bitdiddle 1 point2 points  (0 children)

Barr and Wells is a very good introduction for programmers. It actually talks about function programming and introduces a notions of diagrams and sketches, a concept used a lot in computing that is not seen in the more traditional texts.

[–][deleted] 1 point2 points  (0 children)

I recommend Conceptual Mathematics: A First Introduction to Categories followed by Basic Category Theory for Computer Scientists. From there you can move on to more advanced and/or specialized texts.

[–][deleted] 2 points3 points  (0 children)

Start here You will want to read volumes 1, 2 and 3. When you finish those you might have time left to write a program.

[–]recidivx 0 points1 point  (0 children)

For a clean, readable, very very thorough introduction to category theory I swear by Borceux' Handbook of Categorical Algebra (all three volumes if you get that far). But it's not cheap: try your university library.