Haskell Peano Arithmetic

Eliminate.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Eliminate where

data Nat = Zero | Succ Nat

type family n + m where
  Zero   + m = E m
  Succ n + m = Succ (E n + E m)

type family Pred n where
  Pred Zero = Zero
  Pred (Succ n) = n

data Vec :: (* -> Nat -> *) where
  VNil :: Vec a Zero
  (:>) :: a -> Vec a n -> Vec a (Succ n)

(+++) :: Vec a n -> Vec a m -> Vec a (n + m)
VNil      +++ ys = ys
(x :> xs) +++ ys = x :> (xs +++ ys)