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

[roconnor at theorem.ca]

I'm sure someone else will give you a more detailed answer, but what you 
propose is not so dissimilar to how Seq worked in Haskell 1.4 and Haskell 
1.3 (where the class was called Eval).  This class constraint was removed 
for not very good reasons[1] according to my very limited understanding. 
I would be happy for it to reappear.

[1] A History of Haskell: being lazy with class, Section 10.3

On Fri, 18 Mar 2011, Tyson Whitehead 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
>

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''