haskell - GADT 和 ScopedTypeVariables/PatternSignatures 之间的交互

Question

我正在探索长度索引向量的“陈腐”示例，代码改编自 Richard Eisenberg's thesis 3.1节

{-# LANGUAGE  GADTs, TypeFamilies, DataKinds, KindSignatures,
              TypeOperators, ScopedTypeVariables  #-}
                          -- PatternSignatures  -- deprecated

import GHC.Types (Type)

data Nat = Zero | Succ Nat
data Vec :: Type -> Nat -> Type  where
  Nil :: Vec a Zero                       -- E has 'Zero
  (:>) :: a -> Vec a n -> Vec a (Succ n)  -- E has 'Succ
infixr 5 :>

type family (+) (n :: Nat) (m :: Nat) :: Nat  where
  (+) Zero      m = m
  (+) (Succ n') m = Succ (n' + m)

append :: Vec a n -> Vec a m -> Vec a (n + m)
append (Nil     :: Vec aa Zero) (w :: Vec aa mm) = w :: Vec aa (Zero + mm)
append (x :> (v :: Vec a n'))   (w :: Vec a m)   = x :> ((append v w) :: Vec a (n' + m))

append Nil ... 等式被拒绝(GHC 8.6.5)

* Couldn't match type `m' with `n + m'
  `m' is a rigid type variable bound by
    the type signature for:
      append :: forall a (n :: Nat) (m :: Nat).
                Vec a n -> Vec a m -> Vec a (n + m)
    at ...
  Expected type: Vec a (n + m)
    Actual type: Vec a ('Zero + m)

将结果类型作为 ::Vec aa mm 也被拒绝。

  Expected type: Vec a (n + m)
    Actual type: Vec a m

很奇怪，因为这是被接受的(见下文)。

我真正想做的是使用 PatternSignatures 作为 append 的参数。但是该扩展已被弃用，我必须使用 ScopedTypeVariables。这意味着 append 签名中的 tyvars 在方程式的范围内。所以我使用了新的 tyvar 名称。

GADT 给 Nil::Vec 一个零，所以我把它作为它的模式签名(带有新的 aa)。但似乎 GHC 无法将 append 签名中的 n 与 Zero 统一起来。如果我将该等式更改为其中任何一个，一切都会很高兴:

append (Nil     :: Vec aa nn) (w :: Vec aa mm) = w :: Vec aa (nn + mm)

append (Nil     :: Vec aa nn) (w :: Vec aa mm) = w :: Vec aa (mm)

为了验证这些，GHC 必须从 + 的类型族方程中计算出 Nil::Vec a Zero 和 Zero + m = m 。那么，为什么它对带有 Zero 的模式签名感到不满呢？

(我最初试图用 PatternSignatures 给出 append 的等式，看看 GHC 是否可以推断签名。那没有成功。 )

Answer 1

首先要注意的是，您显示的错误并不是您遇到的唯一错误，实际上，它也不是最重要的错误。您应该看到的另一个错误是:

    * Couldn't match type `n' with 'Zero
      `n' is a rigid type variable bound by
        the type signature for:
          append :: forall a (n :: Nat) (m :: Nat).
                    Vec a n -> Vec a m -> Vec a (n + m)
        at ...
      Expected type: Vec a n
        Actual type: Vec a 'Zero
    * When checking that the pattern signature: Vec a 'Zero
        fits the type of its context: Vec a n
      In the pattern: Nil :: Vec a Zero

这里的关键部分是“当检查模式签名是否符合其上下文的类型时”。事实上，模式的类型 Nil不只是 Vec a Zero ;它实际上类似于 () => (n ~ Zero) => Vec a n .此类型表示模式可能匹配Vec a n 类型的任何内容, 如果匹配，则约束 n ~ Zero被纳入范围。另一方面，类型为 Vec a Zero 的模式类型限制为仅适用于类型 Vec a Zero .在你的定义中 append , 输入的类型为 Vec a n , 所以一个 Vec a Zero 类型的模式不匹配。

(您可以阅读更多关于模式同义词类型的内容，这可能会有所启发，in the docs。)

---

通过更简单的示例和模式同义词的使用，这可能更容易理解。

考虑这种类型和功能:

data Foo a where
  Bar :: Foo Int
  Baz :: Foo Char

doFoo :: Foo a -> a
doFoo Bar = 1
doFoo Baz = 'c'

一切顺利。但是，如果我们把第六行改成

doFoo (Bar :: Foo Int) = 1

然后我们将得到一个与您在 append 中看到的非常相似的错误.现在让我们来研究一下模式同义词。如果我们在 Bar 周围有一个模式同义词怎么办？使用简单类型 Foo Int :

{-# LANGUAGE PatternSynonyms #-}
pattern BarInt :: Foo Int
pattern BarInt = Bar

如果我们在 doFoo 中使用它，我们得到模式类型不匹配的相同错误。这确实有意义，因为此模式仅针对 Foo Int 类型的输入定义。而不是一般的 Foo a .让我们尝试另一种变体:

pattern BarA :: Foo a
pattern BarA <- Bar

注意 <- 的使用这里不是 = ，使它成为单向模式同义词而不是双向模式。我们必须这样做，因为虽然我们可以“忘记”Int然后从 Foo Int 开始到 Foo a ，我们不能反其道而行之。但是，如果我们尝试使用 BarA 会发生什么？在 doFoo ？现在我们得到这样的错误:

    * Couldn't match expected type `a' with actual type `Int'
      `a' is a rigid type variable bound by
        the type signature for:
          dofoo :: forall a. Foo a -> a

这个模式足够松散，可以被接受，但是模式匹配之后，我们仍然不知道a , 所以我们不能返回 Int .

真正重现 Bar模式，我们需要写:

pattern Bar' :: () => (a ~ Int) => Foo a
pattern Bar' = Bar

在这里，我们的模式类型表明没有提前应用模式的限制(初始 () => )，匹配后我们将知道 a ~ Int ，并且此模式可以匹配 Foo a 形式的任何内容.