
On Wed, 04 Aug 2010 17:47:12 +0200, Janis Voigtländer
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. 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