Typový system versus unittesty

Bacsa

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


Re:Typový system versus unittesty
« Odpověď #721 kdy: 21. 08. 2018, 07:02:59 »
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

Re:Typový system versus unittesty
« Odpověď #722 kdy: 21. 08. 2018, 07:54:48 »
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

Re:Typový system versus unittesty
« Odpověď #723 kdy: 21. 08. 2018, 09:55:02 »
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

Re:Typový system versus unittesty
« Odpověď #724 kdy: 21. 08. 2018, 11:31:25 »
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


Re:Typový system versus unittesty
« Odpověď #725 kdy: 21. 08. 2018, 12:40:41 »
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

Re:Typový system versus unittesty
« Odpověď #726 kdy: 21. 08. 2018, 12:54:17 »
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

Re:Typový system versus unittesty
« Odpověď #727 kdy: 21. 08. 2018, 13:10:39 »
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

Re:Typový system versus unittesty
« Odpověď #728 kdy: 21. 08. 2018, 13:24:09 »
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

Re:Typový system versus unittesty
« Odpověď #729 kdy: 21. 08. 2018, 13:35:12 »
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

Re:Typový system versus unittesty
« Odpověď #730 kdy: 21. 08. 2018, 13:47:49 »
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

Re:Typový system versus unittesty
« Odpověď #731 kdy: 21. 08. 2018, 13:48:46 »
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

Re:Typový system versus unittesty
« Odpověď #732 kdy: 21. 08. 2018, 13:50:49 »
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

Re:Typový system versus unittesty
« Odpověď #733 kdy: 21. 08. 2018, 16:10:23 »
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

Re:Typový system versus unittesty
« Odpověď #734 kdy: 21. 08. 2018, 16:19:20 »
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.