Typový system versus unittesty

[listoper]

...
A kdyz zakomponuju overeni spravnosti do konstrukce navratoveho typu zarucim tim ze nepujde vytvorit navratovy typ obsahujici nespravny vysledek.

Huh?

Ano je to v podstate znovuimplementace jinak, ...

Asi tak.

Nekde tady byla otazka na kvadratickou rovnici.
Zkusim tu myslenku v te citaci ukazat na tom.
Podotykam moji myslenku z te citace a ne kompletne problem reseny v tomto vlakne.
BoneFlute se z toho osype, protoze to neni ani zdaleka to o cem mluvil on.
A taky protoze to bude v jazyce velmi podobnem jave :-)
Vlastne jedinny rozdil proti jave je, ze umi presne floating point operace.

Kód: [Vybrat]

    final static RuntimeException up = new IllegalArgumentException("Does not compute");

    private static Result getRoots(double a, double b, double c){
        double detBody = b*b - 4*a*c;
        if(detBody < 0){
            throw new IllegalArgumentException("Fuck it! I don't have imaginary friends. " + detBody);
        }
        double det = Math.sqrt(detBody);
        double root1 = (-b + det)/2*a;
        double root2 = (-b - det)/2*a;
        return new Result(a,b,c,root1,root2);
    }

    static class Result {
        double root1; double root2;

        Result (double a, double b, double c, double root1, double root2){
            if(root1 + root2 != -(b/a) || root1*root2 != c/a) throw up;
            this.root1 = root1;
            this.root2 = root2;
        }
    }


[Reklama]

[listoper]

Ten prispevek je prece o generativnim testovani u dynamicky typovaneho jazyka.
Za behu prece nebudu zapinat "typovou" instrumentaci.

Jak zakomponujete ověření správnosti výsledku do konstukce návratového typu, aby se to ověření nedělalo až za běhu, ale už při překladu?

To prece delat nechci. Ja chci napsat tu specifikaci a pak na to pustit ten generator testu.

[Filip Jirsák]

To prece delat nechci. Ja chci napsat tu specifikaci a pak na to pustit ten generator testu.

Pak tedy nebude ověření správnosti sioučástí typu, ale bude v tom testu.

[listoper]

To prece delat nechci. Ja chci napsat tu specifikaci a pak na to pustit ten generator testu.

Pak tedy nebude ověření správnosti sioučástí typu, ale bude v tom testu.

Ne. Bude v te specifikaci podle ktere se testy vygeneruji.

[JSH]

Narážíš-li na komutativitu, tak tímto způsobem to zase odhalí i Typ.

Jak ten typ bude vypadat?

Přiznávám se bez mučení, že zde mé znalosti končí. Ale mám rámcovou představu, jak by to mělo jít: pokud vím, že operátor sčítání je, a operátor odčítání není komutativní, tak IMHO není problém to kompilátoru říct. Jak konkrétně by se to zapsalo, to netuším. Mám toho ještě hodně k nastudování.

Mám to chápat tak, že netušíš, jak by se to dalo udělat? Ale trváš na tom, že to jde?
Nejde o to, jestli je nebo není komutativní. Jde o to, že ve chvíli kdy to odčítání nebude brát dva stejné typy, tak najednou nemáme grupu. To je kapku drsná cena.

[Reklama]

[BoneFlute]

Nekde tady byla otazka na kvadratickou rovnici.
Zkusim tu myslenku v te citaci ukazat na tom.
Podotykam moji myslenku z te citace a ne kompletne problem reseny v tomto vlakne.
BoneFlute se z toho osype, protoze to neni ani zdaleka to o cem mluvil on.
A taky protoze to bude v jazyce velmi podobnem jave :-)
Vlastne jedinny rozdil proti jave je, ze umi presne floating point operace.

