6

我有以下 GADT

data Vec n a where
    T    :: Vec VZero a
    (:.) :: (VNat n) => a -> (Vec n a) -> (Vec (VSucc n) a)

使用类对固定长度向量进行建模

class VNat n

data VZero
instance VNat VZero

data VSucc n
instance (VNat n) => VNat (VSucc n)

我试图在向量上编写一个附加函数：

vAppend :: Vec n b -> Vec m b -> Vec nm b
vAppend T T = T   -- nonsense, -- its just a minimal def for testing purposes

类型检查器不喜欢它：

 Could not deduce (nm ~ VZero)
    from the context (n ~ VZero)
      bound by a pattern with constructor
                 T :: forall a. Vec VZero a,
               in an equation for `vAppend'
      at VArrow.hs:20:9
    or from (m ~ VZero)
      bound by a pattern with constructor
                 T :: forall a. Vec VZero a,
               in an equation for `vAppend'
      at VArrow.hs:20:11
      `nm' is a rigid type variable bound by
           the type signature for vAppend :: Vec n b -> Vec m b -> Vec nm b
           at VArrow.hs:20:1
    Expected type: Vec nm b
      Actual type: Vec VZero b
    In the expression: T
    In an equation for `vAppend': vAppend T T = T
Failed, modules loaded: Vectors.

谁能解释类型变量的 GHC 问题nm？~错误消息中的确切含义是什么？

4

3 回答 3

10

就目前而言，您是说您可以通过附加任意两个向量来获得任意长度的向量。如果您废弃应该在给定任意两个向量的情况下产生长度为 VZero 的向量的签名推断——这是有道理的，但不是您想要的。您需要一个与您的 s 关联的类型来约束on 向量的结果类型。自然的方式是某种类型的家族，但我无法在课堂上得到它。无论如何，通过扩展的提升类型（在 ghc-7.4 及更高版本中）更清楚地实现了这一整套想法——尽管也许你是故意试图避免这种扩展？这摆脱了令人讨厌的未封闭字符ghcvAppendPlusVNatvAppendVNatDataKindsVSucc，它承认VSucc Char等等。如果你不想避免DataKinds，那么你的模块可能看起来像这样：

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

data Vec n a where                 -- or: data Vec :: VNat -> * -> * where
    T    :: Vec VZero a
    (:.) :: a -> Vec n a -> Vec (VSucc n) a 
                                   -- no class constraint

data VNat  =  VZero |  VSucc VNat  -- standard naturals

type family n :+ m :: VNat         -- note the kind of a ":+" is a promoted VNat
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)

vAppend :: Vec n b -> Vec m b -> Vec (n :+ m) b
vAppend T v = v  
vAppend (a :. u) v  = a :. (vAppend u v)

编辑：看着这个，我突然想到Plus- 或:+- 类型系列的行应该明确限制参数的种类

type family (n::VNat) :+ (m::VNat) :: VNat

将诸如此类的垃圾类型拒之门外Char :+ VZero-也就是说，与过去喜欢使用DataKinds诸如data VSucc n. 此外，我们可以看到这两个实例完全指定了它，尽管我不知道编译器对此有多大用处。

于 2012-08-22T15:06:46.197 回答
9

类型签名中的所有类型变量都是通用量化的。这意味着如果你说函数有类型

Vec n b -> Vec m b -> Vec nm b

那么对于、和的任何选择n，此类型必须是有效的。特别是，例如，mnmb

Vec VZero Int -> Vec VZero Int -> Vec (VSucc VZero) Int

也必须是您的函数的有效类型。但是，追加两个向量没有这样的通用类型。有约束nm，即nm类型级数和 的n总和m。你必须在函数的类型中表达这些约束，否则你会得到类型错误。

就您而言，GHC 抱怨在您的定义中，nmis 实际上VZero，因此您正在假设nm您的类型表明您不允许这样做。这~只是 GHC 类型相等的符号。

于 2012-08-22T14:33:35.440 回答
6

通过对 GADT 的值进行模式匹配来编写函数时，GHC 在对每个子句进行类型检查时使用有关函数运行时预期行为的信息。您的vAppend函数只有一个子句，该模式匹配 type 的值和 typeVec n b的另一个值Vec m b。GHC 的理由是，如果在运行时vAppend应用于与模式匹配的实际参数T，则实际参数的实际类型必须是 form Vec VZero b，这是一种比Vec n bor提供更多信息的类型Vec m b。这种推理在 GHC 中实现的方式是，在对唯一子句 of 的 RHS 进行类型检查时vAppend，它记录了一个假设，该假设n肯定确实是VZero、书面n ~ VZero的，并且同样如此。m ~ VZero.

您为函数编写的类型规定了它必须履行的合同。您收到的错误消息是因为必须通过实施来履行的合同vAppend过于笼统。你是说给定两个长度为n和的向量m，vAppend必须产生一个可以被认为是任意大小的向量。实际上，GHC 注意到您的实现不履行此合同，因为您的 RHS 的类型 与 RHSVec VZero b的预期类型不匹配Vec nm b，并且没有假设说nm ~ VZero. 事实上，GHC 告诉我们，唯一可用的假设是上一段中的假设。

您履行本合同的唯一可能方式是写成undefined您的条款的 RHS。这显然不是你想要的。获得正确类型的技巧vAppend是以某种方式将输出向量的大小与两个输入向量的各自大小相关联。这可能是这样的：

type family Plus n m
type instance Plus VZero m = m
type instance Plus (VSucc n) m = VSucc (Plus n m)

vAppend :: Vec n b -> Vec m b -> Vec (Plus n m) b
vAppend T T = T

我们在这里所做的是，长度是由输入的长度决定的vAppend，通过类型上的一些函数调用Plus。在两个输入长度都是 的情况下VZero，我们知道这与和Plus n m相同。由于是第一类族实例的形状，GHC 知道它与. 因此，在这个分支中，GHC 需要一个 RHS 类型，我们可以很容易地构造它！Plus VZero VZeron ~ VZerom ~ VZeroPlus VZero VZeroVZeroVec VZero b

于 2012-08-22T15:31:23.837 回答