[Haskell] Teach theory then Haskell as example

[Andrzej Jaworski]

Hi,
Although it will not help you to know who your grandparent was it is always better to know what
reason is behind particular formalism that you use. And the better you know it the further you go
with it. So after seeing reappearing questions on the nature and role of fundamental concepts in
Haskell I came to a belief that Haskell should be taught via stressing abstract concepts and
explaining them rather than downplaying or postponing the explanation. It may look like asking to
further expand Haskell's learning curve but I will argue that half learned concepts haunt Haskellers
for ever. So, if you teach Haskell as a tool it will always remain a mystery and haunt. My argument
is that vice versa should be true: if you explain fundamental concepts in their own right the
programmer will gain insight and be able to navigate by power of his own judgment and not by
following alchemical recipes. What is more Haskell should be taught on most abstract terms in a
framework of higher order logic, types and CT right from the start. Not that it is so different but
because:
(0) it can afford it
(1) it is conductive to abstract thinking by giving more control in structuring the code
(2) it matters in what language you think and you cannot think in formalism (you need to root it in
models)
(3) abstract thinking is more effective (than thinking by example) and is the only way to produce
non-trivial solutions.

Just browsing book titles in mathematical literature like "The Concept of Number: From Quaternions to
Monads and Topological Fields","Monads
and automata", "Monads and graphs" should bring confidence that there is deep universe behind
Haskell's abstract stuff. So, why try to hide
this instead of making direct reference to that unique legacy? Explaining wide roots of Haskell
should motivate and disinfect narrow mindedness injected by regular CS courses. Programmers learning
Haskell should forget that they are programmers and try to think mathematically. First few years of
CS history belonged to mathematicians that for amusement created Fortran and Lisp. Then John McCarthy
tried to warn guys proclaiming themselves programmers that to build their skills they should study
logic rather than programming. Obviously they haven't listen;-)

If abstraction has deep natural roots sooner or later it will unleash its power. Just one funny
example:
Till 70s the language of category theory was ridiculed even buy guys who used it, like omnipresent
Serge Lange. One of the exercises in his
"Algebra" (1966) was: "take any book on Homological Algebra and prove all its theorems" (in
elementary way). The categories and functors
were then used only for the fashion introduced by Bourbaki with their terse and purist writing style.
But then surprise, surprise and true reason for homological algebra was discovered - sheaves - which
with schemes dramatically extended the horizon for Algebraic Geometry. The irony is that most
algebraic geometrists were brought up on Lange's "Algebra":-)

Believing that an abstract concept is good for us is not enough however. It must be brought to us
with some intuition, otherwise it will be
a cumbersome formalism allowing at most to understand someone else ideas dressed in such a language.
Intuition is however difficult to
upgrade and the strongest your intuition is the most difficult it is to modify it. Albert Einstein
was the greatest man of intuition of all
time and he had always had very vivid mental model of a theory before dressing it up in mathematics.
But it took him 15 years of agonizing
struggle to come to general relativity formulae. The same task took Henri Poincare less then a week.
Yes, and Poincare published it! But this
great guy gave full credit to Einstein on the merit of him originating the problem. There are couple
of lessons here:
(0) separating formalism from intuition can kill you even if you sit on a solution
(2) big things need more than one kind of intuition
(3) complex problems can be solved only by abstract concepts
(4) nothing is sufficiently abstract, it is an unending race. (it was Grassmann who referred Einstein
to tensors and Riemannian geometry but the irony is that General Relativity would look much better in
Grassmann algebra. Grassmann however was completely uninterested in
making use of his discovery, when he was done with algebra he turned to ... Linguistics where he
received his doctorate)
(5) abstract thinking is not and cannot be motivated bay practical issues. GR may look abstract but
for Poincare it was only another exercise
in tensor analysis. So, when he was done with it he was happy to return to abstract issues:-)  [that
might explain why there are more Haskell
theoreticians than real apps;-) ]

I dedicate this to those who theach these who will teach the rest:-)
-Andrzej