Was ist der Unterschied zwischen einem Typ und einer Art?

Ich lerne die Programmiersprache Haskell und versuche, mich mit dem Unterschied zwischen a typeund a auseinanderzusetzen kind.

Wie ich es verstehe, a kind is a type of type. Zum Beispiel a ford is a type of carund a car is a kind of vehicle.

Ist dies eine gute Möglichkeit, darüber nachzudenken?

Denn so wie mein Gehirn gerade verdrahtet ist, a ford is a **type** of car, aber auch eine car is a **type** of vehicleWeile gleichzeitig a car is a **kind** of vehicle. Dh die Begriffe typeund kindsind austauschbar.

Könnte jemand etwas Licht ins Dunkel bringen?

Hier haben "Werte", "Typen" und "Arten" formale Bedeutungen. Wenn Sie also die gebräuchliche englische Sprache oder Analogien zur Klassifizierung von Automobilen berücksichtigen, werden Sie nur so weit kommen.

Meine Antwort bezieht sich auf die formale Bedeutung dieser Begriffe im Zusammenhang mit Haskell; Diese Bedeutungen basieren auf den Bedeutungen, die in der mathematischen / CS "Typentheorie" verwendet werden (obwohl sie nicht wirklich identisch sind). Das wird also keine sehr gute "Computerwissenschaft" -Antwort sein, aber es sollte eine ziemlich gute Haskell-Antwort sein.

In Haskell (und anderen Sprachen), endet es auf ein Wesen hilfreich zuweisen Typen zu einem Programmausdruck, der die Klasse von beschreiben Werten der Ausdruck erlaubt ist zu haben. Ich gehe davon aus, dass Sie genug Beispiele gesehen haben, um zu verstehen, warum es nützlich wäre, das im Ausdruck zu wissensqrt (a**2 + b**2) , die Variablen aund bwerden immer Werte vom Typ sein Doubleund nicht, sagen, Stringund Booljeweils. Grundsätzlich hilft uns das Haben von Typen beim Schreiben von Ausdrücken / Programmen, die über einen weiten Bereich von Werten korrekt funktionieren .

Vielleicht haben Sie nicht bemerkt, dass Haskell-Typen wie die in Typensignaturen vorkommenden:

fmap :: Functor f => (a -> b) -> f a -> f b

sind eigentlich selbst in einer Typ-Level-Haskell-Subsprache geschrieben. Der Programmtext Functor f => (a -> b) -> f a -> f bist - im wahrsten Sinne des Wortes - ein typischer Ausdruck in diesem Subsprache geschrieben. Die Untersprache enthält Operatoren (beispielsweise ->ist eine rechte assoziative Infixoperator in dieser Sprache), Variablen ( zum Beispiel f, a, und b), und „Anwendung“ eines Typ Ausdruck zu einem anderen ( zum Beispiel f awird fangewandt a).

Habe ich erwähnt, wie hilfreich es in vielen Sprachen ist, Programmausdrücken Typen zuzuweisen, um Klassen von Ausdruckswerten zu beschreiben? Nun, in dieser Subsprache auf Typebene werden Ausdrücke als Typen (und nicht als Werte ) ausgewertet, und es ist letztendlich hilfreich, sie zuzuweisen Arten , um die Klassen von Typen zu beschreiben, die sie darstellen dürfen. Grundsätzlich hilft uns das Haben von Arten beim Schreiben von Typausdrücken, die über einen weiten Bereich von Typen korrekt funktionieren .

So Werte sind Typen als Typen zu sind Arten und Typen helfen uns schreiben Wert -Niveau Programme während Arten helfen uns schreiben Art -Niveau Programme.

Wie sehen diese Arten aus? Nun, betrachten Sie die Typensignatur:

id :: a -> a

Wenn der Typausdruck a -> agültig sein soll, welche Arten von Typen sollten wir die Variablen zulassen a? Nun, die Typausdrücke:

Int -> Int
Bool -> Bool

siehst gültig aus, also die typen Int und Boolsind offensichtlich von der richtigen art . Aber auch kompliziertere Typen wie:

[Double] -> [Double]
Maybe [(Double,Int)] -> Maybe [(Double,Int)]

siehst gültig aus. In der Tat, da wir in der Lage sein sollten, idFunktionen aufzurufen , sogar:

(a -> a) -> (a -> a)

sieht gut aus. Also Int, Bool, [Double], Maybe [(Double,Int)], und a -> aalle sehen aus wie Typen der richtigen Art .

Mit anderen Worten, es scheint nur eine Art zu geben. Nennen wir es *wie einen Unix-Platzhalter und jeden Typ hat die gleiche Art * , Ende der Geschichte.

