Haskell type level literal Nat: status?

Question

GHC has type level literal Nats. I can read a few things about them, for instance, here:

https://ghc.haskell.org/trac/ghc/wiki/TypeNats

Unfortunately, there seems to be little documentation about them, and almost nothing I try to do with them actually works.

Comment 18 from this page mentions this simple example of size parametrized Vecs (I've added LANGUAGE pragmas and an import statement):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits

data Vec :: Nat -> * -> * where
  Nil  :: Vec 0 a
  (:>) :: a -> Vec n a -> Vec (n+1) a

(+++) :: Vec n a -> Vec m a -> Vec (n+m) a
Nil       +++ bs = bs
(a :> as) +++ bs = a :> (as +++ bs)

It wasn't working at the time, but then the implementation was supposedly modified so that this worked. That was 5 years ago... but it doesn't work on my GHC 7.10.1:

trash.hs:15:20:
    Could not deduce ((n + m) ~ ((n1 + m) + 1))
    from the context (n ~ (n1 + 1))
      bound by a pattern with constructor
                 :> :: forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a,
               in an equation for ‘+++’
      at trash.hs:15:2-8
    NB: ‘+’ is a type function, and may not be injective
    Expected type: Vec (n + m) a
      Actual type: Vec ((n1 + m) + 1) a
    Relevant bindings include
      bs :: Vec m a (bound at trash.hs:15:15)
      as :: Vec n1 a (bound at trash.hs:15:7)
      (+++) :: Vec n a -> Vec m a -> Vec (n + m) a
        (bound at trash.hs:14:1)
    In the expression: a :> (as +++ bs)
    In an equation for ‘+++’: (a :> as) +++ bs = a :> (as +++ bs)

What's the deal here? Are type level literal Nats supposed to be usable for this kind of thing? If so, how do I implement the (+++) function? If not, what is their use case?

Answer 1

As commenters have mentioned, the typechecker is currently unable to discharge this equality because they require algebra. Whereas you and I know that n + m = n1 + m + 1 given n = n1 + 1, nobody has taught the GHC typechecker how to perform that kind of arithmetic. In languages like Ada, Idris, or Coq you'd be able to teach the compiler these rules or perhaps the rules of arithmetic would be provided to you in a library, but in Haskell the typechecker is a bit more rigid (but a lot friendlier to real-world programming, in my opinion) and you have to unfortunately resort to a typechecker plugin.

The person that I know of who is most actively on this problem is one Iavor Diatchki. That paper is behind the dumb ACM paywall, but you can find his Haskell Symposium 2015 talk here on YouTube — it's very well-explained!. His talk uses the same example as yours, the ever-popular vector. His branch in the GHC repository works on merging it into mainline GHC, but as far as I know there are no dates set. For now you have to use the typechecker plugin, which is not so bad. After all, the original goal of Plugins/Typechecker was to enable interesting work like this without having to merge everything into the source code. There's something to be said for modularity!