Naivní závislostní typ (úvaha)

[Mirek Prýmek]

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.

[Reklama]

[Mirek Prýmek]

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

[Idris]

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.

[Idris]

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.

[Idris]

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

[Reklama]

[Mirek Prýmek]

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.

[Idris]

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.

[Idris]

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

[BoneFlute]

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.

[Idris]

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

[Mirek Prýmek]

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

[BoneFlute]

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.

[Idris]

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

[Idris]

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.

[Mirek Prýmek]

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