Problém je v tom, že v Idrisu se mi nestane to, co se mi stane v C# v tom příkladu, který jsem uváděl. Že tu chybu neodchytím, tedy nezpracuji, tedy jsem tu chybu nezohlednil.
To je jedno ne? Hodnota toho typu nebude vytvořena, pokud konstruktor vyhodil výjimku...
Zákazník: Tak jsem zkoušel vaši aplikaci a je úplně k ničemu. Jsem tam normálně zadal číslo, a ono to spadlo.
Já: To je jedno ne?
Slušný vývojář tu výjimku odchytí a vypíše třeba “Sorry vole error”.
To je ale něco jiného, to spadlo, protože nebyla dobře ošetřena chyba, ne proto, že by byl porušen invariant.
To samé se stane v Rustu, pokud udělám `.unwrap()` na výsledku toho konstruktoru anebo v Haskellu, pokud bys např. v Either Left větvi udělal `error "shit's on fire yo"` ...
Ano, je to něco jiného. To je rozdíl mezi Idrisem a C#.
Idris:
kompilátor: hele, zapomněl jsi tady zohlednit tenhle scénář
já: nezajímá
kompilátor: mě taky ne, nepustím tě dál
já: ale já to chci přeložit.
kompilátor: nezajímá
já: štveš mě
kompilátor: nezajímá
já: grrr, SO, ha, mám to, musím tam narvat error()
kompilátor: když myslíš
já:
C#
kompilátor: přeloženo
reviewer: hele, hmm, neměl by si tady zohlednit tenhle scénář?
já: to se nestane
reviewer: no, já nevím
já: hele, šéfe, von mě zdržuje
šéf: to je v pořádku, pusť to
klient: ehm, pánové, to si to po sobě neumíte zkontrolovat? Padá to při třech scénářích
reviewer: třech?! Kde?