[Haskell-cafe] Re: Laziness question

[Nicolas Pouillard]

On Tue, 03 Aug 2010 16:36:33 +0200, Janis Voigtländer <jv at informatik.uni-bonn.de> wrote:
> 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