What is the bottom type?

Question

In wikipedia, the bottom type is simply defined as "the type that has no values". However, if b is this empty type, then the product type (b,b) has no values either, but seems different from b. I agree bottom is uninhabited, but I don't think this property suffices to define it.

By the Curry-Howard correspondence, bottom is associated to mathematical falsity. Now there is a logical principle stating that from False follows any proposition. By Curry-Howard, that means the type forall a. bottom -> a is inhabited, ie there exists a family of functions f :: forall a. bottom -> a.

What are those functions f ? Do they help define bottom, maybe as the infinite product of all types forall a. a ?

Cobia

Answer 1

In Math

Bottom is a type that has no value. That is : any empty type can play the bottom role.

Those f :: forall a . Bottom -> a functions are the empty functions. "empty" in the set theoretical definition of functions.

In Programming

Dedicating a concrete empty type to have it as bottom by a programming language base library is for convenience. Readability and compatibility of code benefits from everyone using the same empty type as bottom.

In Haskell

Let us refer to them with the more friendly names "Bottom" -> "Void", "f" -> "absurd".

{-# LANGUAGE EmptyDataDecls #-}
data Void

This definition does not contain any constructors => an instance of it can not be created => it is empty.

absurd :: Bottom -> a
absurd = \ case {}

In the case expression we do not have to handle any cases because there are none.

They are already defined in package base

Pointdevice

I see 3 kinds of formulas in propositional calculus. 1) Tautologies, that are true in every interpretation in a Heyting algebra. 2) Formulas which negations are tautologies, they are false in every Heyting interpretations. 3) Formulas which values depend on the interpretation. By Curry-Howard cases 2 and 3 both correspond to empty types. However I reckon that case 2 should be singled out among empty types : only those types deserve to be called bottom. – Cobia