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. :-)
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.
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.
Best,
Janis.
--
Jun.-Prof. Dr. Janis Voigtländer
http://www.iai.uni-bonn.de/~jv/
mailto:j...@iai.uni-bonn.de
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
