Paul writes:
| Like Ian, I would like to suggest that we lift functions in Haskell.
| Originally there was a good reason not to: there was no need (and
| indeed no way) to distinguish _|_ from \x->_|_. But now there are
| some compelling reasons to make the distinction:
I would say that there is still no compelling reason to distinguish
them.
| 1) It solves the strict constructor business without resorting,
| for example, to Simon's "Data" class.
But perhaps such a class is an entirely appropriate solution to the
problem.
| 2) This in turn solves the lifted/unlifted product and ADT issue
| without resorting to a new kind to datatype decl ("newtype").
Taking Ian's view of ! as a bottomless type constructor, I suppose
that a lifted product of delifted types is something like an unlifted
product, but I wouldn't think this would be a _lazy_ product.
Actually, I agree that it would be better not to have a new kind of
data declaration, but I think a better solution is to have data types
be lifted sums of unlifted proudcts (where a single-constructor type
is not a sum). Of course, this discussion has been with us since day
one of the Haskell committee; I beg the indulgence of those who are
tired of hearing about it, for the possible benefit of some who haven't
been around this block before. In past discussions on this point,
those favoring unlifted products have pointed out that we could maintain
full flexibility by also providing an explicit Lift constructor.
In fact, such a constructor could be programmed:
data Lift a = Lift a | Never
where that second constructor is never used. Some people, quite
reasonably, find this solution unpalatable, however.
Interestingly, there is some evidence that the Yale Haskell project has
implicitly taken the unlifted product view of single-constructor
types:
1. Sandra Loosemore's paper on the optimizer lists "folding
is-constructor when the corresponding data type has only
the one constructor" as one of the miscellaneous
optimizations.
2. John Peterson's paper on the Lisp interface says that a
Lisp type to be regarded as a k-constructor algebraic type
must be provided with the k constructors, k is-constructor
predicates, and component projections (e.g., nil, cons,
null, cons-p, car, cdr), but that the predicate may be
omitted for a single-constructor type.
| 3) It makes theory closer to practice: Haskell will look more like
| Abramsky and Ong's lazy lambda calculus.
The lazy lambda calculus is certainly interesting and valuable as a model
of a pure calculus with head-normal-form reduction, but the question is
how relevant this is to Haskell. The crucial issue is one of abstractness
and observability. I think most of would agree that Haskell, Miranda,
and the like aren't quite like the pure lambda calculus, but more like
the lambda calulus augmented with base types and delta rules, where only
the base types are observable. We say that the only operation on
functions is application, which with a lazy semantics naturally leads to
unlifted functions, since the only reason to evaluate a function is
to apply it.
Similarly, I would say the only operations on products are projections,
so that as a lazy language, Haskell in inconsistent, not in having
unlifted functions, but in having lifted products.
| 4) It conforms better to (at least my) intuition: current Haskell
| implementations in a sense CAN distinguish _|_ from \x->_|_:
| just return a functional value from the whole program, and in
| one case the implementation is likely to print something like
| "function", and in the other case, nothing (or "error", or whatever).
| To formalize this we could include a bulit-in instance decl for
| functions in the class Text.
As a matter of fact, we have, at John Peterson's suggestion:
instance Text (a -> b) where
readsPrec p s = error "readsPrec{PreludeCore}: Cannot read functions."
showsPrec p f = showString "<<function>>"
Notice that showsPrec is a constant function. The argument f need
not be evaluated to print the result. Even if we don't bring show into
the act, if the implementation has the static types of the program
available to it, the same behavior can result: If all the evaluator
needs to tell you about the main value is "It's a function," it doesn't
need to do any evaluation to tell you that. (Now, if the language were
not statically typed, things would be different: The implementation
would have to evaluate the main program just to discover the type,
and also, bottom and (\x -> bottom) could probably be trivially
distinguished by an isFunction type predicate.)
Your implementation may well have different representations corresponding
to bottom and (\x -> bottom), but that's a far cry from saying that
they shouldn't abstractly be regarded as the same value.
If Haskell is fundamentally a lazy language, but for pragmatic reasons
we want a way to introduce some logically unnecessary strictness in
some places, it shouldn't surprise us that adding any such device is
like mixing oil with water. I think we should deal pragmatically with
the difficulties that arise from such an artificial introduction of strictness,
rather than attack the semantic foundations of the language. Rather than
lifting functions, I would say that something like the data class is
the more appropriate solution, using the type system to avoid the cases
where such an introduction of strictness doesn't make semantic sense.
Thus, it would indeed be reasonable for the type of seq to determine
that f x `seq` y is all right, whereas f `seq` y is not permissible.
Similarly, I think it would be consistent to have unlifted products,
but not give them data instances, so that (x,y) `seq` z is not allowed,
the programmer needing to choose between x `seq` y `seq` z and
y `seq` x `seq` z.
Cheers,
--Joe
