What is the role of 'bottom' (⊥) in Haskell function definitions?

Question

I don't understand the role played by bottom (⊥ or _|_) in Haskell function definitions.

The definition of zip for example describes it as "right lazy" because

zip [] _|_ = []

but I'm unclear how this differs from

zip [] _ = []

What role is _|_ playing in function definitions such as the one above? In particular, how is it different from using _?

---

UPDATE AND NOTE: As readers of the excellent answers will discover for themselves, a crucial part of those answers, worth pulling up here, is that ⊥ does not (and cannot), in fact, appear in Haskell function definitions. Read on.

Answer 1

Bottom is essentially the fancy algebraic way of saying undefined.

If you try this, you can see why zip is lazy for its right-hand argument:

λ> zip [] undefined
[]
λ> zip undefined []
*** Exception: Prelude.undefined

This is because undefined only fails when you try to evaluate it.

You might be confusing _|_ with _ because of the way it was presented. I will make it clear: the line zip [] _|_ = [] does not act as a pattern match but an equation, stating the equality of zip [] _|_ and []. That is to say, this is not valid Haskell code, but a notational, abstract-algebraic way of saying "I don't care about the second argument."

In the definition of zip you may of course use _, but that's irrelevant. You could have used any name, just as long as it wasn't a constructor-matching pattern such as (Just x) or (a,b). Values will remain unevaluated until they must be pattern matched in pure code.

You can read more about lazy evaluation here.

You can read more about bottom here and here.

Answer 2

I think the OP already realises this, but for the benefit of others who come here with the same confusion: zip [] _|_ = [] is not actual code!

The symbol _|_ (which is just an ascii-art rendering of the mathematical symbol ⊥) means bottom¹, but only when we're talking about Haskell. In Haskell code it does not have this meaning².

The line zip [] _|_ = [] is a description of a property of the actual code for zip; that if you call it with first argument [] and pass any bottom value as the second argument, the result is equal to []. The reason they would want to say exactly this is because the technical definition of what it means for a function f to be non-strict is when f ⊥ is not ⊥.

But there is no role of _|_ (or ⊥, or undefined, or the concept of bottom at all) in defining Haskell functions (in code). It has to be impossible to pattern match on an argument to see whether it is ⊥, for a number of reasons, and so there is no actual symbol for ⊥ in Haskell code³. zip [] _|_ = [] is documentation of a property that is a consequence of the definition of zip, not part of its definition.

As a description of this property zip [] _ = [] is a less specific claim; it would be saying that whatever you call zip [] on, it returns []. It amounts to exactly the same thing, since the only way zip [] ⊥ can return something non-bottom is if it never examines its second argument at all. But it's speaking less immediately to the definition of non-strict-ness.

As code forming part of the definition of the function zip [] _ = [] can't be compared and contrasted to zip [] _|_ = []. They're not alternatives, the first is valid code, and the second is not.

---

¹ Which is the "value" of an expression that runs forever, throws an exception, or otherwise falls to evaluate to a normal value.

² It's not even a valid Haskell identifier, since it contains both "namey" characters (_) and "operator" characters (|). So it can't actually be a symbol meaning anything at all in Haskell code!

³ undefined is often used for ⊥, but it's more of a variable referring to a ⊥ value than the actual thing itself. Much like if you have let xs = [1, 2, 3] you can use xs to refer to the list [1, 2, 3], but you can't use it as a pattern to match some other list against; the attempted pattern match would just be treated as introducing a new variable named undefined or xs shadowing the old one.

Answer 3

Riffing on AJFarmar's answer, I think this critical point was not made explicit:

• _|_ is not a valid literal or identifier in Haskell code!
• And therefore, zip [] _|_ = [] isn't valid code either!

That is implicit in what AJFarmar means by this quote:

[T]he line zip [] _|_ = [] does not act as a pattern match but an equation, stating the equality of zip [] _|_ and [].

To make it very crystal clear, zip [] _|_ = [] appears in the documentation comment for the definition of zip. It's not Haskell code—it's an English-language comment written in an informal technical notation that looks a little bit like Haskell code. Or, in other words, pseudo-code.

Answer 4

⊥ comes out of mathematical order theory. A partially ordered collection has a bottom element, denoted ⊥, if that element precedes every other element. How does this get into Haskell documentation? At some point, computer scientists realized that it would be useful to think about what a computer program, in whatever language, "means". One approach to that is called denotational semantics. In denotational semantics, each term in the programming language is assigned a "denotation", or meaning, in some universe of mathematical meanings. It would be wonderful to be able to say, for instance, that

1. meaningInteger :: Integer -> mathematical integer
2. meaningList :: [a] -> possibly-infinite sequence of elements of type a

Unfortunately, this doesn't quite work out in Haskell, because, for instance, I can write

oops :: Integer
oops = oops

This gives me a term of type Integer, but there's no sensible way to assign it a meaning as a mathematical integer. More interestingly, I could write things like

undefined
undefined : undefined
3 : undefined
[undefined]
let foo = undefined : 3 : undefined : foo

These all (can) have the same type, but have various different levels of undefinedness. So we need to add to our collection of meanings various sorts of undefined things. It's possible, however, to impose a partial order on them based on how defined they are! For example, 3 : 4 : [] is more defined than 3 : 4 : undefined, and is also more defined than 3 : undefined : 4, but the latter two are not comparable. The bottom element of each type, its very least defined element, is called ⊥.