[Haskell-cafe] Re: Laziness question

[Janis Voigtländer]

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