[Haskell-cafe] On finding the right exposition...
Olaf Klinke
olf at aatal-apotheke.de
Sat Sep 18 23:07:24 UTC 2021
Perhaps one thing that speaks in favour of Anthony Clayden's suggestion
to learn lambda calculus before/along Haskell is this:
Haskell shares the evaluation model with the lambda calculus. One of
Michael Turner's points of criticism was, as I understand it,
insufficient documentation about the inner workings of Haskell [1].
Haskell needs constructs like the ST monad because of the evaluation
model. Once the learner knows, perhaps by experimenting with it on
paper or on [2,3], that a lambda term can be reduced in several ways,
and confluence guarantees that all ways result in the same normal form,
then some things might be much clearer:
* Which freedoms the compiler can exercise in evaluating your program.
* Why one needs the State monad for ordering sequences of effects (the
programmable semicolon) [4].
* How the various tricks and pitfalls around lazy and strict functions
work, e.g. Viktor's new Foldable documentation.
I looked at the first chapter of my K&R. It presents small example C
programs and explains what they do. Taking small Haskell programs and
explaining how these lambda terms are reduced to normal form would be a
comparable (and desirable, in Michael's view) approach? The Haskell
language report does not say anything in this respect, as far as I can
see. Only translation of syntactic constructs to core Haskell is given.
Olaf
[1] Of course the documentation is out there somewhere, but not written
in a style which pleases learners like Michael.
[2] https://lambdacalc.io/
[3] https://capra.cs.cornell.edu/lambdalab/
[4] I tried to convince myself that the state monad indeed sequences
effects. In a pure lambda world I think this should mean that a certain
lambda term has only one way of being reduced. Is the following valid
reasoning?
type State s a = s -> (a,s)
When Church-encoding the tuple (a,s) one finds that
(m :: State s a) >>= (k :: a -> State s b)
= \s -> m s k
so the only applicable rule is beta-reducing m when applying to some s.
More information about the Haskell-Cafe
mailing list