Fórum Root.cz

Hlavní témata => Vývoj => Téma založeno: Topolog 01. 04. 2018, 00:03:09

Název: Vyšší typy
Přispěvatel: Topolog 01. 04. 2018, 00:03:09
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?
Název: Re:Vyšší typy
Přispěvatel: klokan 01. 04. 2018, 11:41:39
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".
Název: Re:Vyšší typy
Přispěvatel: Jester 01. 04. 2018, 13:56:37
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.
Název: Re:Vyšší typy
Přispěvatel: Jester 01. 04. 2018, 14:22:53
P.S. Funktor do kategorie typů (např. Hask v Haskellu) je higher-kinded iff není endofunktorem. Takže přímo z definice *->* není HK.
Název: Re:Vyšší typy
Přispěvatel: GrammarKatzi 01. 04. 2018, 16:09:46
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...
Název: Re:Vyšší typy
Přispěvatel: klokan 01. 04. 2018, 17:11:59
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í.
Název: Re:Vyšší typy
Přispěvatel: Jester 01. 04. 2018, 18:34:58
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.
Název: Re:Vyšší typy
Přispěvatel: klokan 02. 04. 2018, 00:23:34
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.
Název: Re:Vyšší typy
Přispěvatel: Jester 02. 04. 2018, 01:04:25
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.
Název: Re:Vyšší typy
Přispěvatel: klokan 02. 04. 2018, 01:44:37
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".
Název: Re:Vyšší typy
Přispěvatel: Jester 02. 04. 2018, 01:48:11
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 ;)
Název: Re:Vyšší typy
Přispěvatel: klokan 02. 04. 2018, 03:09:44
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) (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 (https://gist.github.com/CMCDragonkai/a5638f50c87d49f815b8)  ;)
Název: Re:Vyšší typy
Přispěvatel: Jester 02. 04. 2018, 03:18:05
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) (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).
Název: Re:Vyšší typy
Přispěvatel: klokan 02. 04. 2018, 03:34:20
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í.
Název: Re:Vyšší typy
Přispěvatel: Jester 02. 04. 2018, 03:57:20
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.
Název: Re:Vyšší typy
Přispěvatel: klokan 02. 04. 2018, 06:39:38

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.

Tak mám dojem, že se snad konečně shodneme. Sám říkáš zcela správně, že *->* je konstruktor prvního ŘÁDU (ovšem ne prvního DRUHU). Hodně lidí si plete řád a druh, ale není to totéž. Druh je v podstatě jenom arita typového konstruktoru, přičemž monomorfní neboli plně instanciovaný typ má aritu 0 (druh *), a arity > 0 jsou vyšší druhy.

Naproti tomu typový konstruktor vyššího řádu je takový, který předpokládá typový argument vyššího druhu, např. (*->*)->*. Ta analogie s funkcemi ve skutečnosti funguje tak, že hodnota je objekt druhu *, funkce je objekt druhu *->* (nebo vyššího) a funkce vyššího řádu je funkce, jejíž parametr je sám funkce (objekt vyššího druhu).

Takže v kostce:

* je první druh prvního řádu (analogicky proměnná).

*->* ale taky *->*->*->* jsou vyšší druhy (HKT) prvního řádu (analogicky klasické funkce).

(*->*)->* je vyšší druh (HKT) vyššího řádu (HRT) (analogicky funkce vyššího řádu).

Ta terminologie je zavádějící, uznávám. Netvrdím, že nikdo nikdy nikde nepoužíval druh ve smyslu řád, ale striktně korektní definice to rozlišuje, stejně jako veškerá peer reviewed literatura, kterou jsem kdy na toto téma četl... nebo napsal.

Mimochodem to, že v jazyku bez HKT nejdou implementovat monády, není kvůli tomu, že údajně teprve (*->*)->* je vyšší druh. Právě naopak. Když si zkusíš definovat monádu jako typovou třídu v Rustu nebo Swiftu, to, na co narazíš, bude typová signatura operátoru bind (>>=). Ono klasické M a -> (a -> M b) -> M b prostě nebude možné vyjádřit, protože M a a M b jsou dvě různé instanciace typu - tradááá - VYŠŠÍHO DRUHU M (*->*), a jazyk bez podpory HKT je tak vidí jako dva naprosto spolu nesouvisející typy druhu *, které obecně a priori nejsou instancemi téže typové třídy Monad.
Název: Re:Vyšší typy
Přispěvatel: Jester 02. 04. 2018, 12:37:32
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.

Tak mám dojem, že se snad konečně shodneme. Sám říkáš zcela správně, že *->* je konstruktor prvního ŘÁDU (ovšem ne prvního DRUHU). Hodně lidí si plete řád a druh, ale není to totéž. Druh je v podstatě jenom arita typového konstruktoru, přičemž monomorfní neboli plně instanciovaný typ má aritu 0 (druh *), a arity > 0 jsou vyšší druhy.

Naproti tomu typový konstruktor vyššího řádu je takový, který předpokládá typový argument vyššího druhu, např. (*->*)->*. Ta analogie s funkcemi ve skutečnosti funguje tak, že hodnota je objekt druhu *, funkce je objekt druhu *->* (nebo vyššího) a funkce vyššího řádu je funkce, jejíž parametr je sám funkce (objekt vyššího druhu).

Takže v kostce:

* je první druh prvního řádu (analogicky proměnná).

*->* ale taky *->*->*->* jsou vyšší druhy (HKT) prvního řádu (analogicky klasické funkce).

(*->*)->* je vyšší druh (HKT) vyššího řádu (HRT) (analogicky funkce vyššího řádu).

Ta terminologie je zavádějící, uznávám. Netvrdím, že nikdo nikdy nikde nepoužíval druh ve smyslu řád, ale striktně korektní definice to rozlišuje, stejně jako veškerá peer reviewed literatura, kterou jsem kdy na toto téma četl... nebo napsal.

Mimochodem to, že v jazyku bez HKT nejdou implementovat monády, není kvůli tomu, že údajně teprve (*->*)->* je vyšší druh. Právě naopak. Když si zkusíš definovat monádu jako typovou třídu v Rustu nebo Swiftu, to, na co narazíš, bude typová signatura operátoru bind (>>=). Ono klasické M a -> (a -> M b) -> M b prostě nebude možné vyjádřit, protože M a a M b jsou dvě různé instanciace typu - tradááá - VYŠŠÍHO DRUHU M (*->*), a jazyk bez podpory HKT je tak vidí jako dva naprosto spolu nesouvisející typy druhu *, které obecně a priori nejsou instancemi téže typové třídy Monad.
Neshodneme, máš v tom guláš (minimálně v anglické terminologii), *→* ani *→*→*→*→*→*→*→*→*→*→*→* nejsou HK, protože "higher-kinded" je synonymní pro "vyšší řád" druhu, což právě - podle mě zcela jasně - popisuje už ta Wikipedie (ta je ostatně taky peer-reviewed). Z vědecké literatury pak třeba "Generics of a higher kind" nebo tak nějak (píšu to z hlavy, je to starý článek). A BTW, *→* i (*→*)→* mají stejnou aritu, ale odlišný druh, druh nemá nic společného s aritou, je to "typ typu". Z těchto dvou jen ten druhý je HK (analogicky k template template - proto jdou v C++ naimplementovat generické monády a v Javě ne). Možná, že polopaticky to je vysvětlené někde na Stackoverflow, kde se lidi ptají, proč Java nemá HKT - má jen *→* (případně s vyšší aritou), tj. končí na prvním řádu, kdežto HK znamená řád >1.
Název: Re:Vyšší typy
Přispěvatel: klokan 02. 04. 2018, 13:51:07
To je neskutečná hromada žvástů. KIND se odjakživa vztahuje k aritě typového konstruktoru a tudíž to NENÍ řád. Typy vyššího řádu se v ustálené terminologii nazývají Higer RANK. Ta tvoje tolik vyzdvihovaná Wikipedie nepřesně používá výraz Higer ORDER, což je sice mimo exaktní terminologii, ale každému, kdo se obtěžuje si to doopravdy přečíst je snad jasné, o čem je řeč. S KINDem aspoň operuje korektně na rozdíl od toho, co sis myslel, že se tam píše.

Oni to totiž není jenom samoůčelné slovíčkaření. Rozdíl mezi vyšším druhem (HK) a vyšším řádem (HR) je zásadní. Pro pochopení si na úvod si přečti třeba https://www.google.com.au/url?sa=t&source=web&rct=j&url=https://www.cl.cam.ac.uk/~jdy22/papers/lightweight-higher-kinded-polymorphism.pdf&ved=2ahUKEwje1dS9wpvaAhXGVbwKHeaiBQMQFjAAegQICBAB&usg=AOvVaw11xOuncGG5HNJIw_d_IaNb (https://www.google.com.au/url?sa=t&source=web&rct=j&url=https://www.cl.cam.ac.uk/~jdy22/papers/lightweight-higher-kinded-polymorphism.pdf&ved=2ahUKEwje1dS9wpvaAhXGVbwKHeaiBQMQFjAAegQICBAB&usg=AOvVaw11xOuncGG5HNJIw_d_IaNb), jinak je zajímavé např. https://www.google.com.au/url?sa=t&source=web&rct=j&url=https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf&ved=2ahUKEwi9763Gv5vaAhWJwbwKHdKtA484ChAWMAJ6BAgIEAE&usg=AOvVaw2VimUnjZAnCN0bVC_h5sV9 (https://www.google.com.au/url?sa=t&source=web&rct=j&url=https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf&ved=2ahUKEwi9763Gv5vaAhWJwbwKHdKtA484ChAWMAJ6BAgIEAE&usg=AOvVaw2VimUnjZAnCN0bVC_h5sV9) nebo https://www.google.com.au/url?sa=t&source=web&rct=j&url=https://nerget.com/thesis.pdf&ved=2ahUKEwi9763Gv5vaAhWJwbwKHdKtA484ChAWMAN6BAgDEAE&usg=AOvVaw2S78pPMtPTxtaPFFkGCaEs (https://www.google.com.au/url?sa=t&source=web&rct=j&url=https://nerget.com/thesis.pdf&ved=2ahUKEwi9763Gv5vaAhWJwbwKHdKtA484ChAWMAN6BAgDEAE&usg=AOvVaw2S78pPMtPTxtaPFFkGCaEs). Pokud máš pro svůj alternativní svět nějaké reference, které nejsou jenom pomýlená představa o tom, co píšou na Wikipedii nebo citace na úrovni "XYZ nebo takňák", sem s nimi. Klidně se s tebou vsadím o učebnici matematiky pro první třídu.

Máš pravdu v tom, že (*->*)->* a *->* mají stejnou aritu - ovšem liší se řádem neboli rankem, což ti stále nedochází. Nicméně gratuluju, poprvé si v tomhle threadu prohlásil něco, co je blbě jenom z poloviny. Jen tak dál  ;)
Název: Re:Vyšší typy
Přispěvatel: Jester 02. 04. 2018, 14:02:55
Typy vyššího řádu se v ustálené terminologii nazývají Higer RANK. [...] Rozdíl mezi vyšším druhem (HK) a vyšším řádem (HR) je zásadní.
Pominu urážky a jen poznamenám, že "řád" je v angličtině v matematickém kontextu "order". Když ani nevíš, co se jak překládá, tak už se nedivím, že píšeš věci bez hlavy a paty. Přečti si tu referenci, co jsem dal, i když evidentně máš problém porozumět (přinejmenším) anglickému textu, tak to asi k ničemu nebude.
Název: Re:Vyšší typy
Přispěvatel: Jester 02. 04. 2018, 14:11:59
...
P.S. Ty tvoje odkazy výslovně uvádí přesně to, to tady píšu furt dokola: *→* není HK. Tímto jsi ze sebe udělal totálního debila. Přečti si ty texty nejdřív sám, pak se můžeš pokorně připlazit zpátky a omluvit se.
Název: Re:Vyšší typy
Přispěvatel: Mirek Prýmek 02. 04. 2018, 18:00:35
P.S. Ty tvoje odkazy výslovně uvádí přesně to, to tady píšu furt dokola: *→* není HK. Tímto jsi ze sebe udělal totálního debila. Přečti si ty texty nejdřív sám, pak se můžeš pokorně připlazit zpátky a omluvit se.
Máš sice pravdu, Jestere, ale škoda, že to shazuješ takhle zbytečnými urážkami. To přece není nutný, ne? (Jo, vím, že sis nezačal :) )
Název: Re:Vyšší typy
Přispěvatel: Mirek Prýmek 02. 04. 2018, 18:18:14
*->* ale taky *->*->*->* jsou vyšší druhy (HKT) prvního řádu (analogicky klasické funkce).

