Fórum Root.cz
Hlavní témata => Vývoj => Téma založeno: BoneFlute 31. 03. 2021, 15:50:31
-
spinof z https://forum.root.cz/index.php?topic=24432.120
Každopádně můj fokus je momentálně na tomto: https://amulet.works/
To vypadá celkem zajímavě.
Když by si se nudil a napadl tě nějaký pěkný demonstrativní příkládek, zlobit se nebudu.
Příklad čeho? Určitě není problém, jen to pls upřesni.
forall patří do skupiny kvantifikačních typů. Takové to každý, žádný. Potuď mi teorie ok. Ale zatím mi nedochází, k čemu v praxi to může být dobré? Myslím tím nějaký vulgární praktický příklad.
Příklad s monádama: Monáda Maybe je dobrá k tomu, když chceš vrátit hodnotu nebo chybu. Užitek: Maybe je generická. Tudíž nemusíš řešit NullObject pro každý svůj vlastní typ. Díky tomu, že je to generické, můžeš udělat takovou tu věc (neznám názvosloví), kdy řadíš Maybe za sebou a nemusíš řešit rozbalení, zabalení. Máš to otypováné, tudíž se ti nemůže stát, že ti uteče nějaká větev programu, protože ty nemůžeš hned pracovat s tou hodnotou, ale musíš ji nejdřív vybalit... A podle signatury hned poznám, zda mi to vrací číslo, či číslo nebo chybu. A tak.
Jiný příklad s třídama. Třídy nedefinují typ, ale povinnost mít správnou funkci, funkce. A tím mi to rozvazuje ruce, že já nemusím řešit co je to za objekt, jeho strukturu, nedejbože jméno, ale má implementované ty funkce? To mi stačí, stejně víc nepotřebuju.
A prostě by se mi líbil nějaký příkládek pro forall. Abych věděl, že "jo ahaá, takže já si tenhle kousek kódu můžu zjednodušit na..."
Haskell má několik rozšíření, přičemž v každém znamená forall něco trochu jiného. IMHO nejpraktičtější je jeho použití v existenčních typech, například:
data Explosive = forall x. Exploder x => Expl xTímto způsobem se dá zbavit explicitního typového parametru, takže pak můžu mít seznam typu [Explosive], třeba [Expl Landmine, Expl Torpedo, Expl Turkey].
Co značí to Exploder?
Takže analogicky:
data Err = forall x. Maybe x => Just x
apply :: [Err] -> String
apply xs = ...
apply [Just "text", Just 42, Just True]
?
Přidám otázku: Dokážeš popsat tu ideu existenčních typů?
Exploder je nějaká třída, třeba s funkcemi explode a defuse. Ve svém příkladu akorát dosaď za Maybe nějakou třídu (a Just bych přejmenoval na nějaký unikátní konstruktor hodnot), pak to bude přesně ono.
{-# LANGUAGE ExistentialQuantification #-}
data Person = Person String String
x = Person "John" "Dee"
x2 = Person "Jan" "Marek"
x3 = 42
data Printable = forall x. Show x => x
instance Show Person where
show (Person name surname) = "name: " ++ name ++ ", surname: " ++ surname
format :: [Printable] -> String
format xs = concat $ map show xs
main = do
putStrLn $ format [x, x2, x3]
Pokud jsem to dobře pochopil, tak si nevím rady s tím data Printable = forall x. Show x => x. Když to zkouším podle typů, tak se mi to celé rozpadne. Evidentně špatně chápu nějaký princip.
-
Tak už to mám:
{-# LANGUAGE ExistentialQuantification #-}
data Person = Person String String
x = Person "John" "Dee"
data Printable = forall x. Show x => Print x
instance Show Person where
show (Person name surname) = "name: " ++ name ++ ", surname: " ++ surname
format :: [Printable] -> String
format xs = concat $ map apply xs
where
apply (Print x) = show x
main = do
putStrLn $ format [Print x, Print 42, Print "!"]
Takže závěr: V tomto případě jsou ExistentialQuantification zneužitý na to, aby šlo vytvářet kolekci tříd, protože toto naivní v Haskellu neprojde:
format :: [Show] -> String
...
... format ["text", 42, True]
Chápu to dobře?
Předpokládám, že je to obecný koncept. Třeba na https://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types píšou, že
data ShowBox = forall s. Show s => SB sje ekvivalentní:
data ShowBox = SBUnit | SBInt Int | SBBool Bool | SBIntList [Int] | ...s tím, že si domýšlím, že jakmile přidám instanci Show, tak se automaticky rozšíří.
Ale furt mi to příjde jen jako řešení problému pole tříd. Užitečné, a supr.
Umí to víc?
-
toto naivní v Haskellu neprojde:
format :: [Show] -> String
...
... format ["text", 42, True]
To neprojde, protože Show má druh *→* a pokud se uvede typová proměnná, musela by mít stejnou hodnotu pro všechny prvky kolekce.
-
Umí to víc?
Umí to "higher-rank types". Když se forall explicitně neuvede, je jeho působnost v případě funkcí přes celý typ. Kvantifikátory jdou vytáhnout jen z konsekventu, takže v antecedentu je nutné uvést forall explicitně.
-
Umí to víc?
Umí to "higher-rank types". Když se forall explicitně neuvede, je jeho působnost v případě funkcí přes celý typ. Kvantifikátory jdou vytáhnout jen z konsekventu, takže v antecedentu je nutné uvést forall explicitně.
Když by si to řekl česky :) (A tím nemám na mysli konsekvent a antecedent.)
-
Umí to víc?
Umí to "higher-rank types". Když se forall explicitně neuvede, je jeho působnost v případě funkcí přes celý typ. Kvantifikátory jdou vytáhnout jen z konsekventu, takže v antecedentu je nutné uvést forall explicitně.
Když by si to řekl česky :) (A tím nemám na mysli konsekvent a antecedent.)
Jde o to, že ∀x.(A→B) je něco jiného, než (∀x.A)→B, to první je běžný rozsah platnosti kvantifikátoru u generických typů (nejen v Haskellu), kdežto to druhé je divná haskellí věc (rank 2). Ten kvantifikátor nejde vytáhnout ven bez změny významu.
-
Umí to víc?
Umí to "higher-rank types". Když se forall explicitně neuvede, je jeho působnost v případě funkcí přes celý typ. Kvantifikátory jdou vytáhnout jen z konsekventu, takže v antecedentu je nutné uvést forall explicitně.
Když by si to řekl česky :) (A tím nemám na mysli konsekvent a antecedent.)
Jde o to, že ∀x.(A→B) je něco jiného, než (∀x.A)→B, to první je běžný rozsah platnosti kvantifikátoru u generických typů (nejen v Haskellu), kdežto to druhé je divná haskellí věc (rank 2). Ten kvantifikátor nejde vytáhnout ven bez změny významu.
Typ je taková věc, která zajistí, aby ti tam nepřišla špatná data.
Maybe je k tomu, aby si mohl vrátit libovolnou hodnotu nebo chybu, a nemusel jsi tu hodnotu na chybu znásilňovat.
Výjimka je systém, který umožní, aby si psal optimistickej kód, protože chyba (například dělení nulou) se ti vrátí jiným způsobem a automaticky a zaručeně.
forall a ExistentialQuantification se v Haskelu používají na to, aby si mohl mít omezení jen na třídu. Například pole prvků nějaké třídy. Protože normálně by si to pole musel mít homogení, tedy pole typu. Pole třídy nejde.
... takhle jsem myslel to česky.
-
[...]
... takhle jsem myslel to česky.
“Takhle česky” to moc nejde, přinejmenším ne slušně, IMHO je to dost na houby, protože univerzálně kvantifikovaná typová proměnná v antecedentu předpokládá generickou funkci, a těch je v praxi jak šafránu. Možná nějaký kovaný haskellista má nějaký triviální příklad.
Takhle polopatisticky umím vysvětlit možná závislostní typy, ale higher rank ne.
-
[...]
... takhle jsem myslel to česky.
“Takhle česky” to moc nejde, přinejmenším ne slušně, IMHO je to dost na houby, protože univerzálně kvantifikovaná typová proměnná v antecedentu předpokládá generickou funkci, a těch je v praxi jak šafránu. Možná nějaký kovaný haskellista má nějaký triviální příklad.
Rozumím. To neva. Už jen s tím forall jsi mi ohromně pomohl. Pánbůch ti to oplať na dětech.
Takhle polopatisticky umím vysvětlit možná závislostní typy, ...
To beru! Rvi to do mě! (Posledně jsem to moc nedal, tak třeba teď mi to půjde líp.)
-
To beru! Rvi to do mě! (Posledně jsem to moc nedal, tak třeba teď mi to půjde líp.)
To není v principu problém, ale vyžaduje to netriviální základy, přinejmenším dobrou znalost Curryho-Howardovy korespondence (což ale není nijak složité). Navíc ta hlavní magie okolo záv. typů ("aha moment") přijde až poté, co se člověk prohrabe mnoha zdánlivě nudnými a neužitečnými příklady. Ale jestli tě to neodrazuje, tak to můžeme zkusit, akorát moc nevím, kde začít, aby to na tebe nebylo ze začátku moc náročné, nebo naopak směšně triviální.
-
To beru! Rvi to do mě! (Posledně jsem to moc nedal, tak třeba teď mi to půjde líp.)
To není v principu problém, ale vyžaduje to netriviální základy, přinejmenším dobrou znalost Curryho-Howardovy korespondence (což ale není nijak složité). Navíc ta hlavní magie okolo záv. typů ("aha moment") přijde až poté, co se člověk prohrabe mnoha zdánlivě nudnými a neužitečnými příklady. Ale jestli tě to neodrazuje, tak to můžeme zkusit, akorát moc nevím, kde začít, aby to na tebe nebylo ze začátku moc náročné, nebo naopak směšně triviální.
Zkusme pro začátek nastřelit, k čemu ZT mohou být dobré. Tím pro blbečky stylem, který jsem ukázal výše.
-
Zkusme pro začátek nastřelit, k čemu ZT mohou být dobré. Tím pro blbečky stylem, který jsem ukázal výše.
To jde sfouknout rychle, prostě přinášejí vyšší bezpečnost v době překladu. Umožňují podchytit některé případy, které by se jinak projevily chybou za běhu, třeba “index out of bounds” nebo dělení nulou. Rozdíl mezi jazyky majícími záv. typy bývá v tom, jestli ty důkazy musí psát vývojář, nebo jestli je překladač musí odvodit sám (to druhé bývá z principu věci nedokonalé). IMHO je pro začátečníka dobré zabývat se nejprve tím prvním případem, tj. naučit se psát vše explicitně.
-
Asi nejjednodušší příklad je dokazování, že nějaké číslo není nula (aby například nedošlo k dělení nulou). Takový predikát se dá jednoduše vyjádřit záv. typem:
data NonZero : Nat -> TypeDá se to brát jako běžná uzavřená formule v logice, jež je unární a říká něco o přirozených číslech.
Aby to bylo k něčemu v praxi, musí se k tomu ale navíc napsat funkce, která pro každý typově správný vstup řekne, zda je predikát splněn:
isNonZero : (n:Nat) -> Dec (NonZero n)Generický typ Dec má dva konstruktory, Yes a No, kde Yes má jako parametr důkaz platnosti predikátu pro daný vstup a No důkaz kontradikce (tj. důkaz Pred->Void, protože jsme v intuicionistické logice). Existence takovéto funkce vlastně říká, že daný predikát je úplný (pro každý vstup existuje důkaz buď jeho platnosti, nebo neplatnosti). Potom můžu mít funkci pro dělení:
div : Nat -> (y:Nat) -> NonZero y -> NatTato funkce je totální, protože pro nulu ve druhém parametru není definovaná (nejde zavolat, protože nejde vytvořit instance (důkaz) predikátu NonZero Z). Takový program je zřejmě bezpečnější, protože za běhu nemůže dojít k chybě při volání div.
-
Asi nejjednodušší příklad je dokazování, že nějaké číslo není nula (aby například nedošlo k dělení nulou). Takový predikát se dá jednoduše vyjádřit záv. typem:
data NonZero : Nat -> TypeDá se to brát jako běžná uzavřená formule v logice, jež je unární a říká něco o přirozených číslech.
NonZero určuje tu nenulovost, ok. Nat určuje přirozené číslo - "pro každé přirozené číslo". A to Type tam hraje jakou roli?
Aby to bylo k něčemu v praxi, musí se k tomu ale navíc napsat funkce, která pro každý typově správný vstup řekne, zda je predikát splněn:
isNonZero : (n:Nat) -> Dec (NonZero n)Generický typ Dec má dva konstruktory, Yes a No, kde Yes má jako parametr důkaz platnosti predikátu pro daný vstup a No důkaz kontradikce (tj. důkaz Pred->Void, protože jsme v intuicionistické logice). Existence takovéto funkce vlastně říká, že daný predikát je úplný (pro každý vstup existuje důkaz buď jeho platnosti, nebo neplatnosti).
Dobře. A tak já si tu funkci takto (humpolácky naimplementuju):
isNonZero 0 = No (NonZero 0)
isNonZero x = Yes (NonZero x)
Chytám se?
Potom můžu mít funkci pro dělení:
div : Nat -> (y:Nat) -> NonZero y -> NatTato funkce je totální, protože pro nulu ve druhém parametru není definovaná (nejde zavolat, protože nejde vytvořit instance (důkaz) predikátu NonZero Z). Takový program je zřejmě bezpečnější, protože za běhu nemůže dojít k chybě při volání div.
Všemu rozumím, až na počet těch argumentů.
let a = 5
let b = 0
let x = div a b .... ?
Proč není ta signatura takto?
div : Nat -> NonZero -> Nat
-
Asi nejjednodušší příklad je dokazování, že nějaké číslo není nula (aby například nedošlo k dělení nulou). Takový predikát se dá jednoduše vyjádřit záv. typem:
data NonZero : Nat -> TypeDá se to brát jako běžná uzavřená formule v logice, jež je unární a říká něco o přirozených číslech.
NonZero určuje tu nenulovost, ok. Nat určuje přirozené číslo - "pro každé přirozené číslo". A to Type tam hraje jakou roli?
NonZero je prachobyčejná funkce, takže Nat->Type je funkce z přirozených čísel do typů. Tohle je v praxi trochu trik, protože Type v překladači reprezentuje nekonečnou množinu (meta)typů různých úrovní (něco na způsob Cantorova paradoxu). To ale není pro základní pochopení záv. typů podstatné. Type je prostě "typ typů".
Aby to bylo k něčemu v praxi, musí se k tomu ale navíc napsat funkce, která pro každý typově správný vstup řekne, zda je predikát splněn:
isNonZero : (n:Nat) -> Dec (NonZero n)Generický typ Dec má dva konstruktory, Yes a No, kde Yes má jako parametr důkaz platnosti predikátu pro daný vstup a No důkaz kontradikce (tj. důkaz Pred->Void, protože jsme v intuicionistické logice). Existence takovéto funkce vlastně říká, že daný predikát je úplný (pro každý vstup existuje důkaz buď jeho platnosti, nebo neplatnosti).
Dobře. A tak já si tu funkci takto (humpolácky naimplementuju):
isNonZero 0 = No (NonZero 0)
isNonZero x = Yes (NonZero x)
Chytám se?
Problém je, že NonZero n je typ, ale Yes musí mít jako parametr nějakou jeho hodnotu. Takže třeba si všimnu, že když n je přirozené číslo, tak jeho následovník je nenulový. Takže můžu mít konstruktor SuccNZ, který mi potřebný důkaz poskytne:
isNonZero : (n:Nat) -> Dec (NonZero n)
isNonZero Z = No absurd
isNonZero (S n) = Yes (SuccNZ n)
U No je to trochu složitější, protože musím prokázat, že NonZero 0 neplatí (implikuje Void). K tomu má překladač magickou pomůcku: absurd.
Potom můžu mít funkci pro dělení:
div : Nat -> (y:Nat) -> NonZero y -> NatTato funkce je totální, protože pro nulu ve druhém parametru není definovaná (nejde zavolat, protože nejde vytvořit instance (důkaz) predikátu NonZero Z). Takový program je zřejmě bezpečnější, protože za běhu nemůže dojít k chybě při volání div.
Všemu rozumím, až na počet těch argumentů.
let a = 5
let b = 0
let x = div a b .... ?Proč není ta signatura takto?
div : Nat -> NonZero -> Nat
Potřebuješ dva číselné parametry, první je dělenec a to y je dělitel. Třetí argument typu NonZero y zajistí, že dělitel není nula, viz SuccNZ výše. Ten třetí "dokazovací" argument může překladač za určitých okolností uhádnout sám, ale o to teď nejde.
-
Asi nejjednodušší příklad je dokazování, že nějaké číslo není nula (aby například nedošlo k dělení nulou). Takový predikát se dá jednoduše vyjádřit záv. typem:
data NonZero : Nat -> TypeDá se to brát jako běžná uzavřená formule v logice, jež je unární a říká něco o přirozených číslech.
NonZero určuje tu nenulovost, ok. Nat určuje přirozené číslo - "pro každé přirozené číslo". A to Type tam hraje jakou roli?
K tomuhle ještě dodám, že NonZero n je typ pro každé přirozené číslo, ale jen pro nenulová je obydlený (anglicky inhabited, tj. má nějakou hodnotu). Tohle je celý princip Curryho-Howardovy korespondence, když totiž neexistuje žádná hodnota nějakého typu, není co předat do funkce očekávající na vstupu tento typ, takže si ji můžu nadefinovat, ale nejde zavolat. IMHO je u záv. typů matoucí, že míchají normální typy (čísla, řetězce...) s logickými výroky, těžko se v tom pak orientuje. Já vždycky v hlavě u záv. typů “přepnu” na predikátovou logiku, abych se v tom vyznal. Asi to je jen o zvyku nebo jako u monád o dosažení “osvícení,” kdy to udělá klik a člověk si řekne “aha, tak takhle to funguje”.
-
Asi nejjednodušší příklad je dokazování, že nějaké číslo není nula (aby například nedošlo k dělení nulou). Takový predikát se dá jednoduše vyjádřit záv. typem:
data NonZero : Nat -> TypeDá se to brát jako běžná uzavřená formule v logice, jež je unární a říká něco o přirozených číslech.
NonZero určuje tu nenulovost, ok. Nat určuje přirozené číslo - "pro každé přirozené číslo". A to Type tam hraje jakou roli?
NonZero je prachobyčejná funkce, takže Nat->Type je funkce z přirozených čísel do typů. Tohle je v praxi trochu trik, protože Type v překladači reprezentuje nekonečnou množinu (meta)typů různých úrovní (něco na způsob Cantorova paradoxu). To ale není pro základní pochopení záv. typů podstatné. Type je prostě "typ typů".
data NonZero : Nat -> Type "typ NonZero je funkce která mi pro přirozené číslo vrátí typ Type". Snad ok.
Aby to bylo k něčemu v praxi, musí se k tomu ale navíc napsat funkce, která pro každý typově správný vstup řekne, zda je predikát splněn:
isNonZero : (n:Nat) -> Dec (NonZero n)Generický typ Dec má dva konstruktory, Yes a No, kde Yes má jako parametr důkaz platnosti predikátu pro daný vstup a No důkaz kontradikce (tj. důkaz Pred->Void, protože jsme v intuicionistické logice). Existence takovéto funkce vlastně říká, že daný predikát je úplný (pro každý vstup existuje důkaz buď jeho platnosti, nebo neplatnosti).
Dobře. A tak já si tu funkci takto (humpolácky naimplementuju):
isNonZero 0 = No (NonZero 0)
isNonZero x = Yes (NonZero x)
Chytám se?
Problém je, že NonZero n je typ, ale Yes musí mít jako parametr nějakou jeho hodnotu. Takže třeba si všimnu, že když n je přirozené číslo, tak jeho následovník je nenulový. Takže můžu mít konstruktor SuccNZ, který mi potřebný důkaz poskytne:
isNonZero : (n:Nat) -> Dec (NonZero n)
isNonZero Z = No absurd
isNonZero (S n) = Yes (SuccNZ n)
U No je to trochu složitější, protože musím prokázat, že NonZero 0 neplatí (implikuje Void). K tomu má překladač magickou pomůcku: absurd.
OK, je to tedy hodně jinak.
Já mám teď problém, že jsi přihodil další neznámé.
Z by mohlo být Neutrální prvek.
S by mohl být ... nechytám se. A SuccNZ by mohl být následující prvek. Ale následující v jaké řadě? Jako definován pro čísla, něco jako Ord? A co znamená to *NZ?
Potom můžu mít funkci pro dělení:
div : Nat -> (y:Nat) -> NonZero y -> NatTato funkce je totální, protože pro nulu ve druhém parametru není definovaná (nejde zavolat, protože nejde vytvořit instance (důkaz) predikátu NonZero Z). Takový program je zřejmě bezpečnější, protože za běhu nemůže dojít k chybě při volání div.
Všemu rozumím, až na počet těch argumentů.
let a = 5
let b = 0
let x = div a b .... ?Proč není ta signatura takto?
div : Nat -> NonZero -> Nat
Potřebuješ dva číselné parametry, první je dělenec a to y je dělitel. Třetí argument typu NonZero y zajistí, že dělitel není nula, viz SuccNZ výše. Ten třetí "dokazovací" argument může překladač za určitých okolností uhádnout sám, ale o to teď nejde.
Proč potřebuju ten dokazovací argument? Proč prostě nemohu napsat div : Nat -> NonZero -> Nat, tím přeci vyjadřuju, že dělenec je nenulový. A mašina si na pozadí odvodí, že nemohu zapsat
let a = 5
let b = 0
let x = div a b, protože nesedí typ, b je Nat, zatímco očekvám NonZero (ten jsem si definoval výše).
Předpokládám, že to bude podobná zábava jako u těch forall. Tedy, že bych sice mohl napsat [Show], ale ExistentialQuantification jsou obecnější, a tak se na to zneužijí. Mýlím se?
-
Aby to bylo k něčemu v praxi, musí se k tomu ale navíc napsat funkce, která pro každý typově správný vstup řekne, zda je predikát splněn:
isNonZero : (n:Nat) -> Dec (NonZero n)Generický typ Dec má dva konstruktory, Yes a No, kde Yes má jako parametr důkaz platnosti predikátu pro daný vstup a No důkaz kontradikce (tj. důkaz Pred->Void, protože jsme v intuicionistické logice). Existence takovéto funkce vlastně říká, že daný predikát je úplný (pro každý vstup existuje důkaz buď jeho platnosti, nebo neplatnosti).
Dobře. A tak já si tu funkci takto (humpolácky naimplementuju):
isNonZero 0 = No (NonZero 0)
isNonZero x = Yes (NonZero x)
Chytám se?
Problém je, že NonZero n je typ, ale Yes musí mít jako parametr nějakou jeho hodnotu. Takže třeba si všimnu, že když n je přirozené číslo, tak jeho následovník je nenulový. Takže můžu mít konstruktor SuccNZ, který mi potřebný důkaz poskytne:
isNonZero : (n:Nat) -> Dec (NonZero n)
isNonZero Z = No absurd
isNonZero (S n) = Yes (SuccNZ n)
U No je to trochu složitější, protože musím prokázat, že NonZero 0 neplatí (implikuje Void). K tomu má překladač magickou pomůcku: absurd.
OK, je to tedy hodně jinak.
Já mám teď problém, že jsi přihodil další neznámé.
Z by mohlo být Neutrální prvek.
S by mohl být ... nechytám se. A SuccNZ by mohl být následující prvek. Ale následující v jaké řadě? Jako definován pro čísla, něco jako Ord? A co znamená to *NZ?
Potom můžu mít funkci pro dělení:
div : Nat -> (y:Nat) -> NonZero y -> NatTato funkce je totální, protože pro nulu ve druhém parametru není definovaná (nejde zavolat, protože nejde vytvořit instance (důkaz) predikátu NonZero Z). Takový program je zřejmě bezpečnější, protože za běhu nemůže dojít k chybě při volání div.
Všemu rozumím, až na počet těch argumentů.
let a = 5
let b = 0
let x = div a b .... ?Proč není ta signatura takto?
div : Nat -> NonZero -> Nat
Potřebuješ dva číselné parametry, první je dělenec a to y je dělitel. Třetí argument typu NonZero y zajistí, že dělitel není nula, viz SuccNZ výše. Ten třetí "dokazovací" argument může překladač za určitých okolností uhádnout sám, ale o to teď nejde.
Proč potřebuju ten dokazovací argument? Proč prostě nemohu napsat div : Nat -> NonZero -> Nat, tím přeci vyjadřuju, že dělenec je nenulový. A mašina si na pozadí odvodí, že nemohu zapsat
let a = 5
let b = 0
let x = div a b, protože nesedí typ, b je Nat, zatímco očekvám NonZero (ten jsem si definoval výše).
Předpokládám, že to bude podobná zábava jako u těch forall. Tedy, že bych sice mohl napsat [Show], ale ExistentialQuantification jsou obecnější, a tak se na to zneužijí. Mýlím se?
Význam Z a S je dán tímto:
data Nat = Z | S NatTakže jde o nulu a funkci následovníka.
SuccNZ (=“my successor is nonzero”) je tady stěžejní, je to konstruktor říkající, že následník jeho argumentu je nenulový. Koukni na to opačně, když chceš dokázat, že nějaké číslo je nenulové, jako důkaz poskytneš jeho předchůdce. U nuly to ale nemůžeš udělat, ta předchůdce nemá.
K té signatuře: dělenec i dělitel jsou typu Nat, navíc všimni si, že typ NonZero je generický a jeho hodnoty nejsou čísla. Jeho hodnota v podstatě říká, že sis dal tu práci a sesmolil důkaz nenulovosti dělitele (nebo že to za tebe udělal překladač). Tohle je princip vývoje se záv. typy, typicky neměníš typy v signaturách, jen přidáváš dokazovací argumenty (které před generováním kódu překladač zahodí).
-
K tomu dotazu na Type, to je taková divná věc, protože správně by to mělo být Typen, tj. typ základních typů Type0, např. Int:Type0 nebo String:Type0. Jenže NonZero je typu Nat->Type0, takže vlastně platí Nat->Type0:Type1, ovšem v praxi se ty indexy neuvádějí. (Tohle se v teorii typů jmenuje kumulativní hierarchie typů.)
Asi to není moc intuitivní, názornější to je na logické straně CH korespondence. Můžu mít formuli nonzero(x), což je nultá úroveň, ale taky decidable(nonzero(x)) (argumentem je formule) atd. Tohle bych nerad dál rozebíral, aby tě to zbytečně nemátlo a neodvádělo od jádra věci. Možná později ;)
-
Proč potřebuju ten dokazovací argument? Proč prostě nemohu napsat div : Nat -> NonZero -> Nat, tím přeci vyjadřuju, že dělenec je nenulový. A mašina si na pozadí odvodí, že nemohu zapsat
let a = 5
let b = 0
let x = div a b, protože nesedí typ, b je Nat, zatímco očekvám NonZero (ten jsem si definoval výše).
Tohle by bylo alternativní řešení (v podstatě bez záv. typů). Mohl bych mít:
div : Nat -> PosNat -> NatJenže to vyžaduje funkce pro převod mezi oběma typy:
data PosNat = One | S' PosNat
posNatFromNat : Nat -> PosNat
posNatFromNat (S Z) = One
posNatFromNat (S n) = S' (posNatFromNat n)
natFromPosNat : PosNat -> Nat
natFromPosNat One = S Z
natFromPosNat (S' n) = S (natFromPosNat n)
Bohužel posNatFromNat není totální, takže aby to bylo "čisté" řešení, musela by ta převodní funkce vracet Maybe PosNat. Ale je to validní alternativa.
Předpokládám, že to bude podobná zábava jako u těch forall. Tedy, že bych sice mohl napsat [Show], ale ExistentialQuantification jsou obecnější, a tak se na to zneužijí. Mýlím se?
Show je generický typ, takže [Show] by byl seznam funktorů a [Show a] s typovým parametrem akorát zafixuje ten parametr. Ale obecně ano, je to hodně silný nástroj aplikovaný na poměrně jednoduchý problém. Neříkal bych tomu zneužití, je to prostě jako kopání základů na dům bagrem, i když by to šlo ručně lopatou.
BTW všimni si, jak se mění signatura. Při použití záv. typů se nemění typy vstupních parametrů ani výstupu, jen se přidá dodatečný parametr, se kterým se pracuje jen v době překladu. Bez použití záv. typů musím buď změnit typ(y) vstupu (PosNat), nebo výstupu (div : Nat -> Nat -> Maybe Nat). Většinou se dělá to druhé, z čehož vyplývá, že musím nějak ověřit nebo rozbalit výstupní hodnotu (jestli tam není Nothing). U záv. typů naopak ověřuju ("dokazuju") správnost vstupu, se špatným nejde funkce vůbec zavolat (resp. vyhodnotit). Dělám tak z nějaké problematické funkce funkci totální omezením jejího def. oboru (domény). Jakmile tohle člověk pochopí, je to hezký praktický příklad omílaného "the analytical and problem solving skills acquired by studying mathematics", sice to není moc praktické (mainstreamové jazyky záv. typy téměř nemají), ale přinejmenším to rozšiřuje obzory, člověk pak ví, že vrcholem typového systému nejsou generické typy ani HKT.
-
mašina si na pozadí odvodí, že nemohu zapsat
let a = 5
let b = 0
let x = div a b, protože nesedí typ
Na tohle jsem zapomněl. Tohle jde snadno odvodit v případě konstant (nebo obecně něčeho na způsob constexpr), ale když dělitel přijde třeba ze vstupu, tak ho musíš na PosNat převést explicitně. Tohle se moc nedělá, IMHO protože kromě testu na nenulovost dělitele (ten se v obecném případě musí provést vždy) je tam i to přetypování za běhu, jenže my chceme řešit typové neshody v době překladu ("well-typedness"), ať to pak nezdržuje (podobně funguje Rust, překladač taky extrémně šaškuje při překladu, aby se za běhu nemusely řešit zbytečnosti).
-
BTW všimni si, jak se mění signatura. Při použití záv. typů se nemění typy vstupních parametrů ani výstupu, jen se přidá dodatečný parametr, se kterým se pracuje jen v době překladu. Bez použití záv. typů musím buď změnit typ(y) vstupu (PosNat), nebo výstupu (div : Nat -> Nat -> Maybe Nat). Většinou se dělá to druhé, z čehož vyplývá, že musím nějak ověřit nebo rozbalit výstupní hodnotu (jestli tam není Nothing). U záv. typů naopak ověřuju ("dokazuju") správnost vstupu, se špatným nejde funkce vůbec zavolat (resp. vyhodnotit). Dělám tak z nějaké problematické funkce funkci totální omezením jejího def. oboru (domény). Jakmile tohle člověk pochopí, je to hezký praktický příklad omílaného "the analytical and problem solving skills acquired by studying mathematics", sice to není moc praktické (mainstreamové jazyky záv. typy téměř nemají), ale přinejmenším to rozšiřuje obzory, člověk pak ví, že vrcholem typového systému nejsou generické typy ani HKT.
Tady si tě trochu nasměruju - toto je mi velmi dobře jasné. I když se hodí, že jsi to vyjádřil.
Já mám problém se dvěma věcmi:
1/ Syntaxe
2/ Myšlenka
Můžeš si všimnout, že si mlátím zuby o to, proč přidáváš argumenty té funkci div. (Skutečně je přidáváš, nebo jen jako přidáváš? Jak vypadá volání té funkce?)
Představuji si následující kód:
divide a b = a `div` b
calculate x = divide 42 x
main :: IO ()
main = do
args <- getArgs
case parseArgs args of
Left x -> putStrLn $ "ERROR: " ++ x
Right x -> putStrLn $ "--> " ++ (show (calculate x))
where
parseArgs [] = Left "uvedte argument"
parseArgs (x:_) = case (readMaybe x :: Maybe Int) of
Nothing -> Left $ "uvedte číselný argument: " ++ (show x)
Just x -> Right x
Jak by si ho upravil aby nepadal na dělení nulou?
Tedy předpokládám, že už někde u volání funkce calculate mi kompiler musí vynadat, že parsuju na prosté Int. Bez závislostních typů bych udělal něco jako readMaybe x :: Maybe NotZeroInt, což by mohlo fungovat (nebo jakkoliv jinak podobně).
Jak to udělám pomocí závislostních typů?
Zatím nabírám pocit, že ty ZT fungují tak nějak jako že mám obecnou kostru nějakého typu/funkce/výrazu - a pak k němu přilepuju další a další podmínky. Ale taky mohu být úplně mimo.
-
BTW všimni si, jak se mění signatura. Při použití záv. typů se nemění typy vstupních parametrů ani výstupu, jen se přidá dodatečný parametr, se kterým se pracuje jen v době překladu. Bez použití záv. typů musím buď změnit typ(y) vstupu (PosNat), nebo výstupu (div : Nat -> Nat -> Maybe Nat). Většinou se dělá to druhé, z čehož vyplývá, že musím nějak ověřit nebo rozbalit výstupní hodnotu (jestli tam není Nothing). U záv. typů naopak ověřuju ("dokazuju") správnost vstupu, se špatným nejde funkce vůbec zavolat (resp. vyhodnotit). Dělám tak z nějaké problematické funkce funkci totální omezením jejího def. oboru (domény). Jakmile tohle člověk pochopí, je to hezký praktický příklad omílaného "the analytical and problem solving skills acquired by studying mathematics", sice to není moc praktické (mainstreamové jazyky záv. typy téměř nemají), ale přinejmenším to rozšiřuje obzory, člověk pak ví, že vrcholem typového systému nejsou generické typy ani HKT.
Tady si tě trochu nasměruju - toto je mi velmi dobře jasné. I když se hodí, že jsi to vyjádřil.
Já mám problém se dvěma věcmi:
1/ Syntaxe
2/ Myšlenka
Můžeš si všimnout, že si mlátím zuby o to, proč přidáváš argumenty té funkci div. (Skutečně je přidáváš, nebo jen jako přidáváš? Jak vypadá volání té funkce?)
Skutečně se přidávají (v době překladu), sice existují i tzv. skryté (automaticky odvozované) "důkazy", ale ty jsem schválně vynechal, protože naučit se to dá jen s explicitním uváděním všech argumentů. Volání by pak bylo něco jako
div 10 5 (SuccNZ 4)
-
Skutečně se přidávají (v době překladu), ... "důkazy", ...
Takže ta funkce je tvořena: jméno + argumenty + důkazy? Tak je to myšleno?
Volání by pak bylo něco jako
div 10 5 (SuccNZ 4)
Takže:
calculate x = divide 42 x (SuccNZ (dec x))?
-
Zatím nabírám pocit, že ty ZT fungují tak nějak jako že mám obecnou kostru nějakého typu/funkce/výrazu - a pak k němu přilepuju další a další podmínky. Ale taky mohu být úplně mimo.
Jo, tak to je (v některých případech, jak u toho dělení nulou), takže tvůj pocit tě neklame.
Pak ale existují i záv. typy jako Vect n a, kde se přidá argument přímo do typu, ne k funkci (tohle je rozšíření List a).
V zásadě to chápeš správně, přilepují se podmínky, čímž se zvýší bezpečnost (nedojde k chybě za běhu).
-
... čímž se zvýší bezpečnost (nedojde k chybě za běhu).
Tato motivace je mi zcela jasná :-) Proto se vůbec statickými jazyky zabejvám.
-
Skutečně se přidávají (v době překladu), ... "důkazy", ...
Takže ta funkce je tvořena: jméno + argumenty + důkazy? Tak je to myšleno?
Přesně tak. V praxi ten důkaz ideálně dodá překladač. Kód příkladu teď píšu :)
-
... čímž se zvýší bezpečnost (nedojde k chybě za běhu).
Tato motivace je mi zcela jasná :-) Proto se vůbec statickými jazyky zabejvám.
U běžných stat. typů to je ale triviální, záv. typy jsou vyšší level :)
-
Jak by si ho upravil aby nepadal na dělení nulou?
V principu nějak takto:
calculate : Nat -> Nat
calculate n = case isNonZero n of
Yes prf => div 42 n prf
No contra => ...
Tahle funkce je už trochu pozdě na ten test na nenulovost, ale podstatné je, že isNonZero ti dá na zlatém podnosu důkaz nenulovosti, jejž chce div. A na rozdíl od testování obsahu Maybe se tady (u Dec) nic nezbaluje, ten důkaz (prf) existuje jen v době překladu, takže za běhu má div pouze dva argumenty, jak by běžný matematik čekal.
-
Tahle funkce je už trochu pozdě na ten test na nenulovost,
Co tím myslíš? Že jsi ten příklad přizpůsobil mému kódu, nebo to je idiomatické použití ZT?
-
Tahle funkce je už trochu pozdě na ten test na nenulovost,
Co tím myslíš? Že jsi ten příklad přizpůsobil mému kódu, nebo to je idiomatické použití ZT?
Myslím jen to, že když calculate vrací číslo, tak není jak ohlásit chybu, proto ty tři tečky. Jinak to je naprosto idiomatické.
Normálně by to chtělo funkci pro načtení nenulového čísla, která vrátí záv. pár, tj. hodnotu typu (n:Nat) ** NonZero n, takže například 27 ** prf. Ale to už jsou nepodstatné detaily.
-
Jak by si ho upravil aby nepadal na dělení nulou?
V principu nějak takto:
calculate : Nat -> Nat
calculate n = case isNonZero n of
Yes prf => div 42 n prf
No contra => ...
Ten pattern mi přijde povědomej:
calculate : Nat -> Maybe Nat
calculate n = case isNonZero n of
Yes prf => Just $ div 42 n prf
No contra => Nothing
versus
calculate : Nat -> Maybe Nat
calculate n = case isNonZero n of
Just x => Just $ div 42 x
Nothing => Nothing
Čímž v žádném případě neútočím proti ZT. Jen chci najít tu pointu.
Tahle funkce je už trochu pozdě na ten test na nenulovost, ale podstatné je, že isNonZero ti dá na zlatém podnosu důkaz nenulovosti, jejž chce div. A na rozdíl od testování obsahu Maybe se tady (u Dec) nic nezbaluje, ten důkaz (prf) existuje jen v době překladu, takže za běhu má div pouze dva argumenty, jak by běžný matematik čekal.
Tady si možná trochu ujasněme výraziva (a následně prosím vypíchni znova tu pointu):
- Za běhu funkce div nikoho nezajímá, nemá dva argumenty, není vůbec... Za běhu je na všechno pozdě a prostě děj se vůle boží.
- Cílem typů (Maybe nebo závislostních), nebo čehokoliv jiného, je přinutit mě, abych ošetřil všechny vstupy. To jsem demonstroval na tom ukázkovém kódu. Přijde string, ten může, ale také nemusí být číslo. A já se musím poprat s oběma variantama. Díky tomu, že funkce div přijímá číslo, a neexistuje funkce pro převod stringu na číslo (ale pouze převod stringu na Maybe číslo), jsem přinucen zohlednit, když se parsování nepovede. To je cíl - nedovolit překlad.
A cílem je něco takového i pro další nevalidní stavy, abych neumožnil nevalidní stav, a pokud to jinak nejde tak byl přinucen zohlednit výjimky.
-
calculate : Nat -> Maybe Nat
calculate n = case isNonZero n of
Yes prf1 => case isNotAllowedValues n of
Yes prf2 => Just $ div 42 n prf1 prf2
No _ => Nothing
No _ => Nothing
Šlo by? Nebo se vzdaluju té myšlence ZT, a přiohýbám si to klasice?
-
- Za běhu funkce div nikoho nezajímá, nemá dva argumenty, není vůbec... Za běhu je na všechno pozdě a prostě děj se vůle boží.
To bych takhle neřekl, myslím, že jádro věci je, že za běhu nikoho nezajímá její třetí argument.
- Cílem typů (Maybe nebo závislostních), nebo čehokoliv jiného, je přinutit mě, abych ošetřil všechny vstupy.[...] jsem přinucen zohlednit, když se parsování nepovede. To je cíl - nedovolit překlad.
Jo, takhle to je. Bez záv. typů si může člověk ohlídat jen běžné typy (číslo vs. řetězec apod.), ktežto u záv. typů jdou hlídat i hodnoty (nenulovost, neprázdnost řetězce atd.). Je to prostě stejný princip o krok dál (i když implementačně to je o dost složitější a matematicky taky, typy už nejsou jedna kategorie, ale celá kumulativní hierarichie toposů).
V praxi rozhoduje, nakolik umí překladač odvodit typy. V Rustu nebo Go se taky většinou neuvádí int nebo i32 a jiné typy, když jdou odvodit automaticky. U záv. typů to jde často taky (naštěstí, protože psát je explicitně by byl opruz). Navíc překladače mají interaktivní mód, když místo výrazu napíšeš otazník (například ?prf), tak se provede typová kontrola a překladač ti napoví hodnotu a typ. To hodně pomáhá, hlavně při psaní důkazů rovnosti (typy tvaru x = y).
-
Teď jsem si uvědomil, že to parsování vstupu je trochu zavádějící. Protože je to jen jedna množina problémů. Pak tu mám druhou, například takto:
divide a b = a `div` b
calculate x = divide 42 x
main :: IO ()
main = do
putStrLn $ "--> " ++ (show (calculate (a + b)))
where
a = 4
b = -4
Tam mě žádné Maybe nezachrání.
-
calculate : Nat -> Maybe Nat
calculate n = case isNonZero n of
Yes prf1 => case isNotAllowedValues n of
Yes prf2 => Just $ div 42 n prf1 prf2
No _ => Nothing
No _ => Nothing
Šlo by? Nebo se vzdaluju té myšlence ZT, a přiohýbám si to klasice?
Jo, to by šlo.
-
Teď jsem si uvědomil, že to parsování vstupu je trochu zavádějící. Protože je to jen jedna množina problémů. Pak tu mám druhou, například takto:
divide a b = a `div` b
calculate x = divide 42 x
main :: IO ()
main = do
putStrLn $ "--> " ++ (show (calculate (a + b)))
where
a = 4
b = -4
Tam mě žádné Maybe nezachrání.
Tohle je super příklad, vybízí k napsání funkce minus nad Nat, která je totální a akceptuje jen vstupy, kde menšenec je větší nebo roven menšiteli.
-
- Za běhu funkce div nikoho nezajímá, nemá dva argumenty, není vůbec... Za běhu je na všechno pozdě a prostě děj se vůle boží.
To bych takhle neřekl, myslím, že jádro věci je, že za běhu nikoho nezajímá její třetí argument.
No, trochu si zatrucuju: já bych to tak řekl :-) Ale rád si to nechám vysvětlit.
- Cílem typů (Maybe nebo závislostních), nebo čehokoliv jiného, je přinutit mě, abych ošetřil všechny vstupy.[...] jsem přinucen zohlednit, když se parsování nepovede. To je cíl - nedovolit překlad.
Jo, takhle to je. Bez záv. typů si může člověk ohlídat jen běžné typy (číslo vs. řetězec apod.), ktežto u záv. typů jdou hlídat i hodnoty (nenulovost, neprázdnost řetězce atd.). Je to prostě stejný princip o krok dál (i když implementačně to je o dost složitější a matematicky taky, typy už nejsou jedna kategorie, ale celá kumulativní hierarichie toposů).
Tady se domnívám že se jeden z nás plete. Podle mne bez závislostních typů si můžeš ohlídat i nenulovost, neprázdnost řetězce, etc. V tom ten problém není. Příklad:
divide a b = a `div` b
calculate :: NotZero -> Int
calculate x = divide 42 x
main :: IO ()
main = do
putStrLn $ "--> " ++ (show (calculate (a + b)))
where
a = 4
b = -4
Bez ZT i s nima, problém vyřeším stejně. Rozdíl je v tom, že, pokud to dobře chápu, bez ZT mi to vynutí (zbytečný) Maybe, což bude trochu matoucí. Zatímco ZT v pohodě při překladu odvodí, že to "nechci" a nepřeloží. Bez ZT runtime, s ZT compiletime.
-
Budu v té úvaze pokračovat dál:
Nadefinuju si typ NotZero, který bude čistě jen značka. Vynutí mi abych vytvořil "validační" funkci. A nic nebrání kompilátoru, aby tu funkci použil při compiletime pro ověření, zda (a + b) je NotZero.
To bychom měli.
Jenže, 4 + (-4) není NotZero, ale Int. Takže typ neprojde stejně. Ledaže bychom zavedli nějakou dědičnost, kdy je NotZero potomkem Int, etc, etc. Nebo automatické castování, etc, etc. To už je ale jinej svět.
Takže pokud to chápu dobře, tak ZT dělají to, že nechají ten Int Intem, jen přidají pravidla navíc. To pravidlo se tam propaguje pomocí těch dalších argumentů. A kompilátor to "nějak" použije pro ověření.
Mám otázky:
- Uvažuju správně?
- Proč jsou ty ZT tak složitý? Proč nestačí primitivní validační funkce? že by mi unikl ještě třetí scénář validace? Nebo to umí víc?
- Umí to víc?
-
- Za běhu funkce div nikoho nezajímá, nemá dva argumenty, není vůbec... Za běhu je na všechno pozdě a prostě děj se vůle boží.
To bych takhle neřekl, myslím, že jádro věci je, že za běhu nikoho nezajímá její třetí argument.
No, trochu si zatrucuju: já bych to tak řekl :-) Ale rád si to nechám vysvětlit.
Ale ta funkce div tam je, ne? A počítá za běhu.
-
Tady se domnívám že se jeden z nás plete. Podle mne bez závislostních typů si můžeš ohlídat i nenulovost, neprázdnost řetězce, etc.
[...]
Rozdíl je v tom, že, pokud to dobře chápu, bez ZT mi to vynutí (zbytečný) Maybe, což bude trochu matoucí. Zatímco ZT v pohodě při překladu odvodí, že to "nechci" a nepřeloží. Bez ZT runtime, s ZT compiletime.
Chápeš to dobře, nenapsal jsem explicitně "v době překladu" (compile time). Mea culpa.
-
Takže pokud to chápu dobře, tak ZT dělají to, že nechají ten Int Intem, jen přidají pravidla navíc. To pravidlo se tam propaguje pomocí těch dalších argumentů. A kompilátor to "nějak" použije pro ověření.
Přesně! Nechají celočíselný typ (nebo jakýkoliv jiný) na pokoji a jen přidají další argument s "důkazem".
Mám otázky:
- Uvažuju správně?
- Proč jsou ty ZT tak složitý? Proč nestačí primitivní validační funkce? že by mi unikl ještě třetí scénář validace? Nebo to umí víc?
- Umí to víc?
1. Zdá se, že správně ;)
2. Zas tak složité to není, jen je v tom trochu guláš, tohle přišlo od akademiků, kterým evidentně nezáleží na hezké čitelné syntaxi a jasném oddělení argumentů pro běh a pro kontrolu typů (např. číselné argumenty pro dělení vs. důkazy). Primitivní validační funkce ti stačí, ale jak jsi sám psal, bude se vyhodnocovat za běhu.
3. Víc to umí třeba u vektorů a matic.
Jestli si to chceš trochu procvičit, zkus si napsat tohle:
safeminus : (n:Nat) -> (m:Nat) -> GreaterEq n m -> Nat(Pochopitelně tak, aby ta funkce byla totální.)
-
Umí to víc?
Z jiného soudku pak jsou záv. součtové a součinové typy, ty se hodí třeba u těch vektorů.
-
- Za běhu funkce div nikoho nezajímá, nemá dva argumenty, není vůbec... Za běhu je na všechno pozdě a prostě děj se vůle boží.
To bych takhle neřekl, myslím, že jádro věci je, že za běhu nikoho nezajímá její třetí argument.
No, trochu si zatrucuju: já bych to tak řekl :-) Ale rád si to nechám vysvětlit.
Ale ta funkce div tam je, ne? A počítá za běhu.
Ta funkce div tam je. Ale nemá žádné argumenty, o kterých by se dalo uvažovat. Nebo ještě jinak, za běhu s ní vůbec nijak nepracuješ. Tobě, jako programátorovi/matematikovi se ta funkce jeví tak, jak ji vidíš v kódu - tedy div se třemi argumenty.
Primitivní validační funkce ti stačí, ale jak jsi sám psal, bude se vyhodnocovat za běhu.
Počkej, počkej, takto mi to neštymuje.
Zkusme změnit syntax:
isNotZero x = x /= 0
divide :: Int -> a:Int -> Float & isNotZero a
divide a b = a `div` b
calculate x = divide 42 x
- Důkaz píšu jako jméno validační funkce za ampersand.
- Ta validační funkce je úplně nudná.
- Funkci divide volám úplně obyčejně, není třeba ji tam explicitně uvádět.
- Při kompilaci mašina projde graf volání, a je schopna staticky, při kompilaci, ověřit, že při volání divide a b, b není nula.
- To ověření proběhne při kompilaci, nikoliv za běhu.
- Statické ověřování se týká konstantního kódu. Jakmile je tam nějaká dynamika, to znamená vnější svět, tak se opět vracíme k Maybe, protože to jinak nejde.
Vidím to příliš jednoduše, nebo je to opravdu v tom, že tohle přišlo od akademiků, kterým evidentně nezáleží na hezké čitelné syntaxi a jasném oddělení argumentů pro běh a pro kontrolu typů (např. číselné argumenty pro dělení vs. důkazy).
?
-
Statické ověřování se týká konstantního kódu. Jakmile je tam nějaká dynamika, to znamená vnější svět, tak se opět vracíme k Maybe, protože to jinak nejde.
Tohle tak úplně neplatí. Když mám třeba
inc : Nat -> Nat
inc n = S n
a vyhodnotím isNonZero (inc anyNat), tak mám dokonalou typovou analýzu i pro dynamická data. Podobně jde pomocí záv. typů udělat filtr podle predikátu na Vect n a, aniž by bylo předem známo, kolik prvků predikát splňuje. Záv. typy (resp. jejich implementace založená na unifikaci) je silnější právě díky symbolickému dokazování (a má v rukávu pár dalších triků, například kvantifikované typy). Proto nejsou záv. typy zbytečná blbost, jsou totiž podstatně mocnější než statická analýza nad kódem jen s generickými typy.
-
isNotZero x = x /= 0
Ta validační funkce je úplně nudná.
Tímto by ses dostal k typům identit, to příslušné jazyky mají, můžeš mít třeba typ n = Z a k tomu funkci:
isZero : (n:Nat) -> Dec (n = Z)Tohle je ta méně nudná část teorie záv. typů :)
(https://en.wikipedia.org/wiki/Intuitionistic_type_theory#=_type_constructor)
-
Statické ověřování se týká konstantního kódu. Jakmile je tam nějaká dynamika, to znamená vnější svět, tak se opět vracíme k Maybe, protože to jinak nejde.
Tohle tak úplně neplatí. Když mám třeba
inc : Nat -> Nat
inc n = S n
a vyhodnotím isNonZero (inc anyNat), tak mám dokonalou typovou analýzu i pro dynamická data. Podobně jde pomocí záv. typů udělat filtr podle predikátu na Vect n a, aniž by bylo předem známo, kolik prvků predikát splňuje. Záv. typy (resp. jejich implementace založená na unifikaci) je silnější právě díky symbolickému dokazování (a má v rukávu pár dalších triků, například kvantifikované typy).
Tady si možná nerozumíme v tom, co si představujeme pod pojmem dynamika. Mám-li parsovací funkci, která mi ze stringu dělá číslo, tak nemůže vracet číslo jen tak. Bez ohledu na to, jaký nástroj zvolím. Prostě je tam rozdvojka. Pokud mám funkci, která na vstupu přijímá číslo, a volá funkci, která vyžaduje jen sudé, tak se nevyhnu rozhodování co s lichejma.
Ale to je jen jeden scénář, na který typy použiju.
Proto nejsou záv. typy zbytečná blbost,
Nic takového jsem ani nenaznačoval. Jen si prošlapávám půdu.
-
Mám-li parsovací funkci, která mi ze stringu dělá číslo, tak nemůže vracet číslo jen tak. Bez ohledu na to, jaký nástroj zvolím. Prostě je tam rozdvojka. Pokud mám funkci, která na vstupu přijímá číslo, a volá funkci, která vyžaduje jen sudé, tak se nevyhnu rozhodování co s lichejma.
Jasně, ale pokud třeba z kódu nějak vyplyne, že například predikát Even dostává vždy dvojnásobek nějakého neznámého čísla, tak taky automaticky víš, že je sudé. Tohle jsou umělé příklady, v praxi jsou vztahy mezi hodnotami, typy a funkcemi mnohem složitější a symbolická analýza obecně odhalí víc chyb, než jen prosté kontroly konstant.
Obecně to je o tom, kde je dno rekurze. U konstant to je nula, ale mnohdy stačí nějaké větší číslo. To je třeba případ konkatenace seznamů.
-
že například predikát Even dostává vždy dvojnásobek nějakého neznámého čísla, tak taky automaticky víš, že je sudé.
Rozumím. Toto jsem si tak docela neuvědomil.
Každopádně tato session byla užitečná, díky moc, hodně mi to dalo. Jdu žvejkat. A někdy zase.
-
že například predikát Even dostává vždy dvojnásobek nějakého neznámého čísla, tak taky automaticky víš, že je sudé.
Rozumím. Toto jsem si tak docela neuvědomil.
Každopádně tato session byla užitečná, díky moc, hodně mi to dalo. Jdu žvejkat. A někdy zase.
Paráda :) Tak příště o těch záv. vektorech a maticích ;) Enjoy