Kód: [Vybrat]

    final static RuntimeException up = new IllegalArgumentException("Does not compute");

    private static Result getRoots(double a, double b, double c){
        double detBody = b*b - 4*a*c;
        if(detBody < 0){
            throw new IllegalArgumentException("Fuck it! I don't have imaginary friends. " + detBody);
        }
        double det = Math.sqrt(detBody);
        double root1 = (-b + det)/2*a;
        double root2 = (-b - det)/2*a;
        return new Result(a,b,c,root1,root2);
    }

    static class Result {
        double root1; double root2;

        Result (double a, double b, double c, double root1, double root2){
            if(root1 + root2 != -(b/a) || root1*root2 != c/a) throw up;
            this.root1 = root1;
            this.root2 = root2;
        }
    }


Nejvíc bych tomu vytknoul, že si nedovedu představit, že by z takového zápisu byl stroj schopen "pochopit" tu kvadratickou rovnici. Takže nemůže (hypoteticky) "vyvinout" jinou, alternativní implementaci. Zdá se mi to jako algoritmus, který musím "otestovat".

[BoneFlute]

Přiznávám se bez mučení, že zde mé znalosti končí. Ale mám rámcovou představu, jak by to mělo jít: pokud vím, že operátor sčítání je, a operátor odčítání není komutativní, tak IMHO není problém to kompilátoru říct. Jak konkrétně by se to zapsalo, to netuším. Mám toho ještě hodně k nastudování.

Mám to chápat tak, že netušíš, jak by se to dalo udělat?

Píšu, že mám rámcovou představu takže evidentně tuším.

[listoper]

Nekde tady byla otazka na kvadratickou rovnici.
Zkusim tu myslenku v te citaci ukazat na tom.
Podotykam moji myslenku z te citace a ne kompletne problem reseny v tomto vlakne.
BoneFlute se z toho osype, protoze to neni ani zdaleka to o cem mluvil on.
A taky protoze to bude v jazyce velmi podobnem jave :-)
Vlastne jedinny rozdil proti jave je, ze umi presne floating point operace.

Kód: [Vybrat]

    final static RuntimeException up = new IllegalArgumentException("Does not compute");

    private static Result getRoots(double a, double b, double c){
        double detBody = b*b - 4*a*c;
        if(detBody < 0){
            throw new IllegalArgumentException("Fuck it! I don't have imaginary friends. " + detBody);
        }
        double det = Math.sqrt(detBody);
        double root1 = (-b + det)/2*a;
        double root2 = (-b - det)/2*a;
        return new Result(a,b,c,root1,root2);
    }

    static class Result {
        double root1; double root2;

        Result (double a, double b, double c, double root1, double root2){
            if(root1 + root2 != -(b/a) || root1*root2 != c/a) throw up;
            this.root1 = root1;
            this.root2 = root2;
        }
    }


Nejvíc bych tomu vytknoul, že si nedovedu představit, že by z takového zápisu byl stroj schopen "pochopit" tu kvadratickou rovnici. Takže nemůže (hypoteticky) "vyvinout" jinou, alternativní implementaci. Zdá se mi to jako algoritmus, který musím "otestovat".

Ano. Je to tak. Pokud bude funkce getRoots spatne tak se vyhodi RuntimeException coz je na produkci stejne nezadouci.
Melo to jen ilustrovat to overeni v ramci konstruktoru navratoveho typu tem co mluvi javistinou.
Ale kdyz si vygeneruju ten bambilion vstupu tak jen odchytim vyjimku a nemusim do testu na tvrdo psat hodnoty.

[andy]

Nějak jsem nepochopil, co to má společného s tím, že když naučíme compiler pracovat se symbolickou matematikou, tak pro něj není problém odvodit, že standardní řešení kvadratické rovnice splňuje specifikace požadovanou po té funkci. Je to asi tak na stejné úrovni, jako že ten Liquid haskell je pro (některé) programy schopen dovodit, že výsledkem funkce je neprázdné pole.

Jenom jsem upřesnil, že to, co popisujete, je jenom vytčení něčeho jednoduchého do knihovny nebo kompilátoru, které pak jako programátor používáte už bez testování. To ale není nic nového. Takhle už máte něco implementováno třeba v C kompilátoru nebo standardní knihovně – a ty implementace se zase testují.