(*->*)->* je vyšší druh (HKT) vyššího řádu (HRT) (analogicky funkce vyššího řádu).
Imho se mýlíš. Snad se shodnem na tom, že List<T> v Javě má kind * -> * a List<Int> má kind *. No a pak si už můžeš snadno kdekoli najít, jestli Java má nebo nemá higher-kinded types. Najdeš, že nemá. Protože * -> * je first order kind a není to teda "higher-order kind" neboli "higher-kinded type". V Javě nejsou typy s kindem (* -> *) -> *, narozdíl od Haskellu.
Název: Re:Vyšší typy
Přispěvatel: Jester 03. 04. 2018, 18:54:52
Tak kde to vázne, kde je ta omluva? Šup šup
Název: Re:Vyšší typy
Přispěvatel: jdusizasvym 03. 04. 2018, 21:24:26
Tak kde to vázne, kde je ta omluva? Šup šup

Ach jo, ty jsi po technické stránce a co se týče hard skills opravdu chytrý a inteligentní, ale sociálně jsi ***... Je to dost škoda kurvit si zbytečně image a tím všechno, co umíš a znáš zahodit do ****
Název: Re:Vyšší typy
Přispěvatel: hawran diskuse 03. 04. 2018, 23:30:52
Ajajaj, přestřelka zboj vs. mirek po bambilijóntéosmé?
OK, lads, fire at will.

