类型函数可能不是单射的

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，并且应添加两次。