[Haskell-cafe] Re: Laziness question

[Nicolas Pouillard]

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.

I agree that the free theorem for foldl does not hold for foldl'''.

However can we derive the free theorem by looking at the type? No because
of the Typeable constraint.

So it is safe to derive free theorems without looking at the usage of seq,
just the type of the function. Taking care of not considering parametric
a type constrained by Typeable.

Finally the difference between your solution and this one is that fewer
(valid) free theorems can be derived (because of the Typable constraints
introduced by seq on functions). Still it is a solution since we no longer
have to fear the usage of seq when deriving a free theorem.

Best regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr