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