Personal tools

Bottom

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(mentioned Prelude.undefined)
Line 9: Line 9:
 
</haskell>
 
</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.
+
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 (thouhg 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:
 
Bottom can be expressed in Haskell thus:
Line 27: Line 27:
 
<haskell>
 
<haskell>
 
undefined = error "Prelude; undefined"
 
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>
 
</haskell>
   

Revision as of 01:09, 5 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 '&perp;' 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 (thouhg 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))