Nicolas Pouillard schrieb:
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.
...
However I would like to here more comments about this seq variant, anyone?
On reflection, isn't Typeable actually much too strong a constraint? Given that it provides runtime type inspection, probably one cannot derive any parametricity results at all for a type variable constrained by Typeable. In contrast, for a type variable constrained via a hypothetical (and tailored to seq) Eval-constraint, one still gets something which looks like a standard free theorem, just with some side conditions relating to _|_ (strictness, totality, ...). In other words, by saying seq :: Typeable a => a -> b -> b, you assume pessimistically that seq can do everything that is possible on members of the Typeable class. But that might be overly pessimistic, since in reality the only thing that seq can do is evaluate an arbitrary expression to weak head normal form.
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.
Hmm, from this answer I still do not see what you meant when you said you want free theorems to always apply when no call to seq is made. You say that seq is less invasive, so do you indeed assume that as soon as you are sure a function f does not itself (syntactically) contain a call to seq you are safe to use the standard free theorem derived from f's type unconstrained? Do you have any justification for that? Otherwise, we are back to banning seq completely from the whole program/language, in which case it is trivial that no seq-related side conditions will be relevant. Best, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de