如何获得依赖类型区间的长度？

Question

说我有一个数据类型

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

这些问题怎么可能被修改过的类型控制器破解？供应的RHS能否对LHS模式的类型方程提出至关重要的暗示,以便非内射性抵消？

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

Answer 1

这是我的程序版本.我正在使用

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

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

更一般地说,我建议制定依赖类型编程问题,尽量减少计划匹配的类型索引中已定义函数的存在.这避免了复杂的统一.(Epigram用于将这些功能着色为绿色,因此建议"不要触摸绿色粘液!".)Le n o,事实证明(因为这是重点leAddOn),一个类型的信息量并不逊色Le n (Plus m n),但它相当容易匹配.

更一般地说,设置依赖数据类型是一种非常正常的体验,这种数据类型可以捕获问题的逻辑但是使用起来非常可怕.这并不意味着捕获正确逻辑的所有数据类型都将非常可怕地使用,只是您需要更加思考定义的人体工程学.让这些定义变得整洁不是很多人在普通的功能编程学习体验中获得的技能,因此期望攀登新的学习曲线.

Answer 2

我在伊德里斯做了一件事.虽然我同意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)

这很好,并且超过了typechecker,但遗憾的是它不相信该函数是完全的:

*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建议不要这样做!