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.
To není definice, je to důkaz (proof) platnosti formule. Hodnoty typů odpovídají důkazům formulí. Nedokazatelné formule odpovídají podle CHK typům bez hodnost (tzv. uninhabited types, “neobydlené”). Typově EvenZ je jedinou hodnotou typu Even 0 atd.Jak uPro každý Even n platí, že má následníka plus 2, přičemž prvním prvkem je EvenZ? to je jako definice následovníka, přičemž EvenZ je definice neutrálního prvku?Kód: [Vybrat]zajistím, že to bude zrovna sudá řada?EvenSS : Even n -> Even (S (S n))
div2 : (n:Nat) -> {auto prf:Even n} -> NatTo prf je “proof”, tady je třeba “přepnout myšlení” z typů na formální logiku (Curry-Howardova korespondence). To prf je důkaz (formální, symbolický), že vstup je sudé číslo. Díky existenci toho důkazu můžu vesele dělit a vím, že dostanu přirozené číslo. U toho následníka si “půjčím” důkaz pro n-2 z konstruktoru predikátu, abych měl co předat v rekurzi. Zkus si to rozepsat ve FOL
čtu jako: Vezmu číslo, a to číslo musí být aplikovatelné na typ Even. Tuto podmínku mám pojmenovanou jako prf.
div2 Z {prf=EvenZ} = 0
čtu jako: Pokud je číslo (n) nula, a je splněna podmínka prf, tzn číslo je Even, přesněji EvenZ. Toto ještě asi chápu.
div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
čtu jako: Pokud následník následníka čísla n, a je splněna podmínka... Tady jsem v háji
Začíná se nulou (“Z”) a (S (S n)) v podstatě znamená n+2, takže to jsou násobky dvou.Jak u“Z” je nula a “S” je successor.div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})Co prosím tě znamená to S?Kód: [Vybrat]zajistím, že to bude zrovna sudá řada?EvenSS : Even n -> Even (S (S n))
Ano, je to generický typ, dostane přirozené číslo a vrátí konkrétní typ.Můžeš mi popsat tu šipku? Můžeš mi prosím rozvést, co dělá to Even : Nat -> Type? To jako že mám typovou funkci, která mi z přirozeného čísla udělá nový typ pomocí těch konstruktorů?“Z” je nula a “S” je successor.div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})Co prosím tě znamená to S?
“Z” je nula a “S” je successor.div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})Co prosím tě znamená to S?
Mohl bych se @Idris připomenout? Samozřejmě chápu, že máš dost svých starostí, ale třeba budu mít štěstí.I'm back
Sorry, teď teprve se k tomu vracím. Stay tunedTo fakt není nejjednodušší příklad na naučení. Lepší je možná začít třeba s typem pro sudá přirozená čísla nebo tak něco.
Jsem pro.Kód: [Vybrat]type Even = 2, 4, 6, ...
inc :: Even -> Number
inc b = a + 1
calculate :: Number -> Number -> Number
-- nepřeloží se
calculate a b = (inc b) + a
-- přeloží se
calculate a b = (inc (toEvenOr b 2)) + a
where
toEvenOr a default = ...
Jak by se to dělalo pomocí dep. types, prosím?
Mohl bych se @Idris připomenout? Samozřejmě chápu, že máš dost svých starostí, ale třeba budu mít štěstí.
Já tady taky moc nechápu, jak to myslíš. Ale to je fuk, dědičnost nechme stranouHele, mám pocit, že tady někdo něco přeskočil. Právě na tomhle scénáři jsem to přeci vysvětloval.A v druhé řadě, nesouhlasil jsem s tím, že by mi to typovej systém neohlídal compile time. Proč by nemohl. Všechny informace má.No, Idris ti to už napsal: máš pole Intů, nic víc nevíš. Třeba jsi ho načetl serializované z disku nebo ze sítě. V compile time víš jenom, že to je pole intů. Teprve až to načteš z toho disku, můžeš zjistit, že třetí, pátý a sedmdesátý osmý je Age
To fakt není nejjednodušší příklad na naučení. Lepší je možná začít třeba s typem pro sudá přirozená čísla nebo tak něco.Jak na to koukám, tak tam není moc co upravovat, prostě musíš zavolat div a b (MkNonZero (prec b)), kde prec: (Succ n) ↦ n. Teď z hlavy nevím, jak přesně to řeší sofistikovanější jazyky, podívám se.No to nejde, musíš zavolat div a b proof.Ne ne, bylo by to div : Numeric -> (y:Numeric) -> Not (y=0) -> Numeric . V těchto jazycích jakákoliv hodnota typu se bere jako důkaz platnosti formule odpovídající tomu typu (Curry-Howard). S tou rovností to je trik, že když předám příslušnou hodnotu ("důkaz"), můžu tu funkci zavolat a mám zaručenou nenulovost. Jinak kód vůbec nepřeložím. Fakt si místo Not (y=0) vezmi NonZero y. Tento typ má konstruktor MkNonZero (S n). No a teď si zkus s tímto zavolat div na nuluJak by vypadalo volání funkce div když by měla závislostní typy?Kód: [Vybrat]div :: Numeric -> (y:Numeric) -> Not (y=0) -> Numeric
div a b = a / b
calculate :: Numeric -> Numeric -> Numeric
calculate a b =
(div a b) + 1
calculate 10 0
Má to tři argumenty, ale volám (volal bych) to jen se dvěma.
Mohl by jsi mi prosím ten můj "zdroják" upravit, jak by to vypadalo?
Tobě se to mluví, ty tomu už rozumíš. Já ještě furt ne.Kód: [Vybrat]prec :: (Succ n) -> n
prec a = ...
div :: Numeric -> (y:Numeric) -> Not (y=0) -> Numeric
div a b = a / b
calculate :: Numeric -> Numeric -> Numeric
calculate a b =
(div a b (MkNonZero (prec b))) + 1
calculate 10 0
Tak, teď už vím, jak se to volá, ale teď zase nevím co je prec, uff.
Když se na to podívám, tak mi ten můj "způsob" přijde jednodužší. Takže předpokládám, že v těch dep. typech musí být něco víc.
Jak na to koukám, tak tam není moc co upravovat, prostě musíš zavolat div a b (MkNonZero (prec b)), kde prec: (Succ n) ↦ n. Teď z hlavy nevím, jak přesně to řeší sofistikovanější jazyky, podívám se.No to nejde, musíš zavolat div a b proof.Ne ne, bylo by to div : Numeric -> (y:Numeric) -> Not (y=0) -> Numeric . V těchto jazycích jakákoliv hodnota typu se bere jako důkaz platnosti formule odpovídající tomu typu (Curry-Howard). S tou rovností to je trik, že když předám příslušnou hodnotu ("důkaz"), můžu tu funkci zavolat a mám zaručenou nenulovost. Jinak kód vůbec nepřeložím. Fakt si místo Not (y=0) vezmi NonZero y. Tento typ má konstruktor MkNonZero (S n). No a teď si zkus s tímto zavolat div na nuluJak by vypadalo volání funkce div když by měla závislostní typy?Kód: [Vybrat]div :: Numeric -> (y:Numeric) -> Not (y=0) -> Numeric
div a b = a / b
calculate :: Numeric -> Numeric -> Numeric
calculate a b =
(div a b) + 1
calculate 10 0
Má to tři argumenty, ale volám (volal bych) to jen se dvěma.
Mohl by jsi mi prosím ten můj "zdroják" upravit, jak by to vypadalo?
Sorry, teď musím pryč, ale vrátím se k tomuNo to nejde, musíš zavolat div a b proof.Ne ne, bylo by to div : Numeric -> (y:Numeric) -> Not (y=0) -> Numeric . V těchto jazycích jakákoliv hodnota typu se bere jako důkaz platnosti formule odpovídající tomu typu (Curry-Howard). S tou rovností to je trik, že když předám příslušnou hodnotu ("důkaz"), můžu tu funkci zavolat a mám zaručenou nenulovost. Jinak kód vůbec nepřeložím. Fakt si místo Not (y=0) vezmi NonZero y. Tento typ má konstruktor MkNonZero (S n). No a teď si zkus s tímto zavolat div na nuluJak by vypadalo volání funkce div když by měla závislostní typy?Kód: [Vybrat]div :: Numeric -> (y:Numeric) -> Not (y=0) -> Numeric
div a b = a / b
calculate :: Numeric -> Numeric -> Numeric
calculate a b =
(div a b) + 1
calculate 10 0
Má to tři argumenty, ale volám (volal bych) to jen se dvěma.
Mohl by jsi mi prosím ten můj "zdroják" upravit, jak by to vypadalo? A kde že vezme tu proof?
Můj cíl je vždycky compile time, i za cenu složitější práce překladače.Jo, to je jediná rozumná cesta. Akorát třeba v Agdě pak kompilace trvá třeba dva dny. A když pak na tebe vyskočí "sorry vole error," tak to nepotěší.
Mám RAM 128GBTohle je fakt non-issueJestli ti pole integerů zabírá 32G nebo 64G úplně non-issue není
On myslí, že když máš instanci List<Int> a žádné další informace, tak jen za běhu můžeš zjistit, že nějaký prvek je třeba typu Age (nebo prostě nějakého podtypu). To je ten základní důvod pro existenci virtuálních metod. Zmíněné aserce v Go jsou vlastně jen (konceptuálně) dynamic_cast.Překladač tohle za tebe řešit nemůže, protože k tomu dochází až v runtime. (Překladač nemůže tušit, že při běhu bude ausgerechnet třetí prvek pole Age a ne Int).Tohle už jsi kdysi kdesi tvrdil, a já s tebou v tomto stále nesouhlasím. Žádný runtime, a překladač to může zajistit. Viz ten kód.
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.
