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

[Tyson Whitehead]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: This is a digitally signed message part.
URL: <http://www.haskell.org/pipermail/libraries/attachments/20110318/9b01f4c3/attachment.pgp>