What is the bottom type?

Question

On Wikipedia, the lower type is simply defined as "a type that has no meaning." However, if b is this empty type, then the product type (b,b) also does not matter, but it seems different from b . I agree that the bottom is uninhabited, but I do not think that this property is enough to define it.

Under the Curry-Howard correspondence, the bottom is associated with mathematical falsity. Now there is a logical principle, which states that any sentence follows from the Lodge. According to Curry-Howard, this means that there is a type of forall a. bottom -> a forall a. bottom -> a , i.e. There is a family of functions f :: forall a. bottom -> a f :: forall a. bottom -> a .

What are these f functions? Do they help identify the bottom, perhaps as an endless product of all types of forall a. a forall a. a ?

Answer 1

In math

Below is a , which does not matter. That is: any empty type can play a lower role.

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

In programming

A dedication to a particular empty type for use as the bottom of a programming language database library for convenience. The readability and compatibility of the code is beneficial for everyone who uses the same empty type as the bottom one.

In Haskell

We turn to them with the more friendly names "Lower" → "Void", "f" → "absurdity".

 {-# LANGUAGE EmptyDataDecls #-} data Void 

This definition does not contain constructors => its instance cannot be created => it is empty.

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

In the case expression, we do not need to handle any cases because they do not exist.

They are already defined in the base package.