Ordering on Type Level Naturals

Question

I've been trying to implement the type level naturals in Haskell using the DataKinds extension. So far, my code looks like this:

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

-- the kind of natural numbers
data Nat = Zero | Succ Nat

-- type synonyms for the naturals
type N0 = Zero
type N1 = Succ N0
type N2 = Succ N1
-- ...

-- singleton natural type
data SNat (n :: Nat) where
    SZero :: SNat Zero
    SSucc :: SNat n -> SNat (Succ n)

-- type level lesser-than operator
type family (<) (x :: Nat) (y :: Nat) :: Bool where
    x < Zero = False
    Zero < y = True
    (Succ x) < (Succ y) = x < y

-- type level addition operator
type family (+) (x :: Nat) (y :: Nat) :: Nat where
    Zero + y = y
    x + Zero = x
    (Succ x) + y = Succ (x + y)
    x + (Succ y) = Succ (x + y)

infixr 5 :::
-- type of vectors with a certain length
data Vector (n :: Nat) a where
    Nil :: Vector N0 a
    (:::) :: a -> Vector n a -> Vector (Succ n) a

-- indexing operator
(!) :: ((k < n) ~ True) => Vector n a -> SNat k -> a
(x ::: _) ! SZero = x
(_ ::: xs) ! (SSucc n) = xs ! n

This code compiles fine and works as expected (giving type errors when expected also).

> (1 ::: 2 ::: 3 ::: Nil) ! (SSucc SZero)
2
> (1 ::: Nil) ! (SSucc SZero)
Couldn't match type 'False with 'True....

However, if I change one of the lines above from this:

(:::) :: a -> Vector n a -> Vector (Succ n) a

To this:

(:::) :: a -> Vector n a -> Vector (n + N1) a

The file suddenly will not compile:

Could not deduce ((n2 < n1) ~ 'True)
from the context ((k < n) ~ 'True)
  bound by the type signature for
             (!) :: (k < n) ~ 'True => Vector n a -> SNat k -> a
  at question.hs:41:8-52
or from (n ~ (n1 + N1))
  bound by a pattern with constructor
             ::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + N1) a,
           in an equation for ‘!’
  at question.hs:43:2-9
or from (k ~ 'Succ n2)
  bound by a pattern with constructor
             SSucc :: forall (n :: Nat). SNat n -> SNat ('Succ n),
           in an equation for ‘!’
  at question.hs:43:15-21
Relevant bindings include
  n :: SNat n2 (bound at question.hs:43:21)
  xs :: Vector n1 a (bound at question.hs:43:8)
In the expression: xs ! n
In an equation for ‘!’: (_ ::: xs) ! (SSucc n) = xs ! n

Why is Haskell able to deduce that n < Succ n but not that n < n + N1? How can I make my type functions behave properly in this case? (I'd prefer not to have to use unsafeCoerce).

Answer 1

You can compile with the changed type signature by cutting down the definition of the (+) type family:

-- type level addition operator
type family (+) (x :: Nat) (y :: Nat) :: Nat where
    -- Zero + y = y
    x + Zero = x
    -- (Succ x) + y = Succ (x + y)
    x + (Succ y) = Succ (x + y)

With your original definition, (n + N1) can't be reduced because GHC doesn't know which of the equations it can apply; the first one may apply depending on whether or not n is Zero.

With the cut down version it's clear (after reducing N1 to its definition) that only the x + Succ y rule can apply, so GHC is able to reduce your new type to the original one.

It's actually more normal to define operations like (+) by case analysis on the first argument, rather than the second as I've done here. That would make things like (N1 + n) work but not (n + N1). However I think that's just a convention rather than having any specific advantages.

By having both sets of definitions at once, you often end up with the worst of both worlds.