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

[Abhay Parvate]

Just for curiocity, is there a practically useful computation that uses
'seq' in an essential manner, i.e. apart from the efficiency reasons?

Abhay

On Wed, May 7, 2008 at 2:48 PM, apfelmus <apfelmus at quantentunnel.de> wrote:

> 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
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080507/b2d5d68e/attachment.htm