CODEWITHSUNDEEP
haskell
Alexey Vagarenko
Alexey Vagarenko

Reputation: 1196

Compare fixed sized vectors

I'm trying to write a fixed size vector like this:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators #-}
import GHC.TypeLits

data NVector (n :: Nat) a where
    Nil :: NVector 0 a
    Cons :: a -> NVector n a -> NVector (n + 1) a

instance Eq a => Eq (NVector n a) where
    Nil == Nil = True
    (Cons x xs) == (Cons y ys) = x == y && xs == ys

but it fails to compile with this message:

 Could not deduce (n2 ~ n1)
from the context (Eq a)
  bound by the instance declaration at prog.hs:8:10-33
or from (n ~ (n1 + 1))
  bound by a pattern with constructor
             Cons :: forall a (n :: Nat). a -> NVector n a -> NVector (n + 1) a,
           in an equation for `=='
  at prog.hs:10:6-14
or from (n ~ (n2 + 1))
  bound by a pattern with constructor
             Cons :: forall a (n :: Nat). a -> NVector n a -> NVector (n + 1) a,
           in an equation for `=='
  at prog.hs:10:21-29

but if I introduce type-level naturals manually, it compiles successfully 

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies #-}
data Nat = Z | S Nat

infixl 6 :+

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

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

instance (Eq a) => Eq (NVector n a) where
    Nil == Nil = True
    (Cons x xs) == (Cons y ys) = x == y && xs == ys

ghc version 7.8.3

Upvotes: 3

Views: 194

Answers (1)

Hans Lub
Hans Lub

Reputation: 5678

ghc cannot (not yet?) deduce the type equality n ~ n' from (n+1) ~ (n'+1) while it has no trouble with deducing it from S n ~ S n' See e.g. Append for type-level numbered lists with TypeLits for an explanation, and a possible way out (i.e. to have both Peano-style naturals and still be able to use literals like5)

But, if you change your definition of Nvector into

data NVector (n :: Nat) a where
    Nil :: NVector 0 a
    Cons :: a -> NVector (n -1) a -> NVector n a

it will have to deduce n-1 ~ n'-1 from n ~ n', a much easier deduction! This compiles, and still yields a correct type for e.g. Cons () Nil:

*Main> :t Cons () Nil
Cons () Nil :: NVector 1 ()

Note that this is pretty useless, as we still cannot define 

append :: NVector n a -> NVector m a -> NVector (n + m) a -- won't work

The Oct. '14 status report for ghc says:

Iavor Diatchki is working on utilizing an off-the-shelf SMT solver in GHC's constraint solver. Currently, the main focus for this is improved support for reasoning with type-level natural numbers [...]

so your example might well work OK with ghc 7.10 or 7.12!

Upvotes: 7

Related Questions