(This message assumes we head for the strictness-annotation-on-constructor-arg
solution. I'll respond to Phil's comments in my next msg.)
The problem with polymorphic strictness
~~~
John asks what the problem is with strict constructor args. As Lennart and
Kevin say, the problem only really arises with function types; for example
data Foo = MkFoo !(Int - Int)
Operationally the idea is that you evaluate the function before building the
constructor. That places some new constraints on implementations, but I suspect
it can always be done.
More seriously, as Lennart says, Haskell says that _|_ = (\x - _|_).
Now, there is no way to find out whether the function given as an
argument to MkFoo is a function which always returns bottom. Consider
case MkFoo (\x - a complicated calculation involving x, which
always fails to terminate)of
MkFoo f - 0
If the implementation just "evaluates the function" and then wraps it in a MkFoo,
then the result of this expression is just 0. But if _|_ = (\x - _|_),
and MkFoo really is strict, then the result should be _|_.
So, as Lennart says, if we allow constructors to be strict in functions
then we have to change the semantics to distinguis _|_ from (\x - _|_).
I, for one, am deeply reluctant to do so; I certainly have no good handle on
the consequences of doing so. Does anyone else?
The problem shows up if a constructor is strict in a polymoprhic position:
data Baz a = MkBaz !a !a
(consider Baz (Int - Int))
All this applies equally to polymorphic seq too, of course.
An alternative
~~
We already have a good mechanism for dealing with problems like this; it's
called overloading. Suppose we had a class
class Data a where
seq :: a - b - b
-- Other things too?
There would be an instance for class Data on every algebraic data type,
automatically derived.
Then we could write
data Data a = Baz a = MkBaz !a !a
and everything is fine, because now Baz can only be applied to data types, not
functions. And we get seq too. The annotation in the MkBaz can be explained by
translation to seq.
Implementations are free to implement seq with a single batch of polymorphic
code if they want, of course.
Ain't that easy? The only tiresome thing is having to write Data a = in places
where you want a strictness annotation on a polymorphic constructor arg. But I
don't mind that one bit.
The only infelicity is that in the special case of single constructors with a
single strict arg (ie the kind we need for ADTs) there is no need for the
arg to be in class data:
data Abstract a = MkAbstract !a
is perfectly ok semantically and pragmatically. I suppose one could allow
the (Data a =) constraint to be omitted in this special case. Or give a
different syntax for ADT decls, as I suggested before.
Simon
