Zobrazit příspěvky

Tato sekce Vám umožňuje zobrazit všechny příspěvky tohoto uživatele. Prosím uvědomte si, že můžete vidět příspěvky pouze z oblastí Vám přístupných.


Příspěvky - BoneFlute

Stran: 1 ... 44 45 [46] 47 48 ... 133
676
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 25. 11. 2019, 13:57:27 »
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))

677
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 25. 11. 2019, 00:58:34 »
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))

(Děkuji za trpělivost.)

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?

678
/dev/null / Re:Těžké OOP problémy
« kdy: 25. 11. 2019, 00:40:23 »
Imho vubec nejlepsi vtipnej film s tematikou nabozenstvi je Zivot Briana.
Až jsem byl sám překvapenej že jsem s ním neměl vůbec problém a docela se mi líbil. (Zatímco třeba Smysl života taky od nich už jsem projížděl rychloposuvem.) Film Noe (s Russell Crowe) jsem vysloveně přetrpěl jako strašnou kravinu.

Já nevím, prostě náboženství je stejně jako politika je emotivní záležitost a přijde mi to o držku. Řekl bych.

679
/dev/null / Re:Těžké OOP problémy
« kdy: 25. 11. 2019, 00:33:28 »
Víš jak, mě se třeba vůbec nelíbí, že by mi měla diktovat nějaká pluralita názorů co bych si měl myslet, a jak bych to měl dělat.
Pluralita má právě zajist, aby jsi si myslel co chceš. :-)
Má zajistit, nebo skutečně zajišťuje? Je to tvá víra, nebo se to dá nějak dokázat?
Uveď příklad kdy naposledy ti pluralita a svoboda zakázala si něco myslet.
To je docela zajímavá myšlenka. Je třeba to rozebrat: Za prvé, je pluralita zárukou něčeho? Ty tvrdíš, že jo. Já bych to rád od tebe něčím doložil. Obecně mám zkušenost, že čím více lidí se do toho vrtá, tím větší nesmysl z toho vyleze.
Druhak, svoboda je samozřejmě krásná věc, ale v praxi většinou shledáváme bojovníky za svou svobodu. Takže je to spíše jen takovej kec zatímco skutek utek.
A zakázat myslet mi přirozeně teoreticky nemůže nikdo nic. V praxi to samozřejmě taky neplatí, protože obecně pozorujeme biblické "špatná společnost kazí užitečné návyky".

Takže shrnuto a podtrženo, když se budu pohybovat ve společnosti svobodně pluralitně uvažujících jedinců, kteří s největší pravděpodobností budou vymejšlet nepraktické až nebezpečné myšlenky, tak se zaručeně začnu chovat a uvažovat podobně. Kde v tom ale vidíš nějaký užitek mi poněkud uniká. Že by to bylo něco sympatického to taky říct nemohu.

Právě proto, že máme svobodu. Pokud jsi se svobodně rozhodl to dělat podle sebe, tak tím potvrzuješ, že je správné, aby na počátku (ještě před vytvořením vlastních morálních hodnot) byla svobodná otevřená mysl.
Proč bych to měl dělat podle sebe? To se musí?
Ty jsi se nerozhodl pro víru v Boha podle sebe? :o Tobě tvoji víru někdo vnutil? Kdo?
Bavíme se o "vytvoření morálních hodnot podle sebe", nebo o tom, jak jsem začal věřit v Boha?
Jestli jsem to pochopil správně, tak u tebe v tom rozdíl není. Tvé morální hodnoty vycházejí z Bible. Takže co bylo na začátku tvé víry a nalezení morálních hodnot z Bible. Byla to otevřená svobodná mysl nebo ti to někdo vnutil?
Zopakuju otázku: To se musí, aby si člověk dělal věci podle sebe?


Mám dojem, že ti docházejí argumenty a místo toho vymýšlíš hru se slovíčky.
Hele, já jsem přistoupil na tvé nesmysly, tak se teď nevykrucuj.
Mě zajímá, jestli pochopíš, že máš v těch pojmech nepořádek.
Jenomže já nerozumím co chceš říct. Použil jsi výraz "diktatura plurality názorů". To mě přijde jako kdybys napsal "krychle je kulatá" nebo "souložíme za panenství". Nelíbí se ti to slovo pluralita, protože tam podle definice nějak nepasuje? Byl bys ochoten napsat i "diktatura svobodné mysli"? Fakt nechápu co chceš říct. Zkus použít nějakého příkladu jako třeba Mirek použil s otrokáři a squattery.
Jestli jsem se dopustil nějakého rouhání, tak se přirozeně omlouvám.

(Otevřená svobodná mysl je jen takovej buzzword. V reálu jsem to nepotkal. V přípaě teoretického konceptu není důvod předpokládat, že to bude dávat nějaké zvlášť výjimečné výsledky.)


Cílem svobody je, aby lidé měli co nejširší možnost se dobrovolně dohodnout mezi sebou a až když se někdo bude cítit ublížený se bude (podle principu, který jsme výše probírali s Mirkem) přemýšlet kdo komu ubližuje více.
Ta podmínka s dohadováním se mezi sebou je nutná? A proč nejdřív ubližovat a až pak řešit co s tím a zda vůbec? Tohle je děsivé.

To máš jako ve škole. Samozřejmě bychom mohli vytvořit svobodně pluralitní třídu plnou otevřené svobodných myslí. Jestli bych se tam ale něco naučil, než ve třídě, kde učitel vládne pevnou rukou, a vysvětluje látku on, to si samozřejmě svobodně a pluralitně vyber.

