Haskell and laziness

Question

I've just started to learn Haskell and I was told that Haskell is lazy, i.e. it does as little work as possible in evaluating expressions, but I don't think that's true.

Consider this:

und :: Bool -> Bool -> Bool
und False y = False
und y False = False

non_term x = non_term (x+1)

The evaluation of und (non_term 1) False never terminates, but it's clear that the result if False.

Is there a way to implement und (i.e. and in German) correctly (not just partially as above) so that both

und (non_term 1) False

and

und False (non_term 1)

return False?

Answer 1

Is there a way to implement und (i.e. and in German) correctly (not just partially as above) so that both

und (non_term 1) False

and

und False (non_term 1)

return False?

If you're interested in theory, there's a classic theoretical result that states that the function above is impossible in the lazy lambda calculus with recursion (which is called PCF). This was due to Plotkin in 1977. You can find a discussion in the Winskel's notes on denotational demantics in Chapter 8 "Full Abstraction".

Even if the proof is more involved, the key idea here is that the lambda calculus is a sequential, deterministic language. As such, once a lazy binary function is fed two boolean values (possibly bottom ones), it needs to decide which one to evaluate before the other, hence fixing an evaluation order. This will break the symmetry of or and and, since if the chosen argument diverges then the or/and will also diverge.

As others mentioned, in Haskell, there's a library defining unamb through non sequential means, i.e. exploiting some concurrency underneath, hence going outside the power of PCF. With that you can define your parallel or or and.

Answer 2

Haskell is indeed lazy. Laziness means that an expression is not evaluated unless required. However, laziness doesn't mean that two expressions can be evaluated in an arbitrary order. The order of evaluation of expressions in Haskell matters. For example, consider your und function:

und :: Bool -> Bool -> Bool
und False y = False
und y False = False

First, I would like to note that this function is incomplete. The complete function is:

und :: Bool -> Bool -> Bool
und False y = False
und y False = False
und y True  = True          -- you forgot this case

In fact, the und function can be written more succinctly (and more lazily) as follows:

-- if the first argument is False then the result is False
-- otherwise the result is the second argument
-- note that the second argument is never inspected

und :: Bool -> Bool -> Bool
und False _ = False
und _     x = x

Anyway, the pattern matching syntax in Haskell is just syntactic sugar for case expressions. For example, your original (incomplete) function would be desugared to (up to alpha equivalence):

und :: Bool -> Bool -> Bool
und x y = case x of False -> False
                    True  -> case y of False -> False
                                       True  -> undefined

From this we can see:

1. Your function is incomplete because the last case is undefined.
2. Your function evaluates the second argument if the first argument is True even though it doesn't need to. Remember that case expressions always force the evaluation of the expression being inspected.
3. Your function first inspects x and then inspects y if x evaluates to True. Hence, there is indeed an explicit order of evaluation here. Note that if x evaluates to False then y is never evaluated (proof that und is indeed lazy).

It is because of this ordering of evaluation that your expression und (non_term 1) False diverges:

  und (non_term 1) False
= case non_term 1 of False -> False
                     True  -> case False of False -> False
                                            True  -> undefined
= case non_term 2 of False -> False
                     True  -> case False of False -> False
                                            True  -> undefined
= case non_term 3 of False -> False
                     True  -> case False of False -> False
                                            True  -> undefined
                .
                .
                .
                .

If you want, you can create a function which has a different order of evaluation:

und :: Bool -> Bool -> Bool
und x y = case y of False -> False
                    True  -> x     -- note that x is never inspected

Now, the expression und (non_term 1) False evaluates to False. However, the expression und False (non_term 1) still diverges. So, your main question is:

Is there a way to implement und (i.e. and in German) correctly (not just partially as above) so that both

und (non_term 1) False

and

und False (non_term 1)

return False?

The short answer is no. You always need a specific order of evaluation; and depending upon the order of evaluation either und (non_term 1) False or und False (non_term 1) will diverge.

Does this mean that Haskell is wrong/faulty? No. Haskell does the right thing and simply doesn't produce any answer. To a human (who can evaluate both expressions in parallel) it would seem apparent that the result of und (non_term 1) False must be False. However, computers must always have an order of evaluation.

So, what is the actual problem? In my humble opinion the actual problem is either/or:

1. Parallel evaluation. Haskell should evaluate the expression both ways in parallel and choose the one that terminates first:

   import Data.Unamb (unamb)
   
   type Endo a = a -> a
   
   bidirectional :: Endo (a -> a -> b)
   bidirectional = unamb <*> flip
   
   und :: Bool -> Bool -> Bool
   und = bidirectional (&&)
   

2. General recursion. In my humble opinion, general recursion is too powerful for most use cases: it allows you to write absurd functions like non_term x = non_term (x + 1). Such functions are quite useless. If we don't consider such useless functions as inputs then your original und function is a perfectly good function to use (just implement the last case or use &&).

Hope that helps.

Answer 3

You can write a complete definition for und that will work on non-terminating expressions... sort of

To make this work, you need your own definition of Bool that makes explicit the delay in any computation:

import Prelude hiding (Bool(..))
data Bool = True | False | Delay Bool
  deriving (Show, Eq)

Then whenever you define a value of type Bool, you have to constrain yourself to co-recursion, where the delays are made explicit with the Delay constructor, rather than via recursion, where you have to evaluate a sub-expression to find the constructor for the top-level return value.

In this world, a non-terminating value could look like:

nonTerm :: Bool
nonTerm = Delay nonTerm

Then und becomes:

und :: Bool -> Bool -> Bool
und False y = False
und x False = False
und True y  = y
und x True  = x
und (Delay x) (Delay y) = Delay $ und x y

which works just fine:

λ und True False
False
λ und False nonTerm
False
λ und nonTerm False
False
λ case und nonTerm nonTerm of Delay _ -> "delayed" ; _ -> "not delayed"
"delayed"

---

Following up on dfeuer's comment, it looks like what you're looking for can be done with unamb

λ :m +Data.Unamb 
λ let undL False _ = False ; undL _ a = a
λ let undR _ False = False ; undR a _ = a
λ let und a b = undL a b `unamb` undR a b
λ und True False
False
λ und False False
False
λ und False True
False
λ und True True
True
λ und undefined False
False
λ und False undefined
False