Příspěvky

706

/dev/null / Re:Těžké OOP problémy

« kdy: 16. 11. 2019, 20:58:21 »

Každopádně by mě třeba zajímalo kolik let vězení by jsi třeba zrovna ty dal někomu, kdo vědomě a čistě pro svůj pocit způsobil smrt čtrnácti miliardám lidí.

Doživotí.

Doživotí =  smrt. Jen za osmedesát let. Takže v tom případě check.

1) Abychom to rozlouskli, člověk má nárok na život? 2) Ty mě přivedeš nějakýho člověka ke mě do baráku, a já jsem povinnen ho živit, šatit, dát mu napít, a on bude jen čumět na bednu a šikanovat moje děti?

Podle lidského práva 1) ano 2) ne.
Nerozumím v čem je pointa.
Aha už chápu...

Jestli tvému přirovnání rozumím správně tak to myslíš takto:
- Bůh je vlastník baráku (vesmíru),
- stvořil člověka, který mu začal šikanovat děti,
- Bůh šikanujícího vyhnal z baráku,
- před barákem šikanující zjistil, že mu hrozí smrt,
- začal něco blekotat o právu na život,
- Bůh ho nevzal zpět do baráku,
- šikanující umírá.

Ve skutečnosti to bylo takto:
- Bůh je vlastník baráku (vesmíru),
- Bůh stvořil člověka a řekl mu, že na tento hrneček mu nešahej, jinak ho vyrazí, a zemře.
- Člověk to velkopansky ignoroval, Bůh ho tedy vyrazil
- Člověk začal nést následky svého rozhodnutí. A bylo mu to jedno. Nezkoušel se vrátit. Nezkoušel se omluvit.
- A každého člověka, který se chtěl vrátit zpátky šikanoval, nebo dokonce zabil (Kain Abela).
- šikanující umírá
- Bůh nastěhuje do Baráku všechny lidi, kteří budou ochotní mu nepít z hrnečku.

Mohl všemohoucí Bůh izolovat šikanujícího návštěvníka ve vesmíru od ostatních šikanovaných ve vesmíru?
Podle mě ano.

Ano mohl. A dokonce by se to teoreticky stát mohlo. Ale to už je právničina.
Otázka je, proč by to dělal.

*Tady se musím zeptat. Má stvořený člověk stejné rozumové schopnosti jako Bůh?

Nemá. Ale ten požadavek zvládne i má dvouletá dcera, takže ten problém byl v něčem jiném.

Budu mluvit za sebe. To, že jsou "stará" náboženství založena na diktatuře je jedna z hlavních překážek, proč se nemohu stát věřícím.

Tohle je celkem přesné. A je to asi většinový důvod, proč lidé nejsou věřící. Ostatně to není nic nového. Přesně tento důvod byl už na počátku. Přesně ze stejného důvodu Adam s Evou dopadli jak dopadli.
Už ti to řekl Mirek Prýmek a řeknu ti to i já. Na tvůj názor, jestli je Bůh diktátor není nikdo zvědavej.

Mirek nic takového neřekl. Navíc si protiřečíš když píšeš, že boží diktatura je "asi většinový důvod, proč lidé nejsou věřící." a následně napíšeš, že na to není nikdo zvědavej. Jestli je to většinový důvod, tak to lidi asi zajímá. Pokud tě ta jedna nebo dvě věty obtěžovaly, tak si jich nevšímej, nikomu to necpu.

Nerozumíš mi.

Tato diskuse řeší otázku Božího morálního kreditu. Můžeš prohlásit, že Bůh je nespravedlivej. Nebudeš jedinej. Sice to s ohledem na tvé seznámení se problematikou bude takové ..., no to je jedno. Ale říct, a myslet si to samozřejmě můžeš. K čemu ti to bude dobré? Protože pokud nevěříš, že Bůh existuje, tak je ta otázka prostě irelevantní. Nebo v čem vidíš souvislost?

Jak průměrně inteligentní člověk může prohlásit, že nemůže věřit v existenci boha, protože je podle jeho přesvědčení nespravedlivej? Jak někoho takového můžu brát vážně?