BTW, zkusili jste se tu už někdy zeptat místního plebsu (kam se počítám i já), esli už někdo pochopil ty gonády a jak je použil ve své lopatorobotě?
 :D
Název: Re:Vyšší typy
Přispěvatel: hawran diskuse 03. 04. 2018, 23:38:25
PS:
Leibnizova filosofie
Monády
Základní pojem jeho filosofie je monáda. Navazuje na Reného Descarta, který soudil, že všechny přírodní jevy lze vyložit pojmy rozlehlosti a pohybu a že základem světa jsou dvě substance – materiální a duchovní. Naproti tomu tvrdí, že je pohyb něco čistě relativního, závisí pouze na stanovisku pozorovatele, které těleso se jeví v pohybu a které ne. Descartovo pojetí substancí kritizuje ještě v druhém ohledu, z hlediska kontinuity a dělitelnosti.

HUH?
Název: Re:Vyšší typy
Přispěvatel: Mirek Prýmek 04. 04. 2018, 01:03:34
přestřelka zboj vs. mirek po bambilijóntéosmé?
Co mám já a zboj společnýho se sporem mezi Jestrem a klokanem?
Název: Re:Vyšší typy
Přispěvatel: klokan 04. 04. 2018, 07:50:23
Tak kde to vázne, kde je ta omluva? Šup šup

