Haskell, ExistentialQuantification, forall

Idris

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


BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #16 kdy: 06. 04. 2021, 01:47:57 »
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ů".
Kód: [Vybrat]
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:
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.
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í:
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.
Proč potřebuju ten dokazovací argument? Proč prostě nemohu napsat
Kód: [Vybrat]
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
Kód: [Vybrat]
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?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #17 kdy: 06. 04. 2021, 02:05:38 »
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.
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í:
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.
Proč potřebuju ten dokazovací argument? Proč prostě nemohu napsat
Kód: [Vybrat]
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
Kód: [Vybrat]
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:
Kód: [Vybrat]
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í).

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #18 kdy: 06. 04. 2021, 02:24:50 »
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 ;)

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #19 kdy: 06. 04. 2021, 12:39:35 »
Proč potřebuju ten dokazovací argument? Proč prostě nemohu napsat
Kód: [Vybrat]
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
Kód: [Vybrat]
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:
Kód: [Vybrat]
div : Nat -> PosNat -> NatJenže to vyžaduje funkce pro převod mezi oběma typy:
Kód: [Vybrat]
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.


Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #20 kdy: 06. 04. 2021, 13:04:19 »
mašina si na pozadí odvodí, že nemohu zapsat
Kód: [Vybrat]
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).

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #21 kdy: 06. 04. 2021, 15:52:54 »
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:

Kód: [Vybrat]
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.
« Poslední změna: 06. 04. 2021, 15:55:01 od BoneFlute »

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #22 kdy: 06. 04. 2021, 16:05:29 »
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
Kód: [Vybrat]
div 10 5 (SuccNZ 4)

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #23 kdy: 06. 04. 2021, 16:11:42 »
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
Kód: [Vybrat]
div 10 5 (SuccNZ 4)

Takže:
Kód: [Vybrat]
calculate x = divide 42 x (SuccNZ (dec x))?

Idris

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

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #25 kdy: 06. 04. 2021, 16:14:12 »
... čí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.

Idris

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

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #27 kdy: 06. 04. 2021, 16:15:47 »
... čí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 :)

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #28 kdy: 06. 04. 2021, 16:25:29 »
Jak by si ho upravil aby nepadal na dělení nulou?
V principu nějak takto:
Kód: [Vybrat]
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.

BoneFlute

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