Typový system versus unittesty

[Bacsa]

Důležitější je asi obsah, než název. Název vlákna naznačuje, že jde o srovnání, ale text prvního příspěvku je jednoznačný pokus (úspěšný) o rozpoutání flamewar.

Já jsem o žádné flamewar zájem neměl. Text mého příspěvku k flamewar nenabádal. Ale beru tě jako nutné zlo.

Teď by tu všichni měli udělat krok zpět, nastudovat si ten Idris a pak pokračovat v debatě.

[Reklama]

[Filip Jirsák]

Teď by tu všichni měli udělat krok zpět, nastudovat si ten Idris a pak pokračovat v debatě.

Myslíte opravdu nastudovat, takže se tu sejdeme znova za pět let? Protože debatu „během půl hodiny jsem si něco přečetl a dospěl jsem k nezdravému přesvědčení“ už tu máme…

[v]

Teď by tu všichni měli udělat krok zpět, nastudovat si ten Idris a pak pokračovat v debatě.

Myslíte opravdu nastudovat, takže se tu sejdeme znova za pět let? Protože debatu „během půl hodiny jsem si něco přečetl a dospěl jsem k nezdravému přesvědčení“ už tu máme…

já bych navrhl začít s přirozenýma číslama a vektorama, to by pro tuto debatu mohlo stačit (substr...)

[JSH]

já bych navrhl začít s přirozenýma číslama a vektorama, to by pro tuto debatu mohlo stačit (substr...)

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.

Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole. Pokud se ta typová kontrola bude provádět až zákazník načte data, tak si musím napsat testy i na ty typy.

[v]

Kód: [Vybrat]

*../idr/test> :t mysubstr
mysubstr : (p : Nat) -> (n : Nat) -> Vect (p + (n + more)) t -> Vect n t
*../idr/test> mysubstr 1 2 [10,20,30,40]
[20, 30] : Vect 2 Integer
*../idr/test> mysubstr 3 2 [10,20,30,40]
(input):1:15-16:When checking argument xs to constructor Data.Vect.:::
        Type mismatch between
                Vect 0 elem (Type of [])
        and
                Vect (S more) t (Expected type)
        Specifically:
                Type mismatch between
                        0
                and
                        S more

<3

[Reklama]

[listoper]

Kód: [Vybrat]

*../idr/test> :t mysubstr
mysubstr : (p : Nat) -> (n : Nat) -> Vect (p + (n + more)) t -> Vect n t
*../idr/test> mysubstr 1 2 [10,20,30,40]
[20, 30] : Vect 2 Integer
*../idr/test> mysubstr 3 2 [10,20,30,40]
(input):1:15-16:When checking argument xs to constructor Data.Vect.:::
        Type mismatch between
                Vect 0 elem (Type of [])
        and
                Vect (S more) t (Expected type)
        Specifically:
                Type mismatch between
                        0
                and
                        S more

<3

Trvalo mi asi 10 minut nez jsem to pochopil, a pak jsem musel dalsich 10 minut rozdychavat ten naval endorfinu 

[ava]

Kód: [Vybrat]

*../idr/test> :t mysubstr
mysubstr : (p : Nat) -> (n : Nat) -> Vect (p + (n + more)) t -> Vect n t
*../idr/test> mysubstr 1 2 [10,20,30,40]
[20, 30] : Vect 2 Integer
*../idr/test> mysubstr 3 2 [10,20,30,40]
(input):1:15-16:When checking argument xs to constructor Data.Vect.:::
        Type mismatch between
                Vect 0 elem (Type of [])
        and
                Vect (S more) t (Expected type)
        Specifically:
                Type mismatch between
                        0
                and
                        S more

<3

Hezké, ale teď mě zajímá klíčová otázka: jak se to použije když budu chtít udělat prográmek, který přečte ze stdin p, zavolá na to mysubstr p 2 [10,20,30,40] , a výsledek vytiskne? Programy bez IO moc užitečné nebývají, že.. Poprosil bych přímo zdroják, je už to jen krůček... ?

[v]

Hezké, ale teď mě zajímá klíčová otázka: jak se to použije když budu chtít udělat prográmek, který přečte ze stdin p, zavolá na to mysubstr p 2 [10,20,30,40] , a výsledek vytiskne? Programy bez IO moc užitečné nebývají, že.. Poprosil bych přímo zdroják, je už to jen krůček... ?

předpokládám, že jste to zkusil napsat a nefunguje vám to, postněte tady váš kód a zkusíme to odladit

[optimizer]

předpokládám, že jste to zkusil napsat a nefunguje vám to, postněte tady váš kód a zkusíme to odladit