Tak si to prosím tě skutečně přečti a podívej se na mou odpověď Mirkovi Prýmkovi. Pokud budeš mít nějakou věcnou připomínku případně pokud můj příklad doopravdy vyvrátíš, můžeme se bavit místo si nadávat. Zatím si stojím za tím, co říkám.
Název: Re:Vyšší typy
Přispěvatel: klokan 04. 04. 2018, 08:09:56
*->* ale taky *->*->*->* jsou vyšší druhy (HKT) prvního řádu (analogicky klasické funkce).

(*->*)->* je vyšší druh (HKT) vyššího řádu (HRT) (analogicky funkce vyššího řádu).
Imho se mýlíš. Snad se shodnem na tom, že List<T> v Javě má kind * -> * a List<Int> má kind *. No a pak si už můžeš snadno kdekoli najít, jestli Java má nebo nemá higher-kinded types. Najdeš, že nemá. Protože * -> * je first order kind a není to teda "higher-order kind" neboli "higher-kinded type". V Javě nejsou typy s kindem (* -> *) -> *, narozdíl od Haskellu.

Proč si myslím, že mám pravdu, se pokusím ilustrovat. K tvé poznámce o Javě: Problém je, že Java je na tohle špatný příklad. Její typový systém má různá jiná omezení, a to, že nejde definovat typ s kindem (*→*)→* není jenom kvůli tomu, že nepodporuje HK. Krásně je to vidět v Rustu, ten taky nemá HK, ale přesto se dá deklarovat např:

struct Kráva<T, I: FromIterator<T>> { ... }

Jako demonstrace toho, na co dojede jazyk bez HK, a potažmo kde vlastně začínají HK, si vezměme starou známou monádu. V Haskellu se operátor bind (>>=) deklaruje následovně:

(>>=):: Monad m => m a → (a → m b) → m b

Typové proměnné a a b jsou volné, implicitně je to forall a,b. Parametr je tady pouze m s kindem *→*. To je přesně ten klíčový moment, který jazyk bez HK nedovolí. Když se totiž budu snažit o totéž v Rustu, compiler mi nevezme nic jako

fn bind<A, B, M<A>: Monad>(a: M<A>, f: FnOnce(A)→M<B>)→M<B>

právě proto, že M tady má kind *→*. Jediná možnost bude něco na následující způsob:

trait Monad<A> {
        fn bind<B, R: Monad<B>>(self, f: FnOnce(A)→R)→R;
}

kde se Self (neboli ekvivalent M<A>) předem zredukuje na kind * instanciací pro dané A. Totéž platí pro R, resp. M<B>.

V praxi to znamená, že v Haskellu se definuje >>= obecně např. pro monádu IO (*→*) a pak se může rovnou napsat

getLine >>= putStrLn

V Rustu to ale nebude možné. Compiler stejně tak nevezme žádné

impl<A> IO<A> for Monad<A> { ... }

protože typové parametry metody bind zůstávají neinstanciované. Aby to fungovalo, musím nejdřív explicitně deklarovat:

impl IO<()> Monad<()> { … }
impl IO<String> Monad<String> { … }

a pak teprve můžu provést getLine.bind(putStrLn). Neboli musím ručně implementovat Monad<A> (*) pro každý možný typ A, což evidentně není možné, a právě proto v takovám jazyku bez HK nejde zkonstruovat obecnou monádu. Respektive jde, pokud například v Rustu tyhle explicitní deklarace automatizuju makrem, což je přesně to samé, jako když použiju template template v C++. Obojí je ohejbák, jak si vynahradit to, že jazyk neumí typové parametry s kindem *→*.
Název: Re:Vyšší typy
Přispěvatel: klokan 04. 04. 2018, 08:12:06
Typy vyššího řádu se v ustálené terminologii nazývají Higer RANK. [...] Rozdíl mezi vyšším druhem (HK) a vyšším řádem (HR) je zásadní.
Pominu urážky a jen poznamenám, že "řád" je v angličtině v matematickém kontextu "order". Když ani nevíš, co se jak překládá, tak už se nedivím, že píšeš věci bez hlavy a paty. Přečti si tu referenci, co jsem dal, i když evidentně máš problém porozumět (přinejmenším) anglickému textu, tak to asi k ničemu nebude.

To, že order je řád, tady nikdo nezpochybňuje. Řád není totéž co kind (druh), a právě proto tam používají termín order a ne kind. To je, řekl bych, jasné.
Název: Re:Vyšší typy
Přispěvatel: klokan 04. 04. 2018, 08:21:54
...
P.S. Ty tvoje odkazy výslovně uvádí přesně to, to tady píšu furt dokola: *→* není HK. Tímto jsi ze sebe udělal totálního debila. Přečti si ty texty nejdřív sám, pak se můžeš pokorně připlazit zpátky a omluvit se.

