Vyšší typy

[Topolog]

Můžete mi někdo objasnit, proč typ funkce přijímající a vracející funkci (například (T->U)->(V->W)) není vyššího druhu (higher-kinded), ale třeba template template v C++ - (*->*)->* - ano?

[Reklama]

[klokan]

Typy funkcí, případně funkcí vyšších řádů, s typy vyšších druhů nijak přímo nesouvisí. Typ vyššího druhu je typ, který připouští typový parametr. Pokud jsou u funkce všechny typy konkrétní, např. int->int, ale klidně i (int->int)->(string->bool), má její typ v každém případě druh *.

Když budeme uvažovat např. vector<T>, kde T je libovolný typ, dosazený při instanciaci, bude mít samotný "vector"  jakožto typ vyšší druh *->*, ovšem typ vector<int> už je *. Stejné je to s funkcemi. Pokud je funkce generická, např v C++ něco jako

template<T> T krava(T a, int b) {
...
}

bude mít taky druh *->*.

Ještě pro pořádek: template a klasický "template template" v C++ NEJSOU typy vyšších druhů, protože to v prvé řadě nejsou typy. Typový model v C++ typové parametry nepřipouští a nic, co by mělo druh *->* v něm nelze definovat. Template jsou jenom zvláštní preprocessor, který generuje zvlášť typy prvního druhu pro každou z instanciací. V C++ tak neexistuje žádný "vector" jako takový, ale jenom "vector<int>", který nemá nic společného s "vector<char>" a tak podobně. Jiné je to v Haskellu, kde lze v takovém případě normálně operovat se samotným "vectorem".

[Jester]

Typy funkcí, případně funkcí vyšších řádů, s typy vyšších druhů nijak přímo nesouvisí. Typ vyššího druhu je typ, který připouští typový parametr. Pokud jsou u funkce všechny typy konkrétní, např. int->int, ale klidně i (int->int)->(string->bool), má její typ v každém případě druh *.

Když budeme uvažovat např. vector<T>, kde T je libovolný typ, dosazený při instanciaci, bude mít samotný "vector"  jakožto typ vyšší druh *->*, ovšem typ vector<int> už je *. Stejné je to s funkcemi. Pokud je funkce generická, např v C++ něco jako

template<T> T krava(T a, int b) {
...
}

bude mít taky druh *->*.

Ještě pro pořádek: template a klasický "template template" v C++ NEJSOU typy vyšších druhů, protože to v prvé řadě nejsou typy. Typový model v C++ typové parametry nepřipouští a nic, co by mělo druh *->* v něm nelze definovat. Template jsou jenom zvláštní preprocessor, který generuje zvlášť typy prvního druhu pro každou z instanciací. V C++ tak neexistuje žádný "vector" jako takový, ale jenom "vector<int>", který nemá nic společného s "vector<char>" a tak podobně. Jiné je to v Haskellu, kde lze v takovém případě normálně operovat se samotným "vectorem".

To s těmi funkcemi tady nedávno chybně tvrdil Sten, nepochopiv význam té hvězdičky. Nicméně blbě to máš i ty, protože druh *->* není vyšší, analogicky jako funkce int->int není vyššího řádu. Vyššího druhu je až třeba monáda. Omlouvá tě, že tato tématika je tak abstraktní a poměrně nová, že v tom plave hodně lidí.

A template template je pochopitelně v C++ “typ vyššího druhu”, instanciace s tím nemá co dělat.

[Jester]

P.S. Funktor do kategorie typů (např. Hask v Haskellu) je higher-kinded iff není endofunktorem. Takže přímo z definice *->* není HK.

[GrammarKatzi]

P.S. Funktor do kategorie typů (např. Hask v Haskellu) je higher-kinded iff není endofunktorem. Takže přímo z definice *->* není HK.

P.P.S. A to jsme se ještě nedostali k závislostním typům...

[Reklama]

[klokan]

To s těmi funkcemi tady nedávno chybně tvrdil Sten, nepochopiv význam té hvězdičky. Nicméně blbě to máš i ty, protože druh *->* není vyšší, analogicky jako funkce int->int není vyššího řádu. Vyššího druhu je až třeba monáda. Omlouvá tě, že tato tématika je tak abstraktní a poměrně nová, že v tom plave hodně lidí.

A template template je pochopitelně v C++ “typ vyššího druhu”, instanciace s tím nemá co dělat.

No zas tak nové to není, pochází to ze 70. let. Monáda je jeden příklad typu vyššího druhu a často si to spojují, snad proto, že monáda je jedna z praktických věcí, které se bez vyšších druhů nedají implementovat. Ale jsou i mnohem přízemnější věci, jako např. ten vector. Každý typový konstruktor, který bere min. jeden parametr, má implicitně vyšší druh.

