Vectors in Haskell

Vec.hs

{-# LANGUAGE GADTs               #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE TypeFamilies        #-}

module Vec where

data Nat = Zero | Succ Nat

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

foldr :: forall a (p :: Nat -> *).
         (forall n. a -> p n -> p ('Succ n)) ->
         p 'Zero ->
         forall n. Vec a n -> p n
foldr cons nil = go where

  go :: Vec a n -> p n
  go (Cons a as) = cons a $ go as
  go Nil         = nil

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

newtype Append (a :: *) (n :: Nat) (m :: Nat) =
  Wrap { unWrap :: Vec a (m :+: n) }

append :: forall a m n. Vec a m -> Vec a n -> Vec a (m :+: n)
append xs ys = unWrap $ Vec.foldr cons nil xs where

  cons :: forall m. a -> Append a n m -> Append a n ('Succ m)
  cons a = Wrap . Cons a . unWrap

  nil  :: Append a n 'Zero
  nil = Wrap ys

newtype Constant a (m :: Nat) = Constant { runConstant :: a }

foldr' :: forall a b. (a -> b -> b) -> b -> forall m. Vec a m -> b
foldr' cons nil = runConstant . Vec.foldr cons' nil' where

  cons' :: forall m. a -> Constant b m -> Constant b ('Succ m)
  cons' a = Constant . cons a . runConstant

  nil'    = Constant nil

toList :: Vec a m -> [a]
toList = foldr' (:) []

instance Show a => Show (Vec a m) where
  show = show . toList

example1 :: Vec Int ('Succ ('Succ ('Succ 'Zero)))
example1 = Cons 1 $ Cons 2 $ Cons 3 Nil

example2 :: Vec Int ('Succ 'Zero)
example2 = Cons 6 Nil

example3 = example1 `append` example2