Tak třeba hned v tom prvním odkazu výslovně stojí mimo jiné:

"when::∀(m::∗ → ∗).Monad m⇒Bool→m()→m()
The kind ascription ∗ → ∗ makes explicit the fact that m is a higher-kinded type variable"

Jasnější to snad být ani nemůže.

A dále:

"Similarly, we can change a program with higher-kinded type expressions into a program where all type expressions are of kind ∗, the kind of types." (všimni si, prosím: eliminovat HK znamená všechno převést na *).

Zbytek a ty ostatní odkazy si už můžeš projít sám. Když budeš mít čas, můžeš ukázat, kdeže tyto samé články údajně tvrdí pravý opak.
Název: Re:Vyšší typy
Přispěvatel: klokan 04. 04. 2018, 10:21:19
PS:
Leibnizova filosofie
Monády
Základní pojem jeho filosofie je monáda. Navazuje na Reného Descarta, který soudil, že všechny přírodní jevy lze vyložit pojmy rozlehlosti a pohybu a že základem světa jsou dvě substance – materiální a duchovní. Naproti tomu tvrdí, že je pohyb něco čistě relativního, závisí pouze na stanovisku pozorovatele, které těleso se jeví v pohybu a které ne. Descartovo pojetí substancí kritizuje ještě v druhém ohledu, z hlediska kontinuity a dělitelnosti.

HUH?

Lapidárně řečeno, v informatice a typové teorii je monáda abstrakce toho, jak se výsledek určitého výpočtu dále použije ve výpočtu dalším. Typicky v jazyku Haskell má kupříkladu "getLine" (přečíst řetězec ze stdin) typ IO String (ve známější syntaxi C++ by to bylo IO<String>). Nemá žádný parametr, dokonce ani prázdný seznam parametrů () a to znamená, že na rozdíl od snad všech běžných jazyků, getLine v Haskellu vlastně není funkce ale... KONSTANTA, jejíž "hodnota" představuje jeden určitý způsob, jak získat String v rámci monády IO.

Když budu chtít echovat řetězec, v "normálním" jazyce to bude vypadat jako:

String s = getLine ();
putStrLn(s);

V Haskellu to ovšem bude, pomocí monád:

getLine >>= putStrLn

kde >>= (čte se bind) znamená získat hodnotu tak, jak to představuje "konstanta" getLine, a předat ji jako parametr funkci putStrLn.

Důležité je to, že bind není syntaxe, ale operátor (tj. funkce), z čehož plynou dvě věci:

1. Původní imperativní kód se úplně nahradil funkcemi a dá se tak vyjádřit ve striktně funkcionálním jazyku jako Haskell, kde jinak neexistuje žádný globální stav, mutabilní proměnné, dokonce ani sekvencování operací.

2. Jakožto funkce se bind dá předefinovat. Zdaleka nejznámější využití monád v Haskellu je IO, ale jsou i jiné, jako je jednoduchá kontrola chyb (monáda Maybe), globální stav (monády ST a State), backtracking (seznamy jsou monáda) a další, nemluvě o externích knihovnách jako Parsec (parserové kombinátory), transparentní průběžné logování, paralelismus apod. To vše v jazyku, který neumí nic jiného, než volat čiré funkce bez žádného mutačního stavu.

A protože monády jsou typy, je teoreticky možné dokonce psát polymorfní kód, který se dá zavolat pro různé monády a podle toho poběží různě a bude dělat různé věci.
Název: Re:Vyšší typy
Přispěvatel: Mirek Prýmek 04. 04. 2018, 10:23:02
Sorry, klokane, Rust neznám natolik, abych mohl to tvoje sdělení dešifrovat :)

To, že order je řád, tady nikdo nezpochybňuje. Řád není totéž co kind (druh), a právě proto tam používají termín order a ne kind. To je, řekl bych, jasné.
Já bych do toho češtinu vůbec nepletl, zbytečně to s ní komplikuješ. Jinak "order" opravdu není "kind". Je to obecný termín používaný v různých kontextech: higher order functions, higher order kinds, higher order logic. Ve všech těhle kontextech má ale analogický význam.