? Vůbec nerozumím. Celý tenhle thread je o tom, že mám k dispozici kompilátor, který "něco"(typy) umí, a zda s pomocí toho "něčeho" jsem schopen nějaký další program verifikovat tak, že unit testy potřebovat nebudu. Takže když píšu, že pokud bychom měli kompilátor schopný řešit matematické výrazy, tak to umí i verifikovat řešení kvadratické rovnice. Vůbec nechápu, co s tím má společného,

Kompilátor, který neví nic o kvadratických rovnicích, ale umí pracovat s matematickými výrazy (nepovažoval bych za vyloučené, že by tím směrem ty idrisy a spol. ohnout šly), je schopen dokázat, že daná funkce tu kvadratickou rovnici řeší.

Ne, kompilátor není schopen dokázat, že daná funkce řeší kvadratickou rovnici. Kompilátor je schopen dokázat, že daná funkce řeší něco, co programátor prohlašuje za kvadratickou rovnici.

Jako chcete říct, že když programátor kompilátoru nesdělí, aby kontroloval kvadratickou rovnici, tak to kompilátor neudělá...?

[Gődel]

Kompilátor, který neví nic o kvadratických rovnicích, ale umí pracovat s matematickými výrazy (nepovažoval bych za vyloučené, že by tím směrem ty idrisy a spol. ohnout šly), je schopen dokázat, že daná funkce tu kvadratickou rovnici řeší.

Tohle umí třeba Coq.

[Gődel]

chvíli kdy to odčítání nebude brát dva stejné typy, tak najednou nemáme grupu. To je kapku drsná cena.

To by byla sice drsná cena, akorát to ale není pravda.

[Filip Jirsák]

Ne. Bude v te specifikaci podle ktere se testy vygeneruji.

To už je jenom nepodstatný detail, čemu přesně říkáte „test“. Já říkám „testy“ celé části kódu, která stojí vedle hlavního kódu a je určená pro testování. Vy asi myslíte nějaký konkrétní testovací framework a „testem“ myslíte například jednu jeho funkci. Na principu to ale nic nemění.

[Filip Jirsák]

? Vůbec nerozumím. Celý tenhle thread je o tom, že mám k dispozici kompilátor, který "něco"(typy) umí, a zda s pomocí toho "něčeho" jsem schopen nějaký další program verifikovat tak, že unit testy potřebovat nebudu. Takže když píšu, že pokud bychom měli kompilátor schopný řešit matematické výrazy, tak to umí i verifikovat řešení kvadratické rovnice. Vůbec nechápu, co s tím má společného,

Kompilátor, který umí řešit matematické výrazy, je jenom knihovna kódu, který programátor používá, ale netestuje. Nic jiného. Kompilátory běžných jazyků například umí zpracovávat základní algebraické výrazy, tj. umí transformovat sčítáí, odčítání, násobení a dělení na instrukce procesoru, umí správně zpracovat prioritu těch operátorů.

Jako chcete říct, že když programátor kompilátoru nesdělí, aby kontroloval kvadratickou rovnici, tak to kompilátor neudělá...?

Ne, chci říct, že kompilátor nezná pojem „kvadratická rovnice“. Ten pojem nijak neplyne z matematického aparátu, ten název tomu dali lidé, klidně by se to mohlo jmenovat třeba „malá rovnice“ nebo „druhá věta“. Jenže lidé to chtějí používat pod názvem „kvadratické rovnice“, takže musí nějaký člověk přijít a kompilátoru vysvětlit, že to, co má tyhle a tyhle vlastnisti, se nazývá „kvadratická rovnice“. A tenhle popis vlastností je to, kde se často dělají chyby a co je nutné testovat. Kvadratickou rovnici dá asi většina programátorů správně, ale dnešní programy obvykle řeší jiné problémy, než jsou přesně definované matematické funkce.

