5

假设我有一个数据类型

data Interval :: Nat -> Nat -> * where
  Go :: Interval m n -> Interval m (S n)
  Empty :: SNat n -> Interval n n

这些是半（右）开区间。Nat是标准的归纳自然数，SNat是相应的单例。

现在我想得到一个Nat给定间隔长度的单例：

intervalLength :: Interval n (Plus len n) -> SNat len
intervalLength Empty = Z
intervalLength (Go i) = S (intervalLength i)

这不起作用，因为该Plus函数不是单射的。我可能可以像这样定义它

intervalLength :: Interval m n -> SNat (Minus n m)

但我猜这需要一些引理（和额外的约束）。此外，我的间隔以前一种形式出现。

背景：我尝试在 Omega 中执行此操作，但没有成功（我提交了 omega 错误）

此外，如何使用修改后的类型检查器来破解这些问题？供应的 RHS 能否对 LHS 模式的类型方程提供关键提示，从而消除非内射性？

Agda 程序员如何解决这些问题？

4

2 回答 2

13

这是我的程序版本。我在用着

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies #-}

我有Nat它的单身人士

data Nat = Z | S Nat

data SNat :: Nat -> * where
  ZZ :: SNat Z
  SS :: SNat n -> SNat (S n)

你的Interval类型对我来说更熟悉“小于或等于”的“后缀”定义：“后缀”，因为如果你从数字升级到列表并S用一个元素标记每个列表，你就会有一个定义列表后缀。

data Le :: Nat -> Nat -> * where
  Len :: SNat n -> Le n n
  Les :: Le m n -> Le m (S n)

这是补充。

type family Plus (x :: Nat) (y :: Nat) :: Nat
type instance Plus Z     y  = y
type instance Plus (S x) y  = S (Plus x y)

现在，您的难题是计算Les某个Le值中的构造函数，提取单例以获取其索引之间的差异。与其假设我们正在使用一些Le n (Plus m n)并尝试计算 a SNat m，我将编写一个函数来计算任意 Le m o-indices 之间的差异并建立与 的连接Plus。

这是 的加法定义Le，提供了单例。

data AddOn :: Nat -> Nat -> * where
  AddOn :: SNat n -> SNat m -> AddOn n (Plus m n)

我们可以很容易地确定这Le意味着AddOn。一些模式匹配AddOn n o显示o为Plus m n一些m，并为我们提供我们想要的单例。

leAddOn :: Le m o -> AddOn m o
leAddOn (Len n) = AddOn n ZZ
leAddOn (Les p) = case leAddOn p of AddOn n m -> AddOn n (SS m)

更一般地说，我建议制定依赖类型的编程问题，以尽量减少您计划匹配的类型索引中已定义函数的存在。这避免了复杂的统一。（警句用于将此类函数着色为绿色，因此建议“不要触摸绿色粘液！”。）Le n o事实证明（因为这是 的重点leAddOn），信息量不亚于 类型Le n (Plus m n)，但它更容易匹配。

更一般地说，设置一个从属数据类型来捕获您的问题的逻辑，但使用起来绝对是可怕的，这是一种非常正常的体验。这并不意味着捕获正确逻辑的所有数据类型都将绝对难以使用，只是您需要更加仔细地考虑定义的人机工程学。让这些定义变得整洁并不是很多人在普通函数式编程学习经验中学到的技能，所以期待攀登一个新的学习曲线。

于 2012-11-25T22:30:09.733 回答
8

我在伊德里斯尝试过这个。虽然我同意 pigworker 重新制定问题的建议，但您必须这样做才能使您的定义通过 Idris 类型检查器。首先，单例 Nats：

data SNat : Nat -> Set where
   ZZ : SNat O
   SS : SNat k -> SNat (S k)

然后，区间的定义：

data Interval : Nat -> Nat -> Set where
  Go : Interval m n -> Interval m (S n)
  Empty : SNat n -> Interval n n

您想要的 intervalLength 定义看起来有点像这样：

intervalLength : Interval n (plus len n) -> SNat len
intervalLength (Empty sn) = ZZ
intervalLength (Go i)     = SS (intervalLength i)

但是你会遇到麻烦，因为正如你所说plus的不是单射的。我们可以通过len显式地进行额外的模式匹配来到达某个地方——然后统一可以取得一些进展：

intervalLength : Interval n (plus len n) -> SNat len
intervalLength {len = O}   (Empty sn) = ZZ
intervalLength {len = S k} (Go i)     = SS (intervalLength i)

这很好，并且通过了类型检查器，但不幸的是它不相信该功能是完整的：

*interval> :total intervalLength
not total as there are missing cases

缺少的案例是这个：

intervalLength {len = O}   (Go i)     = ?missing

如果你尝试这个，并询问 REPL 的类型missing，你会看到：

missing : (n : Nat) -> (i : Interval (S n) n) -> SNat O

现在，我们知道类型Interval (S n) n是空的，但是类型检查器却没有。不知何故我们需要写badInterval : Interval (S n) n -> _|_，然后我们可以说：

intervalLength {len = O}   (Go i)     = FalseElim (badInterval i)

我将把定义badInterval作为练习:-)。这不是特别棘手，但不得不这样做有点无聊 - 有时很难避免不得不使用这种类型的类型，但实施badInterval支持 pigworker 不这样做的建议！

于 2012-11-25T23:26:18.117 回答