Haskell, ExistentialQuantification, forall

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #30 kdy: 06. 04. 2021, 16:57:12 »
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.
« Poslední změna: 06. 04. 2021, 17:01:49 od Idris »


BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #31 kdy: 06. 04. 2021, 17:08:53 »
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 => ...
Ten pattern mi přijde povědomej:
Kód: [Vybrat]
calculate : Nat -> Maybe Nat
calculate n = case isNonZero n of
  Yes prf => Just $ div 42 n prf
  No contra => Nothing
versus
Kód: [Vybrat]
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.
« Poslední změna: 06. 04. 2021, 17:12:51 od BoneFlute »

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #32 kdy: 06. 04. 2021, 17:16:18 »
Kód: [Vybrat]
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?

Idris

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

BoneFlute

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

Kód: [Vybrat]
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í.


Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #35 kdy: 06. 04. 2021, 17:27:48 »
Kód: [Vybrat]
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.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #36 kdy: 06. 04. 2021, 17:31:51 »
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:
Kód: [Vybrat]
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.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #37 kdy: 06. 04. 2021, 17:35:30 »
- 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:

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

BoneFlute

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

Idris

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

Idris

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

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #41 kdy: 06. 04. 2021, 18:24:01 »
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:
Kód: [Vybrat]
safeminus : (n:Nat) -> (m:Nat) -> GreaterEq n m -> Nat(Pochopitelně tak, aby ta funkce byla totální.)

Idris

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

BoneFlute

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

Kód: [Vybrat]
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).
?

Idris

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