707

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

« kdy: 16. 11. 2019, 00:22:57 »

A v druhé řadě, nesouhlasil jsem s tím, že by mi to typovej systém neohlídal compile time. Proč by nemohl. Všechny informace má.

No, Idris ti to už napsal: máš pole Intů, nic víc nevíš. Třeba jsi ho načetl serializované z disku nebo ze sítě. V compile time víš jenom, že to je pole intů. Teprve až to načteš z toho disku, můžeš zjistit, že třetí, pátý a sedmdesátý osmý je Age

Hele, mám pocit, že tady někdo něco přeskočil. Právě na tomhle scénáři jsem to přeci vysvětloval.

Zkusil jsem uvést příklad, popsal jsem skoro komplet kód, popsal jsem to na několik způsobů. Víc po mě už chtít nemůžeš. Asi bych pasáž, compiletime versus runtime vypustil.

A budu se těšit, jestli mi Idris řekne něco k těm sudejm číslům.

708

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

« kdy: 16. 11. 2019, 00:13:16 »

Pak mi rozumíš docela přesně a moc není, s čím bys mohl nesouhlasit Prostě místo pole intů budeš mít pole dvojic (typ, hodnota), kde "typ" říká, jestli na tom konkrétním místě v poli je Int nebo Age (nebo nějaký jiný podtyp) a "hodnota" je ta integerová hodnota. Snadno si to naimplementuješ v Haskellu pomocí dvojic ("product type" - nevím, jak se tomu říká česky). A zároveň si po tom, co to takhle naimplementuješ, vyžereš všechny ty nevýhody Stačí nadefinovat pro takový typ funkce třídy Num a jsi skoro tam, kdes chtěl být, ne?

No jasně. Tak já v prvé řadě nebudu dělat pole dvojic, ale zadrátuju to do toho typového systému.

A v druhé řadě, nesouhlasil jsem s tím, že by mi to typovej systém neohlídal compile time. Proč by nemohl. Všechny informace má.

709

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

« kdy: 15. 11. 2019, 23:41:25 »

To fakt není nejjednodušší příklad na naučení. Lepší je možná začít třeba s typem pro sudá přirozená čísla nebo tak něco.

Jsem pro.

Kód: [Vybrat]

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

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

calculate :: Number -> Number -> Number

-- nepřeloží se
calculate a b = (inc b) + a

-- přeloží se
calculate a b = (inc (toEvenOr b 2)) + a
  where
    toEvenOr a default = ...

Jak by se to dělalo pomocí dep. types, prosím?

710

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

« kdy: 15. 11. 2019, 22:30:22 »

Ne ne, bylo by to div : Numeric -> (y:Numeric) -> Not (y=0) -> Numeric . V těchto jazycích jakákoliv hodnota typu se bere jako důkaz platnosti formule odpovídající tomu typu (Curry-Howard). S tou rovností to je trik, že když předám příslušnou hodnotu ("důkaz"), můžu tu funkci zavolat a mám zaručenou nenulovost. Jinak kód vůbec nepřeložím. Fakt si místo Not (y=0) vezmi NonZero y. Tento typ má konstruktor MkNonZero (S n). No a teď si zkus s tímto zavolat div na nulu Tady je vidět, že to není (u takto jednoduchých příkladů) žádná věda, zvlášť když ten důkaz musíš dodat sám. Síla záv. typů je jen a pouze v tom, co za tebe dosadí ("odvodí") překladač automaticky.

Jak by vypadalo volání funkce div když by měla závislostní typy?

Kód: [Vybrat]

div :: Numeric -> (y:Numeric) -> Not (y=0) -> Numeric
div a b = a / b

calculate :: Numeric -> Numeric -> Numeric
calculate a b =
    (div a b) + 1

calculate 10 0

Má to tři argumenty, ale volám (volal bych) to jen se dvěma.

No to nejde, musíš zavolat div a b proof.

Mohl by jsi mi prosím ten můj "zdroják" upravit, jak by to vypadalo?

