Reversable Vect.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
 
data N = S N | Z
 
data Vect n where
  ZV :: Vect Z
  CV :: Int -> Vect n -> Vect (S n)
 
instance Show (Vect n) where
  show ZV = "Nil"
  show (CV x v) = show x ++ " : " ++ show v
 
class VecReverse n m where
  type Plus n m :: N
  vecReverse :: Vect n -> Vect m -> Vect (Plus n m)

instance VecReverse Z w where
  type Plus Z w = w
  vecReverse ZV w = w

instance (VecReverse n (S m), Plus n (S m) ~ S (Plus n m)) => VecReverse (S n) m where
  type Plus (S n) m = S (Plus n m)
  vecReverse (CV x v) w = vecReverse v (CV x w)

{- |

>>> vecReverse (CV 1 (CV 2 ZV)) ZV
2 : 1 : Nil

-}