Proving m + (1 + n) == 1+ (m + n) in Dependent Haskell

Question

I am experimenting with Haskell's type system and want to write a type safe addition function. This function should accept two singleton witnesses representing numbers and returns a singleton witness of a number whose type carries the proof that it is indeed a sum of the arguments. Here is the code:

{-# language TypeFamilies, KindSignatures, DataKinds, PolyKinds, UndecidableInstances, GADTs #-}

data Nat = Zero | Succ Nat deriving Show
type family Add (m :: Nat) (n :: Nat) :: Nat where
  Add Zero n = n
  Add (Succ m) n = Add m (Succ n)

data SNat :: Nat -> * where
  Zy :: SNat Zero
  Suc :: SNat m -> SNat (Succ m)

data Bounded' m = B m

sum' :: Bounded' (SNat m) -> Bounded' (SNat n) -> Bounded' (SNat (Add m n))
sum' (B m) (B n) = B $ case (m, n) of
                    (Zy,x) -> x
                    (Suc x, y) -> let B z = sum' (B x) (B y) in Suc z

Here is the error:

    • Could not deduce: Add m1 ('Succ n) ~ 'Succ (Add m1 n)
      from the context: m ~ 'Succ m1
      bound by a pattern with constructor:
               Suc :: forall (m :: Nat). SNat m -> SNat ('Succ m),
               in a case alternative
      at main.hs:17:22-26
      Expected type: SNat (Add m n)
      Actual type:   SNat ('Succ (Add m1 n))
    • In the expression: Suc z
      In the expression: let B z = sum' (B x) (B y) in Suc z
      In a case alternative:
        (Suc x, y) -> let B z = sum' (B x) (B y) in Suc z

I understand the error message. How do I provide GHC with the necessary proof that Add m n = Succ (Add k n) in expression Suc z when it learns that m ~ Succ k (in second case match) and are there alternative approaches to doing so. Thank you.

Answer 1

Your definition of addition is not the conventional one.

type family Add (m :: Nat) (n :: Nat) :: Nat where
  Add Zero n = n
  Add (Succ m) n = Add m (Succ n)

This is a "tail recursive" addition. It sure seems like there should be a way to prove your properties using this form of addition, but I can't figure it out. Until then, tail recursion at the type/property level tends to be a lot more difficult to work with than the standard kind:

type family Add (m :: Nat) (n :: Nat) :: Nat where
  Add Zero n = n
  Add (Succ m) n = Succ (Add m n)

This latter definition of addition makes your sum' pass without any convincing at all.

---

EDIT actually it was easy once I saw it right. Here's what I got (importing Data.Type.Equality and enabling LANGUAGE TypeOperators):

propSucc2 :: SNat m -> SNat n -> Add m (Succ n) :~: Succ (Add m n)
propSucc2 Zy _ = Refl
propSucc2 (Suc m) n = propSucc2 m (Suc n)

Tail-recursive definition, tail-recursive proof. Then to use it, you use gcastWith:

sum' (B m) (B n) = ...
        (Suc x, y) -> gcastWith (propSucc2 x y) 
                                (let B z = sum' (B x) (B y) in Suc z)

gcastWith just takes a :~: equality and makes it available to the type checker within the scope of its second argument.

By the way, if you define sum' in a parallel structure to your Add type family, then you don't need any lemmas. Getting things to follow parallel structures is a good technique to keep things easy (this is part of the art of dependent programming, since it's not always obvious how):

sum' :: Bounded' (SNat m) -> Bounded' (SNat n) -> Bounded' (SNat (Add m n))
sum' (B Zy) (B n) = B n
sum' (B (Suc m)) (B n) = sum' (B m) (B (Suc n))