One proposal currently circulating is that Haskell support both lifted
and unlifted products. For example, we could define
> type Lifted = Lifted Int Int
> newtype Unlifted = Unlifted Int Int
and
> f (Lifted x y) = 3
> g (Unlifted x y) = 3
Now we have
f (Lifted _|_ _|_) = g (Unlifted _|_ _|_) = 3
which seems reasonable enough.
On the other hand,
f _|_ = _|_
g _|_ = 3
This doesn't really have anything to do with lifted or unlifted
products! These last two equations say f is strict and g is not! If we
are to be consistent, and require that functions defined using pattern
matching the way f does are strict, then we should also require that g
be strict. (If we look at the definitions of f and g without the type
definitions in front of us, there is nothing to indicate that one is
strict and the other isn't.) With unlifted domains, of course, this
means that x and y must be evaluated concurrently until at least one
produces and integer. In think we can all agree that this is a dump
idea.
I have not completely made up my mind on the best solution to this
problem, but have a couple of ideas I would like to suggest for
consideration.
One solution is to regard algebraic data types as lifted sums of
unlifted products, except that a type with only one constructor is just
an unlifted product. Operationally this seems reasonable, since a
constructor need only be checked when pattern matching is done if there
is more than one possible constructor for the type.
Another solution, which generalizes an earlier proposal of mine for
strictness annotations, is as follows. We allow lifted, unlifted and
smash products. (In a smash product, if any component of a product is
_|_ then the entire product is bottom. That is, a smash product
constructor is strict in every component.)
Consider
> type Lifted = Lifted Int Int
> type Unlifted = ~Unlifted Int Int
> type Smash = !Smash Int Int
where the notation "~" indicates an unlifted product and "!" indicates a
smash product.
The "~" prefix must be used with any unlifted product constructor when
it is used in a pattern. For example, with
> f (Lifted x y) = 3
> g (~Unlifted x y) = 3
it is clear that f and g are different. In particular, it is clear that
f is strict but g may not be.
The "!" prefix must be used with any smash product constructor when it
is used in an expression, but may not be used when the constructor is
used in a pattern.
For example, with
> h (Smash x y) = 3
> z = !Smash expa expb
the use of ! in the definition of z clearly indicates that some
evaluation is performed, and that z is _|_ if either expa or expb is
_|_. On the other hand, the use of "!" is prohibited in the definition
of h.
If we had written
> h (!Smash x y) = 3 -- WRONG!
> x = 4
> y = error "bottom"
> w = h (!Smash x y)
it would certainly look like w should be 3. The fact that we must write
> h (Smash x y) = 3
makes the expression and pattern a bit different, which is appropriate
in this case.
Clearly every argument of a smash product must be in class Data, and no
unlifted product or unlifted function can be in class Data. Lifted and
smash products can be mixed in an algebraic data type, but an algebraic
data type with an unlifted product constructor can have only one
constructor.
Phil Walder would like tuples to be unlifted. I see no problem with
this. Furthermore, I see no need to include an "~" with tuples, since
the tuple constructor is clearly different from an algebraic data type
constructor.
Should we use the "~" in expressions as well as patterns? I don't know.
What do you think?
In many ways this is a minimal change to Haskell 1.2. The unlifted
product almost exists. Adding the "~" in the algebraic data type
definition simply tells the compiler that "~" must be used whenever the
constructor is used in the pattern. We can use unlifted products now
except that the compiler won't prevent us from cheating and sometimes
using an unlifted product as a lifted product. If we are going to have
strictness at all, something needs to be added to the language, and this
approach combines the two concepts in a consistent proposal.
Warren Burton
Simon Fraser University
