Play with Haskell Kinds.

kinds1.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

data Nat = Z | Succ Nat
               deriving Show

data Vec :: (* -> Nat -> *) where
  Nil :: Vec a Z
  Cons :: a -> Vec a n -> Vec a (Succ n)

instance (Show a) => Show (Vec a b) where
  show Nil = "Nil"
  show (Cons x xs) = show x ++ ", " ++ show xs

nil = Nil :: Vec Int Z
cons1 = Cons 1 nil
cons2 = Cons 2 cons1

concat' :: Vec e n -> Vec e m -> Vec e (Add n m)
concat' Nil ys = ys
concat' (Cons x xs) ys = Cons x (concat' xs ys)

type family Add (n :: Nat) (m :: Nat) :: Nat

type instance Add Z m = m
type instance Add (Succ n) m = Succ (Add n m)

type family IsZero (n :: Nat) :: Bool where
  IsZero Z = 'True
  IsZero (Succ n) = 'False