Typový system versus unittesty

Gődel

Re:Typový system versus unittesty
« Odpověď #360 kdy: 25. 06. 2018, 14:45:20 »
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.


BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #361 kdy: 25. 06. 2018, 15:07:01 »
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

Re:Typový system versus unittesty
« Odpověď #362 kdy: 25. 06. 2018, 15:56:00 »
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

Re:Typový system versus unittesty
« Odpověď #363 kdy: 25. 06. 2018, 16:25:23 »
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?  ;D

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #364 kdy: 25. 06. 2018, 16:28:45 »
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?  ;D

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


Gődel

Re:Typový system versus unittesty
« Odpověď #365 kdy: 25. 06. 2018, 16:33:23 »
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?  ;D
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

Re:Typový system versus unittesty
« Odpověď #366 kdy: 25. 06. 2018, 16:36:51 »
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?  ;D
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

  • *****
  • 1 981
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #367 kdy: 25. 06. 2018, 16:38:46 »
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

  • *****
  • 1 981
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #368 kdy: 25. 06. 2018, 16:47:24 »
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í.

« Poslední změna: 25. 06. 2018, 16:49:07 od BoneFlute »

Kit

Re:Typový system versus unittesty
« Odpověď #369 kdy: 25. 06. 2018, 17:23:52 »
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

Re:Typový system versus unittesty
« Odpověď #370 kdy: 25. 06. 2018, 17:41:11 »
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

Re:Typový system versus unittesty
« Odpověď #371 kdy: 25. 06. 2018, 17:43:37 »
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

Re:Typový system versus unittesty
« Odpověď #372 kdy: 25. 06. 2018, 18:45:08 »
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

  • *****
  • 1 981
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #373 kdy: 25. 06. 2018, 21:44:16 »
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

Re:Typový system versus unittesty
« Odpověď #374 kdy: 25. 06. 2018, 22:28:33 »
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.