reklama

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 - Idris

Stran: [1] 2 3 ... 35
1
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 16. 11. 2019, 11:10:42 »
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.
Já tady taky moc nechápu, jak to myslíš. Ale to je fuk, dědičnost nechme stranou :)

2
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 22:46:49 »
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.
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.

3
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 21:49:38 »
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.

4
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 20:07:28 »
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?
Sorry, teď musím pryč, ale vrátím se k tomu ;)

To proof, pokud nemáš dostatečně inteligentní překladač, musíš dodat sám ;)

5
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 19:46:04 »
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...

6
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 19:33:50 »
Tohle je fakt non-issue
Jestli ti pole integerů zabírá 32G nebo 64G úplně non-issue není :)
Mám RAM 128GB :P

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

8
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 19:22:43 »
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.
No, to je právě ta možnost, co má Go. Znamená to, že musíš mít u každé hodnoty zaznamenaný typ. A to je teda pořádný opruz. Tohle v normálním Haskellu není - když to má typ Int, tak je to Int.
U každé? V Go to je jen u rozhraní (de facto "fat pointers"). Tohle není žádná magie, v OOP máš typ za běhu k dispozici vždy, buď jako v Go nebo jako ISA pointer. Jinak by nešel dělat downcasting.

Tohle je fakt non-issue, v čistém OOP to není ani dokonce metaúroveň (viz selektor isKindOfClass).

9
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 18:58:52 »
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.
Trochu odbočím: Ve Swiftu jde pomocí "extension" přidávat typové podmínky je třídám, takže třeba můžu říct, že když mám List a všechny prvky jsou typu Age, tak něco. To jen tak z zamyšlení.

10
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 18:54:43 »
To je ale princip variance typů, že se "zapomíná".
Právě no. Však neříkám žádnou tajemnou pravdu, jenom odpovídám na Boeflutovu otázku "vidíte tam nějaký problém?", že tenhle problém tam má :)

Když mám bifunktor kontravariantní v prvním parametru a kovariantní ve druhém a někam ho předám, tak té funkci to je jedno, protože co se zapomene je typ argumentů (funktoru), ne typ té hodnoty jako celku.
To je ale speciální případ.
V čem je speciální? Vždy se zapomíná typ argumentu/ů.

11
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 18:53:41 »
Numeric > PositiveUnzeroNumeric
Ještě bych doporučil podívat se na to, jak se ve FP pracuje s totálními/částečnými funkcemi, protože tou typovou hierarchií řešíš právě tohle.

Jinak dědičnost a FP se kloubí dost blbě, jsou tam třecí plochy, spíš než dědění se používají klasifikátory podobjektů (subobject classifier), ale to by tady asi nepomohlo.

12
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 18:49:11 »
V tomhle fóru je tolik tatarštiny, že to je jedno :) Ani to není jeho rodný jazyk (předpokládám). Kdo jsi bez viny... ;)
Jasně, však to bylo myšleno přátelsky, ne jako pruzení.
Však víme. Jinak slovo "unzero" existuje :)

13
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 18:48:08 »
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.

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.

Jak jsem říkal, nejsou to neřešitelné problémy, ale je to opruz.
To je ale princip variance typů, že se "zapomíná". Když mám bifunktor kontravariantní v prvním parametru a kovariantní ve druhém a někam ho předám, tak té funkci to je jedno, protože co se zapomene je typ argumentů (funktoru), ne typ té hodnoty jako celku.

14
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 18:43:50 »
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. Když máš štěstí, tak "proof" najde překladač automaticky (kdyby ten druhý parametr vzniknul třeba z length (head : tail)). Tady jen pomůže si ty hodnoty rozepsat. Type checker používá při dokazování unifikaci (resp. paramodulaci) a jakmile narazí např. na x=Succ y, bude vědět, že x není nula, protože je následníkem jiného přirozeného čísla.

15
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 18:19:24 »
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ží?
Načte vektor délky n. Zavoláš třeba readVector1 3 a program se tě zeptá na tři řetězce a vrátí např. ["dependent", "types", "suck"].

Stran: [1] 2 3 ... 35

reklama