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

Question

我正在试验Haskell的类型系统,并希望编写一个类型安全的附加功能.这个函数应该接受两个表示数字的单身证人,并返回一个数字的单身证人,其类型带有证明它确实是参数的总和.这是代码:

{-# 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

我理解错误信息.当我Suc z知道m~Succ k(在第二种情况下是匹配)时,如何为GHC提供表达式中添加mn = Succ(Add kn)的必要证据,并且有其他方法可以做到这一点.谢谢.

Answer 1

您对添加的定义不是常规定义.

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

这是一个"尾递归"的补充.看起来似乎应该有一种方法来证明你的属性使用这种形式的添加,但我无法弄清楚.在此之前,类型/属性级别的尾递归往往比标准类型更难处理:

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只需要:~:相等并使其在第二个参数范围内可用于类型检查器.

顺便说一句,如果你sum'在Add类型系列的并行结构中定义,那么你不需要任何引理.让事情遵循并行结构是保持简单易用的一种好方法(这是依赖编程艺术的一部分,因为它并不总是很明显如何):

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))