An example of type families---length-indexed lists---in Haskell

Vec.hs

{-# LANGUAGE TypeFamilies, DataKinds, KindSignatures, GADTs #-}
{- TypeFamilies is required to define type-level functions -}

data Nat = Zero | Succ Nat 

data Fin :: Nat -> * where 
  FZero :: Fin ('Succ n)
  FSucc :: Fin n -> Fin ('Succ n)

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

-- head only applies to non-empty vectors, so it is always type-safe. 
head :: Vector a ('Succ n) -> a 
head (Cons x _) = x

-- DataKinds prompts every datatype to be a kind, and its constructor to be a type constructor
-- However, values are types are still different and functions are not prompted. Thus 
-- we need to define type-level functions separately by using -XTypeFamilies.

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

concat :: forall n m a. Vector a n -> Vector a m -> Vector a (Add n m)
concat Nil         ys = ys
concat (Cons a xs) ys = Cons a (concat xs ys)