Typový system versus unittesty

v

Re:Typový system versus unittesty
« Odpověď #210 kdy: 20. 06. 2018, 09:20:54 »
ano, v runtime, je to miniaturní překladač, překladače mají  dispozici překládaný kód až v runtime (TExp je syntaktický strom překládaného "jazyka")
Konečně. Takže tady má BoneFlute příklad, kdy unittesty (nebo testy obecně) nejde nahradit typovým systémem. A to ani hypoteticky za jakýchkoliv předpokladů. Prostě proto, že se typový systém dostane ke slovu až v runtimu.
tak to není a pro původní dotaz to moc neznamená, protože ten se týkal teoretických mezí


Re:Typový system versus unittesty
« Odpověď #211 kdy: 20. 06. 2018, 09:47:21 »
tak to není a pro původní dotaz to moc neznamená, protože ten se týkal teoretických mezí
Ani sebelepší typový systém nezajistí, že program bude bez chyby. Teoretické meze neleží v typovém systému nebo kompilátoru, ale ve schopnosti formálně popsat specifikaci. Pak může nastoupit automatické dokazování nebo verifikace, např. Isabelle.

v

Re:Typový system versus unittesty
« Odpověď #212 kdy: 20. 06. 2018, 11:37:58 »

ad "Ani sebelepší typový systém nezajistí, že program bude bez chyby."
ano, stejně jako ten nejlepší testovací framework, musíte ho taky použít, v obou případech musíte napsat správný typ resp. testy

ad "Teoretické meze neleží v typovém systému nebo kompilátoru, ale ve schopnosti formálně popsat specifikaci."
to nejsou teoretické meze ale praktické - "lidský faktor"

ad "Pak může nastoupit automatické dokazování nebo verifikace, např. Isabelle."
tak kontrola souladu datového typu s programem je formální verfikace a přijde mi pozoruhodné, že jste zmínil Isabelle a ne IMHO mnohem známější Coq

andy

Re:Typový system versus unittesty
« Odpověď #213 kdy: 20. 06. 2018, 11:39:20 »
tak to není a pro původní dotaz to moc neznamená, protože ten se týkal teoretických mezí
Ani sebelepší typový systém nezajistí, že program bude bez chyby. Teoretické meze neleží v typovém systému nebo kompilátoru, ale ve schopnosti formálně popsat specifikaci. Pak může nastoupit automatické dokazování nebo verifikace, např. Isabelle.
V čem se liší dostatečně silný typový systém od automatického dokazování?

JSH

Re:Typový system versus unittesty
« Odpověď #214 kdy: 20. 06. 2018, 12:32:19 »
V čem se liší dostatečně silný typový systém od automatického dokazování?
Že typová kontrola může proběhnout až dynamicky za běhu. Automatické dokazování se pokud vím obvykle za běhu neprovádí.


Kiwi

Re:Typový system versus unittesty
« Odpověď #215 kdy: 20. 06. 2018, 12:41:09 »
Mám zápis, čitelný pro stroj:
Kód: [Vybrat]
    case s `hasMinimumLen` 4 of
        Just sn -> Str.sub sn 20
        Nothing -> "default"

Ale pro člověka je mnohem lepší zápis:
Kód: [Vybrat]
    if (Str.len s) < 4 then
        "default"
    else
        Str.sub s 20
Co to má být "zápis čitelný pro stroj"? Program v jakémkoli jazyce, který lze zpracovat překladačem? Nebo strojový kód?

andy

Re:Typový system versus unittesty
« Odpověď #216 kdy: 20. 06. 2018, 13:23:36 »
V čem se liší dostatečně silný typový systém od automatického dokazování?
Že typová kontrola může proběhnout až dynamicky za běhu. Automatické dokazování se pokud vím obvykle za běhu neprovádí.
No.... ne.

Citace
Pierce, TPL: A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
...
The word “static” is sometimes added explicitly—we speak of a “statically typed programming language,” for example—to distinguish the sorts of compile-time analyses we are considering here from the dynamic or latent typing found in languages such as Scheme, where run-time type tags are used to distinguish different kinds of structures in the heap. Terms like “dynamically typed” are arguably misnomers and should probably be replaced by “dynamically checked,” but the usage is standard.
Myslím, že v tomhle bych se o autoritu opřel :)

andy

Re:Typový system versus unittesty
« Odpověď #217 kdy: 20. 06. 2018, 13:26:27 »
Co to má být "zápis čitelný pro stroj"? Program v jakémkoli jazyce, který lze zpracovat překladačem? Nebo strojový kód?
BoneFlute má na mysli, že v tom prvním případě programátor překladači poskytnul důkaz správnosti typů, v tom druhém případě si ten důkaz počítač našel sám (což je obecně nerozhodnutelný problém).

BoneFlute

  • *****
  • 1 983
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #218 kdy: 20. 06. 2018, 13:43:46 »
Co to má být "zápis čitelný pro stroj"? Program v jakémkoli jazyce, který lze zpracovat překladačem? Nebo strojový kód?
BoneFlute má na mysli, že v tom prvním případě programátor překladači poskytnul důkaz správnosti typů, v tom druhém případě si ten důkaz počítač našel sám
Ne tak docela "našel", jako že prostě si řekne, že "if podmínka" aha, to si musím přeložit na  tyhle Maybe typy...

(což je obecně nerozhodnutelný problém)
V jakém smyslu? Buď té konstrukci rozumí, nebo jí odmítne. IMHO nic složitého.

