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.
Já v těch závislostních typech nejsem kovanej, takže takto si to předstvuju v pseudokódu, jak to chápe typový systém:
parseFromDec :: Str -> Int = ('0' -> 0) | ('1' -> 1) | ... | ('9' -> 9)
případně
parseFromDecM :: Str -> Maybe Int = ('0' -> Just 0) | ('1' -> Just 1) | ... | ('9' -> Just 9) | _ -> Nothing
Plus nějaká recurze.
Zkusím tady nadhodit myšlenkový experiment, který snad ukáže, co se mi celé na té myšlence náhrady testů typy nelíbí.
Testy by vypadaly asi takhle (pseudokód):
assert(parseFromDecM "0" == Just 0)
assert(parseFromDecM "42" == Just 42)
assert(parseFromDecM "foo" == Nothing)
assert(parseFromDecM "" == Nothing) // Empty string is not a zero, but parse error
assert(parseFromDecM " 42" == Nothing) // Whitespace results in parse error
∀x: Int( assert(parseFromDecM . toString x == Just x ) // quickcheck test
Když píšu TDD, tedy nejprve testy, rovnou si rozmyslím, co má implementace umět. Dovedu si třeba dost představit, že naivní implementace by pro prázdný string vrátila 0. Neříkám že je to nutně špatně, ale možná že jo, a určitě je dobré mít takové chování zdokumentované. Když píšu testy first, ještě před implementací si chování rozmyslím. Navíc jsem vybral takové příklady, které dobře vystihují "ideu" chování, tady si myslím přesný opak toho co ty, testy jsou pro vystižení myšlenky funkce dost užitečné, naopak nějaké generátory unit testů tam tu "intuici za smyslem funkce" nemají moc šanci postihnout.
A teď dejme tomu, že bych chtěl implementovat tu samou funkci v nějakém vysněném jazyce s typovým systémem který mi umožní úplně všechno co chci.
Když jí dám typ
String -> Maybe Int, je možné udělat nekorektní implementaci, to je z typu evidentní. Není například jasné, jestli je převod každé jedné číslice správně implementován (je to převod z binární soustavy? šestnáctové? desítkové?).
Tak do typu přidáme omezení na převodní funkci:
String -> (Char -> Maybe Int) -> Maybe Int.
Pořád můžeme mít nekorektní implementaci. Co když by funkce brala znaky ze stringu v opačném pořadí? V rekurzi a násobení základem 10 se člověk snadno sekne... Tak přidáme nějaké hypotetické omezení TraversalOrder. Typová signatura nám naroste na
String -> (Char -> Maybe Int) -> TraversalOrder -> Maybe Int. Ale chybí nám tu vlastně ten základ 10, kterým se to má násobit, a ten je navíc svázaný s funkcí ze znaku do čísla. No tak uděláme nějaké
String -> ({convertDigit: Char -> Maybe Intů base: Int}) -> TraversalOrder -> Maybe Int. A taky potřebujeme nějak zahrnout speciální případ, že prázdný string není Just 0 ale Nothing. Naštěstí můj typový systém umí trochu číst myšlenky:
OnEmptyInputNothing: String -> ({convertDigit: Char -> Maybe Int, base: Int}) -> TraversalOrder -> Maybe Int. Taky bych asi měl dodat, že všechny znaky se skutečně použijí, atp.... Každopádně pokud bych chtěl pomocí typového systému opravdu dokázat 100% korektnost implementace, v zásadě musím v tom typovém systému tu implementaci nakonec naimplementovat znovu, což jaksi nedává smysl, a jak už tu někdo psal, stejně bych pak asi pro jistotu ještě musel napsat testy na ty typy...
Možná, opravdu jen možná, by se z těchto základních patternů dali komponovat/odvozovat složitější třeba pro ten polygon.
Z typu funkce to asi zřejmé nebude. Ale když by ten stroj dokázal vygenerovat ukázky na požádání?
Myslím, že alespoň v tom, co dělám já, by ty ukázky často byly k ničemu. Třeba u toho polygonu by ze stroje vypadla řada čísel - souřadnic bodů polygonu, ale dokud si to nenakreslíš, tak nevidíš co to vlastně testuje. A to už je jednodušší si ty zajímavé příklady nejprve nakreslit a potom je, u komplikovaných případů třeba i okomentované a s naskenovaným obrázkem, zadat do unit testů.
976 Odpovědí
127174 Zhlédnutí