# Bottom

### From HaskellWiki

m (Added to (hopefully!) the right category.) |
JaredUpdike (Talk | contribs) m (spelling: thouhg -> though) |
||

(5 intermediate revisions by 4 users not shown) | |||

Line 1: | Line 1: | ||

− | The term 'bottom' refers to a computation which never completes successfully. That includes a computation that fails due to some kind of error, and a computation that just goes into an infinite loop (without returning any data). |
+ | The term '''bottom''' refers to a computation which never completes successfully. That includes a computation that fails due to some kind of error, and a computation that just goes into an infinite loop (without returning any data). |

− | The mathematical symbol for bottom is '⊥'. That's Unicode character 22A5 hex = 8869 decimal. Also available in HTML as '&perp;' and in LaTeX as '\perp' (within math mode). In plain ASCII, it's often written as the extremely ugly character sequence '<code>_|_</code>'. |
+ | The mathematical symbol for bottom is '⊥'. That's Unicode character 22A5 hex = 8869 decimal. Also available in HTML as '&perp;' and in LaTeX as '\bot' (within math mode). In plain ASCII, it's often written as the extremely ugly character sequence '<code>_|_</code>'. |

+ | |||

+ | Bottom is a member of any type, even the trivial type () or the equivalent simple type: |
||

+ | |||

+ | <haskell> |
||

+ | data Unary = Unary |
||

+ | </haskell> |
||

+ | |||

+ | If it were not, the compiler could solve the [http://en.wikipedia.org/wiki/Halting_problem halting problem] and statically determine whether any computation terminated (though note that some languages with dependent type systems, such as [http://en.wikipedia.org/wiki/Epigram_%28programming_language%29 Epigram], can statically enforce termination, based on the type for particular programs, such as those using induction). |
||

+ | |||

+ | Bottom can be expressed in Haskell thus: |
||

+ | |||

+ | <haskell> |
||

+ | bottom = bottom |
||

+ | </haskell> |
||

+ | |||

+ | or |
||

+ | |||

+ | <haskell> |
||

+ | bottom = error "Non-terminating computation!" |
||

+ | </haskell> |
||

+ | |||

+ | Indeed, the Prelude exports a function |
||

+ | |||

+ | <haskell> |
||

+ | undefined = error "Prelude; undefined" |
||

+ | </haskell> |
||

+ | |||

+ | Other implementations of Haskell, such as Gofer, defined bottom as: |
||

+ | |||

+ | <haskell> |
||

+ | undefined | False = undefined |
||

+ | </haskell> |
||

+ | |||

+ | The type of bottom is arbitrary, and defaults to the most general type: |
||

+ | |||

+ | <haskell> |
||

+ | undefined :: a |
||

+ | </haskell> |
||

+ | |||

+ | As bottom is an inhabitant of every type (though with some caveats concerning types of unboxed kind), bottoms can be used wherever a value of that type would be. This can be useful in a number of circumstances: |
||

+ | |||

+ | <haskell> |
||

+ | -- For leaving a todo in your program to come back to later: |
||

+ | foo = undefined |
||

+ | |||

+ | -- When dispatching to a type class instance: |
||

+ | print (sizeOf (undefined :: Int)) |
||

+ | |||

+ | -- When using laziness: |
||

+ | |||

+ | print (head (1 : undefined)) |
||

+ | |||

+ | </haskell> |
||

[[Category:Glossary]] |
[[Category:Glossary]] |

## Revision as of 02:33, 6 January 2008

The term **bottom** refers to a computation which never completes successfully. That includes a computation that fails due to some kind of error, and a computation that just goes into an infinite loop (without returning any data).

The mathematical symbol for bottom is '⊥'. That's Unicode character 22A5 hex = 8869 decimal. Also available in HTML as '⊥' and in LaTeX as '\bot' (within math mode). In plain ASCII, it's often written as the extremely ugly character sequence '`_|_`

'.

Bottom is a member of any type, even the trivial type () or the equivalent simple type:

data Unary = Unary

If it were not, the compiler could solve the halting problem and statically determine whether any computation terminated (though note that some languages with dependent type systems, such as Epigram, can statically enforce termination, based on the type for particular programs, such as those using induction).

Bottom can be expressed in Haskell thus:

`bottom = bottom`

or

bottom = error "Non-terminating computation!"

Indeed, the Prelude exports a function

undefined = error "Prelude; undefined"

Other implementations of Haskell, such as Gofer, defined bottom as:

undefined | False = undefined

The type of bottom is arbitrary, and defaults to the most general type:

undefined :: a

As bottom is an inhabitant of every type (though with some caveats concerning types of unboxed kind), bottoms can be used wherever a value of that type would be. This can be useful in a number of circumstances:

-- For leaving a todo in your program to come back to later: foo = undefined -- When dispatching to a type class instance: print (sizeOf (undefined :: Int)) -- When using laziness: print (head (1 : undefined))