[Haskell-cafe] Re: Laziness question

[Nicolas Pouillard]

On Wed, 04 Aug 2010 18:04:13 +0200, Janis Voigtländer <jv at informatik.uni-bonn.de> wrote:
> Nicolas Pouillard schrieb:
> > On Wed, 04 Aug 2010 17:47:12 +0200, Janis Voigtländer <jv at informatik.uni-bonn.de> wrote:
> >> Nicolas Pouillard schrieb:
> >>> On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer <jv at informatik.uni-bonn.de> 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