Haskell, ExistentialQuantification, forall

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Haskell, ExistentialQuantification, forall
« kdy: 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:
Kód: [Vybrat]
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:
Kód: [Vybrat]
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.


Kód: [Vybrat]
{-# 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.
« Poslední změna: 31. 03. 2021, 15:54:42 od BoneFlute »


BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #1 kdy: 31. 03. 2021, 16:08:13 »
Tak už to mám:

Kód: [Vybrat]
{-# 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:
Kód: [Vybrat]
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
Kód: [Vybrat]
data ShowBox = forall s. Show s => SB sje ekvivalentní:
Kód: [Vybrat]
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?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #2 kdy: 31. 03. 2021, 17:55:59 »
toto naivní v Haskellu neprojde:
Kód: [Vybrat]
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.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #3 kdy: 31. 03. 2021, 18:43:55 »
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ě.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #4 kdy: 31. 03. 2021, 21:22:42 »
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.)


Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #5 kdy: 31. 03. 2021, 21:37:32 »
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.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #6 kdy: 31. 03. 2021, 23:53:47 »
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.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #7 kdy: 03. 04. 2021, 21:40:58 »
[...]
... 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.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #8 kdy: 04. 04. 2021, 22:28:35 »
[...]
... 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.)

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #9 kdy: 04. 04. 2021, 23:01:14 »
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í.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #10 kdy: 04. 04. 2021, 23:10:47 »
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.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #11 kdy: 04. 04. 2021, 23:59:06 »
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ě.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #12 kdy: 05. 04. 2021, 22:13:11 »
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:
Kód: [Vybrat]
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:
Kód: [Vybrat]
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í:
Kód: [Vybrat]
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.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #13 kdy: 06. 04. 2021, 00:34:24 »
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:
Kód: [Vybrat]
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:
Kód: [Vybrat]
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):
Kód: [Vybrat]
isNonZero 0 =  No (NonZero 0)
isNonZero x =  Yes (NonZero x)

Chytám se?

Potom můžu mít funkci pro dělení:
Kód: [Vybrat]
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ů.

Kód: [Vybrat]
let a = 5
let b = 0
let x = div a b .... ?

Proč není ta signatura takto?
Kód: [Vybrat]
div : Nat -> NonZero -> Nat
« Poslední změna: 06. 04. 2021, 00:41:02 od BoneFlute »

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #14 kdy: 06. 04. 2021, 01:04:48 »
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:
Kód: [Vybrat]
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:
Kód: [Vybrat]
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):
Kód: [Vybrat]
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:
Kód: [Vybrat]
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í:
Kód: [Vybrat]
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ů.
Kód: [Vybrat]
let a = 5
let b = 0
let x = div a b .... ?
Proč není ta signatura takto?
Kód: [Vybrat]
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.