Typový system versus unittesty

[Gődel]

vedle typování a jednotkových testů se někdy taky používá obecné dokazování korektnosti při překladu, vývojář napíše podmínky v nějaké deklarativní notaci, které pak překladač vyhodnotí, než vygeneruje kód. Formálně to je jen zobecnění typové kontroly, ale za použití neomezené logiky. Například si můžu “staticky” vyžádat, že odmocnina prvočísla je vždy iracionální apod.

Uniká mi v čem se to liší od typů. Já pomocí typu nemůžu "říct", že odmocnina z prvočísla je vždy iracionální?

Kód: [Vybrat]

nthRoot = x : PrimeNum -> IrrationalNum


To samozřejmě jde, měl jsem na mysli aparát, ve kterém se nadefinuje, co je prvočíslo, co je iracionální číslo a jak se odmocňuje. Možná jsem zvolil špatný příklad.

[Reklama]

[BoneFlute]

To samozřejmě jde, měl jsem na mysli aparát, ve kterém se nadefinuje, co je prvočíslo, co je iracionální číslo a jak se odmocňuje. Možná jsem zvolil špatný příklad.

Jasně.

Právě, že v tom nevidím rozdíl. Pro mě jsou ty typy právě takový aparát.

Napadlo mě něco takového:

Kód: [Vybrat]

Person = {
    name: String 1 50
    surname: String 1 100
    birth: Date * now
    sex: Male | Female
    spouse: Person | None
} where [
    if spouse == Person:
       sex != spouse.sex
       birth < Now - (18 * year)
]

Ale považuji to také za typový systém.

[Gődel]

To samozřejmě jde, měl jsem na mysli aparát, ve kterém se nadefinuje, co je prvočíslo, co je iracionální číslo a jak se odmocňuje. Možná jsem zvolil špatný příklad.

Jasně.

Právě, že v tom nevidím rozdíl. Pro mě jsou ty typy právě takový aparát.

Napadlo mě něco takového:

Kód: [Vybrat]

Person = {
    name: String 1 50
    surname: String 1 100
    birth: Date * now
    sex: Male | Female
    spouse: Person | None
} where [
    if spouse == Person:
       sex != spouse.sex
       birth < Now - (18 * year)
]

Ale považuji to také za typový systém.

Ano. Možná mluvíme o tom samém každý jinak. Na dostatečně abstraktní úrovni a s kvantifikátory se jedná o to samé. Akorát teda pak zápis těch podmínek nebude moc připomínat typování, spíš nějaký lambda kalkul.

[Honza]

Akorát teda pak zápis těch podmínek nebude moc připomínat typování, spíš nějaký lambda kalkul.

Ale hlavně se tomu nesmí říkat unit-testy... že? 

[BoneFlute]

Akorát teda pak zápis těch podmínek nebude moc připomínat typování, spíš nějaký lambda kalkul.

Ale hlavně se tomu nesmí říkat unit-testy... že? 

A tak já proti unittestů zas v zásadě nic nemám. Ale tobě to přijde jako unittest?

[Reklama]

[Gődel]

Akorát teda pak zápis těch podmínek nebude moc připomínat typování, spíš nějaký lambda kalkul.

Ale hlavně se tomu nesmí říkat unit-testy... že? 

Unit testy se neprovádí v době překladu, na rozdíl od typové kontroly. Máš v tom guláš. A nepoužívej přebytečné pomlčky a smailíky.

[Gődel]

Akorát teda pak zápis těch podmínek nebude moc připomínat typování, spíš nějaký lambda kalkul.

Ale hlavně se tomu nesmí říkat unit-testy... že? 

A tak já proti unittestů zas v zásadě nic nemám. Ale tobě to přijde jako unittest?

On neví, o čem mluví. Ale mám za to, že jsme se tu všichni shodli, že typová kontrola nemůže nahradit jednotkové testy ani naopak, byť se do značné míry překrývají (záleží na síle typového systému, v Javě je to tragédie, ale málokdo píše weby w Coqu nebo Agdě, to už spíš tíhnou k horším věcem).

[BoneFlute]

Ale mám za to, že jsme se tu všichni shodli, že typová kontrola nemůže nahradit jednotkové testy ani naopak

Tak na to ať si udělá názor každý sám :-)

[BoneFlute]

Akorát teda pak zápis těch podmínek nebude moc připomínat typování, spíš nějaký lambda kalkul.

Tak jak sis mohl všimnout, pro mnohé jsou Java typy vrchol toho co znají.

Jak jsem už uváděl. Pro mě je pro ty typy zásadní, že jsou deklarativní. Popisují a "vysvětlují" to kompilátoru, co to má být. Jestli to napíšeš tak či onak, je IMHO nepodstatné. Někdy si pomáhám slovíčkem "pravidla". Definuju pravidla, kterým ten element musí odpovídat, aby to označil za korektní. A ty pravdla samozřejmě nemusí být jen o "je" a "má", ale můžou být klidně docela komplexní. Klidně to je naféráka jazyk. Akorád nepoučuješ procesor, co má udělat, ale kompilátor, co má ten graf programu znamenat. V čemž vidím rozdíl oproti unittestů. Ty obvykle nejsou tak deklarativní, a hlavně compilátoru nepomáhají.

[Kit]

Unit testy se neprovádí v době překladu, na rozdíl od typové kontroly.

Kdy jindy bys chtěl dělat jednotkové testy, než při překladu?

[Gődel]

Akorát teda pak zápis těch podmínek nebude moc připomínat typování, spíš nějaký lambda kalkul.

pro mnohé jsou Java typy vrchol toho co znají.

Ano, to jsme si všimnul. Je to smutné.

[Gődel]

Unit testy se neprovádí v době překladu, na rozdíl od typové kontroly.

Kdy jindy bys chtěl dělat jednotkové testy, než při překladu?

Jednotkové testy jsou kód jako každý jiný, normálně se přeloží (compile time) a spustí (run time). Typová kontrola probíhá při překladu nad oanotovaným syntaktickým stromem.

[Kit]

Unit testy se neprovádí v době překladu, na rozdíl od typové kontroly.

Kdy jindy bys chtěl dělat jednotkové testy, než při překladu?

Jednotkové testy jsou kód jako každý jiný, normálně se přeloží (compile time) a spustí (run time). Typová kontrola probíhá při překladu nad oanotovaným syntaktickým stromem.

Nejprve spustím test, ten spustí kompilaci jednotky a otestuje ji. Test tedy spouštím při překladu nebo ne?

[BoneFlute]

Unit testy se neprovádí v době překladu, na rozdíl od typové kontroly.

Kdy jindy bys chtěl dělat jednotkové testy, než při překladu?

Jednotkové testy jsou kód jako každý jiný, normálně se přeloží (compile time) a spustí (run time). Typová kontrola probíhá při překladu nad oanotovaným syntaktickým stromem.

Nejprve spustím test, ten spustí kompilaci jednotky a otestuje ji. Test tedy spouštím při překladu nebo ne?

Ne. Testy se spouští při buildu. Build a compile není to samé.

[Gődel]

Unit testy se neprovádí v době překladu, na rozdíl od typové kontroly.

Kdy jindy bys chtěl dělat jednotkové testy, než při překladu?

Jednotkové testy jsou kód jako každý jiný, normálně se přeloží (compile time) a spustí (run time). Typová kontrola probíhá při překladu nad oanotovaným syntaktickým stromem.

Nejprve spustím test, ten spustí kompilaci jednotky a otestuje ji. Test tedy spouštím při překladu nebo ne?

Viz boneflutovo vysvětlení. Unit testy nejsou compile time.