Fórum Root.cz

Hlavní témata => Vývoj => Téma založeno: BoneFlute 14. 11. 2019, 22:09:42

Název: Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 14. 11. 2019, 22:09:42
Mějme hypotetický jazyk s hypotetickým typovým systémem.

Mějme typ Numeric reprezentující všechna reální čísla, a pak následující kaskádu typů:

Numeric > Int > Age > Young
Numeric > PositiveUnzeroNumeric
Kde Age je rozsah 0 - 255, Young 0 - 19, PositiveUnzeroNumeric rozsah 1 - MAX_INT

Máme funkci pro dělení:
Kód: [Vybrat]
div a b = a / b
A dáme jí takovouto typovou signaturu:
Kód: [Vybrat]
div :: Numeric -> PositiveUnzeroNumeric -> Numeric
Šlo by to? Šlo by tímto způsobem na úrovni typového systému zabránit dělení nulou? Možná ne, ale zajímalo, jestli by se k tomu někdo zkušenější mohl vyjádřit. Protože třeba:

Kód: [Vybrat]
calculate :: Numeric -> Numeric -> Numeric
calculate a b = a `div` (b - 3)
calculate 9 6 -- 3
calculate 9 3 -- divide zero
se IMHO nepřeloží.

Jaké to může mít úskalí?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: gill 14. 11. 2019, 22:41:19
Citace
Jaké to může mít úskalí?

funguje to jen s konstantními výrazy.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 14. 11. 2019, 22:46:22
Citace
Jaké to může mít úskalí?

funguje to jen s konstantními výrazy.

Můžeš to prosím rozvést? Co myslíš konstantními výrazy a co myslíš tím nefunguje.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: gill 14. 11. 2019, 22:52:25
Citace
Jaké to může mít úskalí?

funguje to jen s konstantními výrazy.

Můžeš to prosím rozvést? Co myslíš konstantními výrazy a co myslíš tím nefunguje.

nebudu se dohadovat o definici konstantního výrazu. Tak jak jsi ten problém popsal, je snad jasné, že

Kód: [Vybrat]
calculate a b

kde a b jsou čísla z venku, žádnou compile time chybu generovat nemůže.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 14. 11. 2019, 23:02:23
Tak jak jsi ten problém popsal, je snad jasné, že

Kód: [Vybrat]
calculate a b

kde a b jsou čísla z venku, žádnou compile time chybu generovat nemůže.

Pokud myslíš něco jako:
Kód: [Vybrat]
main :: IO ()
main = do
    a <- getLine
    b <- getLine
    putStrLn $ format $ calculate (parseNumeric a) (parseNumeric b)
Tak mi je jasné, že fungovat bude. Respektive se to nepřeloží. V tomto by být problém neměl.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Jiří Havel 15. 11. 2019, 09:01:02
Nějakou dobu jsem s něčím podobným experimentoval. Konkrétně otagované a ohraničené integery v C++. Je trochu problém vybalancovat poměr přínos/opruz.

1) Interakce s vnějším světem se děje furt. Balení a vybalování toho intu musí být jednoduché. Tvoje typy se vyskytují jen na pár místech. Postupně se rozlézají, ale i tak je interakce s vnějším světem jedna z nejčastějších věcí.
2) Nenulové číslo nevznikne jen tak, ale obvykle nějakým testem na nulu. Takže to balení není jenom na hranici tvého světa.
3) U intů je to jednoznačné, ale s floaty přicházejí další problémy. Takové typy jako "normalizovaný vektor" nebo "ortonormální matice" jsou v praxi dost fuzzy.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 15. 11. 2019, 09:14:42
Na to ti bude umět dobře odpovědět Idris. Já jsem tu jím doporučenou knížku o dependent types ještě pořád nepřelouskal, takže pořádně ti odpovědět neumím, ale aspoň jeden problém tam vidím i tak:

Aby se to dalo nějak rozumně používat, musíš zároveň s tím zavést subtyping. Aby typový systém věděl, že Age je podmnožina Int. No a se subtypingem vzniká spousta otravných problémů, které asi nejsou neřešitelné, ale začnou typový systém a hlavně jeho syntaxi znepřehledňovat. V tématu o OOP jsem zmínil problém (ko|kontra)variance - můžeš do l: List Int vložit x : Age? Když ho potom z listu vybíráš, vrátí se ti Int nebo Age?

Haskell detailně neznám, ale myslím, že se subtyping do něj moc nehodí. Viz např. https://www.reddit.com/r/haskell/comments/423o0c/why_no_subtypingsubtype_polymorphism/

