Wie genau funktionieren Listen?

Question

Ich habe vor kurzem auf vinyl lesen, die seltsame "Liste der Arten" ein bisschen Typen verwendet. Nach der Lektüre ein wenig auf Arten und Vinyl, ich habe so etwas wie ein intuitives Verständnis von ihnen bekommen, und ich habe diese zusammen

{-# LANGUAGE DataKinds, 
      TypeOperators, 
      FlexibleInstances, 
      FlexibleContexts, 
      KindSignatures, 
      GADTs #-} 
module Main where 

-- from the data kinds page, with HCons replaced with :+: 
data HList :: [*] -> * where 
    HNil :: HList '[] 
    (:+:) :: a -> HList t -> HList (a ': t) 

infixr 8 :+: 


instance Show (HList '[]) where 
    show _ = "[]" 
instance (Show a, Show (HList t)) => Show (HList (a ': t)) where 
    show (x :+: xs) = show x ++ " : " ++ show xs 

class ISum a where 
    isum :: Integral t => a -> t 

instance ISum (HList '[]) where 
    isum _ = 0 


instance (Integral a, ISum (HList t)) => ISum (HList (a ': t)) where 
    isum (x :+: xs) = fromIntegral x + isum xs 

-- explicit type signatures just to check if I got them right 
alist :: HList '[Integer] 
alist = (3::Integer) :+: HNil 

blist :: HList '[Integer,Int] 
blist = (3::Integer) :+: (3::Int) :+: HNil 

main :: IO() 
main = do 
    print alist 
    print (isum alist :: Int) 
    print blist 
    print (isum blist :: Integer) 

:i HList ergeben

data HList $a where 
    HNil :: HList ('[] *) 
    (:+:) :: a -> (HList t) -> HList ((':) * a t) 
    -- Defined at /tmp/test.hs:10:6 
instance Show (HList ('[] *)) -- Defined at /tmp/test.hs:17:10 
instance (Show a, Show (HList t)) => Show (HList ((':) * a t)) 
    -- Defined at /tmp/test.hs:19:10 
instance ISum (HList ('[] *)) -- Defined at /tmp/test.hs:25:10 
instance (Integral a, ISum (HList t)) => ISum (HList ((':) * a t)) 
    -- Defined at /tmp/test.hs:29:10 
*Main> :i HList 
data HList $a where 
    HNil :: HList ('[] *) 
    (:+:) :: a -> (HList t) -> HList ((':) * a t) 
    -- Defined at /tmp/test.hs:10:6 
instance Show (HList ('[] *)) -- Defined at /tmp/test.hs:17:10 
instance (Show a, Show (HList t)) => Show (HList ((':) * a t)) 
    -- Defined at /tmp/test.hs:19:10 
instance ISum (HList ('[] *)) -- Defined at /tmp/test.hs:25:10 
instance (Integral a, ISum (HList t)) => ISum (HList ((':) * a t)) 
    -- Defined at /tmp/test.hs:29:10 

aus dem ich in der Lage zu hacken Sammeln Sie, dass '[] Zucker für '[] * und x ': y für (':) * x y ist. Was macht das da? Ist es die Art der Listenelemente? Was genau ist eine solche Liste? Ist es etwas in die Sprache eingebaut?

Answer 1

Das * ist ... unglücklich. Es ist das Ergebnis von GHC's Pretty-Drucker für polykinded Datentypen. Es führt zu Dingen, die syntaktisch ungültig sind, aber es vermittelt einige nützliche Informationen.

Wenn GHC pretty einen Typ mit polymorphen Typen druckt, wird die Art jeder polymorphen Typvariablen nach dem Typkonstruktor ausgegeben. In Ordnung. Also, wenn Sie hatte eine Erklärung wie:

data Foo (x :: k) y (z :: k2) = Foo y 

GHC wäre ziemlich Druck die Art der Foo (die Daten Konstruktor) als y -> Foo k k1 x y z. Wenn Sie einige Verwendung hatte, die die Art eines dieser Typ Variablen etwas festgenagelt, wie ..

foo :: a -> Int -> Foo a Int 5 -- Data Kind promoted Nat 

Die Art der foo "hello" 0 würde als Foo * Nat String Int 5 gedruckt werden. Ja, es ist schrecklich. Aber wenn Sie wissen, was vor sich geht, können Sie es zumindest lesen.

Das '[] Zeug ist Teil der DataKinds Erweiterung. Es ermöglicht die Förderung von Typen zu Arten, und die Konstruktoren dieses Typs werden zu Typkonstruktoren. Diese hochgestuften Typen haben keine gültigen Werte, nicht einmal undefined, weil ihre Art nicht mit * kompatibel ist, was die Art aller Typen ist, die Werte mit ihnen haben können. Sie können also nur an Orten erscheinen, an denen es keinen Typ gibt. Weitere Informationen finden Sie http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-polymorphism-and-promotion.html

Edit:

Ihr Kommentar bringt einige Punkte über die Art und Weise GHCI Werke auf.

-- foo.hs 
{-# LANGUAGE DataKinds, PolyKinds #-} 

data Foo (x :: k) y (z :: k1) = Foo y 

Wenn Sie eine Datei in GHCI laden, es wird nicht aktiviert, um die Erweiterungen interaktiv die in der Datei verwendet wurden.

GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help 
Loading package ghc-prim ... linking ... done. 
Loading package integer-gmp ... linking ... done. 
Loading package base ... linking ... done. 
Prelude> :l foo 
[1 of 1] Compiling Main    (foo.hs, interpreted) 
Ok, modules loaded: Main. 
*Main> :t Foo 
Foo :: y -> Foo * * x y z 
*Main> :set -XPolyKinds 
*Main> :t Foo 
Foo :: y -> Foo k k1 x y z 

Also ja. Die Erweiterung PolyKinds muss in ghci aktiviert sein, damit standardmäßig polymorphe Typen im Typ verwendet werden. Und ich habe versucht, meine foo-Funktion in der Datei zu definieren, aber es hat tatsächlich diese Version von GhC zum Absturz gebracht. Hoppla. Ich denke, das ist jetzt behoben, aber ich denke, die Überprüfung der ghc trac wäre nett. In jedem Fall kann ich es interaktiv definieren und es funktioniert gut.

*Main> :set -XDataKinds 
*Main> let foo :: a -> Int -> Foo a Int 5 ; foo = undefined 
*Main> :t foo "hello" 0 
foo "hello" 0 :: Foo * GHC.TypeLits.Nat [Char] Int 5 
*Main> :m + GHC.TypeLits 
*Main GHC.TypeLits> :t foo "hello" 0 
foo "hello" 0 :: Foo * Nat [Char] Int 5 

Ok, gut, habe ich vergessen, den Import benötigt wurde es Nat unqualifizierte anzuzeigen.Und da ich nur Typendruck demonstrierte, kümmerte ich mich nicht um eine Implementierung, also ist undefined gut genug.

Aber alles funktioniert Arbeit, wie ich sagte, ich verspreche. Ich habe nur einige Details weggelassen, wo welche Erweiterungen benötigt wurden, insbesondere sowohl PolyKinds als auch DataKinds. Ich nahm an, dass du sie verstanden hast, seit du sie in deinem Code benutzt hast. Hier ist die Dokumentation über die PolyKinds Erweiterung: http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/kind-polymorphism.html

Answer 2

Dies ist aufgrund einiger unglücklicher Umsetzung hinsichtlich des Druckens. Arten können als "Arten von Typen" betrachtet werden. Folgendes ist zu beachten:

>:t [] 
[] :: [a] 
>:k '[] 
'[] :: [*] 

Genau wie [a] bedeutet "für alle Arten ein, [a]", [*] bedeutet "für alle Arten *, [*]". Allerdings ist die Menge an Argumenten, die Sie mit Arten machen können, viel kleiner als bei Typen. Zum Beispiel gibt a -> a beide a s sind vom gleichen Typ, aber * -> * bedeutet sowohl * kann jeder Typ sein (es kann als * -> * ist der Typ a -> b "angehoben" auf die Art-Ebene). Aber es gibt keine Möglichkeit, den Typ a -> a auf die Art-Ebene zu heben. Dies bedeutet, dass [a] und [*] nicht ganz analog sind. [*] ist näher an etwas wie [forall a . a]. Genauer gesagt, aber weniger genau, könnte man sagen, dass es keine Möglichkeit gibt, "polymorphe" Arten zu unterscheiden, da es keine "freundlichen Variablen" gibt. (Nebenbemerkung: -XPolyKinds ermöglicht, was die ‚polymorphe Arten‘ Dokumentation Anrufe, aber es gibt immer noch nicht, dass Ihnen echten Polymorphismus)

Also, wenn Sie schreiben HList :: [*] -> * (was wirklich bedeutet HList (k :: [*]) :: *) geben Sie an, dass die Art der ersten Typ Parameter sollten [*] und die ‚Werte‘, die Art von Art [*] nehmen kann, sind '[], * ': '[], * ': * ': '[] usw.

Nun ist das Problem. Beim Drucken von Objekten, deren Art eingeschränkt wurde, wie der erste Typparameter HNil, wird versucht, alle Arten von Informationen einzubeziehen. Aus welchem ​​Grund auch immer, anstatt

HNil :: HList ('[] :: '[*]) 
^ data  ^type ^kind 

des Schreibens, die tatsächlich zeigen würde, dass die * bezieht sich auf die Art von '[], druckt er die Dinge in die wild verwirrend Format, das Sie erlebt haben. Es ist notwendig, diese Informationen zu haben, weil die Art von Dingen, die in der Liste gespeichert sind, nicht notwendigerweise offen sein müssen (wie lautet der Name für die *). Sie könnten etwas wie haben:

data Letter = A | B -- | C .. etc 
data LetterProxy p 

data HList (k :: [Letter]) where 
    HNil :: HList '[] 
    (:+:) :: LetterProxy (a :: Letter) -> HList t -> HList (a ': t) 

das ist extrem dumm, aber immer noch gültig!

Ich glaube, dass dieser Fehler aus zwei Gründen zurückzuführen ist. Erstens würde das Ergebnis von :i für bestimmte Datentypen oder Klassen sehr lang und sehr unlesbar sein, wenn Dinge in dem von mir angegebenen Format gedruckt würden. Zweitens sind die Arten sehr neu (erst seit etwa 7.4?), Also wurde nicht viel Zeit darauf verwendet, zu entscheiden, wie man mit verbundenen Dingen gedruckt wird, weil noch niemand sicher ist, wie die Arten funktionieren sollen/werden.