I’ve already written a fair amount on these topics, and I don’t propose to blog that as I go. If you’d like some background, you might want to look at the following notes of mine:
- Calculating Functional Programs
- Origami Programming
- Design Patterns as Higher-Order Datatype-Generic Programs
Of course, many others have also written on these topics too. Some articles that have particularly inspired me are:
- Richard Bird’s Marktoberdorf notes An Introduction to the Theory of Lists and Lectures on Constructive Functional Programming (which I’m in the process of making electronically available)
- Roland Backhouse’s Exploration of the Bird-Meertens Formalism
- Grant Malcolm’s PhD thesis Algebraic Datatypes and Program Transformation (sadly not online, as far as I know; but his SCP paper is a good approximation)
- Maarten Fokkinga’s and Erik Meijer’s Program Calculation Properties of Continuous Algebras, and (with Ross Paterson) the bananas paper Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire
- Phil Wadler’s papers Theorems for Free! and Monads for Functional Programming
- Richard Bird and Oege de Moor’s book Algebra of Programming
- The AFP notes on Generic Programming, by Roland Backhouse, Patrik Jansson, Johan Jeuring, and Lambert Meertens
- Roland Backhouse and Paul Hoogendijk’s notes on Generic Properties of Datatypes
- Ralf Hinze and Johan Jeuring’s notes on the Practice and Theory and the Applications of Generic Haskell
(I’m sure there are many others too, which I’ve forgotten to mention.)
Jeremy, I’m very interested in the topic, and your blog it’s a really good and clear source of information. Currently i’m reading “Calculating functional programs”, from the link at the top. I’m stuck with some properties which I cannot understand. The docs says “See Exercise 1.7.5 for the proofs” (for example). I found the exercise, but not the answer, so I want to ask you if the doc is from a book or if can I get the complete text in another way.
Thanks
I’m afraid that what I meant by that comment was that Ex 1.7.5 requires you to complete the proof – it doesn’t give the proof. Sorry! Where are you stuck?
Oh, I see, sorry for the misundestanding. When I wrote my problem explanation, I figured it out. Thanks for your help!. I’ll try to finish this lectures as fast I can, so I’ll able to follow your posts in time.
Thanks again,
Hugo.