Příspěvky

1771

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

1772

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

1773

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/ů.

1774

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.

1775

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

1776

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.

1777

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.

1778

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"].

1779

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

« kdy: 15. 11. 2019, 18:15:53 »

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?

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.

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

1780

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

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

PositiveUnzeroNumeric

Prosímtě, neříkej tomu "Unzero", strašně to trhá oči. Správně je Nonzero.

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

1781

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

« kdy: 15. 11. 2019, 18:02:42 »

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.

Taky jsem to bohužel nedal, promiň :-(

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.

1782

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

« kdy: 15. 11. 2019, 17:25:58 »

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.

1783

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

« kdy: 15. 11. 2019, 17:17:59 »

V mé úvaze jsem dospěl k tomu, že potřebuju:

Zavést tu kaskádu typů. Mám Numeric a z něj "dědí" PositiveUnzeroNumeric

Mít "nonzero" typ není asi úplně ideální, to je virální až to bolí. Nechci nikomu kazit iluze, ale tohle je zrovna učebnicový příklad ...

Tak není to virální až dolů, bych řekl.

A zase musíš na mě pomalu. Už vím jak se cejtil kamoš, když jsem mu vysvětloval Promise :-)

Každopádně díky.

Abych řekl pravdu, nevím, jak by záv. typy fungovaly s dědičností. Je to zajímavý problém, zkusím k tomu najít nějaké reference (nebo spíš vyptat od lidí, co se výzkumem záv. typů živí )

1784

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

« kdy: 15. 11. 2019, 16:54:11 »

V mé úvaze jsem dospěl k tomu, že potřebuju:

Zavést tu kaskádu typů. Mám Numeric a z něj "dědí" PositiveUnzeroNumeric

Mít "nonzero" typ není asi úplně ideální, to je virální až to bolí. Nechci nikomu kazit iluze, ale tohle je zrovna učebnicový příklad potřeby důkazu nenulovosti, použije se typ identity (resp. jeho negace), ta funkce pak má typ Nat->y:Nat->Not (y=0)->Nat. Tohle není virální, ale chce to argument navíc. Ta druhá možnost pak jsou ty součtové záv. typy.

Obecně při práci se záv. typy je nutné přepínat "v hlavě" mezi typovým systémem a logickým kalkulem (CH korespondence).

P.S. Ten dodatečný argument někdy může překladač (resp. type checker) odvodit sám, to je právě ta síla těchto jazyků.

1785

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

« kdy: 15. 11. 2019, 16:51:00 »

V mé úvaze jsem dospěl k tomu, že potřebuju:

Zavést tu kaskádu typů. Mám Numeric a z něj "dědí" PositiveUnzeroNumeric

Mít "nonzero" typ není asi úplně ideální, to je virální až to bolí. Nechci nikomu kazit iluze, ale tohle je zrovna učebnicový příklad potřeby důkazu nenulovosti, použije se typ identity (resp. jeho negace), ta funkce pak má typ Nat->y:Nat->Not (y=0)->Nat. Tohle není virální, ale chce to argument navíc. Ta druhá možnost pak jsou ty součtové záv. typy.

Obecně při práci se záv. typy je nutné přepínat "v hlavě" mezi typovým systémem a logickým kalkulem (CH korespondence).