haskell - 在 Dependent Haskell 中证明 m + (1 + n) == 1+ (m + n)
问题描述
我正在试验 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
当 GHC得知 m ~ Succ k (在第二种情况下匹配)时,我如何向 GHC 提供 Add mn = Succ (Add kn) in expression 的必要证明,并且是否有其他方法可以这样做。谢谢你。
解决方案
您对加法的定义不是传统的。
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))
推荐阅读
- shopify - Shopify 边框选择颜色
- assert - 微不足道的引理不能证明
- c++ - 多个默认构造函数
- c++ - C++ 使用未声明的标识符 IOKit 函数
- android - 在生产等待预定发布时向 Playstore 发布新的 Alpha
- python - 如何使用 python 套接字防止通过 wifi 丢失数据?
- c++ - AVL 平衡寻找何时平衡
- html - 是否所有 HTML 元素都允许所有 CSS 规则,它们都可以被继承吗?
- python-3.x - 基于 NetworkX 图节点颜色的图例
- php - 使用 PHP DOMDocument::loadXML 从 docx 文件导入数学方程和图像