Vyšší typy

[klokan]

...

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.

[Reklama]

[klokan]

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.

[Mirek Prýmek]

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

[Mirek Prýmek]

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:

: 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:

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.

[klokan]

Takže omluvu dlužíš spíš ty mě. Šup šup

[Reklama]

[Mirek Prýmek]

Takže omluvu dlužíš spíš ty mě. Šup šup

Jak's na to přišel?! Ještě pořád to není jasný?

[fdrwqerwqer]

v tehle diskuzi hrajou nejvetsi roli GONADY

[klokan]

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

[GrammarKatzi]

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.

[zboj]

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.

[BoneFlute]

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.

[Šáša]

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.

[frufru]

Jste jak malý, hádáte se tu kvůli nějaké blbosti, která nikomu ve výsledku stejně nepomůže.

[Idris]

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.