Haskell and laziness

Question

I was just starting to learn Haskell, and I was told that Haskell is lazy, that is, it does as little work as possible when evaluating expressions, but I do not think this is true.

Consider this:

und :: Bool -> Bool -> Bool und False y = False und y False = False non_term x = non_term (x+1) 

Evaluation und (non_term 1) False never ends, but it is clear that the result is False.

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

 und (non_term 1) False 

and

 und False (non_term 1) 

return False?

Answer 1

You can write a full definition for und that will work with non-limiting expressions ... view

To make this work, you need your own Bool definition, which makes the delay explicit in any calculation:

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

Then, when you define a value of type Bool , you should limit yourself to joint recursion, where delays are explicitly expressed using the Delay constructor, and not through recursion, where you must evaluate the subexpression to find the constructor for the top-level return value.

In this world, a value without end may look like this:

 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 xy 

which works great:

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

---

Following dfeuer's comment , it looks like what you are 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 ab = undL ab `unamb` undR ab λ und True False False λ und False False False λ und False True False λ und True True True λ und undefined False False λ und False undefined False 

Answer 2

Is there a way to implement it correctly (e.g. in German) (not partially as mentioned above), so both

 und (non_term 1) False 

and

 und False (non_term 1) 

return False?

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

Even if the proof is more active, the key idea here is that lambda calculus is a consistent, deterministic language. Thus, as soon as the lazy binary function receives two Boolean values ​​(possibly lower ones), it needs to decide which one should be evaluated before the other, therefore, fixing the evaluation order. This will break the symmetry of or and and , since if the selected argument diverges, then or / and also diverges.

As mentioned earlier, Haskell has a library that defines unamb via non-sequential means, that is, using concurrency under it, therefore, going beyond PCF. With this, you can define your parallel to or or and .

Answer 3

Haskell is really lazy. Laziness means that the expression is not evaluated if it is not required. However, laziness does not mean that two expressions can be evaluated in any order. The order in which expressions are evaluated in Haskell matters. For example, consider the und function:

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

Firstly, I would like to note that this function is incomplete. Full function:

 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 

In any case, the template matching syntax in Haskell is just the syntactic sugar for case expressions. For example, your original (incomplete) function will be directed (before alpha equivalence):

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

From here you can see:

• Your function is incomplete because the last case is undefined .
• Your function evaluates the second argument if the first argument is True , although it is not needed. Remember that case expressions always force evaluations of the checked expression.
• Your function first checks x and then checks y if x evaluates to True . Therefore, there does indeed exist an explicit evaluation procedure. Note that if x evaluates to False , then y never evaluated (proof that und really lazy).

It is because of this und (non_term 1) False ordering 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 that has a different evaluation order:

 und :: Bool -> Bool -> Bool und xy = 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) is still diverging. So your main question is:

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

 und (non_term 1) False 

and

 und False (non_term 1) 

return False?

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

Does this mean that Haskell is wrong / wrong? No. Haskell is doing the right thing and just does not give any answer. For a person (who can evaluate both expressions in parallel), it would seem that the result of und (non_term 1) False should be False . However, computers should always have an evaluation order.

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

• Parallel evaluation. Haskell should evaluate the expression in both directions in parallel and choose the one that ends first:

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

• General recursion. In my humble opinion, general recursion is too efficient for most use cases: it allows you to write absurd functions such as non_term x = non_term (x + 1) . Such functions are completely useless. If we do not consider such useless functions as source data, then your original und function is an excellent function to use (just implement the latter case or use && ).

Hope this helps.