Typový system versus unittesty

Bacsa

Re:Typový system versus unittesty
« Odpověď #750 kdy: 22. 08. 2018, 13:09:24 »
Já myslím, že problém nebude v tom, že bychom si tu nedokázali představit nacpat velikost vektoru do jeho typu. To je celkem jednoduché a umí to kdejaký jazyk. Problém je v tom, že ta potřebná velikost prostě není k dispozici, dokud program neběží u zákazníka.
Ona ale je k dispozici, v existenčním typu.


Bacsa

Re:Typový system versus unittesty
« Odpověď #751 kdy: 22. 08. 2018, 13:15:53 »
Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole.
Toto je zásadní omyl. 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). Za to můžeme poděkovat Currymu a Howardovi (nezávisle). Můžu mít například funkci getVect, co mi načte od uživatele vektor nad ω libovolné délky (typu IO (Maybe ((n:Nat) ** Vect n Nat))). Where's the problem?

optimizer


Re:Typový system versus unittesty
« Odpověď #753 kdy: 22. 08. 2018, 14:47:20 »
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í.

optimizer

Re:Typový system versus unittesty
« Odpověď #754 kdy: 22. 08. 2018, 14:55:29 »
smysluplné použití závislostních typů je compile time kontrola tvarů matic a tenzorů.


Bacsa

Re:Typový system versus unittesty
« Odpověď #755 kdy: 22. 08. 2018, 14:56:24 »
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ě
A vo tom to je :)

A když už jsme u toho, víte o jiných jazycích se záv. typy krom Idrisu, Agdy a Coqu, zejména takových, co se používají v praxi v kritických aplikacích?

Re:Typový system versus unittesty
« Odpověď #756 kdy: 22. 08. 2018, 15:20:44 »
A když už jsme u toho, víte o jiných jazycích se záv. typy krom Idrisu, Agdy a Coqu, zejména takových, co se používají v praxi v kritických aplikacích?
Ony se podle mne tolik nepoužívají ani u kritických aplikací. Tam se to pokud vím řeší spíš tak, že je to naprogramované dvakrát nezávisle na sobě a běží to na dvou nezávislých zařízeních. Pokud se na výsledku neshodnou, následuje reset do nějakého bezpečného stavu.

v

Re:Typový system versus unittesty
« Odpověď #757 kdy: 22. 08. 2018, 15:25:56 »
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ě
A vo tom to je :)

A když už jsme u toho, víte o jiných jazycích se záv. typy krom Idrisu, Agdy a Coqu, zejména takových, co se používají v praxi v kritických aplikacích?
spark ada možná? ale to bude trochu zvláštní případ

v

Re:Typový system versus unittesty
« Odpověď #758 kdy: 22. 08. 2018, 15:35:13 »
A když už jsme u toho, víte o jiných jazycích se záv. typy krom Idrisu, Agdy a Coqu, zejména takových, co se používají v praxi v kritických aplikacích?
Ony se podle mne tolik nepoužívají ani u kritických aplikací. Tam se to pokud vím řeší spíš tak, že je to naprogramované dvakrát nezávisle na sobě a běží to na dvou nezávislých zařízeních. Pokud se na výsledku neshodnou, následuje reset do nějakého bezpečného stavu.
viz IEC61508

BoneFlute

  • *****
  • 1 909
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #759 kdy: 22. 08. 2018, 16:27:58 »
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.
Psal jsem hned můj první příspěvek: "získal jsem nezdravé přesvědčení". A nebo, že "A snažím se zchladit své nadšení hledáním, kde to má hranice." Taky jsem psal, že se snažím použít typy co to jde, a na zbytek testy.

Vidět v tom, že o tom nic nevím, nebo, že jsem si v tom našel modlu chce hodně fantazie.

Pište co k tomu víte. Na posuzování znalostí druhých tu máme Jirsáka.

ava

