{-# Language TypeFamilies, DataKinds, KindSignatures, GADTs, UndecidableInstances #-}
data Nat = Z | S Nat
type family Plus (x :: Nat) (y :: Nat) :: Nat where
Plus 'Z y = y
Plus ('S x) y = 'S (Plus x y)
type family Pred (x :: Nat) :: Nat where
Pred 'Z = 'Z
Pred ('S x) = x
data Vec (n :: Nat) (a :: *) where -- Nat -> * -> * where
Nil :: Vec Z a
(:-) :: a -> Vec n a -> Vec ('S n) a
infixr 5 :-
instance Show a => Show (Vec n a) where
show Nil = "Nil"
show (a :- v) = show a ++ " :- " ++ show v
append :: Vec m a -> Vec n a -> Vec (Plus m n) a
append Nil ys = ys
append (x :- xs) ys = x :- (append xs ys)
vtail :: Vec m a -> Vec (Pred m) a
vtail Nil = Nil
vtail (x :- xs) = xs
main = do
let v1 = 2 :- Nil
let v2 = 5 :- 4 :- 3 :- Nil
putStrLn $ show (v2 `append` v1)
putStrLn $ show (vtail v2)
