[Haskell-cafe] IO is not a monad

[Claus Reinke]

> Adding seq ruins eta reduction.  For normal order lambda calculus
> we have '\x.f x = f' (x not free in f).  If we add seq this is no longer true.

isn't that a problem of seq (and evaluation in Haskell generally) not being 
strict enough (ie, forcing evaluation only to weak head normal form rather 
than to head normal form)?

for instance:

    seq (\x->_|_ x) () = () =/= _|_ = seq _|_ ()

but (assuming a variant, seq-hnf, forcing to hnf instead): 

    seq-hnf (\x-> _|_ x ) () = _|_ = seq-hnf _|_ ()

I don't have my "phone book" here, but didn't Barendregt have a discussion
of what kind of normal form would be an appropriate choice for the meaning
of lambda terms, with hnf being "good" and whnf or nf being "bad"? reduction
to whnf is a pragmatic choice, with a long history, and its own calculus, which 
is not quite the ordinary lambda calculus.

but it's been ages since I learned these things, so I might be misremembering.

Claus

> I'm a fan of eta, it makes reasoning easier.  It also means
> the compiler can do more transformations.

I also like eta conversion, as well as its variations for non-function types. what 
they have in common is that the expanded form provides syntactic/structural 
evidence for properties that are only semantically present in the reduced 
form. for instance, if we add non-functions to the calculus, eta has to be
constrained with type information for f - as the expanded form promises 
that we have a function, holding more information than the reduced form.

variations of eta for non-function types, this allows us to make functions/
contexts less strict (the kind of "borrowing information from the future" so 
often needed in cyclic programming, or in dealing with other potentially 
infinite structures):

    lazy_id_pair x = (fst x,snd x)    -- lazy_id_pair _|_ = (_|_,_|_)

vs

    strict_id_pair (a,b) = (a,b)    -- strict_id_pair _|_ = _|_

at the expense of not having laws like:  

    x = (fst x,snd x)    -- not true in general, even if we know that x::(a,b)

    x = x >>= return    -- not true in general, even if x :: Monad m => m a

    x = \y-> x y    -- not true in general, even if x :: a -> b

we still have the inequalities, though - the expanded form being more
defined than the reduced form.

    x :: t ]= (expand-at-t x) :: t    -- eta conversion at type t

so compilers could use eta-expansion, but not eta-reduction (not without
an approximate analysis of an undecidable property). do you happen to 
have an example in mind where eta-reduction would be beneficial as a 
compiler transformation, but analysis (to demonstrate that the expanded 
functional expression terminates successfully) impractical?