[Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct

[apfelmus]

Luke Palmer wrote:
> It seems that there is a culture developing where people intentionally
> ignore the existence of seq when reasoning about Haskell.  Indeed I've
> heard many people argue that it shouldn't be in the language as it is
> now, that instead it should be a typeclass.
> 
> I wonder if it's possible for the compiler to do more aggressive
> optimizations if it, too, ignored the existence of seq.  Would it make
> it easier to do various sorts of lambda lifting, and would it make
> strictness analysis easier?

The introduction of  seq  has several implications.

The first problem is that parametricity would dictate that the only 
functions of type

    forall a,b. a -> b -> b

are

    const id
    const _|_
    _|_

Since  seq  is different from these, giving it this polymorphic type 
weakens parametricity. This does have implications for optimizations, in 
particular for fusion, see also

   http://www.haskell.org/haskellwiki/Correctness_of_short_cut_fusion

Parametricity can be restored with a class constraint

   seq :: Eval a => a -> b -> b

In fact, that's how Haskell 1.3 and 1.4 did it.


The second problem are function types. With  seq  on functions, 
eta-expansion is broken, i.e. we no longer have

   f = \x.f x

because  seq  can be used to distinguish

   _|_  and  \x. _|_

One of the many consequences of this is that simple laws like

   f = f . id

no longer hold, which is a pity.


But then again, _|_ complicates reasoning anyway and we most often 
pretend that we are only dealing with total functions. Unsurprisingly, 
this usually works. This can even be justified formally to some extend, 
see also

  N.A.Danielsson, J.Hughes, P.Jansson, J.Gibbons.
  Fast and Loose Reasoning is Morally Correct.
http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf


Regards,
apfelmus