Typový system versus unittesty

[v]

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í

[Reklama]

[Filip Jirsák]

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]

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]

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]

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í.

[Reklama]

[Kiwi]

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]

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.

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]

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]

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]

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]

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.

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.

[Filip Jirsák]

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]

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]

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]

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...