...no a druhá možnost je, že to nebudou podtypy. Pak to ale bude strašná otrava používat.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 15. 11. 2019, 09:22:03
P.S. a jestli můžu už vyloženě vařit z vody, tak předpokládám, že když do typů zavedeš dostatečně silné formule, tak ti tam vznikne nějaký silný jazyk, což bude mít předpokládám dopady do rozhodnutelnosti a tak. Známe to, stačí někam prsknout Peanovu aritmetiku a je průser ;)

(Idris mě omluví za humpoláckou mluvu a doupřesní to nebo opraví :) )
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Jiří Havel 15. 11. 2019, 12:46:09
...no a druhá možnost je, že to nebudou podtypy. Pak to ale bude strašná otrava používat.
Další možnost je zneškodnit reference na mutable. Pokud subtyping funguje jen s referencema na const, případně s kopírováním/slicingem, tak je to relativně ok.

Samozřejmě že zůstává problém, že inkrement Age už není Age. Takže není možné napsat ani klasický for cyklus tak, aby to prošlo typovou kontrolou. Musí se implementovat vlastní kontrolní struktury, které uvnitř ten typový systém obcházejí.

Ona je sranda i dělat výpočty s intervaly intů. Intervalová aritmetika trpí na "dependency problem". Nepříjeně často ten automaticky vypočítaný rozsah silně uletí. Tady jsem nebyl schopen dosáhnout nějaké přijatelné úrovně opruzu.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 15. 11. 2019, 13:02:46
Šlo by tímto způsobem na úrovni typového systému zabránit dělení nulou?
Ano, šlo. Je nebetyčná blbost, že by to fungovalo jen s konstantními výrazy, kdo to tvrdí, netuší nic o symbolických výrazech. Ovšem ve složitějším kódu by si to vyžádalo součtové závislostní typy, které jsou “virální” podobně jako zvedání typů pomocí funktorů. Čili technicky to jde a posílí to typovou kontrolu, ale za cenu menší intuitivnosti.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 15. 11. 2019, 13:05:19
P.S. a jestli můžu už vyloženě vařit z vody, tak předpokládám, že když do typů zavedeš dostatečně silné formule, tak ti tam vznikne nějaký silný jazyk, což bude mít předpokládám dopady do rozhodnutelnosti a tak. Známe to, stačí někam prsknout Peanovu aritmetiku a je průser ;)

(Idris mě omluví za humpoláckou mluvu a doupřesní to nebo opraví :) )
Typy jsou intuicionistická logika a ta je rozhodnutelná ;)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 15. 11. 2019, 16:42:49
Šlo by tímto způsobem na úrovni typového systému zabránit dělení nulou?
Ano, šlo. Je nebetyčná blbost, že by to fungovalo jen s konstantními výrazy, kdo to tvrdí, netuší nic o symbolických výrazech. Ovšem ve složitějším kódu by si to vyžádalo součtové závislostní typy, které jsou “virální” podobně jako zvedání typů pomocí funktorů. Čili technicky to jde a posílí to typovou kontrolu, ale za cenu menší intuitivnosti.
Mohl by si to rozvést?

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 který je jeho podmnožinou (subtyp?). A nějaký instrumenty na to, jak to zapsat.

Pak mi všechno začne "magicky" fungovat, a nic dalšího bych neměl potřebovat. Protože typový systém, tak jak by byl, tak jak ho známe, by my automaticky vyhodil místa, kde ty typy nebudou sedět. Konkrétně třeba:
Kód: [Vybrat]
calculate :: Numeric -> Numeric -> Numeric
calculate a b = a `div` (b - 3)

Stejně tak funkce inc a, nebo for cyklus (ve skutečnosti to bude funkce map), to všechno se automaticky vyhodí, protože ty typy nebudou sedět. Což mi přijde intuitivní dost. Ale třeba mi ještě něco nedochází.

Jaké součtové typy by to vyžadovalo v jakém případě? To je asi to co mě zajímá. Protože takhle mi přijde, že víc toho nepoutřebuju.

problém (ko|kontra)variance - můžeš do l: List Int vložit x : Age? Když ho potom z listu vybíráš, vrátí se ti Int nebo Age?
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...
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á?

...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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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).
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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ů.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Filip Jirsák 15. 11. 2019, 16:58:49
Jak by ten váš typový systém řešil tohle?

Kód: [Vybrat]
plus :: Numeric, Numeric → ?
? a
Numeric b
for (;;) {
  a := plus(a, b)
}

Jaké typy by byly místo otazníků?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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?)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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í :) )
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 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
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 15. 11. 2019, 18:02:23
PositiveUnzeroNumeric
Prosímtě, neříkej tomu "Unzero", strašně to trhá oči. Správně je Nonzero.