Jak na to koukám, tak tam není moc co upravovat, prostě musíš zavolat div a b (MkNonZero (prec b)), kde prec: (Succ n) ↦ n. Teď z hlavy nevím, jak přesně to řeší sofistikovanější jazyky, podívám se.

Tobě se to mluví, ty tomu už rozumíš. Já ještě furt ne.

Kód: [Vybrat]

prec :: (Succ n) -> n
prec a = ...

div :: Numeric -> (y:Numeric) -> Not (y=0) -> Numeric
div a b = a / b

calculate :: Numeric -> Numeric -> Numeric
calculate a b =
    (div a b (MkNonZero (prec b))) + 1

calculate 10 0

Tak, teď už vím, jak se to volá, ale teď zase nevím co je prec, uff.

Když se na to podívám, tak mi ten můj "způsob" přijde jednodužší. Takže předpokládám, že v těch dep. typech musí být něco víc.

711

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

« kdy: 15. 11. 2019, 19:52:56 »

Ne ne, bylo by to div : Numeric -> (y:Numeric) -> Not (y=0) -> Numeric . V těchto jazycích jakákoliv hodnota typu se bere jako důkaz platnosti formule odpovídající tomu typu (Curry-Howard). S tou rovností to je trik, že když předám příslušnou hodnotu ("důkaz"), můžu tu funkci zavolat a mám zaručenou nenulovost. Jinak kód vůbec nepřeložím. Fakt si místo Not (y=0) vezmi NonZero y. Tento typ má konstruktor MkNonZero (S n). No a teď si zkus s tímto zavolat div na nulu Tady je vidět, že to není (u takto jednoduchých příkladů) žádná věda, zvlášť když ten důkaz musíš dodat sám. Síla záv. typů je jen a pouze v tom, co za tebe dosadí ("odvodí") překladač automaticky.

Jak by vypadalo volání funkce div když by měla závislostní typy?

Kód: [Vybrat]

div :: Numeric -> (y:Numeric) -> Not (y=0) -> Numeric
div a b = a / b

calculate :: Numeric -> Numeric -> Numeric
calculate a b =
    (div a b) + 1

calculate 10 0

Má to tři argumenty, ale volám (volal bych) to jen se dvěma.

No to nejde, musíš zavolat div a b proof.

Mohl by jsi mi prosím ten můj "zdroják" upravit, jak by to vypadalo? A kde že vezme tu proof?

712

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

« kdy: 15. 11. 2019, 19:49:46 »

Můj cíl je vždycky compile time, i za cenu složitější práce překladače.

Jo, to je jediná rozumná cesta. Akorát třeba v Agdě pak kompilace trvá třeba dva dny. A když pak na tebe vyskočí "sorry vole error," tak to nepotěší.

Jinak nedávno mě málem vypískali, když jsem na přednášce při výkladu potřetí před vysvětlením příkladu řekl "let's take any language, say, Agda." Hulváti...

:-D

713

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

« kdy: 15. 11. 2019, 19:38:57 »

Překladač tohle za tebe řešit nemůže, protože k tomu dochází až v runtime. (Překladač nemůže tušit, že při běhu bude ausgerechnet třetí prvek pole Age a ne Int).

Tohle už jsi kdysi kdesi tvrdil, a já s tebou v tomto stále nesouhlasím. Žádný runtime, a překladač to může zajistit. Viz ten kód.

On myslí, že když máš instanci List<Int> a žádné další informace, tak jen za běhu můžeš zjistit, že nějaký prvek je třeba typu Age (nebo prostě nějakého podtypu). To je ten základní důvod pro existenci virtuálních metod. Zmíněné aserce v Go jsou vlastně jen (konceptuálně) dynamic_cast.

Já mu snad rozumím dobře, ale stejně nesouhlasím :-)

Mám instnaci List<Int> a pokud mohu do List<Int> uložit Age, kterýžto je subtyp Int, tak si sice musím někde evidovat, že zrovna tato třetí hodnota není Int, ale Age, to jako jo, a to asi bude muset být nějak naimplementováno...