Re:Typový system versus unittesty
« Odpověď #760 kdy: 22. 08. 2018, 17:04:22 »
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.
Psal jsem hned můj první příspěvek: "získal jsem nezdravé přesvědčení". A nebo, že "A snažím se zchladit své nadšení hledáním, kde to má hranice." Taky jsem psal, že se snažím použít typy co to jde, a na zbytek testy.

Vidět v tom, že o tom nic nevím, nebo, že jsem si v tom našel modlu chce hodně fantazie.

Pište co k tomu víte. Na posuzování znalostí druhých tu máme Jirsáka.

Ok, beru osobní věci zpět. Každopádně můj příspěvek byl z výrazně větší části k tématu, možná bys tedy mohl zareagovat spíš na ty věcné kusy.

1) K původní otázce - psal jsem příklad, že podle mě není možné pomocí dependent typů ověřit korektnost funkce stringToNum: String -> Maybe Nat. V praxi je přitom asi v každém užitečném programu třeba parsovat uživatelský vstup, čili dělat něco podobného.

2) Už samotná otázka je, nevím jestli úmyslně, zavádějící: "Zajímalo by mě, můžete zkusit uvést nějaký příklad konstrukce, na kterou je nutné napsat test, protože typem to podchytit nejde?". Jak jsem uváděl v předchozím příspěvku, význam unit testů zdaleka není jen v tom, že ověřují správnost nějaké konstrukce. Jejich hodnota je i v dalších aspektech, které typy nemají.

Speedy

Re:Typový system versus unittesty
« Odpověď #761 kdy: 22. 08. 2018, 18:48:56 »
Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole.
Toto je zásadní omyl. 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). Za to můžeme poděkovat Currymu a Howardovi (nezávisle). Můžu mít například funkci getVect, co mi načte od uživatele vektor nad ω libovolné délky (typu IO (Maybe ((n:Nat) ** Vect n Nat))). Where's the problem?
K tomu IO, nechápu význam IO (), proč to může jít do >>=, když ten vnitřní typ nemá žádné hodnoty?

v

Re:Typový system versus unittesty
« Odpověď #762 kdy: 22. 08. 2018, 18:53:25 »
Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole.
Toto je zásadní omyl. 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). Za to můžeme poděkovat Currymu a Howardovi (nezávisle). Můžu mít například funkci getVect, co mi načte od uživatele vektor nad ω libovolné délky (typu IO (Maybe ((n:Nat) ** Vect n Nat))). Where's the problem?
K tomu IO, nechápu význam IO (), proč to může jít do >>=, když ten vnitřní typ nemá žádné hodnoty?
() je normální hodnota
Kód: [Vybrat]
Idris> ()
() : ()

Bacsa

Re:Typový system versus unittesty
« Odpověď #763 kdy: 22. 08. 2018, 18:58:05 »
Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole.
Toto je zásadní omyl. 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). Za to můžeme poděkovat Currymu a Howardovi (nezávisle). Můžu mít například funkci getVect, co mi načte od uživatele vektor nad ω libovolné délky (typu IO (Maybe ((n:Nat) ** Vect n Nat))). Where's the problem?
K tomu IO, nechápu význam IO (), proč to může jít do >>=, když ten vnitřní typ nemá žádné hodnoty?
() je normální hodnota
Kód: [Vybrat]
Idris> ()
() : ()
() je typ ;) Je to void bez hodnot.

v

Re:Typový system versus unittesty
« Odpověď #764 kdy: 22. 08. 2018, 19:04:52 »
Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole.
Toto je zásadní omyl. 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). Za to můžeme poděkovat Currymu a Howardovi (nezávisle). Můžu mít například funkci getVect, co mi načte od uživatele vektor nad ω libovolné délky (typu IO (Maybe ((n:Nat) ** Vect n Nat))). Where's the problem?
K tomu IO, nechápu význam IO (), proč to může jít do >>=, když ten vnitřní typ nemá žádné hodnoty?
() je normální hodnota
Kód: [Vybrat]
Idris> ()
() : ()
() je typ ;) Je to void bez hodnot.
neřekl bych, viz https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Builtins.idr
() je Unit, typ s jednou hodnotou