potom mu neodpovíš, jak je tu zvykem. Protože sám nevíš, jak to napsat. Doufám, že s vámi ava nebude ztrácet čas, dokud neukážete váš kód.

[JS]

Dospěl jsem k nezdravému přesvědčení, že jednotkové testy nejsou potřeba máte-li kvalitní typový systém.

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?

No, je nejde (teoreticky) a nejde (prakticky).

Ja jsem dospel k presvedceni, ze testovat auta neni potreba, pokud je umite matematicky modelovat dokonale na urovni kazde molekuly.

Ostatne, je nejaky priklad konstrukce, kterou je nutne testovat v realnem svete, protoze ji nejde simulovat matematicko-fyzikalnim modelem?

[ava]

Hezké, ale teď mě zajímá klíčová otázka: jak se to použije když budu chtít udělat prográmek, který přečte ze stdin p, zavolá na to mysubstr p 2 [10,20,30,40] , a výsledek vytiskne? Programy bez IO moc užitečné nebývají, že.. Poprosil bych přímo zdroják, je už to jen krůček... ?

předpokládám, že jste to zkusil napsat a nefunguje vám to, postněte tady váš kód a zkusíme to odladit

Nezkusil, a ani nevím jak na to. Opravdu prosím, obětujte 10 minut svého času, napište to a postněte to (přeložitelnou a spustitelnou verzi).

[Bacsa]

Teď by tu všichni měli udělat krok zpět, nastudovat si ten Idris a pak pokračovat v debatě.

Myslíte opravdu nastudovat, takže se tu sejdeme znova za pět let? Protože debatu „během půl hodiny jsem si něco přečetl a dospěl jsem k nezdravému přesvědčení“ už tu máme…

Pět let ne, stačilo by jen pochopit ty závislostní typy. Klidně i v jiném jazyce nebo jen ten teoretický koncept. Ono to není složité, pokud už chápete Curry-Howardovu korespondenci.

[Bacsa]

já bych navrhl začít s přirozenýma číslama a vektorama, to by pro tuto debatu mohlo stačit (substr...)

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.

Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole. Pokud se ta typová kontrola bude provádět až zákazník načte data, tak si musím napsat testy i na ty typy.

To je brutální nepochopení závislostních typů. Který “kdejaký” jazyk to umí?

[JSH]

já bych navrhl začít s přirozenýma číslama a vektorama, to by pro tuto debatu mohlo stačit (substr...)

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.

Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole. Pokud se ta typová kontrola bude provádět až zákazník načte data, tak si musím napsat testy i na ty typy.

To je brutální nepochopení závislostních typů. Který “kdejaký” jazyk to umí?

Přidat do typu rozsahy hodnot a i nějaký ten výraz s abstraktními proměnnými se dá i v C++ šablonách. Jasně, je to hnus a generuje to bloat, ale principielně to jde. Hrál jsem si právě s rozsahy polí a intů. Problém nastal na rozhraní kontrolovaného a normálního kódu. A ty kousky kontrolovaného kódu nemůžou být kdovíjak rozsáhlé, protože je to pro netriviální problémy občas i nerozhodnutelné.

Jedna věc je napsat funkci, ve které nemůže dojít k chybě. Druhá věc je tu funkci zavolat na reálná data. Zavolat to v konzoli přes REPL toho moc neukáže.

[Bacsa]

já bych navrhl začít s přirozenýma číslama a vektorama, to by pro tuto debatu mohlo stačit (substr...)

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.

Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole. Pokud se ta typová kontrola bude provádět až zákazník načte data, tak si musím napsat testy i na ty typy.

To je brutální nepochopení závislostních typů. Který “kdejaký” jazyk to umí?

Přidat do typu rozsahy hodnot a i nějaký ten výraz s abstraktními proměnnými se dá i v C++ šablonách. Jasně, je to hnus a generuje to bloat, ale principielně to jde. Hrál jsem si právě s rozsahy polí a intů. Problém nastal na rozhraní kontrolovaného a normálního kódu. A ty kousky kontrolovaného kódu nemůžou být kdovíjak rozsáhlé, protože je to pro netriviální problémy občas i nerozhodnutelné.

Jedna věc je napsat funkci, ve které nemůže dojít k chybě. Druhá věc je tu funkci zavolat na reálná data. Zavolat to v konzoli přes REPL toho moc neukáže.

IMHO je důležité, aby s těmi hodnotami v typech šla dělat aritmetika a podobné “výpočty”. Jak to je v C++ nevím, ale tam to bude asi dost omezené. V jazycích jako zmíněný Idris (nebo třeba Coq, ten ale blíže neznám) je typový systém v podstatě dokazovač, kde jde napsat libovolná logická formule s proměnnými.