seq/parametricity properties/free theorems and a proposal/question

[Edward Kmett]

Others have commented on the whys and the wherefores of the removal of the
Eval, so I won't belabor that here, but the History of Haskell paper goes
into a bit more depth, IIRC, talking about how this happened during the
refactoring of a large Haskell project.

You may want to read Johann and Voightlander's "Free theorems in the
presence of seq" and "The impact of seq on free theorems".

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.4936
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.71.1777

They have done a lot of work on making more rigorous the strictness side
conditions that exist on many free theorems, and show how with a bit of
unrolling and sideways thinking you can still reason about code equationally
using free theorems, even in a world with fully polymorphic seq.

-Edward

On Fri, Mar 18, 2011 at 10:54 AM, Tyson Whitehead <twhitehead at gmail.com>wrote:

> The haskell (2010) report says:
>
> "The function seq is defined by the equations:
>
>  seq _|_ b  =  _|_
>  seq a b  =  b, if a /= _|_
>
> seq is usually introduced to improve performance by avoiding unneeded
> laziness. Strict datatypes (see Section 4.2.1) are defined in terms of the
> $!
> operator. However, the provision of seq has important semantic
> consequences,
> because it is available at every type. As a consequence, _|_ is not the
> same
> as \x -> _|_ since seq can be used to distinguish them. For the same
> reason,
> the existence of seq weakens Haskell’s parametricity properties."
>
> As has been noted in the literature (and presumably the mailing lists),
> this
> has important consequences for free theorems.  For example, the property
>
>  map f . map g = map (f . g)
>
> should be derivable from the type of map "(a -> b) -> [a] -> [b]" (i.e., as
> map works on all a's and b's, it can't actually do anything other than move
> the a's around, wrap them with the given function to get the b's, or pass
> them
> along to other functions which should be similarly constrained).
>
> However, this last bit about passing them to similarly constrained
> functions
> is not true thanks seq.  There is no guarantee map, or some other
> polymorphic
> function it invokes has not used seq to look inside the universally
> quantified
> types and potentially expose _|_.  For example, consider
>
>  map' f [] = []
>  map' f (x:xs) = x `seq` f x : map f xs
>
> Now "map' f . map' g = map' (f . g)" is not true for all arguments.
>
>  map' (const 0) . map' (const undefined :: Int -> Int) $ [1..10] =
> [undefined]
>  map' (const 0 . undefined :: Int -> Int) $ [1..10] = [0,0,0,0,0,0,0,0,0,0]
>
> My proposal (although I'm sure someone must have brought this up before, so
> it's more of a question) is why not take the magic away from seq by making
> it
> a class function like deepSeq
>
>  class Seq a where
>    seq :: a -> b -> b
>
> It is easily implemented in haskell by simply forces the constructor for
> the
> underlying data type (something also easily derivable by the compiler)
>
>  instance Seq Int where
>    seq' 0 y = y
>    seq' _ y = y
>
> Now, unless I'm missing something, we have restore the strength of
> Haskell's
> parametricity properties
>
>  map :: (a -> b) -> [a] -> [b]
>  map f [] = []
>  map f (x:xs) = f x : map f xs
>
>  map' :: Seq a => (a -> b) -> [a] -> [b]
>  map' f [] = []
>  map' f (x:xs) = x `seq'` f x : map f xs
>
> as the full range of operations that can be performed on universally
> quantified
> types (in addition to moving them around) is reflected in any explicitly
> and
> implicitly (through the dictionaries) passed functions over those types.
>
> Thanks!  -Tyson
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20110318/1853ea75/attachment.htm>