Tühi tüüp

Tühi tüüp ehk absurdtüüp on tüübiteoorias tüüp, millel pole ühtegi termi. See tähendab, et sellest tüübist pole võimalik ette näidata ühtegi väärtust. Seda tavaliselt märgitakse kui $\mathbb {0}$, ning seda võib defineerida kui 0-aarset kaaskorrutist (ehk mitte ühegi tüübiga hulga lõikumatu summa). Seda võib defineerida ka kui polümorfne tüüp $\forall t.t$

Mis tahes tüübi $P$ puhul on tüüp $\neg P$ defineeritud kui $P\to \mathbb {0}$. Kirjapildist tulenevalt ning Curry-Howardi vastavuse järgi on $\mathbb {0}$ tüüpi term väär väide ning term tüübiga $\neg P$ tõestab väite $P$ ebatõesust.

Tüübiteooria ei pea sisaldama tühja tüüpi. Teooriates, kus see eksisteerib, ei ole see tavaliselt unikaalne. Näiteks on $T\to \mathbb {0}$ samuti tühi mistahes mittetühja tüübi $T$ puhul.

Näide

Haskelli keeles on saadaval tühi tüüp nimega Void, millega koos on defineeritud funktsioon absurd, signatuuriga Void -> a. See tähendab, et funktsioon võtab vastu väärtuse tüübiga Void ning tagastab väärtuse tüübiga a. Kuna sellist väärtust ei ole võimalik esitada, ei ole seda funktsiooni võimalik kutsuda.