Construct vectors of length LEQ some bound.

gistfile1.hs

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

-- Construct vectors of length LEQ some bound. :-)

data Natural where
  Zero :: Natural
  Succ :: Natural -> Natural

data SNatural :: Natural -> * where
  SZero :: SNatural 'Zero
  SSucc :: forall (n :: Natural). SNatural n -> SNatural ('Succ n)

data Vector :: * -> Natural -> Natural -> * where
  VNil  :: SNatural n -> Vector _type n n
  VCons :: _type -> Vector _type n ('Succ m) -> Vector _type n m

x :: Vector Char (Succ (Succ Zero)) (Succ (Succ Zero))
x = VNil (SSucc (SSucc SZero))

y :: Vector Char (Succ (Succ Zero)) (Succ Zero)
y = VCons 'a' $ VNil (SSucc (SSucc SZero))

z = VCons 'c' . VCons 'b' . VCons 'a' $ VNil (SSucc (SSucc SZero)) -- Doesn't typecheck! :D