Safe lists in Haskell

SafeLists.hs

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

module SafeList where

data Nat :: * where
  Z :: Nat
  S :: Nat -> Nat

data Vector :: Nat -> * -> * where
  VNil :: Vector Z a
  VCons :: a -> Vector n a -> Vector (S n) a

instance (Show a) => Show (Vector length a) where
  show VNil = "VNil"
  show (VCons x VNil) = "VCons " ++ (show x) ++ " VNil"
  show (VCons y ys) = "VCons " ++ (show y) ++ " (" ++ (show ys) ++ ")"

instance Functor (Vector length) where
  fmap _ VNil = VNil
  fmap f (VCons x xs) = VCons (f x) (fmap f xs)

headV :: Vector (S n) a -> a
headV (VCons x xs) = x

tailV :: Vector (S n) a -> Vector n a
tailV (VCons x xs) = xs

foldrV :: (a -> b -> b) -> Vector n a -> b -> b
foldrV f VNil d = d
foldrV f (VCons x xs) d = f x (foldrV f xs d)

-- | zipWith for Vectors
-- >>> zipWithV (,) (VCons 1 (VCons 2 (VCons 3 VNil))) (VCons 'a' (VCons 'b' (VCons 'c' VNil)))
-- VCons (1,'a') (VCons (2,'b') (VCons (3,'c') VNil))
zipWithV :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWithV _ VNil VNil = VNil
zipWithV f (VCons x xs) (VCons y ys) = VCons (f x y) (zipWithV f xs ys)

-- appendV :: Vector n a -> Vector m a -> Vector (n + m) a