<div dir="auto">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.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Sep 18, 2021, 7:09 PM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de">olf@aatal-apotheke.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Perhaps one thing that speaks in favour of Anthony Clayden's suggestion<br>
to learn lambda calculus before/along Haskell is this: <br>
Haskell shares the evaluation model with the lambda calculus. One of<br>
Michael Turner's points of criticism was, as I understand it,<br>
insufficient documentation about the inner workings of Haskell [1].<br>
Haskell needs constructs like the ST monad because of the evaluation<br>
model. Once the learner knows, perhaps by experimenting with it on<br>
paper or on [2,3], that a lambda term can be reduced in several ways,<br>
and confluence guarantees that all ways result in the same normal form,<br>
then some things might be much clearer: <br>
* Which freedoms the compiler can exercise in evaluating your program.<br>
* Why one needs the State monad for ordering sequences of effects (the<br>
programmable semicolon) [4]. <br>
* How the various tricks and pitfalls around lazy and strict functions<br>
work, e.g. Viktor's new Foldable documentation.<br>
<br>
I looked at the first chapter of my K&R. It presents small example C<br>
programs and explains what they do. Taking small Haskell programs and<br>
explaining how these lambda terms are reduced to normal form would be a<br>
comparable (and desirable, in Michael's view) approach? The Haskell<br>
language report does not say anything in this respect, as far as I can<br>
see. Only translation of syntactic constructs to core Haskell is given.<br>
<br>
Olaf<br>
<br>
[1] Of course the documentation is out there somewhere, but not written<br>
in a style which pleases learners like Michael. <br>
[2] <a href="https://lambdacalc.io/" rel="noreferrer noreferrer" target="_blank">https://lambdacalc.io/</a><br>
[3] <a href="https://capra.cs.cornell.edu/lambdalab/" rel="noreferrer noreferrer" target="_blank">https://capra.cs.cornell.edu/lambdalab/</a> <br>
[4] I tried to convince myself that the state monad indeed sequences<br>
effects. In a pure lambda world I think this should mean that a certain<br>
lambda term has only one way of being reduced. Is the following valid<br>
reasoning?<br>
type State s a = s -> (a,s)<br>
When Church-encoding the tuple (a,s) one finds that <br>
  (m :: State s a) >>= (k :: a -> State s b)<br>
= \s -> m s k<br>
so the only applicable rule is beta-reducing m when applying to some s.<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>