I don't think it quite makes sense to say that Haskell shares the evaluation model with lambda calculus, because I don't think it's fair to say that lambda calculus has any specific evaluation model at all.  Do you mean substitution, for example?  But that's only one way to implement lambda calculus, and not one that is shared by any widely used Haskell implementation.

But I do agree there's a point here.  There's a simplicity that the purely functional fragment of Haskell shares with the lambda calculus, which I wish were easier to get across to new Haskell programmers.  That simplicity is precisely what allows the lambda calculus, as well as the purely functional fragment of Haskell, to have a meaning without answering the question of how it is evaluated.  (Even in more complex programming languages, the notion of evaluation that is used to define the language is often not the same one that's used by implementations, of course.  But nevertheless these languages must be defined in terms of some model of evaluation, where the purely functional fragment of Haskell doesn't.)

I struggle with this.  In some very real ways, I consider it the most important point of learning Haskell for many programmers.  But it's also not a prerequisite to using Haskell for practical purposes.  For me, since I learned Haskell in order to just experience the cool ideas that it contains (and only 15 years later got my first job programming in Haskell), that's reason enough.  But, within reason at least, it's the learner's goals that matter most when learning.  Someone who isn't looking to understand the fundamental simplicity of a portion of Haskell isn't likely to be motivated to work through the effort it takes to understand it.  So there must be some ways, at least, to learn Haskell without focusing on that particular aspect of the language.  A Haskell programmer won't be as good of a Haskell programmer as they could be without understanding it, and will struggle to write idiomatic pure code.  But one must start somewhere.  New Python programmers don't write idiomatic or perfect Python, either!

On Sat, Sep 18, 2021 at 7:11 PM Olaf Klinke <olf@aatal-apotheke.de> wrote:
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.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.