A question about the "awkward squad"

[Judah Jacobson]

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