Zobrazit příspěvky
Tato sekce Vám umožňuje zobrazit všechny příspěvky tohoto uživatele. Prosím uvědomte si, že můžete vidět příspěvky pouze z oblastí Vám přístupných.
A kromě toho nemožné, typový systém může být zároveň korektní i nekorektní. Proto jsem navrhoval vzít STλC, to lidi poberou a jde na tom vše kolem typů krásně vysvětlit, včetně metalogických důkazů (ne)korektnosti/úplnosti. A jde v tom přímo programovat za účelem názornosti.Každopádně Blbec se vypařil, takže nám svoje tvrzení nedoloží na ničem
Ono by nejen této diskusi prospělo, kdyby každý diskutující rozlišoval věcné argumenty a subjektivní názory...Ano, velmi. Ale je to obtížné. Pro někoho přílíš obtížné.
Já mám takovou krásnou ukázku flexibility dynamického jazyka.Spíš je to krásná ukázka toho, že "krása" je veskrze subjektivní pojem.
Příklad: Mám batoh s danou nosností a objemem a (netypový) seznam blíže neurčených předmětů (= nezajímá mě, co to je), jejichž jediným společným prvkem (a to ještě ne nutně) je, že odpovídají na zprávu "hmotnost" a "velikost", a chci zjistit, zda se mi do toho batohu vlezou. Jak se to řeší typovaným seznamem???Proč je tam to "ne nutně"? Pokud chci zjistit, jestli se mi tam vlezou, pak musí na ty zprávu odpovídat nutně, jinak nemůžu rozhodnout, jestli se mi tam vlezou.
Ne že by to v diskusi bylo podstatné, ale ne vše je zakuklený dict, viz __slots__ (ono pro malé třídy je dict dost overkill).To je ale jenom optimalizace, která pro to, o čem se bavíme, nejenom že není podstatná, ale nemá to vůbec žádný vliv.
(dle pravidla Liskovové).A ještě lepší by bylo tam podtypový polymorfismus vůbec nemít, ušetřili bysme si spoustu bolehlavů
treba typove systemy Javy a stare Scaly jsou nekorektniPořád ještě jsme si neřekli, co by to ta korektnost (a (ne)dokazatelnost) u typového systému měla být, takže tvrdit, že nějaký typový systém je nekorektní, je předčasné.
Pokoušel jsem se na ladit ne ten váš problém, co řešíte. Evidentně se mi to nepovedlo :-)Ne, nepovedlo
Pointa je v tom, že v obou systémech se program větví na základě typu a v obou k tomu dojde až za běhu. Prostě pořád je to ta samá chyba.
Než se pustíte dál, taková malá odbočka.Krása! Konečně někdo, kdo mluví jazykem mého kmene! Jdu do toho!
Jde o to tvé jednoznačné Ne v odpovědi. Výrok Godel se posleze zbláznil v odpovědi nepopíráš, takže se asi shodneme, že je to výrok pravdivý (pomiňme teď definici zbláznění). Vše se teda točí kolem slovíčka z toho. Řekl bych, že nemáme dost informací na to, aby se dalo jednoznačně říct, že se jedná o nepravdivý výrok. Za prvé není úplně jasné, co přesně znamená to "z toho" a za druhé asi úplně nevíme, z čeho konkrétně se Godel zbláznil a zda na to "to" nemohlo mít nějaký vliv.
Nepustí:No dobře, tak ten string bude trochu víc zakuklenej no. Třeba do atributu.
Nevidím důvod, proč by v dynamicky typovaném jazyce měla aplikace padat v produkci. Ovšem pokud někdo píše testy jen podle metrik...Mohl úplně jednoduše na otestování nějakého edge casu zapomenout. Probublal mu None někam, kde správně neměl být povolený, uložilo se to na disk, nikdo na ty data deset let nešáhl a nikdo už dneska neví, že tam kdysi None být mohl.
V tom řádku s Just je právě schválně chyba. Kde statický jazyk si "všimne" při překladu, že x není string. To považuju za dost "světodějný".Ajo, promiň, toho jsem si nevšiml. Ale co tím demonstruješ? Jenom to, že statické jazyky umí některé chyby odhalit už v době překladu. To ale přece všichni víme, ne?!
def some_func_anywhere():
return 1 + "x"
Mám trochu pocit, že na to jdete moc rychle a zbytečně zužujete počet lidí, kteří vám budou rozumět. Nešlo by začít tím, že to trochu zpřehledníte např. vymezením pojmů? Např.: Čemu říkám "důkaz"? Jakými prostředky je veden? V rámci jakého systému? Atd. Tohle vaše povídání je fakt srozumitelné asi jenom tomu, kdo víceméně už zná výsledekTak pro primitivně rekurzivní funkce to platí vždy, takže vlastně ani důkaz (otypování) nemusíme ověřovat. Ale proč to neplatí pro obecné programy?zabývat tím, jestli existuje takový algoritmus/systém, že pro každý program, který pro všechny validní vstupy skončí, existuje důkaz.To bohužel neplatí, důkaz lze zaručeně najít pouze pro primitivně rekurzivní funkce.
Ve všem souhlas, jenom tomuhle nerozumím:Jenže dynamický jazyk tu chybu pustí.
Root.cz (www.root.cz), informace nejen ze světa Linuxu. ISSN 1212-8309
Copyright © 1998 – 2023 Internet Info, s.r.o. Všechna práva vyhrazena. Powered by Linux.