type_list.hs

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

import Data.Monoid ((<>))

data Nat = Zero | Succ Nat

data List (n :: Nat) (a :: *) where
    Nil :: List 'Zero a
    Cons :: a -> List n a -> List ('Succ n) a

instance Show a => Show (List n a) where
    show Nil         = "Nil"
    show (Cons a as) = "Cons" <> show a <> " (" <> show as <> ") "

-- add
type family Add (n :: Nat) (m :: Nat) where
    Add 'Zero m = m
    Add ('Succ n) m = 'Succ (Add n m)

append :: List n a -> List m a -> List (Add n m) a
append Nil ys         = ys
append (Cons x xs) ys = Cons x (append xs ys)