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

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