Haskell 无法统一类型​​实例方程

Question

我正在尝试使用(偶数/奇数)奇偶校验类型标记规范的 Nat 数据类型，以查看我们是否可以获得任何免费定理。这是代码:

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

-- Use DataKind promotion with type function for even-odd

module EvenOdd where

  data Parity = Even | Odd
  -- Parity is promoted to kind level Parity.
  -- Even & Odd to type level 'Even & 'Odd of kind Parity

  -- We define type-function opp to establish the relation that
  -- type 'Even is opposite of 'Odd, and vice-versa
  type family Opp (n :: Parity) :: Parity
  type instance Opp 'Even = 'Odd
  type instance Opp 'Odd = 'Even

 -- We tag natural number with the type of its parity
  data Nat :: Parity -> * where
     Zero :: Nat 'Even
     Succ :: Nat p -> Nat (Opp p)

  -- Now we (should) get free theorems.
  -- 1. Plus of two even numbers is even
  evenPlus :: Nat 'Even -> Nat 'Even -> Nat 'Even
  evenPlus Zero n2 = n2  -- Line 31
  evenPlus (Succ (Succ n1)) n2 = Succ (Succ (evenPlus n1 n2))

但是，GHC 抛出类型错误:

Could not deduce (p1 ~ 'Even)
from the context ('Even ~ Opp p)
  bound by a pattern with constructor
             Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
           in an equation for `evenPlus'
  at even-odd.hs:31:13-26
or from (p ~ Opp p1)
  bound by a pattern with constructor
             Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
           in an equation for `evenPlus'
  at even-odd.hs:31:19-25
  `p1' is a rigid type variable bound by
       a pattern with constructor
         Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
       in an equation for `evenPlus'
       at even-odd.hs:31:19
Expected type: Nat 'Even
  Actual type: Nat p
In the first argument of `evenPlus', namely `n1'
In the first argument of `Succ', namely `(evenPlus n1 n2)'

据我了解，上述错误的要点是，当上下文具有等式时，GHC 无法推导出 (p1 ~ 'Even):((Opp (Opp p1)) ~ 'Even)。

为什么会发生这种情况？我的方法有问题吗？

Answer 1

我不认为 GADT 模式匹配改进是这样工作的。您有 Opp p作为构造函数的结果类型。所以如果你写类似的东西

f :: Nat 'Even -> ...
f (Succ n) = ...

然后类型检查器知道 Nat (Opp t) ~ Nat 'Even因此 Opp t ~ 'Even .但是要解决这个问题，类型检查器必须反转函数 Opp ，这要求很多。

我建议你改变 Nat的定义说:

data Nat :: Parity -> * where
  Zero :: Nat 'Even
  Succ :: Nat (Opp p) -> Nat p

这应该可以正常工作。

编辑

实际上，让我稍微扩展一下。

上面的建议并非没有(次要)价格。你失去了一些类型推断。例如 Succ Zero的类型现在是 Succ Zero :: Opp p ~ 'Even => Nat p而不是 Nat 'Odd .使用显式类型注释，它可以解决。

您可以通过向 Succ 添加约束来改进这一点。这需要 Opp是自逆。 Parity的唯一两个元素是 Even和 Odd ，并且对于这些约束保持不变，因此它永远不会引起任何问题:

data Nat :: Parity -> * where
  Zero :: Nat 'Even
  Succ :: (Opp (Opp p) ~ p) => Nat (Opp p) -> Nat p

现在 Succ Zero推断为 Nat 'Odd 类型，并且模式匹配仍然有效。