Jestli je ten program korektní z hlediska výstupu, o tom nerozhoduješ ty, ale uživatel.
Tak to bude problém, protože my se tu nebavíme, zda je korektní z hlediska výstupů. Bavíme se o tom, jestli ten program jako takový dává smysl. Vrátím se k důkazu, že 0=1. Když vezmeš výsledek, vynásobíš obě strany 0 a přičteš 5, vyjde ti "5=5". A to je "korektní výstup". Ale celý ten důkaz je blbě.
Ty pořád přemýšlíš na úrovni "operational semantics" - mám tady interpret/překladač, a pokud program, který jsem do něj dal, používá pouze funkce dle specifikace a dává správné výsledky, pak je "korektní". Takže ten důkaz "5=5" by byl korektní.
Tenhle přístup se v haskellu vůbec nepoužívá. Je to funkcionální programování, celý program je zápis nějaké funkce, které vyjadřuje nějakou transformaci světa z jednoho stavu do jiného. A korektní program je takový, který je ekvivalentní specifikaci toho problému, který řešíš. V momentě, kdy se ti tam vyskytne "undefined", tak to není korektní. Ne, že by se občas takové programy nepsaly, ale prostě to není korektní a můžeš očekávat, že ti prostě jazyk v ten moment toho bude garantovat výrazně méně. Třeba ti přestane garantovat, že Strict -> Lazy transformace je ekvivalentní.
Mně celkem pobavilo, jak se strašně snažíš tvrdit, že to je "akademický jazyk" - ale pokud bys chtěl haskell mít v tomhle akademický, tak bys tam měl typy bez bottom (přitom by to bylo lazy) a ty tvoje programy by tím vůbec neprošly. Jenomže takovéhle jazyky jsou strašně těžko použitelné (protože programátor musí dokazovat, že jsou všechny funkce totální). Takže v Haskellu to dokazovat nemusíš, typy obsahují bottom, ale když se ti tam nějaký bottom dostane, tak neseš následky. Deterministické následky, ale ten tvůj program pak prostě není korektní.
To je v rozporu s něčím v Haskell language report? Říká se tam, že se to nesmí dělat? Neříkám, že je to best practice, ale reálně to lidi (minimálně začátečníci) dělají: https://stackoverflow.com/questions/20822365/how-to-catch-a-divide-by-zero-error-in-haskell?answertab=votes#tab-top
V rozporu? Ne. Jenom to není korektní program. Ten příklad ze stackoverflow je v pohodě - něco zkusil provést a slítlo to. Rozbitý program, informujeme uživatele, že to celý upadlo a proč. Nikdo se netváří, že to funguje korektně. Pro některé typy programů je to zcela dostačující, nevadí, že to crashne na vadném vstupu. Ale nikdo se taky netváří, že v takovém případě program pracuje korektně. Což je to, co tvrdíš ty.