dostat ze stdin Nat by mělo být triviální
Jak se to dělá?
načte se řetězec a pak se z něj udělá Nat
*Data/String> the (Maybe Nat) (parsePositive "1")
Just 1 : Maybe Nat
Jde o to, jak načtu Nat po kompilaci. Nat je typ s teorií následník/nula, ne? To bych musel nejdřív načíst číslo a pak program přeložit se vstupem jako konstantou.
hm, to by bylo blbé
Měl jsem za to, že tento problém každý vidí.
No pro mě právě tohle taky bylo záhadou. Trochu mi pomohly následující články:
https://stackoverflow.com/questions/48128884/https://news.ycombinator.com/item?id=12349899tedy pomohly spíš tak, že už vidím, že na konci tunelu může být světlo, než že by se mi vysloveně rozsvítilo.
Každopádně co se týče (abych trochu poskočil v tématu) původního dotazu BoneFluteho, mám dost podobný dojem jako Jirsák, že BoneFlute našel novou modlu, o které téměř nic neví, ale o to více ji chválí. Tím dependent typy nechci shazovat, je možné že se v budoucnu ukáží užitečné a rozšíří se. Abych ovšem byl také trochu konstruktivní a vyjádřil se k původnímu dotazu, podle mě dependent typy nemohou nahradit unit testy v následujícím:
Dependent typy z principu nemohou dokázat korektnost např. převodu stringu na číslo. Jak by se v typu fce convert: String -> Maybe Nat vyjádřilo, zda se očekává stringový vstup v desítkové nebo šestnáctkové soustavě? Podle mě je to principiálně nemožné, a stejně tak není možné ani vyjádřit korektnost implementace převodu. V Idris se asi dá vyjádřit, že funkce doběhne, a že nezpanikaří, ale to je málo.
Unit testy slouží jako vždy up-to-date dokumentace. U jednoduchých věcí se dá samozřejmě hodně věcí vyčíst z typů (hezký příklad je tady:
http://funkcionalne.cz/2014/08/types-will-carry-you-over-the-monads/), ale u složitějších je prostě hezké mít chování zdokumentované na příkladech, místo potřeby rozjímat nad důsledky komplikované typové signatury. Navíc je slušnost mít knihovny zdokumentované, tak proč to rovnou nedělat unit testy? (podívejte např. sem:
https://doc.rust-lang.org/std/iter/trait.Iterator.html), všechny Examples jsou rovnou spustitelné unittesty zapsané do docstringů funkcí.
Unit testy jednoduchým způsobem ověřují chování v krajních a nečekaných případech. Když jsem psal implementaci funkce testující, zda je bod uvnitř polygonu, rovnou napíšu test, jak se chová bod na hraně, jak se chová v polygonu, který není uzavřený, jak se chová v polygonu který protíná sám sebe. Nedovedu si představit, jak by mohlo být takové chování zřejmé z typu funkce. Možná, až BoneFlute přestane "být stále student", nějak pěkně to vyřeší, to by mě pak docela zajímalo.
Unit testy jsou šablony funkčního kódu, který používá knihovnu kanonickým způsobem. Kód mohu copy'n'pastnout do vlastního projektu a upravit podle potřeby. Typy tohle neumí.
Na závěr: Typy a unit testy se doplňují, líbí se mi tahle asi minuta a půl:
https://www.youtube.com/watch?v=pMgmKJyWKn8&feature=youtu.be&t=317
976 Odpovědí
127185 Zhlédnutí