[Haskell-cafe] On finding the right exposition...

[Chris Smith]

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 at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210918/23c81d88/attachment.html>