Naivní závislostní typ (úvaha)

BoneFlute

  • *****
  • 1 475
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #15 kdy: 15. 11. 2019, 17:10:45 »
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.


BoneFlute

  • *****
  • 1 475
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #16 kdy: 15. 11. 2019, 17:15:03 »
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?)

Idris

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #17 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í :) )

Idris

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #18 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.

BoneFlute

  • *****
  • 1 475
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #19 kdy: 15. 11. 2019, 17:45:39 »
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?


Re:Naivní závislostní typ (úvaha)
« Odpověď #20 kdy: 15. 11. 2019, 17:51:51 »
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.

Go tenhle problém (ztráta "přesnosti" typu) řeší pomocí type switche, popř. type assertion. To není vůbec blbej nápad. Ale je to ukecaný.

...no a druhá možnost je, že to nebudou podtypy. Pak to ale bude strašná otrava používat.
A co to pak bude? A jak by to teda vypadalo?
Typ Int a Age by prostě pro typový systém byly úplně jiné typy, bez jakéhokoliv vztahu. Stejně jako třeba Int a String. Takže bys je musel převádět pomocí nějaké speciální funkce

Kód: [Vybrat]
intToAge: Int -> Maybe Age
« Poslední změna: 15. 11. 2019, 17:53:33 od Mirek Prýmek »

BoneFlute

  • *****
  • 1 475
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #21 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) -> Numericnebo 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?

Re:Naivní závislostní typ (úvaha)
« Odpověď #22 kdy: 15. 11. 2019, 18:02:23 »
PositiveUnzeroNumeric
Prosímtě, neříkej tomu "Unzero", strašně to trhá oči. Správně je Nonzero.

:)

Idris

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #23 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.

Idris

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #24 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... ;)

BoneFlute

  • *****
  • 1 475
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #25 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ě?

BoneFlute

  • *****
  • 1 475
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #26 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ží?

Idris

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #27 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) -> Numericnebo 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í.

Idris

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #28 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"].

BoneFlute

  • *****
  • 1 475
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #29 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.