[Haskell-cafe] Re: Laziness question

[Janis Voigtländer]

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 at iai.uni-bonn.de