In Lazier functional programming, part 1, I suggested that some of the standard tools of lazy functional programming are not as lazy as they might be, including even
Generalizing from boolean conditionals, I posed the puzzle of how to define a lazier
either function, which encapsulates case analysis for sum types.
The standard definition:
The comments to part 1 fairly quickly converged to something close to the laxer definition I had in mind:
which is a simple generalization of Luke Palmer‘s laxer if-then-else (reconstructed from memory):
bool c a b = (a ⊓ b) ⊔ (if c then a else b)
My thanks to Dave for “laxer” as a denotational alternative to the operational term “lazier”.
Note in the
either definition that the argument ordering allows computing
(f ⊥ ⊓ g ⊥) just once and reusing the result for different values of the third argument.
Let’s look at some examples:
cond 6 8 ⊥ ≡ (6 ⊓ 8) ⊔ ⊥ ≡ 6 ⊓ 8 ≡ ⊥ cond 7 7 ⊥ ≡ (7 ⊓ 7) ⊔ ⊥ ≡ 7 ⊓ 7 ≡ 7 cond (3,4) (4,5) ⊥ ≡ ((3,4) ⊓ (4,5)) ⊔ ⊥ ≡ (⊥,⊥) cond (3,4) (3,5) ⊥ ≡ ((3,4) ⊓ (3,5)) ⊔ ⊥ ≡ (3,⊥) cond [2,3,5] [1,3] ⊥ ≡ ([2,3,5] ⊓ [1,3]) ⊔ ⊥ ≡ ⊥ : 3 : ⊥
These results are more useful than they might at first appear.
Monotonicity implies that the following information-inequalities also hold for an arbitrary boolean
cond 6 8 c ⊒ ⊥ cond 7 7 c ⊒ 7 cond (3,4) (4,5) c ⊒ (⊥,⊥) cond (3,4) (3,5) c ⊒ (3,⊥) cond [2,3,5] [1,3] c ⊒ (⊥ : 3 : ⊥)
In other words, given only
b, we can already start extracting some information about the value of
cond a b c.
c takes a long time to compute (forever in the extreme case), we may be able to get some useful information out of
cond gets any information out of
Moreover, the presence of “⊔” hints at parallelization.
a ⊓ b can proceed in one thread, while another computes the standard conditional.
At the function level,
This observation is handy when
cond is partially applied to two arguments and the resulting function is reused.
We can even compute
a ⊓ b once and share the results among many calls.
These same considerations apply more generally to the laxer
either definition above.
Does the definition of
either above really satisfy the conditions of the puzzle, and how did I come up with it?
A key insight is that monotonicity implies the following two inequalities for all
eitherL f g ⊥ ⊑ eitherL f g (Left a) eitherL f g ⊥ ⊑ eitherL f g (Right b)
Consistency with the defining equations then imply that
eitherL f g (Left a) ≡ f a eitherL f g (Right b) ≡ g b
eitherL f g ⊥ ⊑ f a eitherL f g ⊥ ⊑ g b
eitherL f g ⊥ ⊑ f a ⊓ g b
a ≡ b ≡ ⊥ gives us an single least of these upper bounds:
eitherL f g ⊥ ⊑ f ⊥ ⊓ g ⊥
similarly to Albert’s reasoning for the similar case of
I asked for a information-maximal version of
eitherL so as to get as much information out with as little information in, in the spirit of lax (non-strict) functional programming.
For the maximal version, choose equality:
eitherL f g ⊥ ≡ f ⊥ ⊓ g ⊥
There are three fairly simple proofs remaining, namely that (a) this equality holds for the definition of
eitherL above, (b) the use of (⊔) is legitimate in that definition, and (c) the definition as a whole is consistent with the defining equations.
Finally, note that lub (⊔) is used in a restricted way here.
In this use
u ⊔ v, not only are the arguments
v information-compatible (the semantic pre-condition of lub), but also,
u ⊑ v.
This property shows up in several applications of lub, and I suspect it can be useful in efficient implementation.