Příspěvky

1741

Vývoj / Re:Naivní závislostní typ (úvaha)

« kdy: 25. 11. 2019, 14:42:18 »

To jsou dvě různé věci, já se nebavil o typu reprezentujícím množinu sudých přirozených čísel, to by byl prostě podtyp bez záv. typů. Šlo o vytvoření typu, který zaručí sudost čísla *na úrovni typů*, třeba u toho div2 mi zabrání tomu, aby někdo předal liché číslo. Záv. typy se většinou používají k vynucení kontraktů, to je jejich hlavní přínos.

Každopádně ještě zopakuji otázku: Při volání té funkce na sudá čísla si stejně bude muset volající zajistit aby předával jen sudá. DT tomu nedodají žádnou další magii proti mému řešení?

Ano, volající to musí zajistit, většinou to ale zařídí překladač automaticky. To je princip záv. typů, když volající něco nezajistí, co je dáno kontraktem, program se nepřeloží místo zkolabování za běhu.

1742

Vývoj / Re:Naivní závislostní typ (úvaha)

« kdy: 25. 11. 2019, 14:39:19 »

Trochu jsem se v tom ztratil. Co platí:

Kód: [Vybrat]

Even n → Even (S (S n))

nebo

Kód: [Vybrat]

EvenZ : Even Z a
EvenSS : Even n -> Even (S (S n))

To první je typ, to druhé konstruktory typu Even (z toho logického pohledu důkazy sudosti). Možná to umí lépe vysvětlit MiPr.

É, jasně. Chtěl jsem vlastně jenom vědět, jestli se pro ta lichá čísla taky uvádí explicitně počáteční prvek, nebo jak. Takže takhle?

Kód: [Vybrat]

Odd n → Odd (S (S n))
OddZ : Odd (S Z)
OddSS : Odd n -> Odd (S (S n))

Takhle by to neslo?

Kód: [Vybrat]

Odd n → Odd (S (S n))
OddZ : Odd 1
OddSS : Odd n -> Odd (S (S n))

Jo, takto. Ta 1 se expanduje na (S Z), ale to je jen pozornost od překladače.

1743

Vývoj / Re:Naivní závislostní typ (úvaha)

« kdy: 25. 11. 2019, 10:48:53 »

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?

Stejně, ale dno redukce pak je OddSZ : Odd (S Z).

Pak bych měl ještě jednu otázku:
Já jsem (narozdíl od tebe) vytvářel typ pro sudá čísla tak nějak "jako":

Kód: [Vybrat]

type Even = 2, 4, 6, ...

Každopádně to je typ. A pak jde o jeho použití. Zatímco já jsem si "vystačil" s funkcí:

Kód: [Vybrat]

inc :: Even -> Number
inc a = a + 1

ty tam máš spoustu bordelu kolem:

Kód: [Vybrat]

div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})

Každopádně by mě zajímalo, když zavolám:

Kód: [Vybrat]

calculate b = (inc b) + (div2 b)
calculate 3

Tak to v obou způsobech selže a v obou případech mě to přinutí vytvářet omáčku kolem na ošetření zda tam leze sudé číslo - což je cíl. Každopádně závislostní typy mi v tom žádnou zvláštní magii navíc nepřidají, že?

To jsou dvě různé věci, já se nebavil o typu reprezentujícím množinu sudých přirozených čísel, to by byl prostě podtyp bez záv. typů. Šlo o vytvoření typu, který zaručí sudost čísla *na úrovni typů*, třeba u toho div2 mi zabrání tomu, aby někdo předal liché číslo. Záv. typy se většinou používají k vynucení kontraktů, to je jejich hlavní přínos.

1744

Vývoj / Re:Naivní závislostní typ (úvaha)

« kdy: 25. 11. 2019, 10:44:28 »

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?

Stejně, ale dno redukce pak je OddSZ : Odd (S Z).

Trochu jsem se v tom ztratil. Co platí:

Kód: [Vybrat]

Even n → Even (S (S n))

nebo

Kód: [Vybrat]

EvenZ : Even Z a
EvenSS : Even n -> Even (S (S n))

To první je typ, to druhé konstruktory typu Even (z toho logického pohledu důkazy sudosti). Možná to umí lépe vysvětlit MiPr.

1745

Vývoj / Re:DevOps hranie pre vyvojara

« kdy: 23. 11. 2019, 22:38:17 »

Btw koukam co tedy znamena DevOps... takze programator ma konecne tuseni na cem jeho appka/soft bezi? Lol. To jsme po 20 letech separace a vitualizace zas zpet v pocatcich IT, ne?

To ne. DevOps právě znamená, že vývojář netuší, na čem to běží, protože mezi jeho programem a železem je Kubernetes, Docker, KVMko a pak možná někde hodně daleko hluboko nějaké železo, o kterém ale nikdo nic neví a vědět nemá. Takže DevOps je o tom, že znáš příkaz, kterým se nahazuje kontejner

Můžu to použít i na své programovatelné kalkulačce se Z80?

1746

Vývoj / Re:Naivní závislostní typ (úvaha)

« kdy: 23. 11. 2019, 08:54:43 »

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?

Stejně, ale dno redukce pak je OddSZ : Odd (S Z).

1747

Vývoj / Re:Naivní závislostní typ (úvaha)

« 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.

1748

Vývoj / Re:Naivní závislostní typ (úvaha)

« 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í.

1749

Vývoj / Re:Naivní závislostní typ (úvaha)

« 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.

1750

Vývoj / Re:Naivní závislostní typ (úvaha)

« 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í.

1751

Vývoj / Re:Naivní závislostní typ (úvaha)

« 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

1752

Vývoj / Re:Naivní závislostní typ (úvaha)

« 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ý?

1753

Vývoj / Re:Naivní závislostní typ (úvaha)

« 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.

1754

Vývoj / Re:Naivní závislostní typ (úvaha)

« 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é?

1755

Vývoj / Re:Naivní závislostní typ (úvaha)

« 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.