gmane.comp.lang.haskell.general

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

(Continue reading)

headers

Rodney Price | 14 Jan 07:10

Re: Teach theory then Haskell as example

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

(Continue reading)

headers

Apfelmus, Heinrich | 16 Jan 11:00

Re: Teach theory then Haskell as example

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

headers

Dave Bayer | 16 Jan 16:46

Re: Re: Teach theory then Haskell as example

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
>
>  http://en.wikibooks.org/wiki/Haskell/Category_theory

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

(Continue reading)

headers

Max Rabkin | 16 Jan 19:15

Re: Re: Teach theory then Haskell as example

On Fri, Jan 16, 2009 at 7:46 AM, Dave Bayer <bayer <at> 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},

(Continue reading)

headers

ajb | 18 Jan 02:33

Re: Re: Teach theory then Haskell as example

G'day all.

Quoting Max Rabkin <max.rabkin <at> 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

headers

Benjamin L. Russell | 14 Jan 12:05

Re: Teach theory then Haskell as example

On Wed, 14 Jan 2009 04:37:33 +0100, "Andrzej Jaworski"
<himself <at> 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/dp/0521478170

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

(Continue reading)

headers

Andrzej Jaworski | 15 Jan 05:12

Re: Re: Teach theory then Haskell as example

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

(Continue reading)