[Haskell-cafe] Re: Control.Exception.evaluate - 'correct
definition' not so correct
Abhay Parvate
abhay.parvate at gmail.com
Wed May 7 07:12:50 EDT 2008
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
More information about the Haskell-Cafe
mailing list