Here is a remark about irrefutability,
something that has bothered me for some time.
First, the well-known bit:
Haskell has irrefutable patterns. This is an adaptation of Miranda.
However, irrefutable patterns in Miranda are implicit, in Haskell they
are explicit. As a consequence, Miranda has "surjective pairing",
i.e. any expression e of tuple type is indistinguishable from
(p1 e,p2 e,...,pn e) where p1...pn are the corresponding projections.
This is not true for Haskell, because Haskell also has refutable
pair patterns, making (p1 e,p2 e,...,pn e) in general to be more
defined than e. [I might argue that this defeats the main purpose of
having irrefutable patterns in the first place, but this isn't really
the point I wanted to make.] Semantically one could say that products
in Miranda are unlifted, they don't have an extra bottom element.
Now, the other bit:
Haskell/Miranda don't have irrefutable case-expressions --- thus their
coproducts are always lifted.
In other words, case distinction always triggers evaluation, we cannot
delay or circumvent it. There are alternatives. For instance, we
could consider a specific form of case-evaluation, Prolog style:
evaluating a refutable case-expression means to make a choice point.
We choose the first constructor (of the datatype) regardless of what
the case argument actually looks like and only when we need to access
the constructor argument we'll have a look what the argument is and
force an evaluation. If it then turns out that the constructor
differs from our guess we have to abandon this computation and go back
to the last choice point, picking the next alternative. Effectively,
this technique identifies bottom with C1 bottom for all but printing purposes.
The described technique isn't ideal, because the (wrongly) chosen
path of the case may fail to terminate without ever forcing the
evaluation of the case argument, so one may want to modify this in
some way to prevent this from happening. Besides, the eta-rule
for case is more like
(case e of {I1 x -> f (I1 x) ; I2 x -> f (I2 x)}) ==> f e
which one can split into
(case e of {I1 x -> I1 x ; I2 x -> I2 x}) ==> e
and (case e of {I1 x -> f a ; I2 x -> f b}) ==>
f (case e of { I1 x -> a ; I2 x -> b})
i.e. going underneath a case without looking at the case argument
should only take place if there is a common bit of computation
for all cases.
Are there any realistic and non-contrived examples where this has any
effect? Well, I suppose rather few, but there's at least one.
Miranda used to have in an older version the following
definition of scan:
scan op = g
where
g r [] = [r]
g r (a:x) = r : g (op r a) x
This was later found out not to be as lazy as it could be, because
both alternatives of g start with (r:) and consequently a lazier
version was devised later. Instead, one could blame the absence of
refutable-case for the lack of laziness. The mentioned eta-rule for
case would transform the definition into:
scan op = g
where
g r xs = r:aux xs
where
aux [] = []
aux (a:x) = g (op r a) x
arriving at a lazier version of scan.
There is also one situation which occurs rather frequently
in which some extra laziness is gained. Whenever we write a function
the result-type of which is a tuple then it is quite likely (judging
from practical experience) that all cases end with a tuple formation,
and -- as observed earlier -- tuple formation
tupleform ~(x,y) = (x,y)
isn't quite the identity in Haskell, it increases content.
[Thus the definition of such a function f would be transformed into
f = tupleform . f'
where f' is the old version of f.]
I am not seriously suggesting to extend the language behaviour in that
way, although it's perhaps worth to make some experiments.
I merely wanted to point out that there is something dual to
irrefutable patterns which people seemed to have overlooked,
and see whether there any strong opinions on that matter.
Stefan Kahrs
Edinburgh
