On Tue, 03 Aug 2010 16:36:33 +0200, Janis Voigtländer
Nicolas Pouillard schrieb:
- If there is no class instance for function types, then those problems go away, of course. But it is doubtful whether that would be a viable solution. Quite a few programs would be rejected as a consequence. (Say, you want to use the strict version of foldl. That will lead to a type class constraint on one of the type variables. Now suppose you actually want to fold in a higher-order fashion, like when expressing efficient reverse via foldr. That would not anymore be possible for the strict version of foldl, as it would require the type-class-constrained variable to be instantiated with a function type.)
I think it would be a step forward. The old seq would still exists as unsafeSeq and such applications could continue to use it. In the mean time parametricity results would better apply to programs without unsafe functions. And this without adding extra complexity into the type system.
Yes, I agree. Of course, you (and Lennart, and others advocating putting seq into a type class) could work toward that solution right away, could have done so for quite some time: write a package with an Eval type class and method safeSeq (and *no* class instance for function types), upload it on Hackage, encourage people to use it. Modulo the naming difference seq/safeSeq vs. unsafeSeq/seq, that's exactly the solution you want. I wonder why it is not happening. :-)
Yes it would be a starting point.
Actually I think we can keep the old generic seq, but cutting its full polymorphism:
seq :: Typeable a => a -> b -> b
I guess I don't know enough about Typeable to appreciate that.
Basically the Typeable constraints tells that we dynamically know the identity of the type being passed in. So this may be a bit challenging to cleanly explain how this safely disable the parametricity but in the mean time this is the net result the type is dynamically known at run time. The same trick is known to work for references as well when effects are everywhere: newRef :: Typeable a => a -> Ref a readRef :: Ref a -> a writeRef :: Ref a -> a -> () In the same vein it would make unsafePerformIO less dangerous to add such a constraint. However I would like to here more comments about this seq variant, anyone?
OK, I better understand now where we disagree. You want to see in the type whether or not the free theorem apply,
Oh, YES. That's the point of a free theorem, isn't it: that I only need to look at the type of the function to derive some property about it.
I want them to always apply when no call to unsafe function is made.
Well, the question is what you mean by "no call to unsafe function is made". Where? In the function under consideration, from whose type the free theorem is derived? Are you sure that this is enough? Maybe that function f does not contain a call to unsafeSeq, but it has an argument which is itself a function. Maybe in some function application, unsafeSeq is passed to f in that argument position, directly or indirectly. Maybe f does internally apply that function argument to something. Can you be sure that this will not lead to a failure of the free theorem you derived from f's type (counting on the fact that f does not call an unsafe function)?
Of course, preventing the *whole program* from calling unsafeSeq is enough to guarantee validity of the free theorems thus derived. But that's equivalent to excluding seq from Haskell altogether.
It depends on the unsafe function that is used. Using unsafeCoerce or unsafePerformIO (from which we can derive unsafeCoerce) badely anywhere suffice to break anything. So while seq is less invasive I find it too much invasive in its raw form. -- Nicolas Pouillard http://nicolaspouillard.fr