GADT类型的奇怪类型推断行为(对于固定长度向量)

Question

我有以下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)

我试图在vector上编程一个append-function:

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.

任何人都可以解释类型变量的GHCs问题nm吗？究竟是什么意思~在错误信息中？

Answer 1

就目前而言,你说你可以通过附加任意两个向量来获得任意长度的向量.如果你废弃了签名推断,它应该产生长度为VZero的矢量给定任意两个向量 - 这是有道理但不是你想要的.您需要与s 关联的类型来约束矢量的结果类型.自然的方式是某种类型的家庭,但我不能在课堂上得到它.在任何情况下,使用推广的扩展类型(在ghc-7.4及更高版本中)可以更清楚地实现这种想法- 尽管您可能是故意避免扩展？这摆脱了令人讨厌的不受约束的角色,承认等等.如果你不想避免,那么你的模块可能看起来像这样:ghcvAppendPlusVNatvAppendVNatDataKindsVSuccVSucc CharDataKinds

{-#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.此外,我们可以看到两个实例完全指定它,但我不知道编译器可以使用多少.

Answer 2

类型签名中的所有类型变量都是普遍量化的.这意味着如果你说该函数有类型

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

那么对于任何选择n,m,nm和b,这种类型必须是有效的.特别是,例如,

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

也必须是您的函数的有效类型.但是,附加两个向量不具有这种通用类型.有约束nm,即nm类型级数n和的总和m.您必须在函数类型中表达这些约束,否则您将获得类型错误.

在你的情况下,GHC抱怨说,在你的定义中,nm实际上VZero,你正在假设nm你的类型表明你是不允许的.这~只是GHC的类型平等的象征.

Answer 3

当通过模式匹配在GADT的值上编写函数时,GHC在类型检查每个子句时使用有关函数运行时的预期行为的信息.您的vAppend函数只有一个子句,该模式匹配type的值Vec n b和另一个type 的值Vec m b.GHC的理由是,如果在运行时vAppend将其应用于既与模式匹配的实际参数T,那么实际参数的实际类型必须是形式Vec VZero b,这是一种比仅仅Vec n b或更具信息性的类型Vec m b.在GHC中实现这种推理的方式是,当类型检查RHS的唯一子句时vAppend,它会记录一个n必须确实实际上VZero,写入n ~ VZero和同样的假设m ~ VZero.

您为函数编写的类型列出了它必须满足的契约.您获得的错误消息是因为实现必须满足的合同vAppend过于笼统.您是说,鉴于一些长度的两个矢量n和m,vAppend必须产生可以被认为是一个向量的任何尺寸.实际上,GHC注意到您的实施不符合此合同,因为您的RHS的类型与RHS Vec 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与Plus VZero VZerofrom n ~ VZero和m ~ VZero.由于Plus VZero VZero是第一类家庭实例的形状,GHC知道它是相同的VZero.因此,在这个分支GHC期望一个类型的RHS Vec VZero b,我们可以很容易地构建!