Least-strict (*)

Question

Is it possible to implement (*) with least-strict semantics in Haskell (standardized Haskell preferred, but extensions are OK. Using compiler internals is cheating)? For example, such a definition should result in the following being true:

0 * ⊥ = 0
⊥ * 0 = 0

and only:

⊥ * ⊥ = ⊥

I can build pattern matches that satisfy one of the above cases, but not both, because the zero check forces the value.

Answer 1

Yes, but only using constrained impurity.

laziestMult :: Num a => a -> a -> a
laziestMult a b = (a * b) `unamb` (b * a)

here unamb is Conal Elliott's "pure" variant of amb. Operationally, amb runs two computations in parallel, returning which ever comes first. Denotationally unamb takes two values where one is strictly greater (in the domain theory sense) than the other, and returns the greater one. Edit: also this is unamb, not lub, so you need to have them equal unless one is bottom. Thus, you have a semantic requirement that must hold even though it can't be enforced by the type system. This is implemented as essentially:

unamb a b = unsafePerformIO $ amb a b

much work goes into making this all work correctly with exceptions/resource management/thread safety.

laziestMult is correct if * is commutative. It is "least strict" if * is non strict in one argument.

For more, see Conal's blog

Answer 2

Phillip JF's answer only applies to flat domains, but there are Num instances which are not flat, for example the lazy naturals. When you go into this arena, things get quite subtle.

data Nat = Zero | Succ Nat
    deriving (Show)

instance Num Nat where
    x + Zero = x
    x + Succ y = Succ (x + y)

    x * Zero = Zero
    x * Succ y = x + x * y

    fromInteger 0 = Zero
    fromInteger n = Succ (fromInteger (n-1))

    -- we won't need the other definitions

It is especially important for lazy naturals that operations be least-strict, since that is the domain of their usage; e.g. we use them to compare lengths of possibly infinite lists, and if its operations are not least-strict, then that will diverge when there is useful information to be found.

As expected, (+) is not commutative:

ghci> undefined + Succ undefined
Succ *** Exception: Prelude.undefined
ghci> Succ undefined + undefined
*** Exception: Prelude.undefined

So we will apply the standard trick to make it so:

laxPlus :: Nat -> Nat -> Nat
laxPlus a b = (a + b) `unamb` (b + a)

which seems to work, at first

 ghci> undefined `laxPlus` Succ undefined
 Succ *** Exception: Prelude.undefined
 ghci> Succ undefined `laxPlus` undefined
 Succ *** Exception: Prelude.undefined

but in fact it does not

 ghci> Succ (Succ undefined) `laxPlus` Succ undefined
 Succ (Succ *** Exception: Prelude.undefined
 ghci> Succ undefined `laxPlus` Succ (Succ undefined)
 Succ *** Exception: Prelude.undefined

This is because Nat is not a flat domain, and unamb only applies to flat domains. It is for this reason that I consider unamb a low-level primitive that should not be used except to define higher level concepts -- it should be irrelevant whether a domain is flat. Using unamb will be sensitive to refactors that change the domain structure -- the same reason seq is semantically ugly. We need to generalize unamb the same way seq is generalized to deeqSeq: this is done in the Data.Lub module. We first need to write a HasLub instance for Nat:

instance HasLub Nat where
    lub a b = unambs [
                  case a of
                      Zero -> Zero
                      Succ _ -> Succ (pa `lub` pb),
                  case b of
                      Zero -> Zero
                      Succ _ -> Succ (pa `lub` pb)
              ]
        where
        Succ pa = a
        Succ pb = b

Assuming this is correct, which is not necessarily the case (it's my third try so far), we can now write laxPlus':

laxPlus' :: Nat -> Nat -> Nat
laxPlus' a b = (a + b) `lub` (b + a)

and it actually works:

ghci> Succ undefined `laxPlus'` Succ (Succ undefined)
Succ (Succ *** Exception: Prelude.undefined
ghci> Succ (Succ undefined) `laxPlus'` Succ undefined
Succ (Succ *** Exception: Prelude.undefined

So we are driven to generalize that the least-strict pattern for commutative binary operators is:

leastStrict :: (HasLub a) => (a -> a -> a) -> a -> a -> a
leastStrict f x y = f x y `lub` f y x

At the very least, it is guaranteed to be commutative. But, alas, there are further problems:

ghci> Succ (Succ undefined) `laxPlus'` Succ (Succ undefined)
Succ (Succ *** Exception: BothBottom

We expect the sum of two numbers which are at least 2 to be at least 4, but here we get a number which is only at least 2. I cannot come up with a way to modify leastStrict to give us the result we want, at least not without introducing a new class constraint. To fix this problem, we need to dig into the recursive definition, and simultaneously pattern match on both arguments at every step:

laxPlus'' :: Nat -> Nat -> Nat
laxPlus'' a b = lubs [
    case a of
        Zero -> b
        Succ a' -> Succ (a' `laxPlus''` b),
    case b of
        Zero -> a
        Succ b' -> Succ (a `laxPlus''` b')
    ]

And finally we get one that gives as much information as possible, I believe:

ghci> Succ (Succ undefined) `laxPlus''` Succ (Succ undefined)
Succ (Succ (Succ (Succ *** Exception: BothBottom

If we apply the same pattern to times, we get something that seems to work as well:

laxMult :: Nat -> Nat -> Nat
laxMult a b = lubs [
    case a of
        Zero -> Zero
        Succ a' -> b `laxPlus''` (a' `laxMult` b),
    case b of
        Zero -> Zero
        Succ b' -> a `laxPlus''` (a `laxMult` b')
    ]

ghci> Succ (Succ undefined) `laxMult` Succ (Succ (Succ undefined))
Succ (Succ (Succ (Succ (Succ (Succ *** Exception: BothBottom

Needless to say, there is some repeated code here, and developing the patterns to express these functions as succinctly (and thus with as few opportunities for error) as possible would be an interesting exercise. However, we have another problem...

asLeast :: Nat -> Nat
atLeast Zero = undefined
atLeast (Succ n) = Succ (atLeast n)

ghci> atLeast 7 `laxMult` atLeast 7
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ ^CInterrupted.

It is dreadfully slow. Clearly this is because it is (at least) exponential in the size of its arguments, descending into two branches on each recursion. It will require yet more subtlety to get it to run in reasonable time.

Least-strict programming is relatively unexplored territory, and there is necessity for more research, both in implementation and practical applications. I am excited by it and consider it promising territory.