haskell - 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 中，我希望这会随着新的 type literals 而过时。 ，但直接转换无效:

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

不幸的是，这给出了一个错误: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

Type-level naturals 还没有真正进行计算。 GHC 7.10 计划集成一个 SMT 求解器，以最终处理您认为它应该能够处理的所有事情。

作为对您的实际问题的理论上不健全但有效的答案 - unsafeCoerce当您知道两个表达式具有相同类型但编译器没有时，存在这种情况。