Naivní závislostní typ (úvaha)

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #75 kdy: 22. 11. 2019, 21:35:40 »
V obecnosti je vhodné představit si opravdu hodnoty typů jako důkazy příslušných výroků. Názornější je promyslet si reifikovanou verzi EvenReif : Nat -> Bool -> Type.
Mluvíš v jazyce, ve kterém se vůbec nechytám :-(


Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #76 kdy: 22. 11. 2019, 22:03:02 »
V obecnosti je vhodné představit si opravdu hodnoty typů jako důkazy příslušných výroků. Názornější je promyslet si reifikovanou verzi EvenReif : Nat -> Bool -> Type.
Mluvíš v jazyce, ve kterém se vůbec nechytám :-(
Pokusím se to vysvětlit nejdřív úplně bez typů, ale než začnu, jen bych si rád ujasnil - Curry-Howardovu korespondenci chápeš? Na tom se dá hezky stavět.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #77 kdy: 22. 11. 2019, 22:08:00 »
V obecnosti je vhodné představit si opravdu hodnoty typů jako důkazy příslušných výroků. Názornější je promyslet si reifikovanou verzi EvenReif : Nat -> Bool -> Type.
Mluvíš v jazyce, ve kterém se vůbec nechytám :-(
Pokusím se to vysvětlit nejdřív úplně bez typů, ale než začnu, jen bych si rád ujasnil - Curry-Howardovu korespondenci chápeš? Na tom se dá hezky stavět.
Promiň, vůbec. Pravděpodobně bych se trochu zorientoval, ale já znám jen Haskell, věci v něm, a některé věci spíše intuitivně. Ale mám bujnou fantazii :-)

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #78 kdy: 22. 11. 2019, 22:14:21 »
Jak jsem slíbil, vezmu to nejdříve trochu obecněji a zeširoka, počínaje formální logikou. Zůstal bych u příkladu s predikátem Even, který je typu ω→τ (ω jsou přirozená čísla). Reifikace (český odborný překlad asi není, doslova by to bylo “zpředmětnění”) znamená, že zavedu nový predikát typu ε→ω→τ, takže můžu napsat například Even’(e, 4) nebo i Even’(e, 5) a tento predikát vždy platí a to e představuje skutečnost, jestli je ono číslo sudé nebo ne. K tomu je predikát absolutní nejvyšší nezpochybnitelné pravdy, True, takže True(e) buď platí nebo neplatí. Je toto zatím jasné?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #79 kdy: 22. 11. 2019, 22:27:55 »
V obecnosti je vhodné představit si opravdu hodnoty typů jako důkazy příslušných výroků. Názornější je promyslet si reifikovanou verzi EvenReif : Nat -> Bool -> Type.
Mluvíš v jazyce, ve kterém se vůbec nechytám :-(
Pokusím se to vysvětlit nejdřív úplně bez typů, ale než začnu, jen bych si rád ujasnil - Curry-Howardovu korespondenci chápeš? Na tom se dá hezky stavět.
Promiň, vůbec. Pravděpodobně bych se trochu zorientoval, ale já znám jen Haskell, věci v něm, a některé věci spíše intuitivně. Ale mám bujnou fantazii :-)
Aha. To je právě pro pochopení závislostních typů nezbytně nutné. Naštěstí to není žádná raketová věda. Ti dva pánové si všimli, že existuje isomorfismus mezi typy (tak, jak jsou definovány v Churchově teorii typů v rámci λ kalkulu) a formulemi predikátové logiky, přičemž hodnoty typů odpovídají důkazům formulí. Nepravdě odpovídá prázdný typ (bottom type, tj. uninhabited, “neobydlený”), pravdě jednotkový typ (unit type, má jen jednu hodnotu), konjunkci odpovídá dvojice a disjunkci součtový typ. Akorát nejde o “starou dobrou známou” klasickou logiku prvního řádu, ale o logiku intuicionistickou (to je ovšem detail). Závislostní typy používají právě tuto korespondenci k dokazování korektnosti programů, překladač si typ představí jako formuli, kterou se pokusí dokázat, čímž ověří, že program je správně otypovaný (nebo dojde ke sporu, což signalizuje chybu v typech). To nejlepší na tom je, že funkční typ odpovídá implikaci, třeba v případě toho Even n → Even (S (S n)) se vlastně říká, že když je n sudé, tak je sudé i n+2. Závislostní typy pak jen implementují kvantifikátory, jinak bychom byli ve výrokové logice.


BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #80 kdy: 22. 11. 2019, 23:06:03 »
Jak jsem slíbil, vezmu to nejdříve trochu obecněji a zeširoka, počínaje formální logikou. Zůstal bych u příkladu s predikátem Even, který je typu ω→τ (ω jsou přirozená čísla). Reifikace (český odborný překlad asi není, doslova by to bylo “zpředmětnění”) znamená, že zavedu nový predikát typu ε→ω→τ, takže můžu napsat například Even’(e, 4) nebo i Even’(e, 5) a tento predikát vždy platí a to e představuje skutečnost, jestli je ono číslo sudé nebo ne. K tomu je predikát absolutní nejvyšší nezpochybnitelné pravdy, True, takže True(e) buď platí nebo neplatí. Je toto zatím jasné?
Takže Even’(True, 4), Even’(False, 5) ? Respektive jako v Prologu: co je e pro Even’(e, 4)? e :- True. Tak?


Aha. To je právě pro pochopení závislostních typů nezbytně nutné. Naštěstí to není žádná raketová věda. Ti dva pánové si všimli, že existuje isomorfismus mezi typy (tak, jak jsou definovány v Churchově teorii typů v rámci λ kalkulu) a formulemi predikátové logiky, přičemž hodnoty typů odpovídají důkazům formulí. Nepravdě odpovídá prázdný typ (bottom type, tj. uninhabited, “neobydlený”), pravdě jednotkový typ (unit type, má jen jednu hodnotu), konjunkci odpovídá dvojice a disjunkci součtový typ. Akorát nejde o “starou dobrou známou” klasickou logiku prvního řádu, ale o logiku intuicionistickou (to je ovšem detail). Závislostní typy používají právě tuto korespondenci k dokazování korektnosti programů, překladač si typ představí jako formuli, kterou se pokusí dokázat, čímž ověří, že program je správně otypovaný (nebo dojde ke sporu, což signalizuje chybu v typech).
Ta tabulka je hezká.


To nejlepší na tom je, že funkční typ odpovídá implikaci, třeba v případě toho Even n → Even (S (S n)) se vlastně říká, že když je n sudé, tak je sudé i n+2. Závislostní typy pak jen implementují kvantifikátory, jinak bychom byli ve výrokové logice.
OK, Even n → Even (S (S n))  jsem asi pochopil. Přičemž tedy, pokud není uveden další, hmm, omezení, tak to neplatí jen pro sudé, ale i pro liché. Že každé n, je-li liché, tak další n je taky liché. (Takže ta definice je nepřesná, ale už nebudu zabředávat.)

Co mě asi hodně mate je ta šipka. Protože pro mě je šipka funkce. Haskellovsky bych to přečetl: máš číslo n, a z něho aplikací vyleze další číslo o dvě větší stejného typu (odlišnosti má mysl vypouští). Takže jsem to původně pochopil jako jakýsi generátor, který mi vytvoří množinu hodnot na základě nějakého vzoru. A to celé je typ. Jak moc jsem mimo?

Re:Naivní závislostní typ (úvaha)
« Odpověď #81 kdy: 22. 11. 2019, 23:10:23 »
Akorát nejde o “starou dobrou známou” klasickou logiku prvního řádu, ale o logiku intuicionistickou (to je ovšem detail).
Jenom tak ze zvědavosti: Takže ten typový systém pak je korektní, ale není úplný? Takže i pro dobře otypovaný program může říct "nevím, jestli je to správně"? Platí to pro všechny DT systémy? Je dokázáno, že úplný nemůže existovat?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #82 kdy: 22. 11. 2019, 23:22:49 »
Akorát nejde o “starou dobrou známou” klasickou logiku prvního řádu, ale o logiku intuicionistickou (to je ovšem detail).
Jenom tak ze zvědavosti: Takže ten typový systém pak je korektní, ale není úplný? Takže i pro dobře otypovaný program může říct "nevím, jestli je to správně"? Platí to pro všechny DT systémy? Je dokázáno, že úplný nemůže existovat?
Teď nevím, kam míříš. Proč by neměl být úplný?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #83 kdy: 22. 11. 2019, 23:23:35 »
Aha. To je právě pro pochopení závislostních typů nezbytně nutné. Naštěstí to není žádná raketová věda. Ti dva pánové si všimli, že existuje isomorfismus mezi typy (tak, jak jsou definovány v Churchově teorii typů v rámci λ kalkulu) a formulemi predikátové logiky, přičemž hodnoty typů odpovídají důkazům formulí. Nepravdě odpovídá prázdný typ (bottom type, tj. uninhabited, “neobydlený”), pravdě jednotkový typ (unit type, má jen jednu hodnotu), konjunkci odpovídá dvojice a disjunkci součtový typ. Akorát nejde o “starou dobrou známou” klasickou logiku prvního řádu, ale o logiku intuicionistickou (to je ovšem detail). Závislostní typy používají právě tuto korespondenci k dokazování korektnosti programů, překladač si typ představí jako formuli, kterou se pokusí dokázat, čímž ověří, že program je správně otypovaný (nebo dojde ke sporu, což signalizuje chybu v typech).
Ta tabulka je hezká.
Jo, je cool :)

Re:Naivní závislostní typ (úvaha)
« Odpověď #84 kdy: 22. 11. 2019, 23:25:14 »
Teď nevím, kam míříš. Proč by neměl být úplný?
Myslel jsem kvuli te intuicionisticke logice. Jen intuitivni :) otazka, bez hlubsiho promysleni, na ktery ted bohuzel nemam cas.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #85 kdy: 22. 11. 2019, 23:26:45 »
Jak jsem slíbil, vezmu to nejdříve trochu obecněji a zeširoka, počínaje formální logikou. Zůstal bych u příkladu s predikátem Even, který je typu ω→τ (ω jsou přirozená čísla). Reifikace (český odborný překlad asi není, doslova by to bylo “zpředmětnění”) znamená, že zavedu nový predikát typu ε→ω→τ, takže můžu napsat například Even’(e, 4) nebo i Even’(e, 5) a tento predikát vždy platí a to e představuje skutečnost, jestli je ono číslo sudé nebo ne. K tomu je predikát absolutní nejvyšší nezpochybnitelné pravdy, True, takže True(e) buď platí nebo neplatí. Je toto zatím jasné?
Takže Even’(True, 4), Even’(False, 5) ? Respektive jako v Prologu: co je e pro Even’(e, 4)? e :- True. Tak?
Je to trochu složitější, e je nějaká entita (“individuum z univerza”), které reprezentuje nějaký výrok, který může platit, nebo taky ne. V případě Even’(e, 5) je e reifikace výroku, že 5 je sudé číslo. V tomto případě tedy True(e) neplatí.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #86 kdy: 22. 11. 2019, 23:35:00 »
Teď nevím, kam míříš. Proč by neměl být úplný?
Myslel jsem kvuli te intuicionisticke logice. Jen intuitivni :) otazka, bez hlubsiho promysleni, na ktery ted bohuzel nemam cas.
Intuicionistická logika je úplná, ve skutečnosti je slabší než klasická predikátová. Jde dokázat, že je to vůbec nejslabší logika, ve které platí modus ponens. Já mířil na druhou stranu formální síly, reifikací se dá simulovat logika vyššího řádu v logice prvního řádu.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #87 kdy: 22. 11. 2019, 23:36:21 »
Teď nevím, kam míříš. Proč by neměl být úplný?
Myslel jsem kvuli te intuicionisticke logice. Jen intuitivni :) otazka, bez hlubsiho promysleni, na ktery ted bohuzel nemam cas.
P.S. Ještě jsem zapomněl dodat, že v int. logice splývá dokazatelnost s vyčíslitelností.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #88 kdy: 22. 11. 2019, 23:41:20 »
To nejlepší na tom je, že funkční typ odpovídá implikaci, třeba v případě toho Even n → Even (S (S n)) se vlastně říká, že když je n sudé, tak je sudé i n+2. Závislostní typy pak jen implementují kvantifikátory, jinak bychom byli ve výrokové logice.
OK, Even n → Even (S (S n))  jsem asi pochopil. Přičemž tedy, pokud není uveden další, hmm, omezení, tak to neplatí jen pro sudé, ale i pro liché. Že každé n, je-li liché, tak další n je taky liché. (Takže ta definice je nepřesná, ale už nebudu zabředávat.)
Ta definice je přesná, ta implikace platí i pro lichá čísla, jenže pro ně je antecedent vždy nepravda, a z nepravdy plyne cokoliv. Trik je v tom, že nula je sudá, kdežto jednička ne.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #89 kdy: 23. 11. 2019, 02:08:12 »
To nejlepší na tom je, že funkční typ odpovídá implikaci, třeba v případě toho Even n → Even (S (S n)) se vlastně říká, že když je n sudé, tak je sudé i n+2. Závislostní typy pak jen implementují kvantifikátory, jinak bychom byli ve výrokové logice.
OK, Even n → Even (S (S n))  jsem asi pochopil. Přičemž tedy, pokud není uveden další, hmm, omezení, tak to neplatí jen pro sudé, ale i pro liché. Že každé n, je-li liché, tak další n je taky liché. (Takže ta definice je nepřesná, ale už nebudu zabředávat.)
Ta definice je přesná, ta implikace platí i pro lichá čísla, jenže pro ně je antecedent vždy nepravda, a z nepravdy plyne cokoliv. Trik je v tom, že nula je sudá, kdežto jednička ne.

Aha. A jak by vypadala definice pro liché čísla?