Možná se míjíme cílem. Můj cíl je, abych byl dobrým člověkem. I za tu cenu, že věci nebudou po mém. I za tu cenu, že budu muset uznat, že jsem se spletl, a mé morální cítění je pošahané. I za tu cenu, že budu poslouchat někoho chytřejšího.

Samozřejmě si dokážu představit, že pro někoho je to příliš veliká cena za to být dobrým člověkem.

680
Vývoj / Re:Naivní závislostní typ (úvaha)
« 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?

681
Vývoj / Re:Naivní závislostní typ (úvaha)
« 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?

682
Vývoj / Re:Naivní závislostní typ (úvaha)
« 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 :-)

683
Vývoj / Re:Naivní závislostní typ (úvaha)
« 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 :-(

684
/dev/null / Re:Těžké OOP problémy
« kdy: 22. 11. 2019, 00:40:26 »
A jestli je pravda co jsi psal, že vám ta "vláda Bible pevné ruky" ve tvojí církvi funguje fantasticky, tak je do důkaz, že si můžeš i dělat co chceš.

Ale já si samozřejmě nemůžu dělat co chci. Nemůžu ubližovat druhým (aniž bych za to nesl postih)!

685
/dev/null / Re:Těžké OOP problémy
« kdy: 21. 11. 2019, 23:07:36 »
Víš jak, mě se třeba vůbec nelíbí, že by mi měla diktovat nějaká pluralita názorů co bych si měl myslet, a jak bych to měl dělat.
Pluralita má právě zajist, aby jsi si myslel co chceš. :-)
Má zajistit, nebo skutečně zajišťuje? Je to tvá víra, nebo se to dá nějak dokázat?


Právě proto, že máme svobodu. Pokud jsi se svobodně rozhodl to dělat podle sebe, tak tím potvrzuješ, že je správné, aby na počátku (ještě před vytvořením vlastních morálních hodnot) byla svobodná otevřená mysl.
Proč bych to měl dělat podle sebe? To se musí?
Ty jsi se nerozhodl pro víru v Boha podle sebe? :o Tobě tvoji víru někdo vnutil? Kdo?
Bavíme se o "vytvoření morálních hodnot podle sebe", nebo o tom, jak jsem začal věřit v Boha?


Mám dojem, že ti docházejí argumenty a místo toho vymýšlíš hru se slovíčky.
Hele, já jsem přistoupil na tvé nesmysly, tak se teď nevykrucuj.

Mě zajímá, jestli pochopíš, že máš v těch pojmech nepořádek.

686
/dev/null / Re:Těžké OOP problémy
« kdy: 21. 11. 2019, 21:15:06 »
Proč bych to měl dělat podle tebe?
Nemusíš.
Uff, to jsem rád.


Právě proto, že máme svobodu. Pokud jsi se svobodně rozhodl to dělat podle sebe, tak tím potvrzuješ, že je správné, aby na počátku (ještě před vytvořením vlastních morálních hodnot) byla svobodná otevřená mysl.
Proč bych to měl dělat podle sebe? To se musí?

687
/dev/null / Re:Těžké OOP problémy
« kdy: 21. 11. 2019, 21:11:31 »
Z jakékoliv "vlády pevnou rukou" mám strach, protože nepřipouští pluralitu názorů a místo naslouchání chce jen diktovat. A diktatura je opak svobodné otevřené mysli.

Takže chceš diktaturu plurality názorů? Víš jak, mě se třeba vůbec nelíbí, že by mi měla diktovat nějaká pluralita názorů co bych si měl myslet, a jak bych to měl dělat. Tím spíše, že většina těch názorů bude vulgárně řečeno hloupých.

688
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 21. 11. 2019, 19:59:42 »
Jak u
Kód: [Vybrat]
EvenSS : Even n -> Even (S (S n))
zajistím, že to bude zrovna sudá řada?

Pro každý Even n platí, že má následníka plus 2, přičemž prvním prvkem je EvenZ? to je jako definice následovníka, přičemž EvenZ je definice neutrálního prvku?

689
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 21. 11. 2019, 19:33:07 »
div2 : (n:Nat) -> {auto prf:Even n} -> Nat
čtu jako: Vezmu číslo, a to číslo musí být aplikovatelné na typ Even. Tuto podmínku mám pojmenovanou jako prf.

div2 Z {prf=EvenZ} = 0
čtu jako: Pokud je číslo (n) nula, a je splněna podmínka prf, tzn číslo je Even, přesněji EvenZ. Toto ještě asi chápu.

div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
čtu jako: Pokud následník následníka čísla n ???, a je splněna podmínka... Tady jsem v háji  :(

690
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 21. 11. 2019, 19:17:47 »
div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
Co prosím tě znamená to S?
“Z” je nula a “S” je successor.
Supr.

Můžeš mi popsat tu šipku? Můžeš mi prosím rozvést, co dělá to Even : Nat -> Type? To jako že mám typovou funkci, která mi z přirozeného čísla udělá nový typ pomocí těch konstruktorů? Takže pokud je číslo 0, udělá z něho Even Z 0, pokud je to 4, udělá z něho Even 4 -> ... - tady se trochu ztrácím. Vidím rekurzi, vidím, že tam přeskakuje jednu hodnotu, takže to nějak vytvoří řadu ob hodnotu, ale nedokážu to přečíst.

Jak u
Kód: [Vybrat]
EvenSS : Even n -> Even (S (S n))
zajistím, že to bude zrovna sudá řada?

Stran: 1 ... 44 45 [46] 47 48 ... 133