sandwood
sandwood

Reputation: 2167

Order of function evaluation and laziness

A bit of thinking about how "Laziness" and order of evaluation of a function

Consider this code :

testF x =  ((length x) >= 1) && ((head x) == "foo")

testG x =  ((head x) == "foo") && ((length x) >= 1)

testH x = False && ((head x) == "foo") 

testI x = ((head x) == "foo") && False

and the result of execution with an empty list

*Main> testF []
False
*Main> testG []
*** Exception: Prelude.head: empty list
*Main> testH []
False
*Main> testI []
*** Exception: Prelude.head: empty list

Question concerning testF and testG : I read that Haskell evaluate leftmost outermost which would garantee the result; is it really a requirement of the language or is this testF [] evaluation is actually undefined behaviour ( for example in C++ it was the case until C++11).

Question concerning testH and testI : what seems obvious at first glance does not appear so obvious: even if it evaluates leftmost outermost, which garantee do we have than implementation does not perform some kind of reverse ordering evaluation:

Consider that:

myAnd _ False = False
myAnd False _ = False
myAnd a b = (&&) a b

testJ x =  myAnd ((head x) == "foo") False 
testK x =  myAnd False ((head x) == "foo")  

gives reverted behaviour

*Main> testJ []
False
*Main> testK []
*** Exception: Prelude.head: empty list

Finally, all the examples above make the (&&) operator failing regarding the commutativity law ( a&&b == b&&a ), so I end up thinking that all those calls , ideally, should evaluate both arguments and raise an exception.

Upvotes: 2

Views: 330

Answers (2)

that other guy
that other guy

Reputation: 123410

This behavior is guaranteed.

|| and && from Prelude are defined to behave like this in Haskell 2010 section 9:

-- Boolean functions
(&&), (||) :: Bool -> Bool -> Bool
True && x = x
False && _ = False
True || _ = True
False || x = x

Pattern matching is also defined to work left-to-right (3.17.2) with _ matching ⊥:

Pattern matching proceeds from left to right, and outside to inside, according to the following rules: [...] Matching the wildcard pattern _ against any value always succeeds, and no binding is done.

The same is true in the older Haskell 98 specification.

Upvotes: 9

AJF
AJF

Reputation: 11913

Haskell doesn't evaluate the leftmost first for all cases. As you saw, this is due to your definitions. Take the definition of &&:

(&&) :: Bool -> Bool -> Bool
(&&) False _ = False
(&&) _ False = False
(&&) _ _     = True

Notice that it requires a pattern from the left argument first. This forces the left argument to be evaluated first, and could leave the second argument unevaluated. In your myAnd function, you switch the order of evaluation due to your pattern matching. If you swapped the 2nd and 3rd lines (which you did) the order of evaluation would also swap.

There is absolutely no undefined behaviour occuring here. Don't get your head stuck in C!

However, if a function pattern matches on two (or more) arguments, then it does evaluate the leftmost first. So, for example:

func1 True False = True -- Both arguments evaluated
func1 _ _        = False

test1 = func1 (error "leftmost") (error "rightmost")
-- Running test1 results in the error "leftmost"

Your point about commutativity is sharp. Technically, this does indeed not allow for the commutativity law. However, when reasoning about Haskell code we usually ignore bottom (error and undefined to non-mathematicians) for two reasons. One, it makes things nicer, and two, you shouldn't be encountering error anyway: that means that you've gone wrong. So in practice, no: && is functionally commutative. errors should not be happening in your Haskell code, and there's no way to catch them for this reason; it breaks the nice algebraic properties as you pointed out. Use them only for events that should not occur, as in the implementation of head.

There are many other languages similar to Haskell, in particular Agda and Idris, which do away with error and undefined entirely for this reason, mostly because they have a specific goal of logical consistency, in order to be able to quite literally prove that your code is correct. However, Haskell (likely in a bid to stay more mainstream) does not do so.

Upvotes: 12

Related Questions