Haskell Peano Arithmetic

Eliminate.hs

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

data Nat = Zero | Succ Nat | Pred Nat

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

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

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)

eliminate_error.txt

    • Could not deduce: E m ~ m
      from the context: n ~ 'Zero
        bound by a pattern with constructor: VNil :: forall a. Vec a 'Zero,
                 in an equation for ‘+++’
        at Eliminate.hs:27:1-4
      ‘m’ is a rigid type variable bound by
        the type signature for:
          (+++) :: forall a (n :: Nat) (m :: Nat).
                   Vec a n -> Vec a m -> Vec a (n + m)
        at Eliminate.hs:26:1-44
      Expected type: Vec a (n + m)
        Actual type: Vec a m
    • In the expression: ys
      In an equation for ‘+++’: VNil +++ ys = ys
    • Relevant bindings include
        ys :: Vec a m
          (bound at Eliminate.hs:27:15)
        (+++) :: Vec a n -> Vec a m -> Vec a (n + m)
          (bound at Eliminate.hs:27:11)

Peano.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Peano where

data Nat = Zero | Succ Nat

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

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