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

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