Append for type-level numbered lists with TypeLits

Question

Using GHC.TypeLits, we can write a simple type-level numbered list (or vector.)

> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, DataKinds, ScopedTypeVariables #-}

> import GHC.TypeLits

> data Vec :: * -> Nat -> * where
>   VNil :: Vec e 0
>   (:-) :: e -> Vec e n -> Vec e (n+1)

This is the canonical vector definition with TypeLits. The append operation, intuitively, should look as follows:

> vecAppend :: Vec e n -> Vec e m -> Vec e (n + m)
> vecAppend VNil vec = vec
> vecAppend (a :- as) vec = a :- vecAppend as vec

But GHC's solver has trouble with the arithmetic:

Could not deduce (((n1 + m) + 1) ~ (n + m))
from the context (n ~ (n1 + 1))

Of course, since n1 + 1 ~ n, (n1 + m) + 1 ~ n1 + 1 + m ~ n + m, but the solver does not seem to know about the commutativity and associativity of + (a type function isn't in general commutative or associative!)

I know that it is possible if I define type-level Peano naturals, but I wanted to know if there is a way to do it with the current implementation of type nats in GHC (7.8.0 here.)

So I tried to help:

> vecAppend :: Vec e (n+1) -> Vec e m -> Vec e ((n + 1) + m)
> vecAppend VNil vec = vec
> vecAppend (a :- as) vec = a :- vecAppend as vec

But that just defers the problem to proper instantiation of type variables.

Could not deduce (((n1 + 1) + m) ~ ((n + m) + 1))
from the context ((n + 1) ~ (n1 + 1))
  bound by a pattern with constructor
             :- :: forall e (n :: Nat). e -> Vec e n -> Vec e (n + 1),
       in an equation for ‘vecAppend’
NB: ‘+’ is a type function, and may not be injective
Expected type: Vec l ((n + 1) + m)
  Actual type: Vec l ((n + m) + 1)
Relevant bindings include
  l :: Vec l m
  as :: Vec l n1
  vecAppend :: Vec l (n + 1) -> Vec l m -> Vec l ((n + 1) + m)

And two more much like this one.

So let's scope them.

> vecAppend ∷ ∀ e n m. Vec e (n+1) → Vec e m → Vec e (n + 1 + m)
> vecAppend VNil l = l
> vecAppend ((a :- (as ∷ Vec e n)) ∷ Vec e (n+1)) (l ∷ Vec e m) = a :- (vecAppend as l ∷ Vec e (n+m))

Alas,

Could not deduce (n1 ~ n)
from the context ((n + 1) ~ (n1 + 1))
  bound by a pattern with constructor
             :- :: forall e (n :: Nat). e -> Vec e n -> Vec e (n + 1),
           in an equation for ‘vecAppend’
  ‘n1’ is a rigid type variable bound by
       a pattern with constructor
         :- :: forall e (n :: Nat). e -> Vec e n -> Vec e (n + 1),
       in an equation for ‘vecAppend’
  ‘n’ is a rigid type variable bound by
      the type signature for
        vecAppend :: Vec e (n + 1) -> Vec e m -> Vec e ((n + 1) + m)
Expected type: Vec e n1
  Actual type: Vec e n
Relevant bindings include
  vecAppend :: Vec e (n + 1) -> Vec e m -> Vec e ((n + 1) + m)
In the pattern: as :: Vec e n
In the pattern: a :- (as :: Vec e n)
In the pattern: (a :- (as :: Vec e n)) :: Vec e (n + 1)

Is there a way to do this with the current solver, and without resorting to defining your own Peano nats? I prefer the look of 3 to Succ (Succ (Succ Zero))) in my type signatures.

EDIT: Since it seems that there is no way to do it currently (until GHC 7.10) I'll rephrase my question: can anybody show my why there is no way? I unfortunately have not yet looked at SMT solvers, so I don't know what is in principle possible or not.

The idea is that I'm not very experienced with type-level computations, and I want learn to discern situations where I can rephrase my problem so that it works, and situations where I cannot (this being (for now) an instance of the latter.)

Answer 1

Sure there's a way. It's not a good way, but there's a way.. The entire purpose of putting unsafeCoerce in the language is for the case where you know something is correctly typed, but GHC can't figure it out itself. So.. There's a way.

The story is supposed to improve significantly in GHC 7.10. The current plans are to include an SMT solver for working with type-level Nat values.

Edit:

Oh. As for why it's easy with Peano naturals, and hard with type-level literals: With Peano naturals, adding one is applying a type constructor. GHC knows that applying a type constructor is an injective operation. In fact, it's one of the key points underlying GHC's type system. So when you work with Peano naturals, you're working solely with constructs GHC is already well-suited to handle.

In contrast, GHC doesn't know a darned thing about arithmetic. It doesn't know that (+1) is an injective function on Nat. So it has no way of knowing that it can derive m ~ n from (m + 1) ~ (n + 1). It also has no ideas about the basic properties of arithmetic on Nat, like the associative, distributive, and commutative properties. The idea behind integrating an SMT solver is that SMT solvers are quite good at working with those sorts of properties.

With GHC 7.8, you can rather painlessly translate type-level literals to Peano naturals, though:

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

import GHC.TypeLits

data Z
data S a

type family P (n :: Nat) where
    P 0 = Z
    P n = S (P (n - 1))

This takes advantage of the new closed type families feature to make a type function P for converting from a literal to a Peano representation, as such:

*Main> :t undefined :: P 5
undefined :: P 5 :: S (S (S (S (S Z))))