If you want vectors indexed by their length you can do something like this:
{-# LANGUAGE
DataKinds, GADTs, TypeOperators, TypeFamilies, StandaloneDeriving
#-}
data N = P N | Z
type family Add (n :: N) (m :: N) :: N
type instance Add Z a = a
type instance Add (P a) b = P (Add a b)
infixr 5 :>
data Vect n a where
V0 :: Vect Z a
(:>) :: a -> Vect n a -> Vect (P n) a
deriving instance Show a => Show (Vect n a)
concatV :: Vect n a -> Vect m a -> Vect (Add n m) a
concatV V0 y = y
concatV (x :> xs) y = x :> concatV xs y
In ghc 7.8 I was hoping this would become obsolete with the new type literals, but the direct conversion is invalid:
{-# LANGUAGE
DataKinds, GADTs, TypeOperators, TypeFamilies, StandaloneDeriving
#-}
import GHC.TypeLits
infixr 5 :>
data Vect (n :: Nat) a where
V0 :: Vect 0 a
(:>) :: a -> Vect n a -> Vect (n+1) a
deriving instance Show a => Show (Vect n a)
concatV :: Vect n a -> Vect m a -> Vect (n + m) a
concatV V0 y = y
concatV (x :> xs) y = x :> concatV xs y
Unfortunatley this gives an error: NB:
+' is a type function, and may not be injective `. I understand why this happens, but since the type literals are compiler magic anyways, I don't know why the compiler could not magic this away either.
I tried changing Vect
: (:>) :: a -> Vect (n-1) a -> Vect n a
. This way there is an explicit formula for the inner vector, but this gives the error:
Couldn't match type `(n + m) - 1' with `(n - 1) + m'
Expected type: Vect ((n + m) - 1) a
Actual type: Vect ((n - 1) + m) a
So now it requires a proof of basic arithmetic. I haven't been able to make either version work. Is there a way to write a proof of (n + m) - o == (n - o) + m
for the compiler, or somehow make the first version work?