I think we should be pretty cautious about jumping in with lifed function
spaces. I have come up with two distinct unintended effects. While neither
is fatal to the idea, I don't think either obvious, and I am nervous that
others may pop out of the woodwork somewhere down the road (to mix
metaphors).
So far I am unconvinced about lifted function spaces. I'd still buy the
Data class idea. Remember, you don't have to implement it with all the glory
of dictionaries etc. You can implement seq etc just as you do now!
A few other brief rejoinders to things people have said
* My taste is that isomorphic possibly-abstract types should get a new kind
of type declaration (newtype, isotype, or whatever), perhaps defined to be
exactly equivalent to a algebraic data type with just one strict
constructor. But I don't feel strongly about this.
(At least we appear to be agreed on the idea that there should
be an explicit constructor.)
* I'd misunderstood Phil's position about liftedness. He advocates
- unlifted functions
- lifted algebraic data types (all of them)
- unlifted tuples (just tuples, not all single-constr types)
I have never, never been tripped up by the liftedness of tuples, but the
argument that ``we are prepared to pay for laziness so why not this too''
has a certain masochistic charm. I'll try the effect on performance of
making all tuple-matching lazy in the nofib suite.
* Phil remarks that pattern-matching in let/where is implicitly twiddled.
That's true, and it is inconsistent; but while we might fix it for tuples,
we can't fix it for general algebraic data types --- so is it important to
fix it for tuples...?
Simon
Effect 1: strictness becomes less straightforward
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f x y = x+y
Quick! Is this strict in x? Would your answer be any
different if I wrote
f x = \y -> x+y
or
f = \xy -> x+y
(I hope not.)
The point is this. We would usually say that f is strict iff
f _|_ = _|_
But, if function space is lifted, then f _|_ is
certainly not _|_! So is f strict or not? Blargh.
At the cost of extra complexity we can fix this. We have to run off to our
strictness analysis abstract interpreters, and fix up the rule which
currently says
apply fun Bot | isStrict fun = Bot
Instead we have to return some abstract value which ``remembers'' that
when it has eaten up another argument it should give Bot, but which meanwhile
is definitely not Bot.
I can't say I relish this.
Effect 2: useful transformations become invalid
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's already been pointed out that the eta-rule becomes invalid if
function spaces are lifed. I didn't use to think that was important till
I came across this example:
putString (c:cs) = putChar c `thenIO_` putString cs
Once we unfold thenIO_ ,and make pattern-matching explicit,
we get
putString = \cs -> case cs of
(c:cs) -> \s -> case (putChar c) of
(_,s') -> putString cs s
Never mind the details, just focus on that \s inside the branch of
the case. I'd *like* now to transform to
putString = \cs s -> case cs of
(c:cs) -> case (putChar c) of
(_,s') -> putString cs s
That is, I'd like to float the \s outside the case. Currently
I'm allowed to do that, and it is advanatageous to do so because
it brings the two \'s together. (I'll elaborate for anyone who's interested.)
But with lifted function spaces this transformation is Wrong.
What upsets me about this example is that the sort of inner loop which
appears a lot in our I/O and array-manipulation system, so I'm reluctant to
take a performance hit there.