:)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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... ;)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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ě?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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ží?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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í.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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"].
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 15. 11. 2019, 18:34:35
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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 15. 11. 2019, 18:35:48
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í.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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 :)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 15. 11. 2019, 18:53:16
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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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/ů.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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í.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 15. 11. 2019, 19:02:32
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.

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).
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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).
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 15. 11. 2019, 19:28:54
U každé?
U každé, která má být součástí nějaké hierarchie. Go to má jenom u interfejsů, protože to je jediná věc, u které hierarchii má.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 15. 11. 2019, 19:32:41
Tohle je fakt non-issue
Jestli ti pole integerů zabírá 32G nebo 64G úplně non-issue není :)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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...
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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 ;)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 16. 11. 2019, 00:00:41
Mám RAM 128GB :P
V tom případě tě bude zajímat, jestli pole Intů zabírá 128G  nebo 256G ;)

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.
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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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á.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 16. 11. 2019, 00:16:59
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 :)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 16. 11. 2019, 00:25:11
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, versu runtime vypustil. A budu se těšit, jestli mi Idris řekne něco k těm sudejm číslům.
Fair enough :)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 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 :)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 17. 11. 2019, 22:03:07
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?

Mohl bych se @Idris připomenout? Samozřejmě chápu, že máš dost svých starostí, ale třeba budu mít štěstí.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 20. 11. 2019, 19:58:45
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?

Mohl bych se @Idris připomenout? Samozřejmě chápu, že máš dost svých starostí, ale třeba budu mít štěstí.
Sorry, teď teprve se k tomu vracím. Stay tuned ;)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 20. 11. 2019, 23:13:52
Mohl bych se @Idris připomenout? Samozřejmě chápu, že máš dost svých starostí, ale třeba budu mít štěstí.
I'm back :)
No, vezmu to zkrátka, jako jednoduchý příklad budeme mít unární predikát Even : Nat -> Type. Konstruktory budou dva, a sice
EvenZ : Even Z a
EvenSS : Even n -> Even (S (S n))
(tady je krásně vidět, jak typový konstruktor pro funkce je vlastně implikace, včetně stejného zápisu).
Jako příklad použití mějme funkci pro dělení dvěma, která akceptuje pouze sudá čísla:
div2 : (n:Nat) -> {auto prf:Even n} -> Nat
Pro nulu máme
div2 Z {prf=EvenZ} = 0
a jinak
div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
Takže teď můžu jednoduše volat div2 n, přičemž ten druhý argument (důkaz sudosti) mi překladač odvodí sám.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 21. 11. 2019, 18:23:21
div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
Co prosím tě znamená to S?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 21. 11. 2019, 18:43:51
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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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  :(
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 21. 11. 2019, 20:52:54
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.
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ů?
Ano, je to generický typ, dostane přirozené číslo a vrátí konkrétní typ.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 21. 11. 2019, 20:54:45
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.
Jak u
Kód: [Vybrat]
EvenSS : Even n -> Even (S (S n)) zajistím, že to bude zrovna sudá řada?
Začíná se nulou (“Z”) a (S (S n)) v podstatě znamená n+2, takže to jsou násobky dvou.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 21. 11. 2019, 20:59:49
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  :(
To prf je “proof”, tady je třeba “přepnout myšlení” z typů na formální logiku (Curry-Howardova korespondence). To prf je důkaz (formální, symbolický), že vstup je sudé číslo. Díky existenci toho důkazu můžu vesele dělit a vím, že dostanu přirozené číslo. U toho následníka si “půjčím” důkaz pro n-2 z konstruktoru predikátu, abych měl co předat v rekurzi. Zkus si to rozepsat ve FOL ;)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 21. 11. 2019, 21:48:45
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?
To není definice, je to důkaz (proof) platnosti formule. Hodnoty typů odpovídají důkazům formulí. Nedokazatelné formule odpovídají podle CHK typům bez hodnost (tzv. uninhabited types, “neobydlené”). Typově EvenZ je jedinou hodnotou typu Even 0 atd.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 11:16:48
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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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 :-(
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 22:03:02
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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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 :-)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 22:14:21
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é?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 22:27:55
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 :-)
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). 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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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á. (https://cs.wikipedia.org/wiki/Curryho–Howardův_isomorfismus)


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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 22. 11. 2019, 23:10:23
Akorát nejde o “starou dobrou známou” klasickou logiku prvního řádu, ale o logiku intuicionistickou (to je ovšem detail).
Jenom tak ze zvědavosti: Takže ten typový systém pak je korektní, ale není úplný? Takže i pro dobře otypovaný program může říct "nevím, jestli je to správně"? Platí to pro všechny DT systémy? Je dokázáno, že úplný nemůže existovat?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 23:22:49
Akorát nejde o “starou dobrou známou” klasickou logiku prvního řádu, ale o logiku intuicionistickou (to je ovšem detail).
Jenom tak ze zvědavosti: Takže ten typový systém pak je korektní, ale není úplný? Takže i pro dobře otypovaný program může říct "nevím, jestli je to správně"? Platí to pro všechny DT systémy? Je dokázáno, že úplný nemůže existovat?
Teď nevím, kam míříš. Proč by neměl být úplný?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 23:23:35
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á. (https://cs.wikipedia.org/wiki/Curryho–Howardův_isomorfismus)
Jo, je cool :)
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Mirek Prýmek 22. 11. 2019, 23:25:14
Teď nevím, kam míříš. Proč by neměl být úplný?
Myslel jsem kvuli te intuicionisticke logice. Jen intuitivni :) otazka, bez hlubsiho promysleni, na ktery ted bohuzel nemam cas.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 23:26:45
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?
Je to trochu složitější, e je nějaká entita (“individuum z univerza”), které reprezentuje nějaký výrok, který může platit, nebo taky ne. V případě Even’(e, 5) je e reifikace výroku, že 5 je sudé číslo. V tomto případě tedy True(e) neplatí.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 23:35:00
Teď nevím, kam míříš. Proč by neměl být úplný?
Myslel jsem kvuli te intuicionisticke logice. Jen intuitivni :) otazka, bez hlubsiho promysleni, na ktery ted bohuzel nemam cas.
Intuicionistická logika je úplná, ve skutečnosti je slabší než klasická predikátová. Jde dokázat, že je to vůbec nejslabší logika, ve které platí modus ponens. Já mířil na druhou stranu formální síly, reifikací se dá simulovat logika vyššího řádu v logice prvního řádu.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 23:36:21
Teď nevím, kam míříš. Proč by neměl být úplný?
Myslel jsem kvuli te intuicionisticke logice. Jen intuitivni :) otazka, bez hlubsiho promysleni, na ktery ted bohuzel nemam cas.
P.S. Ještě jsem zapomněl dodat, že v int. logice splývá dokazatelnost s vyčíslitelností.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 22. 11. 2019, 23:41:20
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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 23. 11. 2019, 08:54:43
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).
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 25. 11. 2019, 10:44:28
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))
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.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 25. 11. 2019, 10:48:53
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).
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?
To jsou dvě různé věci, já se nebavil o typu reprezentujícím množinu sudých přirozených čísel, to by byl prostě podtyp bez záv. typů. Šlo o vytvoření typu, který zaručí sudost čísla *na úrovni typů*, třeba u toho div2 mi zabrání tomu, aby někdo předal liché číslo. Záv. typy se většinou používají k vynucení kontraktů, to je jejich hlavní přínos.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 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))
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: BoneFlute 25. 11. 2019, 14:05:51
To jsou dvě různé věci, já se nebavil o typu reprezentujícím množinu sudých přirozených čísel, to by byl prostě podtyp bez záv. typů. Šlo o vytvoření typu, který zaručí sudost čísla *na úrovni typů*, třeba u toho div2 mi zabrání tomu, aby někdo předal liché číslo. Záv. typy se většinou používají k vynucení kontraktů, to je jejich hlavní přínos.

