Nad záv. typy se korektnost dokazuje symbolicky, nevadí, není-li nějaká hodnota známa. Matoucí IMHO je, že se tomu říká typová kontrola, kterou lidi znají tak nanejvýš z Javy nebo céčka (pythonisti a spol. vůbec).
Nevidím nic matoucího na tom, že se to nazývá typová kontrola – je to přesně to, co lidé znají z JavaScriptu, Pythonu, C nebo Javy, akorát je to na škále důslednosti kontrol ještě dál, než Java nebo C. A tím, jak je to na škále ještě dál, zvětšuje se množství chyb, které dokáže typová kontrola odhalit, a zároveň jsou ty typy čím dál víc svazující a musí se různě „obcházet“.
U dynamicky typovaných jazyků je s hodnotami pracuje tak, že teprve když něco od hodnoty potřebuju, zjistím, zda je požadovaného typu. Třeba uživatel něco zadá, a teprve tam, kde s tím chci pracovat jako s číslem, zjistím, jestli to číslo je. Když někdo přejde na C nebo Javu, může mu připadat svazující, že musí typ určit dopředu a problém s tím, že uživatel nezadal číslo, musí řešit daleko dřív, třeba i zbytečně, protože by se k tomu zpracování jako čísla ani nedostal. Podobně svazující jsou dál generické typy, třeba u kolekcí – bez generických typů si do kolekce naházím jaké objekty mne napadne, a typy řeším až při jejich použití. S generickými kolekcemi najednou musím řešit typ prvků a mám problém do jedné kolekce dostat různé typy. Spousta věcí se přitom vyřeší tak, že „to nemůže nastat“. Třeba vím, že do kolekce strkám jenom stringy, takže nemusím řešit, že by se tam objevilo něco jiného. A závislostní typy jdou ještě dál.
Třeba obyčejné sčítání dvou čísel. V C nebo Javě sečtu dvě 32bitová čísla, a výsledek uložím opět do 32bitové hodnoty. Protože vím, že se tam budou sčítat malá čísla a přetečení „nemůže nastat“. Závislostní typy tohle neumožní, součet dvou 32bitových čísel musím uložit jako 64bitové číslo (nebo jako 33bitové, pokud bude takový typ povolen). A k tomu můžu chtít přičíst další číslo, a můžu dokonce chtít udělat sumu neznámého prvku čísel. Najednou musím řešit „hypotetické“ problémy, které bych v Javě nebo C řešit nemusel, protože přece vím, že tak velká čísla se tam nikdy sčítat nebudou – a jestli bude mít někdo problém, že se suma transakcí na jeho bankovním účtu nevejde do 32bitového čísla, tak mu to rád za nějaké promile z jeho zisku upravím. Stejně tak v Javě nebo C musím řešit „hypotetické“ problémy, které bych nemusel řešit v dynamicky typovaném jazyce.
Přísnost typové kontroly je pak jenom otázka míry, nalezení optimální hranice, kdy při dalším zpřísňování kontrol už nenajdu žádné reálné chyby, za to budu muset řešit „hlouposti“ typu „co kdyby firma měla trilion zaměstnanců“. Když pojedu vlakem, budu radši, když zabezpečovací zařízení bude používat závislostní typy a bude logicky dokázané, že nemůže pustit dva vlaky proti sobě (pokud o nich ví, že), u multimideálního systému pro výběr videa zabudovaného v sedačce přede mnou mi naopak vůbec nebude vadit použití dynamického typování.
976 Odpovědí
127191 Zhlédnutí