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.
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.
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 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)V jakém smyslu? Buď té konstrukci rozumí, nebo jí odmítne. IMHO nic složitého.
case s `hasMinimumLen` 4 of
Just sn -> Str.sub sn 20
Nothing -> "default" if (Str.len s) < 4 then
"default"
else
Str.sub s 20add x y = x + y
add x y = y + x
add x y = if x == 0 then y else x + y
add x y = if x < 1 then y else x + y
Obávám se, že toto je ta samá věc, kterou uváděl Filip Jirsák. A tuším, že tu bylo minimálně dvakrát poukazováno, že to by problém být neměl - viz závislostní typy.Pro pořádek, hodíte sem link na ten příspěvek, prosím? Protože je možné, že jsem to mezi spoustou toho smetí přehlédl.
Zde: https://forum.root.cz/index.php?topic=18804.msg270520#msg270520
Nejsou ty formule náhodou takové ty "grupové axiomy"? Abych si to nějak srovnal.Vypadají tak. Formule se prostě poskládá z elementárních hodnot (ty závisí na úrovni, o kterou se jedná) a operací (grupy mají např. jen jednu). Hlavní rozdíl je, že u grup nejsou typy. Jakmile je přidáme, dostaneme kategorie, ale o těch se tu nemluví, jinak přijde Voldemort a sežere nám všechny monády...
Ano, bavíme. Jen jsem psal (možná to trochu zapadlo), že operace (výpočty) na všech úrovních jsou dány formulemi a základními hodnotami. Co jde vypočítat na té které úrovni je dáno těmito hodnotami stanovenými úmluvou.Nejsou ty formule náhodou takové ty "grupové axiomy"? Abych si to nějak srovnal.
tak možná jsem zvolil trochu matoucí příklad, JIT je tam to co se implementuje, ne technika, která se využívá k implementaci něčeho jiného (uff)Wow!
kouzelný typ tam je "data TExp a" a pointa je, že nejde vytvořit hodnota tohoto typu, která by reprezentoval chybně typovaný syntaktický strom
Neměl by si prosím nějakou pěknu demonstraci principu toho metaIsRed. Nebo link na nějaké zdroje. Přeci jenom to hned z fleku nedávám (už jen ty množiny mi chvilku trvaly, než jsem dosáhl aha efektu).Ano, bavíme. Jen jsem psal (možná to trochu zapadlo), že operace (výpočty) na všech úrovních jsou dány formulemi a základními hodnotami. Co jde vypočítat na té které úrovni je dáno těmito hodnotami stanovenými úmluvou. Na té nejnižší úrovni se utvořeným výrazům říká funkce, protože odpovídají funkcím v teorii množin (nebo prostě aritmetice apod.). Stejně tvořeným výrazům na vyšší úrovni už se říká jinak (podle kontextu metavýrazy, metahodnoty apod.), ale v podstatě to je to samé, jen o úroveň výše. V případě isRed můžu jednoduše napsat funkci a stejně jednoduše můžu vytvořit součtový typ nad RGB implementující isRed o úroveň výše (něco jako "metaIsRed"), jenž by šel použít v typovém systému pro kontrolu v době překladu.že těla formulí jsou "běh" a typové výrazy "překlad".Možná ti jen nerozumím, ale:
mám množiny
Bool = True | False
RGB = Red | Green | Blue
pak mám funkci
isRed :: RGB -> Bool
která se dá zapsat takto:
isRed :: RGB -> Bool = (Red -> True) | (Green -> False) | (Blue -> False)
Té množině isRed ale obvykle říkáme funkce, a něco počítá, ale je to stejně jen množina, respektive pohled na průnik dvou množin. (Nebudu se pokoušet trefit se do přesného pojmosloví.)
Bavíme se cca o tom samém?
Ale jak už jsem psal nejméně dvakrát, moc praktické takové počínání není, už jen proto, že takové typy by se nikdy nepoužily za běhu.Jak už jsem psal taky nejméně dvakrát, na praktičnost vám prdim :-)
Pro pořádek, hodíte sem link na ten příspěvek, prosím? Protože je možné, že jsem to mezi spoustou toho smetí přehlédl.Proč @v dokázal pochopit, že se táži na limity toho typového systému vůči unittestům, zatímco jiní se mě pokouší přesvědčit že jsem idiot a ani nejsou schopni uvést zajímavé argumenty?
Omezené možnosti kontroly správnosti programu typovým systémem jsem vám přímočaře a bleskově (a vypadá to, že nejen já, nečetl jsem vše) předvedl na příkladu, víceméně důkazu sporem. Takže odpověď na váš původní dotaz už máte. Je třeba ještě něco řešit?
že těla formulí jsou "běh" a typové výrazy "překlad".Možná ti jen nerozumím, ale:
Obecně asi platí, že když se program převede do churchovského λ-kalkulu (kde se nerozlišuje mezi dobou překladu a běhu), tak jakákoliv totální funkce, jejíž doména je konečná, se dá verifikovat typově (čili v době překladu v nějaké implementaci s dostatečně silným typovým systémem). Odhalování a charakteristika chyb tímto způsobem souvisí (na úrovni pusté teorie) s ι-operátorem.Limit typů jsou časová náročnost. Limit testů zase neúplnost. Dokážete si někdo představit, že by se dal uělat nějaký kompromis, omezit ultimátnost typů, aby to otestování proběhlo v kontrolovaném čase. Nebo optimalizovat compiler, aby si dokázal domyslet některé věci a nepočítal to hrubou silou?
Tý vozo, jsem ani nedoufal, že to v Haskellu jde. To bude zase propálených hodin.co tohle https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell ?co si vlastně představujete pod pojmem "silný typový systém"?Rozhodně něco s HKT (tím se vyloučí Java apod.), to by byl středně silný, nicméně jak tu už někdo zmiňoval, adjektivum "silný" by mělo implikovat alespoň běžné závislostní typy à la Agda/Coq/Idris.
asi neumím říct, kde závislostní typy začínají
a "silný" je asi dost blbé označení
Rád bych, když bychom se nedrželi jen toho, co se zatím někomou podařilo implementovat. Zajímá mě klidně i to, co by teoreticky šlo.co si vlastně představujete pod pojmem "silný typový systém"?Rozhodně něco s HKT (tím se vyloučí Java apod.), to by byl středně silný, nicméně jak tu už někdo zmiňoval, adjektivum "silný" by mělo implikovat alespoň běžné závislostní typy à la Agda/Coq/Idris.
tak když někdo špatně pochopí problém, tak mu taky nic nezabrání napsat chybný test
To už ale nemá co dělat s problematikou testování, ale chápání řešené úlohy, zde nevznikne rozdíl při použití typového systému, nebo testů.
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.