Regarding Lifted vs. Unlifted Function Spaces
---------------------------------------------
Gee, maybe lifted functions aren't such a good idea after all! (:-)
But before reaching that conclusion, there are a few points that need
clarification. In particular, Simon mentions two problems that I
think need further discussion:
First, Simon points out that this version of putString:
putString = \cs -> case cs of
(c:cs) -> \s -> case (putChar c) of
(_,s') -> putString cs s
cannot be transformed into this version:
putString = \cs s -> case cs of
(c:cs) -> case (putChar c) of
(_,s') -> putString cs s
if we have lifted function spaces. True! However, one of the
motivations (for me, at least) for having lifted function spaces was
so that we could define strict as well as non-strict functions. I
suggested earlier that there might be an "annotation" for doing this,
just as LML does for strict constructors. Using "!" for such an
annotation, the following version of putString IS equivalent to the
first above:
putString = \!cs s -> case cs of
(c:cs) -> case (putChar c) of
(_,s') -> putString cs s
The root of this transformation is the following:
\cs -> case cs of (c:cs) -> \s -> exp <==>
\!cs s -> case cs of (c:cs) -> exp
In fact, we can observe the following two tidy transformations as
being valid over lifted function spaces:
f cs s = case cs of (c:cs) -> exp <==> f ~(c:cs) s = exp
f !cs s = case cs of (c:cs) -> exp <==> f (c:cs) s = exp
So, we could have lifted function spaces and Simon could still achieve
his transformation safely.
Simon's second problem is the following:
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.
Jonathan Young and I observed this distinction in our POPL '84 paper
on higher-order strictness analysis (Alan Mycroft and Christine
Ernoult recently re-did our stuff in a more semantically sound way
which will soon appear in JFP). One must in fact make a choice about
primitives such as (+). You can have either:
(+) _|_ = _|_
or (+) _|_ = \y -> _|_
(Just because _|_ /= \x->_|_ does not mean that there can't be
functions which when applied to _|_ yield _|_! putString is one such
function.) To get the first behavior out of f above, one could write:
f !x y = x+y
I agree that this may complicate strictness analysis, although I think
(but don't know for sure) that it is manageable.
-Paul
P.S. Similar arguments can be used to explain Ian's examples given in
a subsequent message (and it should be pointed out that "symmetry of
arguments" is not something lost with lifted function spaces, because
Haskell never had it to begin with! :-)
