Já myslím, že je problém v tom, že jsi se neobtěžoval odpovědět na tu otázku ohledně toho, co považuješ za korektnost programu. Ta otázka byla v tom stylu, jestli, za předpokladu, že ten program dává správné výsledky a v jazyce neexistují konstrukce s nedefinovaným chováním, jestli vůbec je možné v takovém jazyce napsat nekorektní program. Vypadá to, že ta odpověď by měla znít "ANO", ale ty jako židle trváš na svém a strašně se bojíš mi na cokoliv takového odpovědět.
Stejně tak otázka byla, jestli ten program s těmi chybnými typy, ale který lze přeložit s defer-type-check je korektní a opět by odpověď měla být ANO. Ale ty se prostě bojíš diskutovat. Člověk by čekal, že si za svým názorem budeš stát, ale ty se bojíš.
Navíc když se podíváš do těch 20 let starých paperů, kde ty výjimky zaváděli, tak ti lidi v té době přesně takhle, jako ty, mysleli. Akorát že od té doby uteklo hodně vody a dneska se ten náhled trošku změnil. S bottom se strašně blbě pracuje, to, co před 20 lety vypadalo jako skvělý nápad se ukázalo jako v zásadě naprosto nepoužitelné. Ona to prostě je chyba programu. No a dneska s různými snahami o formální verifikace a odstranění chybných stavů se od toho totálně upustilo. Naopak se hodně pracuje s různými zaměnami typů, čistě prakticky pak s tím, jak jednoduše vyrábět třeba ty unit-testy na non-pure kód apod. A tohle všechno prostě přestane fungovat, pokud ten program dojde do nekorektního stavu.
Ono to fakt je něco ve stylu null-pointer-exception. Vzhledem k tomu, že na UNIXu je to všechno definované, pak lze tímto způsobem (na UNIXu) vyrobit korektní program. Splňuje všechny tvé požadavky... které se domnívám, že bereš pod pojmem "korektní".
Takže ano, z hlediska operational-semantics to korektní je. Což už říkám asi tak od začátku. Z hlediska smyslu těch rovnic nikoliv. Což taky říkám od začátku. Ano, je to akademické. Ono vůbec Haskell je takový akademický. Není pro lopaty.
Mimochodem co máš pořád s tím undefined? Já nechytám undefined. Chytám aritmetickou výjimku, to není undefined.
Celý rozdíl mezi undefined a aritmetickou výjimkou je to, že to je jiný typ. Tak asi na té úrovni, že z jednoho vylítně "UserError" a z druhého "ArithException". V pure kódu se to chytnout nedá, v IO se to liší akorát v typu. Já tu větu pochopil, že se to v něčem zásadním liší... a vysvětlil bys mi teda v čem?
Ale víš, tohle je sranda - fakt mě baaaaví, jak píšeš že tomu nerozumím, to je fakt psina... ale teď jsem si prošel svoje zdrojáky, a kromě toho, že v těch starších místo "throwIO . userError" používám přímo "error" (protože holt se člověk učí..), tak asi tak v 95% případů v pure funkcích tam u toho jsou popisky "internal errror, cannot happen", v 5% "nebudu řešit chybu v dekódování toho, co jsem sám zakódoval, slítni" a v 0% ve stylu "signalizuj něco někam, kde se to chytá".
Takže když tady přijdeš s tím, že Haskell je strašný jazyk, jak XStrict může rozbít kód...tak mi to připadá...poněkud úsměvné. Programy, které to rozbije, si to zaslouží, jakýkoliv náznak nějaké formální verifikace by je vyhodil z okna i s tím programátorem.