Subtilní problém, kvůli kterému je mnoho nejasností, je to, že samotný typový systém nemusí umět vyšší druhy na to, aby se takové typy daly používat. Např. Rust, Swift ani ADA vyšší druhý nemají, ale umí generické typy, ačkoli tyto jsou vyšší druh. Je to proto, že se v těchto jazycích nikdy nepracuje s typovým konstruktorem samotným, ale vždycky jenom buď z konkrétní monomorfní instanciací, nebo aspoň se symbolickým typovým parametrem. Neboli nikdy se nepracuje s vectorem (*->*), ale vždycky jenom s vector<T> (*). To je právě ten důvod, proč se v těchto jazycích mimo jiné nedá monáda přímo implementovat.

K template: Template není typ a proto nemá ani druh, natož vyšší. V C++ totiž neexistuje ani ten vector<T>, ale jenom jeho konkrétní instanciace jako vector<int>. Samozřejmě, že template template se dá *modelovat* jako vyšší druh a některé statické analyzátory to tak dělají, ale v samotném C++ to žádný typový konstruktor není.

[Jester]

To s těmi funkcemi tady nedávno chybně tvrdil Sten, nepochopiv význam té hvězdičky. Nicméně blbě to máš i ty, protože druh *->* není vyšší, analogicky jako funkce int->int není vyššího řádu. Vyššího druhu je až třeba monáda. Omlouvá tě, že tato tématika je tak abstraktní a poměrně nová, že v tom plave hodně lidí.

A template template je pochopitelně v C++ “typ vyššího druhu”, instanciace s tím nemá co dělat.

Každý typový konstruktor, který bere min. jeden parametr, má implicitně vyšší druh.

Ne, nemá, viz vysvětlení výše.

[klokan]

Ne, nemá, viz vysvětlení výše.

To vysvětlení je IMO blbě, protože ta analogie s funkcemi je zavádějící. Obdobou druhu * totiž není funkce, ale proměnná. Teprve *->* je endofunktor v kategorii typů tak jako funkci lze charakterizovat jako endofunktor v kategorii hodnot.

Funkce vyššího řádu už endofunktor není. A stejně tak je nutné rozlišovat typy vyššího druhu (higher kind types) a typové konstruktoy vyššího řádu (higher rank types). To, co říkáte, platí o konstruktorech, kde konstruktor je vyššího *řádu* iff není endofunktor. Např. jednoduchá monáda (v Haskellu např. Maybe, nebo seznam) má druh *->*, stejně jako ten vector. Oba tak mají vyšší druh. Jenomže vector je současně konstruktor prvního řádu, kdežto *konstruktor* monády je vyššího řádu.

[Jester]

Ne, nemá, viz vysvětlení výše.

To vysvětlení je IMO blbě, protože ta analogie s funkcemi je zavádějící. Obdobou druhu * totiž není funkce, ale proměnná. Teprve *->* je endofunktor v kategorii typů tak jako funkci lze charakterizovat jako endofunktor v kategorii hodnot.

Funkce vyššího řádu už endofunktor není. A stejně tak je nutné rozlišovat typy vyššího druhu (higher kind types) a typové konstruktoy vyššího řádu (higher rank types). To, co říkáte, platí o konstruktorech, kde konstruktor je vyššího *řádu* iff není endofunktor. Např. jednoduchá monáda (v Haskellu např. Maybe, nebo seznam) má druh *->*, stejně jako ten vector. Oba tak mají vyšší druh. Jenomže vector je současně konstruktor prvního řádu, kdežto *konstruktor* monády je vyššího řádu.

No tvl. Na čem fičíš? Zdržím se komentáře, protože toto už jsou totální nesmysly.

[klokan]

No tvl. Na čem fičíš? Zdržím se komentáře, protože toto už jsou totální nesmysly.

Tak si něco přečti. Pouč se, co jsou HKT a co jsou HRT, jak se liší, nech si vysvětlit, jak to s těmi monádami vlastně je, že monáda samotná z definice je HRT konstruktor a ne typ, projdi si základy C++ abys nekecal blbosti o templatech kterým evidentně rozumíš jako koza náklaďáku, a pak to zkus znova. Zatím mi připomínáš jeden citát od Enrica Fermiho: "this is so bad that it's not even wrong".

[Jester]

No tvl. Na čem fičíš? Zdržím se komentáře, protože toto už jsou totální nesmysly.

