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:
Num is not, because, it an instance of class Num.1 is not, because, it is a Num.String is not, because, it is a list of Char"aa" is not, because it is a StringA-Bottom: following are all a bottom, because they cannot be further broken down.
CharInt1::IntWord1::WordApple and Orange in data Fruit = Apple | OrangeYour 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).
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With