[Haskell-cafe] Re: Laziness question

[Nicolas Pouillard]

On Wed, 04 Aug 2010 15:41:54 +0200, Janis Voigtländer <jv at informatik.uni-bonn.de> wrote:
> 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?

It is indeed "too strong", or "not precise enough" we could say.

However at least this simple change make it "correct" (i.e. restore
the parametricity results).

I would call this function genericSeq :: Typeable a => a -> b -> b

> Given that it provides runtime type inspection, probably one cannot
> derive any parametricity results at all for a type variable constrained
> by Typeable.

Exactly. We could say that we no longer car derive wrong parametricity
results about it.

> 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, ...).

Indeed, that's why I want both!

In particular for the instance on functions which could be defined using
genericSeq.

> >>> 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.

Actually given genericSeq, I no longer advocate the need for a polymorphic
seq function. So both genericSeq and the seq from the type class would
both safe.

However the rule is still the same when using an unsafe function you are on
your own.

Clearer?

Best regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr