Пустой тип

В теории типов или пустой тип абсурдный тип , обычно обозначаемый $\mathbb {0}$это тип без терминов. Такой тип может быть определен как нулевое копроизведение (т.е. непересекающаяся сумма без типов). Его также можно определить как полиморфный тип. $\forall t.t$

Для любого типа $P$, тип $\neg P$ определяется как $P\to \mathbb {0}$. Как следует из обозначений, по соответствию Карри–Говарда терм типа $\mathbb {0}$ является ложным суждением и термином типа $\neg P$ является опровержением предложения П.

Теория типов не обязательно должна содержать пустой тип. Пустой тип там, где он существует, обычно не уникален. Например, $T\to \mathbb {0}$ также необитаем для любого населенного типа $T$.

Если система типов содержит пустой тип, нижний тип также должен быть необитаем. поэтому между ними не проводится никакого различия, и оба обозначаются $\bot$.