Já to zkusím ještě jinak.
Představ si třeba Javu. Je následující korektní kód?
int a = 3 + "test";
Není. Proč? Protože ti nesedí typy. Teď si představ, že Java by měla switch, který vypne typovou konverzi, tohle se normálně zkompiluje a při běhu to vyhodí přesně specifikovanou výjimku. Stane se z toho korektní kód? Já bych řekl, že ne. Jenom prostě překladač v daném momentě není schopen/ochoten zkontrolovat, že ten kód, co jsi mu dal, je korektní a že je to blbě zjistí až při běhu.
Podobně máš třeba null pointer exception.
Object x = null; x.equals(x);
Tohle taky není korektní kód, ale typovou kontrolou ti projde, protože typový systém Javy tohle není schopen při kompilaci odhalit. V kotlinu už ty typy postavili trošku jinak, a najednou to ten typový systém odhalí.
A teď k Haskellu: je to lazy jazyk, takže všechny typy obsahují bottom. -XStrict to de-fakto v rámci toho modulu přepneš do strikt sémantiky; takže v rámci toho modulu typy přestanou obsahovat bottom. Když pak uděláš nějakou funkci ve stylu:
f :: Int -> Int
f 0 = error "Chyba"
f x = x
Tak to je nekorektní kód, protože z funkce, která by měla vracet Int vracíš bottom (resp. do následující funkce, která očekává Int bez bottomu to dopluje). To je typová chyba, akorát to překladač není schopen to zkontrolovat (mimo jiné, protože to je obecně nerozhodnutelný problém), takže se spoléhá na to, že uživatel v tomhle nelže. Jsou jazyky, které jsou schopny v typovém systému řešit, jestli typ obsahuje bottom nebo ne, haskell to neumí.
Pokud jde o souvislost s důkazem: to je takový pěkný poznatek, že typový signature je "tvrzení" a implementace funcke je "důkaz". (
https://wiki.haskell.org/Curry-Howard-Lambek_correspondence). Pokud ti z implementace nic nevypadne (což je bottom - nekonečné zacyklení), tak jsi nic nedokázal. No a speciálně v tom Strict režimu je to úplně přesně jako to dělení 0 v tom důkazu 0=1. Ty mechanicky klidně můžeš pokračovat dál, interpret klidně mechanicky bude vykonávat ten kód podle nějakých pravidel, možná to i povede k nějakému korektnímu výsledku, ale to nic nemění na tom, že ten důkaz je blbě.