Hi, I was reading SPJ's excellent "Tackling the Awkward Squad" paper, which (among other things) uses the operational semantics POV for describing IO formally. It notes at the end of section 2.8 that the implementation type IO a = State -> (a, State) is "a bit of a hack. Why? Because it relies for its correctness on the fact that the compiler never duplicates a redex...In practice, GHC is careful never to duplicate an expression whose duplication might give rise to extra work (a redex)." The paper also gives an example of how a compiler might apply an expansion which is correct according to the above representation but incorrect semantically. What exactly are redex's, in this context, and is it (still?) true that GHC never expands them? Or are there certain types of redex's that aren't? Or is it just really complicated? :-) For example, if I understand this right, does it mean that in the classic top-level unsafePerformIO+NOINLINE hack, the NOINLINE is actually unnecessary in some or all cases? Not to start yet another long TWI debate here...but I do think that this issue of balance between clean outer operational semantics and inner hackery is very interesting as a matter of language design. Thanks in advance, -Judah