How to convince ghc that type level addition is commutative (to implement dependently typed reverse)?

Question

This does not compile because as ghc tells me Add is not injective. How do I tell the compiler that Add is really commutative (maybe by telling it that Add is injective)? It seems from the hasochism paper that one has to provide a proxy somehow.

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}

data Nat = Z | S Nat

type family Add a b where
  Add  Z    n = n
  Add  n    Z = n
  Add (S n) k = S (Add n k)

data VecList n a where
  Nil  :: VecList Z a
  Cons :: a -> VecList n a -> VecList (S n) a

safeRev :: forall a n . VecList n a -> VecList n a
safeRev xs = safeRevAux Nil xs
  where
    safeRevAux :: VecList p a -> VecList q a -> VecList (Add p q) a
    safeRevAux acc Nil = acc
    safeRevAux acc (Cons y ys) = safeRevAux (Cons y acc) ys

One can do this but it feels like too much is going on under the covers for my taste.

{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}

import Data.Proxy
import Data.Type.Equality

data Nat = Z | S Nat

type family n1 + n2 where
  Z + n2 = n2
  (S n1) + n2 = S (n1 + n2)

-- singleton for Nat
data SNat :: Nat -> * where
  SZero :: SNat Z
  SSucc :: SNat n -> SNat (S n)

-- inductive proof of right-identity of +
plus_id_r :: SNat n -> ((n + Z) :~: n)
plus_id_r SZero = Refl
plus_id_r (SSucc n) = gcastWith (plus_id_r n) Refl

-- inductive proof of simplification on the rhs of +
plus_succ_r :: SNat n1 -> Proxy n2 -> ((n1 + (S n2)) :~: (S (n1 + n2)))
plus_succ_r SZero _ = Refl
plus_succ_r (SSucc n1) proxy_n2 = gcastWith (plus_succ_r n1 proxy_n2) Refl

data VecList n a where
  V0  :: VecList Z a
  Cons :: a -> VecList n a -> VecList (S n) a

reverseList :: VecList n a -> VecList n a
reverseList V0 = V0
reverseList list = go SZero V0 list
  where
    go :: SNat n1 -> VecList n1  a-> VecList n2 a -> VecList (n1 + n2) a
    go snat acc V0 = gcastWith (plus_id_r snat) acc
    go snat acc (Cons h (t :: VecList n3 a)) =
      gcastWith (plus_succ_r snat (Proxy :: Proxy n3))
              (go (SSucc snat) (Cons h acc) t)

safeHead :: VecList (S n) a -> a
safeHead (Cons x _) = x

test = safeHead $ reverseList (Cons 'a' (Cons 'b' V0))

See https://www.haskell.org/pipermail/haskell-cafe/2014-September/115919.html for the original idea.

EDIT:

@user3237465 This is very interesting and more what I had in mind (although on reflection my question was probably not very well formulated).

It seems I have "axioms"

type family n1 :+ n2 where
  Z :+ n2 = n2
  (S n1) :+ n2 = S (n1 + n2)

and thus can produce proofs like

plus_id_r :: SNat n -> ((n + Z) :~: n)
plus_id_r SZero = Refl
plus_id_r (SSucc n) = gcastWith (plus_id_r n) Refl

I find this quite terse. I would normally reason something like this

• In the last clause of the above we have SSucc n :: SNat (S k) so n :: k
• We thus need to prove S k + Z :~: S k
• By the second "axiom" S k + Z = S (k + Z)
• We thus need to prove S (k + Z) :~: S k
• plus_id_r n gives a "proof" that (k + Z) :~: k
• and Refl gives a "proof" that m ~ n => S m :~: S n
• We can thus unify these proofs using gcastWith to give the desired result.

For your solution you give the "axioms"

type family n :+ m where
    Z   :+ m = m
    S n :+ m = n :+ S m

With these, the proof for (n + Z) :~: n will not work.

