Teach theory then Haskell as example
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
So where do I as a practicing programmer and researcher go to learn all this stuff? My background is theoretical physics (PhD, 1993) so I'm no stranger to math. I've been using Haskell off and on since Haskell 1.4, and while I see lots of theoretical discussions on this list, I have yet to find a Haskell text that gives me a clue where to look. I have the impression that I would have to take three or four graduate courses just to pick up the bits and pieces here and there that I (apparently) need for Haskell. Suggestions? -Rod On Wed, 2009-01-14 at 04:37 +0100, Andrzej Jaworski wrote:
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
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Rodney Price wrote:
So where do I as a practicing programmer and researcher go to learn all this stuff? My background is theoretical physics (PhD, 1993) so I'm no stranger to math. I've been using Haskell off and on since Haskell 1.4, and while I see lots of theoretical discussions on this list, I have yet to find a Haskell text that gives me a clue where to look. I have the impression that I would have to take three or four graduate courses just to pick up the bits and pieces here and there that I (apparently) need for Haskell. Suggestions?
-Rod
The Haskellwiki is a pretty good resource aggregator http://www.haskell.org/haskellwiki/Category_theory In the long term, the aim of the Haskell Wikibook is to become a gentle introduction to "this stuff. It's nowhere near finished yet, but there's already some preliminary material http://en.wikibooks.org/wiki/Haskell/Category_theory Regards, H. Apfelmus
On Jan 16, 2009, at 2:00 AM, Apfelmus, Heinrich wrote:
Rodney Price wrote:
So where do I as a practicing programmer and researcher go to learn all this stuff?
...
In the long term, the aim of the Haskell Wikibook is to become a gentle introduction to "this stuff. It's nowhere near finished yet, but there's already some preliminary material
As a mathematician, Haskell has renewed my interest in category theory. I had thought one learns category theory most easily at age 20, because it paints such an eviscerated view of flesh-and-blood subjects like geometry, but at age 20 one doesn't care. Now, it is clear to me that functional programming is THE application of category theory. They're both about combining functions. If one wants to become fluent at combining functions, one needs an operational understanding of category theory, whether or not one likes the formal language. I'm struck, reading various papers that translate functional programming constructs back to category theory, how messy something simple in Haskell has to look in classical category theory, because Haskell is "higher order" and classical category theory is not. What some people might like is a no-holds-barred intro to category theory that updates it to fit Haskell, with a higher order presentation reworking the theory to match current functional programming practice. I'm the wrong person to try to write this, but I may, to teach myself. Among the intro texts out there, \bib{MR1120026}{book}{ author={Pierce, Benjamin C.}, title={Basic category theory for computer scientists}, series={Foundations of Computing Series}, publisher={MIT Press}, place={Cambridge, MA}, date={1991}, pages={xiv+100}, isbn={0-262-66071-7}, review={\MR{1120026 (93c:18002)}}, } is excellent, with a functional programming focus.
On Fri, Jan 16, 2009 at 7:46 AM, Dave Bayer <bayer@cpw.math.columbia.edu> wrote:
As a mathematician, Haskell has renewed my interest in category theory. I had thought one learns category theory most easily at age 20, because it paints such an eviscerated view of flesh-and-blood subjects like geometry, but at age 20 one doesn't care.
Yep, 20 year olds like me like to see the guts ripped out of geometry (actually, my dislike of geometry probably peaked around 17, but nevertheless I like what I've seen of category theory). Hopefully I'll still like category theory when I'm 21 and I'm taking a course in it :)
I'm struck, reading various papers that translate functional programming constructs back to category theory, how messy something simple in Haskell has to look in classical category theory, because Haskell is "higher order" and classical category theory is not.
I believe this is what higher-dimensional category theory is about, and my understanding is that even going a few dimensions up makes things significantly more difficult (and things that are "obviously" equivalent become hard to prove so). Haskell of course has no bounds on the dimension (you can use millionth-order functions if you like, though I don't know if you'll have success on a real-world compiler).
Among the intro texts out there,
\bib{MR1120026}{book}{ author={Pierce, Benjamin C.}, title={Basic category theory for computer scientists}, series={Foundations of Computing Series}, publisher={MIT Press}, place={Cambridge, MA}, date={1991}, pages={xiv+100}, isbn={0-262-66071-7}, review={\MR{1120026 (93c:18002)}}, }
is excellent, with a functional programming focus.
Good to have a recommendation -- my future CT lecturer has a hard time recommending anything not written by Mac Lane. --Max
G'day all. Quoting Max Rabkin <max.rabkin@gmail.com>:
Good to have a recommendation -- my future CT lecturer has a hard time recommending anything not written by Mac Lane.
One more suggestion: "Conceptual Mathematics" by Lawvere and Schanuel is the gentlest introduction that you're going to find. Cheers, Andrew Bromage
On Wed, 14 Jan 2009 04:37:33 +0100, "Andrzej Jaworski" <himself@poczta.nom.pl> wrote:
[...]
Programmers learning Haskell should forget that they are programmers and try to think mathematically.
Along that line, then, for example, where would you place, say, _The Haskell Road to Logic, Maths and Programming_ (see http://homepages.cwi.nl/~jve/HR/)? That book does not seem to focus on category theory, though; would you recommend an alternative book on that subject? If so, then which of the following would you recommend (these are just a few that I know of): Category Theory Books: Conceptual Mathematics: A First Introduction to Categories (Paperback) An elementary introduction http://www.amazon.com/Conceptual-Mathematics-First-Introduction-Categories/d... An introduction to category theory in four easy movements A somewhat informal, reportedly in-depth introduction to category theory, which some students have described as being intricately layered http://www.cs.man.ac.uk/~hsimmons/BOOKS/CatTheory.pdf Category Theory by Magic A somewhat more advanced text than _An introduction to category theory in four easy movements_ http://www.cs.man.ac.uk/~hsimmons/MAGIC-CATS/CourseNotes.pdf Toposes, Triples and Theories An often-referenced introduction to category theory, reportedly discussing monads as "triples" http://www.cwru.edu/artsci/math/wells/pub/ttt.html Categories and Computer Science Reportedly a straightforward introduction to category theory, with many examples from computer science http://www.cambridge.org/us/catalogue/catalogue.asp?isbn=0521419972 Arrow, Structures and Functors - The Categorical Imperative According to the HaskellWiki page on category theory (see http://haskell.org/haskellwiki/Category_theory), an out-of-print book covering monads and the Yoneda lemma, with very little prerequisite knowledge Category Theory Lecture Notes: Category Theory Lecture Notes for ESSLLI Distilled version of _Toposes, Triples and Theories,_ discussing category theory from a computer science perspective http://www.math.upatras.gr/~cdrossos/Docs/B-W-LectureNotes.pdf A Gentle Introduction to Category Theory - the calculational approach Another set of lecture notes referenced on the HaskellWiki page on category theory http://wwwhome.cs.utwente.nl/~fokkinga/mmf92b.html One difficulty with the above titles is that they do not provide Haskell-specific programming examples to help to illustrate the concepts. To address this problem, would you recommend books on categorical programming with examples in Haskell? Categorical Programming with Examples in Haskell: Categorical Programming with Inductive and Coinductive Types A thesis on categorical programming, exploring inductive and coinductive types, and several programming constructs related to them in Haskell http://www.cs.ut.ee/~varmo/papers/thesis.pdf (Actually, I just discovered the last title on the above HaskellWiki page on category theory.) If you have any other specific titles to recommend in category theory, for students of various levels of mathematical proficiency and computer science background, I would be very interested. I would believe that having specific Haskell code to help interact with the categorical examples would help to motivate study of the abstract theory for many programmers. One problem that many people have with studying abstract theory in isolation is that they often tend to lose motivation unless they can see how the theory directly relates to and influences the semantics and data structures in the code. Having specific examples of Haskell code to tie together immediately with the abstract theory would most likely help to motivate and maintain interest. -- Benjamin L. Russell -- Benjamin L. Russell / DekuDekuplex at Yahoo dot com http://dekudekuplex.wordpress.com/ Translator/Interpreter / Mobile: +011 81 80-3603-6725 "Furuike ya, kawazu tobikomu mizu no oto." -- Matsuo Basho^
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
participants (7)
-
ajb@spamcop.net -
Andrzej Jaworski -
Apfelmus, Heinrich -
Benjamin L.Russell -
Dave Bayer -
Max Rabkin -
Rodney Price