Druh (teorie typů) - Kind (type theory)

tento článek může být pro většinu čtenářů příliš technická na to, aby je pochopili. Prosím pomozte to vylepšit na aby to bylo srozumitelné pro neodborníky, aniž by byly odstraněny technické podrobnosti. (Červen 2020) (Zjistěte, jak a kdy odstranit tuto zprávu šablony)

V oblasti matematická logika a počítačová věda známý jako teorie typů, a druh je typ a konstruktor typu nebo méně často typ a operátor typu vyššího řádu. Laskavý systém je v zásadě a jednoduše zadaný lambda kalkul „o úroveň výš“, označený primitivním typem, označený ${ displaystyle *}$ a nazývá se „typ“, což je jakýkoli druh datový typ který žádné nepotřebuje parametry typu.

Druh je někdy matoucí popisován jako „typ a (datový typ ", ale ve skutečnosti jde spíše o arity specifikátor. Syntakticky je přirozené považovat polymorfní typy za konstruktory typů, tedy nepolymorfní typy za nullary konstruktory typu. Ale všechny nullary konstruktory, tedy všechny monomorfní typy, mají stejný, nejjednodušší druh; a to ${ displaystyle *}$.

Vzhledem k tomu, že operátoři typu vyššího řádu jsou neobvyklí programovací jazyky Ve většině programovacích postupů se druhy používají k rozlišení mezi datovými typy a typy konstruktorů, které se používají k implementaci parametrický polymorfismus. Druhy se objevují, ať už explicitně, nebo implicitně, v jazycích, jejichž typové systémy zohledňují parametrický polymorfismus programově přístupným způsobem, například C ++,^[1] Haskell a Scala.^[2]

Příklady

• ${ displaystyle *}$, vyslovuje se „typ“, je druh všeho typy dat viděn jako nullary konstruktory typů a v tomto kontextu se také nazývají správné typy. To obvykle zahrnuje typy funkcí v funkční programovací jazyky.
• ${ displaystyle * rightarrow *}$ je druh a unární konstruktor typu, např. a typ seznamu konstruktor.
• ${ displaystyle * rightarrow * rightarrow *}$ je druh a binární konstruktor typu (přes kari ), např. a typ páru konstruktor, a také to a typ funkce konstruktor (nezaměňovat s výsledkem jeho aplikace, která je sama o sobě typem funkce, tedy druhu ${ displaystyle *}$)
• ${ displaystyle (* rightarrow *) rightarrow *}$ je druh operátoru typu vyššího řádu od konstruktérů unárního typu po správné typy.^[3]

Druhy v Haskellu

(Poznámka: Dokumentace Haskell používá stejnou šipku pro typy i druhy funkcí.)

Laskavý systém Haskell 98^[4] zahrnuje přesně dva druhy:

• ${ displaystyle *}$, vyslovovaný „typ“ je druh všeho typy dat.
• ${ displaystyle k_ {1} rightarrow k_ {2}}$ je druh a unární konstruktor typu, který má určitý druh druhu ${ displaystyle k_ {1}}$ a vytváří druh druhu ${ displaystyle k_ {2}}$.

Obydlený typ (jak se správné typy v Haskellu nazývají) je typ, který má hodnoty. Například ignorování tříd typu které komplikují obraz, 4 je hodnota typu Int, zatímco [1, 2, 3] je hodnota typu [Int] (seznam Ints). Proto, Int a [Int] mít laskavý ${ displaystyle *}$, ale stejně tak funguje jakýkoli typ funkce Int -> Bool nebo dokonce Int -> Int -> Bool.

Konstruktor typu přebírá jeden nebo více argumentů typu a produkuje datový typ, když je zadán dostatek argumentů, tj. Podporuje částečná aplikace díky kari.^[5][6] Takto Haskell dosahuje parametrických typů. Například typ [] (list) je konstruktor typu - k určení typu prvků seznamu je potřeba jediný argument. Proto, [Int] (seznam bodů), [Plovák] (seznam plováků) a dokonce [[Int]] (seznam seznamů Ints) jsou platné aplikace [] konstruktor typu. Proto, [] je druh druhu ${ displaystyle * rightarrow *}$. Protože Int má laskavý ${ displaystyle *}$, přihlašování [] má za následek [Int], svého druhu ${ displaystyle *}$. 2-n-tice konstruktor (,) má laskavý ${ displaystyle * rightarrow * rightarrow *}$, konstruktor 3 řazené kolekce členů (,,) má laskavý ${ displaystyle * rightarrow * rightarrow * rightarrow *}$ a tak dále.

Laskavý závěr

Standardní Haskell neumožňuje polymorfní druhy. To je v rozporu s parametrický polymorfismus na typech, které podporuje Haskell. Například v následujícím příkladu:

data Strom z  = List | Vidlička (Strom z) (Strom z)

druh z může být cokoli, včetně ${ displaystyle *}$, ale také ${ displaystyle * rightarrow *}$ atd. Haskell ve výchozím nastavení vždy odvodí druhy, které mají být ${ displaystyle *}$, pokud typ výslovně neurčuje jinak (viz níže). Proto kontrola typu odmítne následující použití Strom:

typ FunnyTree = Strom []     - neplatný

protože ten druh [], ${ displaystyle * rightarrow *}$ neodpovídá očekávanému druhu pro z, což je vždy ${ displaystyle *}$.

Jsou však povoleni operátoři vyššího řádu. Například:

data Aplikace ne z = Z (ne z)

má laskavý ${ displaystyle (* rightarrow *) rightarrow * rightarrow *}$, tj. ne se očekává, že bude unárním datovým konstruktorem, který se použije na jeho argument, kterým musí být typ, a vrátí jiný typ.

GHC má příponu PolyKinds, který společně s Druh podpisů, umožňuje polymorfní druhy. Například:

data Strom (z :: k) = List | Vidlička (Strom z) (Strom z)typ FunnyTree = Strom []     -- OK

Od verze GHC 8.0.1 jsou typy a druhy sloučeny.^[7]

Viz také

• Systém F-omega
• Systém čistého typu

Reference