Tak si něco přečti. Pouč se, co jsou HKT a co jsou HRT, jak se liší, nech si vysvětlit, jak to s těmi monádami vlastně je, že monáda samotná z definice je HRT konstruktor a ne typ, projdi si základy C++ abys nekecal blbosti o templatech kterým evidentně rozumíš jako koza náklaďáku, a pak to zkus znova. Zatím mi připomínáš jeden citát od Enrica Fermiho: "this is so bad that it's not even wrong".

Koukni na Wikipedii, tam máš příklady HKT vyvracející tvoje bláboly. Až si doděláš aspoň Bc., můžeme se bavit dál

[klokan]

Koukni na Wikipedii, tam máš příklady HKT vyvracející tvoje bláboly. Až si doděláš aspoň Bc., můžeme se bavit dál

Beze všeho, když na Wikipedii, tak na Wikipedii. Pokud máš na mysli https://en.m.wikipedia.org/wiki/Kind_(type_theory), tak tam uvidíš svoje vlastní příklady jako ukázky - jaká náhoda! - higher ORDER type OPERATOR, nikoli higher KIND TYPE, což je přesně ten rozdíl, který ti stále uniká.

Neboli Bc mám dávno šťastně za sebou, díky za optání, tak až se sám naučíš číst, podívej se třeba na https://gist.github.com/CMCDragonkai/a5638f50c87d49f815b8 

[Jester]

Koukni na Wikipedii, tam máš příklady HKT vyvracející tvoje bláboly. Až si doděláš aspoň Bc., můžeme se bavit dál

Beze všeho, když na Wikipedii, tak na Wikipedii. Pokud máš na mysli https://en.m.wikipedia.org/wiki/Kind_(type_theory), tak tam uvidíš svoje vlastní příklady jako ukázky - jaká náhoda! - higher ORDER type OPERATOR, nikoli higher KIND TYPE, což je přesně ten rozdíl, který ti stále uniká.

Hele, nauč se aspoň opisovat. HKT je higher-kindED type, “higher-kind” je negramatická blbost. Jinak na té Wikipedii máš příklad, proč generické typy nejsou vyššího druhu. Vrať se k funkcím vyššího řádu, to je vhodná analogie. Pak ti dojde ten zbytek (snad).

[klokan]

Hele, nauč se aspoň opisovat. HKT je higher-kindED type, “higher-kind” je negramatická blbost. Jinak na té Wikipedii máš příklad, proč generické typy nejsou vyššího druhu. Vrať se k funkcím vyššího řádu, to je vhodná analogie. Pak ti dojde ten zbytek (snad).

Za kind/kinded může nový mobil posedlý automatickou korekturou kterou se mi ještě nepodařilo vypnout, za čež se omlouvám. Jestli tam je někde odkaz na to, proč generické typy nejsou vyššího druhu, rád bych ho viděl, protože to je absolutní volovina. Ať to čtu jak to čtu, nic takového tam nestojí.

[Jester]

Hele, nauč se aspoň opisovat. HKT je higher-kindED type, “higher-kind” je negramatická blbost. Jinak na té Wikipedii máš příklad, proč generické typy nejsou vyššího druhu. Vrať se k funkcím vyššího řádu, to je vhodná analogie. Pak ti dojde ten zbytek (snad).

Za kind/kinded může nový mobil posedlý automatickou korekturou kterou se mi ještě nepodařilo vypnout, za čež se omlouvám. Jestli tam je někde odkaz na to, proč generické typy nejsou vyššího druhu, rád bych ho viděl, protože to je absolutní volovina. Ať to čtu jak to čtu, nic takového tam nestojí.

Ne, není to volovina, ani absolutní, ani relativní. Pokusím se o vysvětlení ještě jednou. U funkcí je ω→ω typ funkce, konkrétně prvního řádu. Funkce vyššího řádu je například (ω→ω)→ω. Podobně v případě druhů * značí konkrétní (=plně instanciovaný) typ a *→* je funktor (přesněji endofunktor) prvního řádu, tj. není to konkrétní typ (v Haskellu by se řeklo "typový konstruktor"), ale pořád je jen prvního řádu. Vyššího řádu je např. (*→*)→* (shodou okolností druh monád). V AJ je výraz "higher-kinded type" zkratkou za "type of a higher-order kind", přičemž celá ta terminologie pochází z formální logiky. Uznávám, že je trochu zmatená, ale je ustálená a nemá smysl se o ni hádat (konec konců je logická, viz ta analogie a funkcemi). Ať tak či onak, takto se toto výrazivo používá v Haskellu a jiných funkcionálních jazycích.