Recht?

Nicht ganz. Es stellt sich heraus, dass Maybeein Typ-Ausdruck für sich genommen genauso gültig ist wie Maybe Int(in etwa der gleiche Weg sqrt, für sich genommen, ist ein Wert-Ausdruck genauso gültig wie sqrt 25). jedoch folgende Typausdruck ist jedoch ungültig:

Maybe -> Maybe

Denn während Maybeein Ausdruck des Typs ist, ist es nicht die repräsentiert Art von Typ , die Werte aufweisen können. Also, das ist , wie wir definieren sollte *- es ist die Art von Typen , die Werte aufweisen; es enthält "vollständige" Typen wie DoubleoderMaybe [(Double,Int)] schließt jedoch unvollständige, wertlose Typen wie aus Either String. Der Einfachheit halber werde ich diese vollständigen Arten von Arten *"konkrete Arten" nennen, obwohl diese Terminologie nicht universell ist, und "konkrete Arten" können etwas ganz anderes bedeuten als beispielsweise ein C ++ - Programmierer.

Nun, in der Art Ausdruck a -> a, solange Art ahat Art * (die Art von Beton - Typen), das Ergebnis der Art Ausdrucks a -> awird auch haben Art * (dh die Art von Beton - Typen).

Also, welche Art von Typ ist Maybe? Nun, Maybekann auf einen Betontyp angewendet werden, um einen anderen Betontyp zu ergeben. Also, Maybesieht aus wie ein wenig wie eine Typ-Level - Funktion , die eine nimmt Art von Art * und gibt eine Art von Art * . Wenn wir einen Wert Level - Funktion haben , die einen nahm Wert von Typ Int und einen zurück Wert von Typ Int , würden wir ihm eine geben Art Unterschrift Int -> Int, so analog sollten wir geben Maybeeine Art Unterschrift * -> *. GHCi stimmt zu:

> :kind Maybe
Maybe :: * -> *

Zurück gehen zu:

fmap :: Functor f => (a -> b) -> f a -> f b

In dieser Typensignatur hat Variable fArt * -> *und Variablen aund bArt *; Der eingebaute Operator ->hat Art * -> * -> *(er nimmt eine Art *auf der linken und eine auf der rechten Seite und gibt auch eine Art zurück *). Daraus und aus den Rückschlüssen auf die Art können Sie ableiten, dass a -> bes sich um einen gültigen Typ mit Art *handelt f aund dass f bes sich auch um gültige Typen mit Art *handelt und dass es sich um einen gültigen Typ (a -> b) -> f a -> f bhandelt *.

Mit anderen Worten, der Compiler kann den Typausdruck " (a -> b) -> f a -> f büberprüfen" sqrt (a**2 + b**2), um zu überprüfen, ob er für Typvariablen des richtigen Typs gültig ist, ebenso wie er "überprüft" , ob er für Variablen des richtigen Typs gültig ist.

Der Grund für die Verwendung separater Ausdrücke für "Typen" gegenüber "Arten" (dh nicht über die "Typen von Typen" zu sprechen) ist meist nur, um Verwirrung zu vermeiden. Die Arten oben Blick sehr verschieden von Typen und, zumindest auf dem ersten, scheinen ganz anders zu verhalten. (Zum Beispiel dauert es einige Zeit , den Kopf wickeln sich um die Idee , dass jeder „normalen“ hat die gleiche Art *und die Art a -> bist *nicht * -> *.)

Einiges davon ist auch historisch. Mit der Entwicklung von GHC Haskell verschwimmen die Unterschiede zwischen Werten, Typen und Arten. In diesen Tagen können Werte in Typen "befördert" werden, und Typen und Arten sind wirklich dasselbe. Daher haben in modernen Haskell-Werten sowohl Typen als auch ARE- Typen (fast), und die Typenarten sind nur mehr Typen.

@ user21820 fragte nach einer zusätzlichen Erklärung für "Typen und Arten sind wirklich dasselbe". Um es ein bisschen klarer zu machen: In modernen GHC Haskell (seit Version 8.0.1, glaube ich) werden Typen und Arten im Compiler-Code weitgehend einheitlich behandelt . Der Compiler unternimmt einige Anstrengungen bei Fehlermeldungen, um zwischen "Typen" und "Arten" zu unterscheiden, je nachdem, ob er sich über den Typ eines Werts oder den Typ eines Typs beschwert.

Auch wenn keine Erweiterungen aktiviert sind, sind sie leicht zu unterscheiden in der Oberflächensprache. Zum Beispiel haben Typen (von Werten) eine Darstellung in der Syntax (z. B. in Typensignaturen), aber Arten (von Typen) sind - glaube ich - völlig implizit und es gibt keine explizite Syntax, in der sie erscheinen.