BoneFlute

  • *****
  • 1 983
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #219 kdy: 20. 06. 2018, 13:46:50 »
Co to má být "zápis čitelný pro stroj"? Program v jakémkoli jazyce, který lze zpracovat překladačem? Nebo strojový kód?
Bavíme se o typech, a v tomto kontextu strojem nazývám kompilátor.

JSH

Re:Typový system versus unittesty
« Odpověď #220 kdy: 20. 06. 2018, 14:07:48 »
V čem se liší dostatečně silný typový systém od automatického dokazování?
Že typová kontrola může proběhnout až dynamicky za běhu. Automatické dokazování se pokud vím obvykle za běhu neprovádí.
No.... ne.

Citace
Pierce, TPL: A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
...
The word “static” is sometimes added explicitly—we speak of a “statically typed programming language,” for example—to distinguish the sorts of compile-time analyses we are considering here from the dynamic or latent typing found in languages such as Scheme, where run-time type tags are used to distinguish different kinds of structures in the heap. Terms like “dynamically typed” are arguably misnomers and should probably be replaced by “dynamically checked,” but the usage is standard.
Myslím, že v tomhle bych se o autoritu opřel :)
OK. Pak ale zase padá spousta argumentů, které tu tahali v a BoneFlute. Padá např. ten odkaz od v o přesunu překladu Haskellu do runtime. Protože to pak říká jenom to, že pomocí LLVM mašinerie se dá z Haskellu udělat “dynamically checked” jazyk.

Re:Typový system versus unittesty
« Odpověď #221 kdy: 20. 06. 2018, 14:12:36 »
ano, stejně jako ten nejlepší testovací framework, musíte ho taky použít, v obou případech musíte napsat správný typ resp. testy
Máte testy zařazené na špatnou úroveň. Na jedné úrovni jsou typy nebo algoritmy – ty musí být správně, aby program fungoval správně. Pak je volitelná druhá úroveň – můžete napsat testy, které otestují nějaké zajímavé případy. Žádný systém algoritmizace, typů nebo psaní testů nezajistí bezchybnost programu – testy slouží jen ke zvýšení pravděpodobnosti, že chybu odhalíte.

to nejsou teoretické meze ale praktické - "lidský faktor"
Myslel jsem, že se bavíme o tom, co je reálně dosažitelné. Ne že prohlásíme, že program předhodíme nějakému orákulu nebo CML, který nám řekne, zda je správně nebo špatně. No a že takový CML neumíme vytvořit? To je „lidský faktor“…

JSH

Re:Typový system versus unittesty
« Odpověď #222 kdy: 20. 06. 2018, 14:37:09 »
Myslel jsem, že se bavíme o tom, co je reálně dosažitelné. Ne že prohlásíme, že program předhodíme nějakému orákulu nebo CML, který nám řekne, zda je správně nebo špatně. No a že takový CML neumíme vytvořit? To je „lidský faktor“…
A navrch se těma typama a dokazováním zabýváme právě kvůli tomu lidskému faktoru.

v

Re:Typový system versus unittesty
« Odpověď #223 kdy: 20. 06. 2018, 14:39:09 »
OK. Pak ale zase padá spousta argumentů, které tu tahali v a BoneFlute. Padá např. ten odkaz od v o přesunu překladu Haskellu do runtime. Protože to pak říká jenom to, že pomocí LLVM mašinerie se dá z Haskellu udělat “dynamically checked” jazyk.
ne, ten článek říká, že jde v haskellu udělat překladač (AOT/JIT nezáleží), který bude pracovat s dočasnou reprezentací (TExp), která má stejné typové garance, jako by to byl kód v haskellu, tj. TExp garantuje, že žádná funkce nad ním (funkce, která je součástí kompilátoru, staticky ověřená při překladu překladače) neudělá blbost typu string + int (nejprovařenější příklad, jde to rozšířit na další vlastnosti) a dále ukazuje, že k takové reprezentaci lze přejít za běhu (proto jsem ten link postnul), což je docela normální, protože překladač dostane zdroják až za běhu, ne při překladu překladače

andy

Re:Typový system versus unittesty
« Odpověď #224 kdy: 20. 06. 2018, 14:56:25 »
OK. Pak ale zase padá spousta argumentů, které tu tahali v a BoneFlute. Padá např. ten odkaz od v o přesunu překladu Haskellu do runtime. Protože to pak říká jenom to, že pomocí LLVM mašinerie se dá z Haskellu udělat “dynamically checked” jazyk.
Zrovna tu mám projektík, kde se podobnou mašinérii budu snažit vyrobit... ne, ten článek říká něco jiného.

Autor píše "interpret" jazyka. Za tímto účelem si vyrobil Abstrat syntax tree, který je postavený na GADT... což se hezky dá využít k tomu, že v tom stromě nelze sestavit špatně typovaný program (uzel má typ "TExp Bool" - tak ho nejde dát jako potomka "+", který očekává jako parametry "TExp Double"). Při parsingu si vyrobí AST bez typů (takže tam tyhle chybné operace vyjádřit jde) - a ten článek je o tom, jak té netypované reprezentace přejde k té typované.

Je to v podstatě ta otázka o tom sčítání - když bych měl tu funkci
Kód: [Vybrat]
add :: SNat n -> SNat m -> SNat (n + m)
tak je to hezké, ale jak vyrobit tu funkci
Kód: [Vybrat]
toNat :: Int -> SNat n
Kdy ten typ závisí na vstupu od uživatele. No a..ono to nějak jde (někdy)...doufám, že až si to implementuju, tak i pochopím jak...