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@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.