Každopádně překladač a nikoliv runtime mi zajistí, abych nemohl k těm prvkům List<Int> přistupovat jen jako k Age, a že k nim mohu přistupovat (po patřičném switchi) jako Age, a nemůžu jako k String.

Můj cíl je vždycky compile time, i za cenu složitější práce překladače. A v tomto případě bych řekl, že to stále jde.

714

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

« kdy: 15. 11. 2019, 19:17:23 »

Znamená to, že musíš mít u každé hodnoty zaznamenaný typ. A to je teda pořádný opruz.

Proč by to byl opruz? Pro mě? Pro mě je to transparentní. Pro kompilátor? Ať se s tím popere, nezajímá.

Překladač tohle za tebe řešit nemůže, protože k tomu dochází až v runtime. (Překladač nemůže tušit, že při běhu bude ausgerechnet třetí prvek pole Age a ne Int).

Tohle už jsi kdysi kdesi tvrdil, a já s tebou v tomto stále nesouhlasím. Žádný runtime, a překladač to může zajistit. Viz ten kód.

715

/dev/null / Re:Těžké OOP problémy

« kdy: 15. 11. 2019, 19:13:55 »

Když máš rád logické hádanky, tak dvě bych měl:
Může všemohoucí Bůh zařídit, aby vesmír fungoval bez něj?
Může všemohoucí Bůh ukončit svoji vlastní existenci?

Ano a ano. Je to děsně jednoduchý. A je to přesně ten problém, který jsme rozebírali na začátku. Zřejmě jsi vůbec nedával pozor, když to bylo vysvětlováno.

Možná, že nejsi ty ani BoneFlute nejzarytější demokrat. ...nebo nejzarytější věřící.

Já nejsem demokrat ani náhodou. Já jsem hmmm, teo-royalista. A nevím na základě čeho zpochybňuješ mou víru.

Děsivost lidských diktátorů je právě v tom, že jsou to lidi.

A kdyby to byl mimozemšťan co přiletěl létajícím talířem?

Měli by ti mimozemšťani stejné špatné charakterové vlastnosti jako lidstvo? Nebo by měli vlastnosti jako má Biblický Bůh?

Pak po čtyřech tisíci letech přijde někdo, kdo se s případem ani neseznámí, komu se to baj oko zdá moc, a začne to komentovat.

Ano, po čtyřech tisících let přišel člověk (a určitě né jeden) a začal do toho šťourat a klást nepříjemné otázky:

Asi tě zklamu, ale nijak zvlášť.

Dovolil bych si nasměrovat tvou pozornost na biblickou knihu Job, konkrétně prvních pět a poslední kapitolu. Tam zjistíš, že Bůh připustil aby Satan zabil všechny Jobovi děti. Zdá se, že tomu mohl zabránit, ale neudělal to. A v poslední kapitole se dozvíš, že Bůh mu všechno vrátil, až na ty děti. Takže jestli hledáš nějakou nespravedlnost, tak toto mi přijde jednodužší. Užij si to.

Každopádně, když by si náhodou měl zájem pochopit, proč v tomto, ani v případě Sodomy v tom nevidíme nespravedlnost, tak zkus pouvažovat nad tím, že Bůh je pánem nad životem a smrtí. Až nad tím pouvažuješ, a pochopíš důsledky, tak pochopíš, že se na to prostě díváš z pohledu toho, jak by to zvládl člověk. A ten toho nezvládne moc. To, že by si si měl uvědomit, že Bůh není povinnen nás ochraňovat před naší vlastní volbou, to už jsem říkal a nebudu se k tomu vracet.

716

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

« kdy: 15. 11. 2019, 18:55:05 »

1/ Paměť neřeším. To ať si vyřeší kompilátor.

Nejde o paměť, ale o typ. Referenci na Age nesmíš změnit na referenci na Int. Ledaže bys měl čítač referencí a ten byl roven jedné.

Předpokládám ale, že uvažuješ o nějakém Haskell-like jazyku, tak na reference prdíme.