Wenn Sie jedoch die entsprechenden Erweiterungen aktivieren, verschwindet die Unterscheidung zwischen Typen und Arten weitgehend. Beispielsweise:

{-# LANGUAGE GADTs, TypeInType #-}
data Foo where
  Bar :: Bool -> * -> Foo

Hier Barist (sowohl ein Wert als auch) ein Typ. Als Typ ist seine Art Bool -> * -> Fooeine Funktion auf Typebene, die einen Typ Bool(der ein Typ, aber auch eine Art ist) und einen Typ einer Art annimmt und einen Typ einer Art *erzeugt Foo. So:

type MyBar = Bar True Int

korrekt überprüft.

Wie @AndrejBauer in seiner Antwort erklärt, ist diese Unterscheidung zwischen Typen und Arten unsicher - ein Typ / eine Art, *deren Typ / Art selbst ist (was im modernen Haskell der Fall ist), führt zu Paradoxen. Das Typensystem von Haskell ist jedoch aufgrund der Nichtbeendigung bereits voller Paradoxien, weshalb es nicht als große Sache angesehen wird.

• Bool ist ein Typ
• Type ist eine Art, weil ihre Elemente Typen sind
• Bool -> Int ist ein Typ
• Bool -> Type ist eine Art, weil ihre Elemente Funktionen sind, die Typen zurückgeben
• Bool * Int ist ein Typ
• Bool * Type ist eine Art, weil ihre Elemente Paare mit einer Komponente eines Typs sind

$U_0$$U_1$$U_2$$U_0$$\mathtt{Bool}$$\mathtt{Nat}$$\mathtt{Nat} \to \mathtt{Nat}$$U_1$$U_0$$\mathtt{Bool} \to U_0$$U_0 \to U_0$$U_{n+1}$$U_n$$U_n$$\times$$\to$

$U_0$$U_1$$U_0$$U_1$$U_0$* . Somit *handelt es sich um ein Element U_1, das Haskell nicht explizit benennt.

EIN Wert ist wie der spezifische rote 2011 Ford Mustang mit 19.206 Meilen darauf, den Sie in Ihrer Fahrstraße sitzen haben.

Informell könnte dieser spezifische Wert viele haben Arten haben : Es ist ein Mustang und es ist ein Ford und es ist ein Auto und es ist ein Fahrzeug, neben vielen anderen Arten, die man erfinden könnte (die Art von "Dingen") Ihnen gehören ", oder die Art der" Dinge, die rot sind ", oder ...).

(In Haskell haben Werte in erster Näherung (GADTs unterbrechen diese Eigenschaft, und die Magie um Zahlenliterale und die OverloadedStrings-Erweiterung verdecken sie ein wenig) einen Haupttyp anstelle der Fülle informeller "Typen", die Sie angeben können. ' stach. 42 ist im Sinne dieser Erklärung ein Int; es gibt in Haskell keinen Typ für "Zahlen" oder "sogar ganze Zahlen" - oder Sie könnten einen machen, aber es wäre ein disjunkter Typ vonInt .)

Jetzt kann "Mustang" ein Untertyp von "Auto" sein - jeder Wert, der ein Mustang ist, ist auch ein Auto. Aber der Typ - oder, um Haskells Terminologie zu verwenden, ist die Art von "Mustang" nicht "Auto". "Mustang" der Typ ist keine Sache, die Sie in Ihrer Einfahrt parken oder in der Sie herumfahren können. "Mustang" ist ein Substantiv oder eine Kategorie oder nur ein Typ. Das sind informell die Arten von "Mustang".

(Wiederum erkennt Haskell nur eine Art für jede Sache auf Typebene. Also Inthat Art *und keine anderen Arten. MaybeHat Art * -> *und keine anderen Arten. Aber die Intuition sollte immer noch halten: 42ist eine Int, und Sie können IntDinge damit tun . wie Addieren und Subtrahieren Intselbst ist nicht Int, es als eine solche Zahl ist Int + IntSie können formlos Leute sagen hören , dass. Inteine ist Num, durch die sie bedeuten , dass ein dort ist beispielsweise der NumTyp - Klasse für den Typ Int-Das ist nicht das gleiche als zu sagen, dass Inthat Art Num . Inthat Art "Typ", die in Haskell geschrieben ist *.)

Ist also nicht jeder informelle "Typ" nur ein Substantiv oder eine Kategorie? Haben alle Typen die gleiche Art? Warum überhaupt über Arten reden, wenn sie so langweilig sind?

Dies ist der Punkt, an dem die englische Analogie ein wenig steiniger wird, aber bedenken Sie: Stellen Sie sich vor, dass das Wort "Eigentümer" auf Englisch für sich genommen keinen Sinn ergibt, ohne dass eine Beschreibung des Eigentums vorliegt. Stellen Sie sich vor, dass jemand, der Sie "Eigentümer" nennt, für Sie überhaupt keinen Sinn ergibt. Aber wenn dich jemand einen "Autobesitzer" nennt, kannst du verstehen, was er meint.

"Besitzer" hat nicht die gleiche Art wie "Auto", weil man in dieser erfundenen Version des Englischen nicht über ein Auto sprechen kann, aber über einen Besitzer. Man kann nur von einem "Autobesitzer" sprechen. "Eigentümer" erstellt nur dann ein "Nomen", wenn es auf etwas angewendet wird, das bereits ein "Nomen" hat, wie "Auto". Wir würden sagen, dass die Art von "Eigentümer" "Nomen -> Nomen" ist. "Owner" ist wie eine Funktion, die ein Nomen annimmt und daraus ein anderes Nomen erzeugt; Aber es ist kein Substantiv.

Beachten Sie, dass "Autobesitzer" kein Untertyp von "Auto" ist! Es ist keine Funktion, die Autos akzeptiert oder zurückgibt! Es ist nur eine völlig andere Art von "Auto". Es beschreibt Werte mit zwei Armen und zwei Beinen, die zu einem bestimmten Zeitpunkt einen bestimmten Geldbetrag hatten und dieses Geld zu einem Händler brachten. Es werden keine Werte beschrieben, die über vier Räder und eine Lackierung verfügen. Beachten Sie auch, dass "Autobesitzer" und "Hundebesitzer" unterschiedliche Typen sind und Dinge, die Sie mit einem machen möchten, möglicherweise nicht auf den anderen zutreffen.

(Ebenso, wenn wir in Haskell sagen, dass das Maybeeine Art hat * -> *, ist es unsinnig (formal; informell tun wir es die ganze Zeit), über "ein Maybe" zu sprechen . Stattdessen können wir ein Maybe Intoder ein haben Maybe String, da dies Dinge von sind Art *.)

Es geht also darum, überhaupt über Arten zu sprechen, damit wir unsere Argumentation in Bezug auf Wörter wie "Eigentümer" formalisieren und durchsetzen können, dass wir immer nur Werte von Typen verwenden, die "vollständig konstruiert" und nicht unsinnig sind.

So wie ich es verstehe, ist eine Art eine Art von Typ.

Das ist richtig - also lasst uns untersuchen, was das bedeutet. Intoder Textsind konkrete Typen, aber Maybe aein abstrakter Typ. Es wird erst dann zu einem konkreten Typ, wenn Sie entscheiden, welchen bestimmten Wert Sie afür eine bestimmte Variable (oder Wert / Ausdruck / was auch immer) möchten, z Maybe Text.

Wir sagen, das Maybe aist ein Typkonstruktor, weil es wie eine Funktion ist, die einen einzelnen konkreten Typ annimmt (z. B. Text) und einen konkreten Typ zurückgibt ( Maybe Textin diesem Fall). Andere Typkonstruktoren benötigen jedoch möglicherweise noch mehr "Eingabe-Parameter", bevor sie einen konkreten Typ zurückgeben. ZB Map k vmüssen zwei konkrete Typen (z. B. Intund Text) verwendet werden, bevor ein konkreter Typ ( Map Int Text) erstellt werden kann.

Die Konstruktoren Maybe aund List atype haben also dieselbe "Signatur", die wir bezeichnen * -> *(ähnlich wie die Haskell-Funktionssignatur), da sie, wenn Sie ihnen einen konkreten Typ geben, einen konkreten Typ ausspucken. Wir nennen dies die "Art" des Typs Maybeund Listhaben die gleiche Art.

Die konkreten Typen haben eine Art *, und unser Kartenbeispiel ist eine Art, * -> * -> *da zwei konkrete Typen als Eingabe verwendet werden, bevor ein konkreter Typ ausgegeben werden kann.

Sie können sehen , es ist meist nur über die Anzahl der „Parameter“ , dass wir in die Art Konstruktor übergeben - aber erkennen , dass wir auch innerhalb Typkonstruktoren verschachtelt Typkonstruktoren erhalten können, so dass wir mit einer Art können am Ende , dass sieht aus wie * -> (* -> *) -> *zum Beispiel .

Wenn Sie ein Scala / Java-Entwickler sind, finden Sie diese Erklärung möglicherweise auch hilfreich: https://www.atlassian.com/blog/archives/scala-types-of-a-higher-kind