GHC 7.8中类型级自然的行为

Question

如果你想要按长度索引的向量,你可以这样做:

{-# 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

在ghc 7.8中我希望这对于新类型文字会过时,但是直接转换是无效的:

{-# 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这给出了一个错误:NB:+'是一个类型函数,可能不是单射的.我理解为什么会发生这种情况,但由于类型文字仍然是编译器魔术,我不知道为什么编译器也不能将其魔术化.

我试着改变Vect:(:>) :: a -> Vect (n-1) a -> Vect n a.这种方式有一个内部向量的显式公式,但这给出了错误:

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

所以现在它需要基本算术的证明.我无法使任何一个版本工作.有没有办法(n + m) - o == (n - o) + m为编译器编写证明,或以某种方式使第一个版本工作？

Answer 1

类型级自然仍然没有真正做计算.GHC 7.10预计将集成一个SMT求解器,最终处理您认为应该能够实现的所有内容.

作为一个理论上不健全但可以回答你实际问题的答案 - unsafeCoerce当你知道两个表达式具有相同类型但编译器没有相同的情况时存在.