všimni si, prosím: eliminovat HK znamená všechno převést na *
Přesně tak, ale imho ne z toho důvodu, který si myslíš.

Úplně stejně je to s funkcemi - pokud máš HO functions, můžeš napsat
Kód: [Vybrat]
>>> def f(x):
...   return x+1
...
>>> def g(x):
...   return x(2)
...
>>> g(f)
3
- všimni si, že předáváš "samotné f", neaplikuješ ho na žádné parametry. f má typ number -> number a proto g má typ (number -> number) -> number. f je prvního řádu, g je druhého/vyššího řádu.

Pokud bys HO functions v jazyce neměl, udělat to nemůžeš. Jediné, co můžeš, je:
Kód: [Vybrat]
>>> def f(x):
...   return x+1
...
>>> def g(x):
...   return x+2
...
>>> g(f(1))
4
f i g jsou prvního řádu a obě mají typ number -> number. Jazyk typ (number -> number) -> number nepodporuje.

Tj. pokud jazyk nepodporuje higher order functions, nemůžeš do funkce předat "samotnou funkci", tj. funkci, která není aplikovaná na všechny parametry, které přijímá. Prvně musíš "díry pro parametry zalepit", tím z funkce uděláš hodnotu. Tj. z number -> number se aplikací na hodnotu typu number stane z celé té věci jenom number, což je hodnota. Předáváš tedy hodnotu, ne funkci.

...a úplně stejně pokud jazyk nepodporuje higher-kinded types, nemůžeš v jazyce použít "typový konstruktor" (funkci přijímající typ a vracející typ) per se - s "nezalepenými dírami pro parametry". Prvně musíš typový konstruktor aplikovat na nějaký proper type, tím se z toho celého stane taky proper type a ten už předat můžeš. Proto v Javě nemůžeš nijak operovat se samotným List (bez parametru). Všude mu nějaký parametr musíš dát, abys z něj vytvořil proper type, který už předat můžeš.
Název: Re:Vyšší typy
Přispěvatel: Mirek Prýmek 04. 04. 2018, 10:43:33
Tak třeba hned v tom prvním odkazu výslovně stojí mimo jiné:

"when::∀(m::∗ → ∗).Monad m⇒Bool→m()→m()
The kind ascription ∗ → ∗ makes explicit the fact that m is a higher-kinded type variable"

Jasnější to snad být ani nemůže.
Zjevně by být mohlo, protože to interpretuješ špatně.

Ono to taky pokračuje dál:
Citace
: it abstracts type constructors such as Maybe and [ ]
- tj. předáváš parametr kindu * -> *, což můžeš udělat jenom v jazyce, který má "higher order kinds" (="higher-kinded types") - naprosto analogicky jako můžeš funkci (typ T -> U) předávat jako parametr jenom v jazyce, který podporuje higher order functions.

Tahle citovaná věta říká, že jako parametr můžeš použít samotný List nebo samotný Array. A to třeba v Javě nejde, protože typy kindu * -> * jako parametr použít nemůžeš. Protože Java HKT nemá.