Rozumím. Zatímco já jsem vytvořil klasickou funkci kde platilo jen omezení na typ, ty jsi vytvořil košaťejší omezení jen pro tu funkci. Správně?
Díky tomu by šlo pak vytvořit “pravidla” kde by se výstupní typ funkce měnil podle toho co má za vstupy. Tak?

Každopádně ještě zopakuji otázku: Při volání té funkce na sudá čísla si stejně bude muset volající zajistit aby předával jen sudá. DT tomu nedodají žádnou další magii proti mému řešení?
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 25. 11. 2019, 14:39:19
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))
Jo, takto. Ta 1 se expanduje na (S Z), ale to je jen pozornost od překladače.
Název: Re:Naivní závislostní typ (úvaha)
Přispěvatel: Idris 25. 11. 2019, 14:42:18
To jsou dvě různé věci, já se nebavil o typu reprezentujícím množinu sudých přirozených čísel, to by byl prostě podtyp bez záv. typů. Šlo o vytvoření typu, který zaručí sudost čísla *na úrovni typů*, třeba u toho div2 mi zabrání tomu, aby někdo předal liché číslo. Záv. typy se většinou používají k vynucení kontraktů, to je jejich hlavní přínos.
Každopádně ještě zopakuji otázku: Při volání té funkce na sudá čísla si stejně bude muset volající zajistit aby předával jen sudá. DT tomu nedodají žádnou další magii proti mému řešení?
Ano, volající to musí zajistit, většinou to ale zařídí překladač automaticky. To je princip záv. typů, když volající něco nezajistí, co je dáno kontraktem, program se nepřeloží místo zkolabování za běhu.