Janis Voigtländer jv at informatik.uni-bonn.de
Wed Aug 4 13:53:33 EDT 2010

```Nicolas Pouillard schrieb:
> Right let's make it more explicit, I actually just wrote a Control.Seq
> module and a test file:
>
> module Control.Seq where
>   genericSeq :: Typeable a => a -> b -> b
>   genericSeq = Prelude.seq
>
>   class Seq a where
>     seq :: a -> b -> b
>
>   instance (Typeable a, Typeable b) => Seq (a -> b) where
>     seq = genericSeq
>
>   ... Other seq instances ...
>
> \$ cat test.hs
> import Prelude hiding (seq)
> import Data.Function (fix)
> import Control.Seq (Seq(seq))
> import Data.Typeable
>
> ...
>
> foldl''' :: (Typeable a, Typeable b) => (a -> b -> a) -> a -> [b] -> a
> -- GHC infer this one
> -- foldl''' :: Seq (a -> b -> a) => (a -> b -> a) -> a -> [b] -> a
> -- however this one require FlexibleContext, and the first one is accepted.
> foldl''' c = seq c (fix (\h n ys -> case ys of
>                                       [] -> n
>                                       x : xs -> let n' = c n x in h n' xs))

Well, in this example you were lucky that the function type on which you
use seq involves some type variables. But consider this example:

f :: (Int -> Int) -> a -> a
f h x = seq h x

I think with your definitions that function will really have that type,
without any type class constraints on anything.

So let us derive the free theorem for that type. It is:

forall t1,t2 in TYPES, g :: t1 -> t2, g strict.
forall p :: Int -> Int.
forall q :: Int -> Int.
(forall x :: Int. p x = q x)
==> (forall y :: t1. g (f p y) = f q (g y))

Now, set

p :: Int -> Int
p = undefined

q :: Int -> Int
q _ = undefined

Clearly, forall x :: Int. p x = q x holds.

So it should be the case that for every strict function g and
type-appropriate input y it holds:

g (f p y) = f q (g y)

But clearly the left-hand side is undefined (due to strictness of g and
f p y = f undefined y = seq undefined y), while the right-hand side is
not necessarily so (due to f q (g y) = f (\_ -> undefined) (g y) = seq
(\_ -> undefined) (g y) = g y).

So you have claimed that by using seq via genericSeq in the above
definition of f you are guaranteed that any free theorem you derive from
its type is correct. But as you see above it is not!

I think you have to face it: if you want a solution that both gives
meaningful free theorems and still allows to write all programs
involving seq that you can currently write in Haskell, then using type