类型函数可能不是单射的

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,应该添加两次.