Ano, to jsem dostatečně nezdůraznil.

2/ Mě se tam žádnej typ nezměnil. O žádnou informaci jsem nepřišel. Já mám pole Intů. Mám funkci:

No pokud se na to díváš takhle, tak ano, máš pole intů. V tom případě jsi o tu informaci, že "a" je "Age" přišel ve chvíli, kdy jsi "a" vložil do toho pole intů. Tím se totiž z Age stal Int = ztratil jsi informaci o tom, že to číslo je kladné. Odteď už to nevíš.

Nebo řečeno jinak: intuitivně člověk asi očekává, že když do listu něco vloží a pak to z něj vyndá, dostane to samý. Ty ale říkáš, že dostane typ prvku toho listu.

Ne tak docela.

V List Int může být cokoliv, co se vejde do Int. Takže i Age. Když do List Int dám Age, tak smím, a bude tam Age, neproběhne konverze (nedělal bych to). Když ale z List Int čtu, tak sice můžu zjišťovat, zda nejde o nějaký podtyp, ale nemůžu k tomu přistupovat jako k List Age, protože je to List Int. Kompilátor mi bude hlídat, abych k těm položkám nepřistupoval jako k Age, protože tam samozřejmě může být Int, a obráceně to už nejde.

Možná trochu zmatenej popis, ale tak viz ten můj Haskell like kód.

Jak jsem říkal, nejsou to neřešitelné problémy, ale je to opruz.

Pokud tě napadá nějaký příklad, stál bych o něj.

717

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

« kdy: 15. 11. 2019, 18:26:48 »

Ne ne, bylo by to div : Numeric -> (y:Numeric) -> Not (y=0) -> Numeric . V těchto jazycích jakákoliv hodnota typu se bere jako důkaz platnosti formule odpovídající tomu typu (Curry-Howard). S tou rovností to je trik, že když předám příslušnou hodnotu ("důkaz"), můžu tu funkci zavolat a mám zaručenou nenulovost. Jinak kód vůbec nepřeložím. Fakt si místo Not (y=0) vezmi NonZero y. Tento typ má konstruktor MkNonZero (S n). No a teď si zkus s tímto zavolat div na nulu Tady je vidět, že to není (u takto jednoduchých příkladů) žádná věda, zvlášť když ten důkaz musíš dodat sám. Síla záv. typů je jen a pouze v tom, co za tebe dosadí ("odvodí") překladač automaticky.

Jak by vypadalo volání funkce div když by měla závislostní typy?

Kód: [Vybrat]

div :: Numeric -> (y:Numeric) -> Not (y=0) -> Numeric
div a b = a / b

calculate :: Numeric -> Numeric -> Numeric
calculate a b =
    (div a b) + 1

calculate 10 0

Má to tři argumenty, ale volám (volal bych) to jen se dvěma.

P.S. Kdybys měl to tvé NonzeroNat a nevěděl vůbec nic o druhém parametru, musel bys použít např. funkci Nat -> Maybe NonzeroNat, aby ošetřil nenulovost před voláním div. V některých případech tě záv. typy jen donutí ke kontrole vstupu/ošetření chyby, žádná magie v tom není.

No šak.

718

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

« kdy: 15. 11. 2019, 18:14:16 »

Když by si uvedl nějaký příklad s něčím tedy jednodužším?

Tak třeba ty součtové záv. typy, které odpovídají existenční kvantifikaci. Řekněme, že mám typ Vector T n:Nat a chci funkci readVector1: Nat -> Vector String n. S tím asi nebude problém, že? Ovšem pokud chci nejdřív načíst i tu délku, nemůžu mít readVector2: Vector String n, protože to n nespadne z nebe. Aby to typový systém pobral, musím vrátit Σ_n:NatVector String n. Teď už to type checker vezme, protože mu explicitně říkám, že takové n existuje (z pohledu logiky, tedy dokazování). Z pohledu výpočetního vracím pár číslo+seznam, akorát typ toho seznamu závisí na tom čísle. Tohle je asi nejjednodušší praktický příklad, který k záv. typům znám.

