Vlákno názorů k článku Datové typy Option, Result a Array v programovacím jazyku OCaml od Calculon - Už klasicky bezpečný divide v Leanu (bez monád)...
-
Oprav mě, pokud se pletu.
Pokud je možné nějaký (validační) problém vyřešit pomocí Option, je to lepší jak závislostní/rovnostní/anything typy, protože je to rychlejší.
Aktuálně se domnívám, že na problémy typu dělení nulou jsou nejlepší způsob Checked exceptions. Protože jsou ideálním kompromisem výkonu a čitelnosti. (Ještě nejlíp, když by to bylo ve skutečnosti jen zamaskované Option :-))Postrádám nějaké pěkné demonstrace ne v čem Lean řeší problémy jinak, ale s čím si Lean poradí, zatímco jiné jazyky to nedokážou.
Abychom si rozuměli, třeba právě dělení nulou tento případ není. Obvykle totiž nemáš problém v tom, že ti funkce calculate(15, 65) zbuchne na dělení nulou, ale že ti zbuchne calculate(uservstup1, uservstup2). Takže potřebuješ kontrolu zda počítáš s neočekávaným, což už mainstreamové jazyky umějí.
-
Option je pomalejší, protože přidává režii za běhu. Typy se řeší jen při překladu (takže teoreticky můžou zpomalit překlad, to ostatně dělají i implicitní koerce, proto je vyhodili ze Swiftu). Příklad s dělením není moc zajímavý, protože je triviální, ale je převzatý z článku.
V praxi se používá kombinace. Option/Result je de facto standard (v Haskellu se to tak píše dekády a rozšířilo se to i jinam, protože se to osvědčilo) a pochopí to každý, to je výhoda. Sofistikované typy dává smysl používat někde hluboko v knihovnách, kde jsou schované, dělají svou užitečnou práci a nematou běžného Pepu :)
Jinak samozřejmě platí to o "exhaustive unit tests", ale to taky chce podporu standardní knihovny jazyka a vysokou úroveň abstraktního myšlení.
-
Rozumím. Jako čistě teoreticky je asi možné, že ten Option bude něco málo žrát, a ano uvědomuji si, že Typy řeší compiletime, ale má poznámka směřoval k tomu, že:
1/ těch míst, kde by typy tu aserci vyhodili jako nepotřebnou a kompilátor s Option ne bude malinko. V drtivé většině případů ty Typy udělají úplně to samé a vynutí logiku do runtime stejně jako Option.
2/ že Option je hnusnej. -
Jestli “asercí” myslíš tu podmínku, tak tu překladač odstraní vždy, ta je jen pro typovou kontrolu a za běhu reprezentaci nemá (je to i popsané v dokumentaci).
Obecně jde asi spíš o signaturu, funkce bez Option je hezčí a obecně je rozumnější, když validaci dělá volající. Nic víc bych v tom nehledal.
-
Samozřejmě to zajistí nenulovost v době překladu. Dělitel je třeba připravit pomocí NonZeroUsize::new(x), což vrací Option<NonZeroUnsize> a nevhodnou hodnotu to prostě odmítne. To znamená, že se ta invalidní hodnota vyřeší někde na vstupu, což je stejně obecně nutno dělat v každém jazyce, pokud se vstup čte zvenku.
-
“kdyz je typovej system takto silnej, je to pekne”
Bych nejásal ;)
https://doc.rust-lang.org/stable/std/num/struct.NonZeroUsize.html#method.new_unchecked
Tento typ je brutální antipattern.
-
Ale jo prakticky to urcite tak nevadi. Urcite solidnejsi a lepsi reseni nez v jakemkoliv mainstream jazyku. Ale to pak to deleni nulou lze osetrit podobne v kazdem jayzce jako v tom Rustu s trochou práce.
Ja teda produkcni software s dependent types tedy nevidel, to je fakt, ale lze s nima modelovat fakt precizne.12. 10. 2023, 17:38 editováno autorem komentáře
-
radekmStříbrný podporovatel
Ja teda produkcni software s dependent types tedy nevidel, to je fakt, ale lze s nima modelovat fakt precizne.Ano, dokonce tak, že není třeba psát ani ty programy a stačí psát pouze typy.
Třeba do OCamlu extrahuje verifikované programy Coq. A tam už pár netriviálních programů existuje: https://github.com/coq-community/awesome-coq#verified-software Blbé je, že OCaml není verifikovaný, takže tam se to může rozbít.
Problém je, že by člověk potřeboval verifikovaný kompilátor, os i hw.
-
My ale nepotrebujeme hneď nejaký dokolaný jazyk. Stačí aby sa táto pokročilá práca s typmi postupne dostala do mainstreamu, tak ako funkcionálne programovanie a kvalita progamov sa zvýši.
Unit tests with exhaustive coverage -- another name for mathematical theorems.
https://www.youtube.com/watch?v=8WFMK0hv8bE
Pekne to vysvetľuje v tomto videu jeden matematik na príklade Agdy. Pokročílá práca s typmi môže trebárs v budúcnosti nahradiť unit testy.
-
radekmStříbrný podporovatel
Pak překladač musí dokázat, že dělitel je nenulový. Což může být pro překladač o občas i pro člověka celkem netriviální.
Nebo to má třeba jako Isabelle možnost napojení automatických dokazovačů?
