[Haskell] Re: Teach theory then Haskell as example

[Andrzej Jaworski]

If such guys like you two have problem then Haskell is in a dire trouble!

To my knowledge the best theoretical writing on functional programming was done around Categorical
Machine and Caml. You need to speak Caml/ML to read Benjamin Pierce, Chris Okasaki or use Huet's
course/software (http://pauillac.inria.fr/~huet/CCT). Even "The Functional Approach to Programming
with Caml" feels for mathematician better than the analogous Haskell stuff.

Some of this however cannot be made easily accessible for us because Haskell's module system has been
joyfully messed up, which is partly responsible for the need to patch Haskell with a piece of logic
here and there (Tamplet Haskell and other extensions) and make Haskell tilt towards logic and away
from Categorical Machine. Thus the introduction to its theoretical foundations should follow from
higher order logic to Category Theory as its necessity (higher order logic has real sense only when
category theory foundations for mathematics are considered, mathematics based on axioms can be proven
by much simpler first order logic). There is as yet no such book but there are many very good
articles addressing specific issues of Haskell's theoretical foundations (e.g.
http://www.cs.ut.ee/~varmo/papers/thesis.pdf).  They however always assume more than they target to
explain making student turn around them like a dog not knowing which ball to catch first.

What we need is a meaningful introduction covering all Haskell's high level concepts, demonstrating
convincingly their usefulness and their interplay where it is possible. It is not enough to explain
concepts as a collection, whether simplified (http://www.cs.unibo.it/~asperti/PAPERS/book.pdf) or
written for mathematicians (equally dull formalism for someone lacking adequate "mathematical
maturity"; also mathematicians can afford to consider large collections while you need to see things
in action). Doets and Eijck show good approach but their mathematics is too trivial (e.g.
combinatorics should be presented via lattice theory like Rota taught). They also miss the boat
presenting Haskell (no higher gear at all).

The concepts might be introduced as problem solvers or as explaining each other like in Tatsuja
Hagino's "Categorical investigation of types" (http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf ).
Intuition should get strong priority over completeness. Building intuition is however closer to
athlete's training than to body building. A boxer or swimmer don't build one muscle independently
from another. One muscle must trigger action of another and be goal oriented. If a boxer treated his
body as a collection of muscles and worked on them independently he would not survive 10 seconds of
fight. Likewise concepts cannot be addressed in isolation from each other.

Any presentation might be good enough as long as it gives justice to the concepts, presents them all
in one place and gives clues how to reinforce their use. The introduction to the theory should also
set high aesthetic standard, easy to achieve due to pure mathematical components. This should equip
programmers prone to dirty tricks with a sort of gyroscope, so if he later chooses to puke he should
at least remember what the taste of beer was;-)

I am done but if somebody feels like adding something take it to Haskell-cafe please.
-Cheers