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

[David Feuer]

GHC's use of a State-like monad to represent I/O is semantically bogus, a
fact that rears its head in a few compiler transformations (including
strictness analysis). I wouldn't take it as a good mental model.

On Sat, Sep 18, 2021, 7:09 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/45e9e353/attachment.html>