• In the last clause, we again have that SSucc x has type SNat (S k)
• We thus need to prove S k :+ Z :~: S k
• By the second new "axiom" we have S k + Z = k + S Z
• We thus need to prove k + S Z :~: S k
• So we have something more complex to prove :-(

I can produce a proof for the original second "axiom" from the new second "axiom" (so my second "axiom" is now a lemma?).

succ_plus_id :: SNat n1 -> SNat n2 -> (((S n1) :+ n2) :~: (S (n1 :+ n2)))
succ_plus_id SZero _ = Refl
succ_plus_id (SSucc n) m = gcastWith (succ_plus_id n (SSucc m)) Refl

So now I should be able to get the original proofs to work but I am not sure how currently.

Is my reasoning correct thus far?

PS: ghc agrees with my reasoning for why the proof of the existence of a right identity will not work

Could not deduce ((n1 :+ 'S 'Z) ~ 'S n1)
...
or from ((n1 :+ 'Z) ~ n1)

Answer 1

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExplicitForAll #-}

import Data.Type.Equality

data Nat = Z | S Nat

type family (n :: Nat) :+ (m :: Nat) :: Nat where
    Z   :+ m = m
    S n :+ m = n :+ S m

-- Singleton for Nat
data SNat :: Nat -> * where
  SZero :: SNat Z
  SSucc :: SNat n -> SNat (S n)

succ_plus_id :: SNat n1 -> SNat n2 -> (((S n1) :+ n2) :~: (S (n1 :+ n2)))
succ_plus_id SZero _ = Refl
succ_plus_id (SSucc n) m = gcastWith (succ_plus_id n (SSucc m)) Refl

plus_id_r :: SNat n -> ((n :+ Z) :~: n)
plus_id_r SZero = Refl
plus_id_r (SSucc x) = gcastWith (plus_id_r x) (succ_plus_id x SZero)

data Vec a n where
    Nil   :: Vec a Z
    (:::) :: a -> Vec a n -> Vec a (S n)

size :: Vec a n -> SNat n
size Nil         = SZero
size (_ ::: xs)  = SSucc $ size xs

elim0 :: SNat n -> (Vec a (n :+ Z) -> Vec a n)
elim0 n x = gcastWith (plus_id_r n) x

accrev :: Vec a n -> Vec a n
accrev x = elim0 (size x) $ go Nil x where
    go :: Vec a m -> Vec a n -> Vec a (n :+ m)
    go acc  Nil       = acc
    go acc (x ::: xs) = go (x ::: acc) xs

safeHead :: Vec a (S n) -> a
safeHead (x ::: _) = x

Answer 2

You can simplify the definition of reverse a bit:

{-# LANGUAGE GADTs, KindSignatures, DataKinds    #-}
{-# LANGUAGE TypeFamilies, UndecidableInstances  #-}
{-# LANGUAGE TypeOperators                       #-}

data Nat = Z | S Nat

data Vec a n where
    Nil   :: Vec a Z
    (:::) :: a -> Vec a n -> Vec a (S n)

type family n :+ m where
    Z   :+ m = m
    S n :+ m = n :+ S m

elim0 :: Vec a (n :+ Z) -> Vec a n
elim0 = undefined

accrev :: Vec a n -> Vec a n
accrev = elim0 . go Nil where
    go :: Vec a m -> Vec a n -> Vec a (n :+ m)
    go acc  Nil       = acc
    go acc (x ::: xs) = go (x ::: acc) xs

The (:+) operator is defined accordingly to the (:::) operator. Unification in the (:::) case proceeds as follows:

x ::: xs induces n to be S n. So the type of the result becomes Vec a (S n :+ m) or, after beta-reduction, Vec a (n :+ S m). While

x ::: acc         :: Vec a (S m)
xs                :: Vec a  n
go (x ::: acc) xs :: Vec a (n :+ S m)

So we have a match. However now you need to define elim0 :: Vec a (n :+ Z) -> Vec a n, which requires both the proofs from your question.

The whole code in Agda: http://lpaste.net/117679

---

BTW, it's not true, that you would need proofs in any case. Here is how reverse defined in the Agda's standard library:

foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
        (∀ {n} → B n → A → B (suc n)) →
        B zero →
        Vec A m → B m
foldl b _⊕_ n []       = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs

reverse : ∀ {a n} {A : Set a} → Vec A n → Vec A n
reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []

That's because foldl carries additional type information about the behavior of _⊕_, so you satisfy the typechecker at each step and no proofs are needed.