在 Dependent Haskell 中证明 m + (1 + n) == 1+ (m + n)

Question

我正在试验 Haskell 的类型系统，想编写一个类型安全的附加函数。这个函数应该接受两个代表数字的单例见证和 returns 一个数字的单例见证，其类型证明它确实是参数的总和。这是代码：

{-# language TypeFamilies, KindSignatures, DataKinds, PolyKinds, UndecidableInstances, GADTs #-}

data Nat = Zero | Succ Nat deriving Show
type family Add (m :: Nat) (n :: Nat) :: Nat where
  Add Zero n = n
  Add (Succ m) n = Add m (Succ n)

data SNat :: Nat -> * where
  Zy :: SNat Zero
  Suc :: SNat m -> SNat (Succ m)

data Bounded' m = B m

sum' :: Bounded' (SNat m) -> Bounded' (SNat n) -> Bounded' (SNat (Add m n))
sum' (B m) (B n) = B $ case (m, n) of
                    (Zy,x) -> x
                    (Suc x, y) -> let B z = sum' (B x) (B y) in Suc z

这是错误：

    • Could not deduce: Add m1 ('Succ n) ~ 'Succ (Add m1 n)
      from the context: m ~ 'Succ m1
      bound by a pattern with constructor:
               Suc :: forall (m :: Nat). SNat m -> SNat ('Succ m),
               in a case alternative
      at main.hs:17:22-26
      Expected type: SNat (Add m n)
      Actual type:   SNat ('Succ (Add m1 n))
    • In the expression: Suc z
      In the expression: let B z = sum' (B x) (B y) in Suc z
      In a case alternative:
        (Suc x, y) -> let B z = sum' (B x) (B y) in Suc z

我理解错误信息。当 GHC 知道 m ~ Succ k（在第二种情况下匹配）时，我如何向 GHC 提供必要的证明 Add m n = Succ (Add k n) in expression Suc z 并且是否有其他方法可以这样做。谢谢。

Answer 1

你对加法的定义不是常规的

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

这是一个 "tail recursive" 添加。看起来确实应该有一种方法可以使用这种加法形式来证明您的属性，但我无法弄清楚。在那之前，type/property 级别的尾递归往往比标准类型更难处理：

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

加法的后一个定义使你的 sum' 毫无说服力地通过了。

编辑实际上，一旦我看对了就很容易了。这是我得到的（导入 Data.Type.Equality 并启用 LANGUAGE TypeOperators）：

propSucc2 :: SNat m -> SNat n -> Add m (Succ n) :~: Succ (Add m n)
propSucc2 Zy _ = Refl
propSucc2 (Suc m) n = propSucc2 m (Suc n)

尾递归定义，尾递归证明。然后使用它，你使用 gcastWith:

sum' (B m) (B n) = ...
        (Suc x, y) -> gcastWith (propSucc2 x y) 
                                (let B z = sum' (B x) (B y) in Suc z)

gcastWith 只需要一个 :~: 相等性，并使其在第二个参数的范围内可供类型检查器使用。

顺便说一句，如果您在 Add 类型族的并行结构中定义 sum'，则不需要任何引理。让事情遵循并行结构是一种让事情变得简单的好技术（这是依赖编程艺术的一部分，因为它并不总是很明显）：

sum' :: Bounded' (SNat m) -> Bounded' (SNat n) -> Bounded' (SNat (Add m n))
sum' (B Zy) (B n) = B n
sum' (B (Suc m)) (B n) = sum' (B m) (B (Suc n))

在 Dependent Haskell 中证明 m + (1 + n) == 1+ (m + n)

Proving m + (1 + n) == 1+ (m + n) in Dependent Haskell

haskell

dependent-type