How exactly do kind lists work?

Question

I've been reading on vinyl recently, which uses weird "list of kinds" kinda types. After reading a bit on kinds and vinyl, I've gotten somewhat of an intuitive understanding of them, and I've been able to hack this together

{-# 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 yields

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

From which I gather that '[] is sugar for '[] * and x ': y for (':) * x y. What is that * doing there? Is it the kind of the list elements? Also, what exactly is such a list anyway? Is it something built into the language?

Answer 1

That * is... Unfortunate. It's the result of GHC's pretty-printer for polykinded data types. It results in things that are syntactically invalid as heck, but it does convey some useful information.

When GHC pretty-prints a type with polymorphic kinds, it prints the kind of each polymorphic type variable after the type constructor. In order. So if you had a declaration like:

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

GHC would pretty-print the type of Foo (the data constructor) as y -> Foo k k1 x y z. If you had some use that pinned down the kind of one of those type variables somewhat, like..

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

The type of foo "hello" 0 would be printed as Foo * Nat String Int 5. Yeah, it's terrible. But if you know what's going on, at least you can read it.

The '[] stuff is part of the DataKinds extension. It allows promoting types to kinds, and the constructors of that type become type constructors. Those promoted types have no valid values, not even undefined, because their kind is not compatible with *, which is the kind of all types that can have values with them. So they can only show up in places where there is no type of that value. For more information, see http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-polymorphism-and-promotion.html

Edit:

Your comment brings up some points about the way ghci works.

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

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

When you load a file in ghci, it doesn't activate the extensions interactively that were used in the file.

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

So, yeah. The PolyKinds extension must be enabled in ghci for it to default to polymorphic kinds in the type. And I tried defining my foo function in the file as well, but it did indeed crash this version of ghc. Whoops. I think that's fixed now, but I suppose checking the ghc trac would be nice. In any case, I can define it interactively and it works fine.

*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, well, I forgot the import was needed for it display Nat unqualified. And since I was only demonstrating type printing, I didn't care about an implementation, so undefined is good enough.

But everything does work how I said, I promise. I just left out some details about where what extensions were needed, in particular both PolyKinds and DataKinds. I assumed that since you were using those in your code, you understood them. Here's the documentation on the PolyKinds extension: http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/kind-polymorphism.html

Answer 2

This is due to some unfortunate implementation concerning printing. Kinds can be thought of as 'types of types'. Note the following:

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

Just like [a] means "for all types a, [a]", [*] means "for all kinds *, [*] ". However, the amount of reasoning you can do with kinds is much smaller than with types. For example, a -> a indicates both as are the same type, but * -> * means both * can be any type (it can be thought of as * -> * is the type a -> b "lifted" to the kind level). But there is no way to lift the type a -> a to the kind level. This means that [a] and [*] are not quite analogous. [*] is closer to something like [forall a . a]. More tersely, but less accurately, you could say that there is no way to distinguish 'polymorphic' kinds as there are no such thing as 'kind variables'. (side note: -XPolyKinds enables what the documentation calls 'polymorphic kinds', but it still doesn't give you true polymorphism)

So when you write HList :: [*] -> * (which really means HList (k :: [*]) :: *) you are indicating that the kind of the first type parameter should be [*], and the 'values' that types of kind [*] can take are '[], * ': '[], * ': * ': '[], etc.

Now the problem. When printing things whose kind has been constrained, like the first type parameter of HNil, it will try to include all kind information. For whatever reason, instead of writing

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

which would actually indicate that the * is referring to the kind of '[], it prints things in the wildly confusing format you have witnessed. It is necessary to have this information, because the kind of thing 'stored' inside the list doesn't necessarily have to be open-kind (which is the name for the *). You could have something like:

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

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

which is extremely stupid but still valid!

I believe that this misfeature is due to two reasons. Firstly, if things were printed in the format I have stated, the result of :i for certain data types or classes would be very long and very unreadable. Secondly, kinds are very new (only around since 7.4?) so not a lot of time has been spent on deciding how to print kinded things, because noone is yet certain of how kinds should/will work.