Co ta funkce readVector1 dělá? Vrací n-tý prvek vektoru? A čím se to n naplní? Možná ukázku jak se ta funkce zavolá. Takhle?

readVector1 42 ["a", "b", "c"] ? Kde tam figuruje to n a k čemu tam slouží?

719

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

« kdy: 15. 11. 2019, 18:05:49 »

Tak naivně předpokládám, že ano, může ho tam vložit, protože Age je Int (zatímco Int není Age). A když ho vyberu tak...

...tak nastanou problémy

No, to by chtělo příklad. Protože tak co, může to vráti Age. A funkce, která vyžaduje pole Intů a dostane pole Ageů, tak s tím Age bude pracovat jako s Intem, tak by furt mělo všechno fungovat... Co mi uniká?

Uniká ti to, že se ti tam "samovolně" přeměnil typ Age na typ Int - tj. na obecnější = při nejmenším jsi ztratil nějakou informaci. V horším případě by i mohlo dojít k nějaké chybě, pokud by to byla reference (do té konkrétní paměťové buňky jsi původně dovolil zapisovat jenom kladná čísla (Age) a teď tam máš povoleno zapsat i záporná (Int). Samozřejmě u imutable jazyka ten druhý problém nevzniká, ten první ale pořád jo.

Počkej, počkej...

1/ Paměť neřeším. To ať si vyřeší kompilátor.

2/ Mě se tam žádnej typ nezměnil. O žádnou informaci jsem nepřišel. Já mám pole Intů. Mám funkci:

Kód: [Vybrat]

calculate :: List Int -> (Int -> Int) -> List Int
calculat xs f =
    map f xs

Když do pole Intů narvu Age tak to furt bude fungovat. (V tomto případě pravděpodobně dojde k přetypování.)

Kód: [Vybrat]

calculate :: List Int -> List String
calculat xs =
    map f xs
    where
        f (x :: Int) = "Int"
        f (x :: Age) = "Age"

V tomto případě tam taky nepřijdu o žádnou informaci.

Kód: [Vybrat]

calculate :: List Int -> List Int
calculat xs =
    map f xs
    where
        f (x :: Age) = x + 1

se mi nepřeloží.

Co mi tedy uniká, símtě?

720

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

« kdy: 15. 11. 2019, 17:55:24 »

ta funkce pak má typ Nat->y:Nat->Not (y=0)->Nat.

Můžeš mi prosím, v nějakém srozumitelnějším pseudo jazyku s hodně komentáři popsat, cože to vlastní říká? Jsem na to Nat už narazil mnohokrát. Vždycky tím začíná každá učebnice Idris a Agdy, a já to prostě neumím přečíst. (Předpokládám, že Nat je jako Natural - přirozené číslo?)

Jo, Nat jsou přirozená čísla. Když T je typ, tak Not T se definuje jako T->Void (kde Void je typ bez hodnot, odpovídající false v intuicionistické logice), typ třetího parametru je tedy (y=0)->Void. Možná si spíš představ něco jako typ NonZero n:Nat, kde bude konstruktor NonZero (Succ n). Popravdě tento příklad není úplně nejjednodušší, protože obsahuje rovnostní typ a negaci.

Takže Nat -> y : ... je typ pojmenovaný jako Nat, mající jeden argument. Něco podobného jako Maybe a = ... (eee deklarace typu, nebo deklarace uplatnění typu?)

Tak jinak:

Takže já mám funkci:

Kód: [Vybrat]

div a b = ...

Anotace moje:

Kód: [Vybrat]

div :: Numeric -> PositiveUnzeroNumeric -> Numeric

Anotace tvoje:

Kód: [Vybrat]

div Numeric y :: Numeric -> Not (y = 0) -> Numeric

nebo třeba:

Kód: [Vybrat]

div :: Numeric -> Numeric y, Not (y = 0) -> Numeric

A jak se potom ta funkce zavolá, explicitně, bez type inference. Jak tam bude figurovat ta typová proměnná y?