haskell - 类型函数不能是单射的

Question

我试图证明一些关于奇数和偶数自然数的公理。我在证明中使用了三种定义的数据类型。

data Nat = Z | S Nat

data Even (a :: Nat) :: * where
  ZeroEven :: Even Z
  NextEven :: Even n -> Even (S (S n))

data Odd (a :: Nat) :: * where
  OneOdd :: Odd (S Z)
  NextOdd :: Odd n -> Odd (S (S n))

我还为加法和乘法定义了以下类型系列。

type family   Add (n :: Nat) (m :: Nat) :: Nat
type instance Add Z m = m
type instance Add (S n) m = S (Add n m)

type family   Mult (n :: Nat) (m :: Nat) :: Nat
type instance Mult Z m = Z
type instance Mult (S n) m = Add (Mult n m) n

我定义了函数来证明两个偶数之和是偶数以及两个偶数的乘积是偶数。

evenPlusEven :: Even n -> Even m -> Even (Add n m)
evenPlusEven ZeroEven m = m
evenPlusEven (NextEven n) m = NextEven (evenPlusEven n m)

evenTimesEven :: Even n -> Even m -> Even (Mult n m)
evenTimesEven ZeroEven m = ZeroEven
evenTimesEven (NextEven n) m = evenPlusEven (EvenTimesEven n m) n

我正在使用 GADTs、DataKinds、TypeFamilies 和 UndecidableInstances 语言扩展和 GHC 版本 7.10。 3.运行 evenPlusEven 给出了我期望的结果，但是当我包含 evenTimesEven 时，我收到编译错误。错误是:

Could not deduce (Add (Add (Mult n1 m) n1) ('S n1)
                  ~ Add (Mult n1 m) n1)
from the context (n ~ 'S ('S n1))
  bound by a pattern with constructor
             NextEven :: forall (n :: Nat). Even n -> Even ('S ('S n)),
           in an equation for `evenTimesEven'
  at OddsAndEvens.hs:71:16-25
NB: `Add' is a type function, and may not be injective
Expected type: Even (Mult n m)
  Actual type: Even (Add (Mult n1 m) n1)
Relevant bindings include
  m :: Even m
    (bound at OddsAndEvens.hs:71:28)
  n :: Even n1
    (bound at OddsAndEvens.hs:71:25)
  evenTimesEven :: Even n -> Even m -> Even (Mult n m)
    (bound at OddsAndEvens.hs:70:1)
In the expression: evenPlusEven (evenTimesEven n m) n
In an equation for `evenTimesEven':
    evenTimesEven (NextEven n) m = evenPlusEven (evenTimesEven n m) n

Mult 的类型族实例可以正常编译，如果我用错误抛出替换 evenTimesEven 的最后一行，我可以编译代码，并且该函数可以正常运行ZeroEven 的输入让我认为我的 Mult 实例是正确的，而我的 evenTimesEven 实现是问题所在，但我不确定为什么。

Even (Mult n m) 和 Even (Add (Mult n1 m) n1) 不应该具有相同的类型吗？

Answer 1

下面，我将滥用常见的数学符号。

from the context (n ~ 'S ('S n1))

由此，我们得到n = 2+n1。

Expected type: Even (Mult n m)

我们需要证明n*m偶数，即(2+n1)*m偶数。

Actual type: Even (Add (Mult n1 m) n1)

我们已经证明了(n1*m)+n1。这不一样。附加项应该是m，而不是n1，并且应该添加两次。