kirancodes.me
To Proof Maintenance & Beyond!

Thinking Functionally with Haskell by Richard Bird, Cambridge University Press, 2014

Torsten Grust

Abstract

With Thinking Functionally in Haskell Richard Bird steps up to continue a family of textbook classics.Bird and Wadler jointly started the series with two editions of Introduction to Functional Programming (in Haskell) in 1988 and 1998, respectively.Let me begin with the outright spoiler that I think that this third edition breathes new life into the series and indeed presents a worthy continuation.The 12 chapters of the 340-page volume contain more material than most layouts of a one-term introductory course on functional programming can accommodate.If the many exercises are considered in depth and a discussion of Haskell-specifics is added (more on both points below), we hold the syllabus of a two-term course in our hands.According to the blurb, the book addresses first-or second-year undergraduates.I agree, but gained the impression that true programming novices would probably struggle starting with the fifth chapter when concepts, scripts, and exercises become more complex.This is also where the exposition generally picks up speed.From the outset, Bird consistently adopts a style of programming in which complex functions are composed from simpler constituents that are useful on their own (". . .functions that seem to be basic in programming are often composed of even simpler functions.A bit like protons and quarks.")Already the earliest exercises in Chapter 1 adhere to this principle: an elaborate pipeline of function types has to be designed even before students can be expected to write the functions' bodies.Early on lazy evaluation is established as a principle that makes this rigorous compositional style viable.Here, and at many occasions later in the book, Bird relates the discussion to the research literature or blog posts. 1 This provides welcome entry points for deep dives into the subject.When Chapter 4 introduces lists it carefully distinguishes finite, infinite, and partial values, a discussion that has its dedicated Chapter 9 but permeates the entire book.Chapter 5 is entirely devoted to a Sudoku solver that readers of Bird's Pearls of Functional Algorithm Design (Cambridge University Press, 2010) will recognize.The present book significantly expands on the earlier treatment through an in-depth discussion of the many involved component functions.The derivation of an efficient solver from the "clearest specification" also marks the first larger showcase of equational reasoning.Bird consequently uses the "Wim Feijen style" e 1 = {justification} e 2 to simplify and optimize programs or to establish proofs of their properties.The rewriting of compositions of functions remains one of Bird's grand themes.Calculations pervade the entire book, from its preface(!) to the final Chapter 12 where a (semi-)automatic equational rewriter is developed.Lawful program construction encourages "wholemeal programming", 1 Regarding a discussion of strict vs. lazy evaluation, Bird points to a blog post by Robert Harper and the extensive thread of comments that followed (http://existentialtype.wordpress.

Related papers