[Haskell-cafe] Re: Laziness question

[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. :-)

> 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:jv at iai.uni-bonn.de