Pořád jde jen o to, že kompilátor dokáže vyřešit jenom to, co má formálně a bezrosporně zadané. Jenže takováhle zadání programátoři obvykle nemají, ostatně je to jejich práce převádět neformální a neúplné zadání popsané přirozeným jazykem do formální a přesné řeči počítačů. V tomhle převodu se dělají chyby a je snaha těm chybám předcházet, mimo jiné i testováním.

[listoper]

Ne. Bude v te specifikaci podle ktere se testy vygeneruji.

To už je jenom nepodstatný detail, čemu přesně říkáte „test“. Já říkám „testy“ celé části kódu, která stojí vedle hlavního kódu a je určená pro testování. Vy asi myslíte nějaký konkrétní testovací framework a „testem“ myslíte například jednu jeho funkci. Na principu to ale nic nemění.

Testovaci framework je spis ten testcheck. Spec je podle me spis neco jako typovy system. Ale to uz jsem psal vyse. To jak to spolu hezky integruje je bonus.

[andy]

? Vůbec nerozumím. Celý tenhle thread je o tom, že mám k dispozici kompilátor, který "něco"(typy) umí, a zda s pomocí toho "něčeho" jsem schopen nějaký další program verifikovat tak, že unit testy potřebovat nebudu. Takže když píšu, že pokud bychom měli kompilátor schopný řešit matematické výrazy, tak to umí i verifikovat řešení kvadratické rovnice. Vůbec nechápu, co s tím má společného,

Kompilátor, který umí řešit matematické výrazy, je jenom knihovna kódu, který programátor používá, ale netestuje. Nic jiného. Kompilátory běžných jazyků například umí zpracovávat základní algebraické výrazy, tj. umí transformovat sčítáí, odčítání, násobení a dělení na instrukce procesoru, umí správně zpracovat prioritu těch operátorů.

No..vždyť jo. Bavíme se o tom, že tu máme kompilátor, který něco umí (typy) a BoneFlute se ptá, jestli tímto nástrojem (typy) lze nahradit unit testy při ověřování, že ten kód je správně. Což nemá nutně nic společného s tím, jestli to pak skutečně počítá to, co má (z důvodu chyby HW, kompileru apod.).

Jako chcete říct, že když programátor kompilátoru nesdělí, aby kontroloval kvadratickou rovnici, tak to kompilátor neudělá...?

Ne, chci říct, že kompilátor nezná pojem „kvadratická rovnice“. Ten pojem nijak neplyne z matematického aparátu, ten název tomu dali lidé, klidně by se to mohlo jmenovat třeba „malá rovnice“ nebo „druhá věta“. Jenže lidé to chtějí používat pod názvem „kvadratické rovnice“, takže musí nějaký člověk přijít a kompilátoru vysvětlit, že to, co má tyhle a tyhle vlastnisti, se nazývá „kvadratická rovnice“. A tenhle popis vlastností je to, kde se často dělají chyby a co je nutné testovat. Kvadratickou rovnici dá asi většina programátorů správně, ale dnešní programy obvykle řeší jiné problémy, než jsou přesně definované matematické funkce.

Kvadratická rovnice je definovaná jako ax^2 + bx +c = 0. Takže když se člověk zeptá "kompilátore, řeší tenhle vzoreček ax^2+bx+c=0, tak se ptá, jestli řeší kvadratickou rovnici jazykem, kterému kompilátor rozumí. Když tam dá jiný (neekvivalentní) vzoreček, tak se na to neptá.

Pořád jde jen o to, že kompilátor dokáže vyřešit jenom to, co má formálně a bezrosporně zadané. Jenže takováhle zadání programátoři obvykle nemají, ostatně je to jejich práce převádět neformální a neúplné zadání popsané přirozeným jazykem do formální a přesné řeči počítačů. V tomhle převodu se dělají chyby a je snaha těm chybám předcházet, mimo jiné i testováním.

No, takže fakt říkáte, že když kompilátor nepožádám, aby ověřil, že funkce řeší kvadratickou rovnici, tak to kompilátor neověří. Bingo.