Toying around with proofy-lookin Haskell code

200-proof.hs

{-# LANGUAGE
  BangPatterns,
  DataKinds,
  GADTs,
  KindSignatures,
  PolyKinds,
  ScopedTypeVariables,
  TypeFamilies,
  TypeOperators #-}




data N where
  Z :: N
  S :: N -> N

data N' (n :: N) where
  Z' ::                   N' 'Z
  S' :: forall n. N' n -> N' ('S n)

type family (a :: N) + (b :: N) :: N where
  'Z   + n = n
  'S m + n = 'S (m + n)




right_identity
  :: forall n.   N' n         -> (n + 'Z)   := n
addition
  :: forall n m. N' n -> N' m -> (n + 'S m) := 'S (n + m)
commutative
  :: forall n m. N' n -> N' m -> (n + m)    := (m + n)
add
  :: forall m n. N' m -> N' n -> N' (m + n)
add_commutative
  :: forall m n. N' m -> N' n -> N' (n + m)




right_identity--base
    (Z'  :: N' n)
  -----------------------
  = Refl :: (n + 'Z) := n

right_identity--inductive
    (S' n :: N' n)
  | Refl  <- right_identity n
  ---------------------------
  = Refl :: (n + 'Z) := n




addition--base
    (Z'  :: N' n)
    (_   :: N' m)
  ----------------------------------
  = Refl :: (n + 'S m) := 'S (n + m)

addition--inductive
    (S' n' :: N' n)
    (m     :: N' m)
  | Refl   <- addition n' m
  ------------------------------------
  = Refl   :: (n + 'S m) := 'S (n + m)




commutative--base
    (Z'  :: N' n)
    (m   :: N' m)
  | Refl <- right_identity m
  ----------------------------
  = Refl :: (n + m) := (m + n)

commutative--inductive
    (S' n :: N' n)
    (m    :: N' m)
  | Refl  <- commutative n m
  , Refl  <- addition m n
  -----------------------------
  = Refl  :: (n + m) := (m + n)



add--base
    (Z' :: N' m)
    (x  :: N' n)
  -------------------
  = x   :: N' (m + n)

add--inductive
    (S' x        :: N' m)
    (y           :: N' n)
  ----------------------------
  = S' (add x y) :: N' (m + n)




add_commutative
    (x      :: N' m)
    (y      :: N' n)
  | Refl    <- commutative x y
  ----------------------------
  = add x y :: N' (n + m)




data (a :: k1) := (b :: k2) where
  Refl :: a := a

instance Show N where
  show = show . go 0
    where
      go !acc Z = acc
      go !acc (S n) = go (succ acc) n

instance Show (N' n) where
  show = show . go 0
    where
      go :: forall n. Integer -> N' n -> Integer
      go !acc Z' = acc
      go !acc (S' n) = go (succ acc) n