Re: [Haskell-cafe] Re: Laziness question

4 Aug 2010

      On Wed, 04 Aug 2010 18:04:13 +0200, Janis Voigtländer  wrote:
...
Nicolas Pouillard schrieb:
...
On Wed, 04 Aug 2010 17:47:12 +0200, Janis Voigtländer  wrote:
...
Nicolas Pouillard schrieb:
...
On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer  wrote:
...
Nicolas Pouillard schrieb:
...
However the rule is still the same when using an unsafe function you are on
your own.
Clearer?
Almost. What I am missing is whether or not you would then consider your
genericSeq (which is applicable to functions) one of those "unsafe
functions" or not.
I would consider it as a safe function.
Well, then I fear you have come full-circle back to a non-solution. It
is not safe:
I feared a bit... but no
...
Consider the example foldl''' from our paper, and replace seq therein by
your genericSeq. Then the function will have the same type as the
original foldl, but the standard free theorem for foldl does not hold
for foldl''' (as also shown in the paper).
So foldl''' now has some Typeable constraints.
No, I don't see how it has that. Or maybe you should make explicit under
what conditions a type (a -> b) is in Typeable. What exactly will the
type of foldl''' be, and why?
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 :: (a -> b -> a) -> a -> [b] -> a
foldl c = fix (\h n ys -> case ys of
                            [] -> n
                            x : xs -> let n' = c n x in h n' xs)

foldl' :: Seq a => (a -> b -> a) -> a -> [b] -> a
foldl' c = fix (\h n ys -> case ys of
                            [] -> n
                            x : xs -> let n' = c n x in seq n' (h n' xs))

foldl'' :: (Typeable a, Typeable b, Seq b) => (a -> b -> a) -> a -> [b] -> a
foldl'' c = fix (\h n ys -> seq (c n) (case ys of
                                         [] -> n
                                         x : xs -> seq xs (seq x
                                                     (let n' = c n x in h n' xs))))

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))

Best regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr