Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What a bottom (which is _|_) in haskell?

Tags:

haskell

In Haskell document, sometime I find the word bottom (_|_). Is it correct that a bottom (_|_) is a value cannot be further broken down?

Example,

Non-bottom:

  • a Num is not, because, it an instance of class Num.
  • 1 is not, because, it is a Num.
  • a String is not, because, it is a list of Char
  • "aa" is not, because it is a String
  • ...

A-Bottom: following are all a bottom, because they cannot be further broken down.

  • a Char
  • an Int
  • 1::Int
  • a Word
  • 1::Word
  • Apple and Orange in data Fruit = Apple | Orange
  • ...
like image 430
Johnson Cheung Avatar asked Dec 04 '25 04:12

Johnson Cheung


1 Answers

Your intuition is incorrect. A bottom is a fictional value representing a non-terminating program. In Haskell, because of laziness, this value is present in any type.

For example:

x1 :: Integer
x1 = 42 -- not a bottom

x2 :: Integer
x2 = sum [1..]  -- bottom, it does not terminate

x3 :: (Integer, String)
x3 = x3   -- bottom, infinite recursion

x4 :: (Integer, String)
x4 = (x2, "hello")   -- not a bottom, but a pair (_|_, "hello")

We also pretend that undefined and error ".." are bottoms, since these are exceptional values of expression that fail to evaluate to a "proper" value in their type.

The name bottom comes from theoretical computer science, where mathematical models of computation are studied. In practice, it is common there to "order" the values in functional programming languages so that "non-termination" corresponds to the smallest possible value, which lies at the "bottom" of the ordering, hence the "bottom" name.

E.g. the following pairs are in increasing order.

p1 :: (Integer, Integer)
p1 = p1   -- bottom, infinite recursion

p2 :: (Integer, Integer)
p2 = (sum [1..], sum [1..])   -- not a bottom, but (_|_, _|_) which is only slightly larger

p3 :: (Integer, Integer)
p3 = (42, sum [1..])   
-- (42, _|_) which is larger since it's more defined
-- (fewer bottoms inside, roughly speaking)

p4 :: (Integer, Integer)
p4 = (42, 23)
-- even larger, no larger values exist from here since it's a completely defined value

You can also make infinitely increasing sequences in some types:

l1 :: [Int]
l1 = l1   -- bottom

l2 :: [Int]
l2 = 1 : l1  -- not a bottom, 1 : _|_

l3 :: [Int]
l3 = 1 : 2 : l1  -- more defined, 1 : 2 : _|_


l4 :: [Int]
l4 = 1 : 2 : 432 : l1  -- more defined

-- etc. we can go on forever

This ordering of values is important in programming language theory because recursive definitions always find the least value satisfying the recursive equation.

E.g. the equation x1=x1 in Int is satisfied by _|_, 0, 1, -1, ..., but if we consider that it's a recursive definition, we have to take the least solution, namely _|_.

Similarly, in p :: (Integer, Integer) defined as p = (32, snd p), we find the solutions (32, _|_), (32, 0), (32, 1), (32, -1), .... but we need to take the least so we have (32, _|_). This models the fact that when we evaluate the expression the second component is never defined (because of infinite recursion).

like image 167
chi Avatar answered Dec 06 '25 20:12

chi



Donate For Us

If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!