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 $\mathrm{𝟘}$, 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 $\mathrm{\forall }t.t$

Mis tahes tüübi $P$ puhul on tüüp $\mathrm{\neg }P$ defineeritud kui $P\to \mathrm{𝟘}$. Kirjapildist tulenevalt ning Curry-Howardi vastavuse järgi on $\mathrm{𝟘}$ tüüpi term väär väide ning term tüübiga $\mathrm{\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 \mathrm{𝟘}$ 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.