Prostě nevím, co tam hledáš za složitosti. Je to úplně prostá, doslovná analogie, jenom "o úroveň výš" (nad "jinou doménou): type ~ kind, function ~ type constructor, higher order function ~ higher order type constructor. Stejně jako higher order function je funkce, která přijímá jinou funkci (per se), higher order type constructor je type constructor, který přijímá jiný type constructor (per se, bez "zaplněných děr pro parametry").

Máš to hned na začátku toho článku:
Citace
Higher-kinded polymorphism takes things a step further, abstracting both types and type constructors,
just as higher-order functions abstract both first-order values and functions.
Název: Re:Vyšší typy
Přispěvatel: klokan 09. 04. 2018, 20:43:29
Takže omluvu dlužíš spíš ty mě. Šup šup
Název: Re:Vyšší typy
Přispěvatel: Mirek Prýmek 09. 04. 2018, 20:48:10
Takže omluvu dlužíš spíš ty mě. Šup šup
Jak's na to přišel?! Ještě pořád to není jasný?
Název: Re:Vyšší typy
Přispěvatel: fdrwqerwqer 09. 04. 2018, 20:57:18
v tehle diskuzi hrajou nejvetsi roli GONADY
Název: Re:Vyšší typy
Přispěvatel: klokan 09. 04. 2018, 21:56:58
Takže omluvu dlužíš spíš ty mě. Šup šup
Jak's na to přišel?! Ještě pořád to není jasný?

Vám dvěma asi ne. Ještě jednou a pečlivěji si přečtěte, co jsem psal, viz
V Haskellu se operátor bind (>>=) deklaruje následovně:

(>>=):: Monad m => m a → (a → m b) → m b
Název: Re:Vyšší typy
Přispěvatel: GrammarKatzi 09. 04. 2018, 21:58:07
Takže omluvu dlužíš spíš ty mě. Šup šup
Jak's na to přišel?! Ještě pořád to není jasný?
Přátelské upozornění: ”na rozdíl” se vždy píše zvlášť a v “jaks” se nepíše apostrof.
Název: Re:Vyšší typy
Přispěvatel: zboj 09. 04. 2018, 22:02:18
Takže omluvu dlužíš spíš ty mě. Šup šup
Jak's na to přišel?! Ještě pořád to není jasný?

Vám dvěma asi ne. Ještě jednou a pečlivěji si přečtěte, co jsem psal, viz
V Haskellu se operátor bind (>>=) deklaruje následovně:

(>>=):: Monad m => m a → (a → m b) → m b
M. Prýmek má v tomto případě pravdu.
Název: Re:Vyšší typy
Přispěvatel: BoneFlute 09. 04. 2018, 22:42:10
Kód: [Vybrat]
>>> def f(x):
...   return x+1
...
>>> def g(x):
...   return x(2)
...
>>> g(f)
3

Tohle znám pod pojmem first-class citizen. Jako "funkce je first-class citizen". Je to to samé (podobný pohled na věc), nebo jen podobné, a first-class je ještě koncept obsahující další zajímavosti? Nebo je to jen o tom, že u typů řeším typ - tedy určitým způsobem validnost, zatímco u first-class řeším "zda to v tom jazyce jde" a můžu tou funkcí pracovat jako s hodnotou (ale furt tam vidím určitou podobnost)?

Zaujalo mě to i díky tomu, že můžu mět jako first-class i typ.
Název: Re:Vyšší typy
Přispěvatel: Šáša 09. 04. 2018, 23:04:14
Takže omluvu dlužíš spíš ty mě. Šup šup
Jak's na to přišel?! Ještě pořád to není jasný?

Vám dvěma asi ne. Ještě jednou a pečlivěji si přečtěte, co jsem psal, viz
V Haskellu se operátor bind (>>=) deklaruje následovně:

(>>=):: Monad m => m a → (a → m b) → m b
Máš v tom solidní zmatek a tvé příklady podporují tvrzení, proti kterým bojuješ. V tvém bindu je m druhu *->*, takže signatura prostě je HKT a v Javě to neuděláš. Plácáš se v tom, něco sis o tom evidentně přečetl, ale nepochopils to a teď se jen zbytečně hádáš, aniž bys tušil, o co vlastně jde.
Název: Re:Vyšší typy
Přispěvatel: frufru 11. 04. 2018, 14:19:32
Jste jak malý, hádáte se tu kvůli nějaké blbosti, která nikomu ve výsledku stejně nepomůže.
Název: Re:Vyšší typy
Přispěvatel: Idris 10. 06. 2019, 10:07:22
Ha, tak už je má od verze 5.1 i Swift, ale v té nejdivnější podobě, typ se uvede jako “some AProtocol”, překladač zná konkrétní typ, akorát uživatel třídy/funkce je udržován v nevědomosti. Tohle žádný jiný jazyk nemá a fakt to je hlavolam.