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 classes is not the answer. Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de