haskell - 如何获得依赖类型间隔的长度？

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

此外，如何使用修改后的类型检查器来破解这些问题？供应的 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 中的构造函数-value，提取单例以获取其索引之间的差异。而不是假设我们正在处理一些 Le n (Plus m n)并尝试计算 SNat m , 我要写一个函数来计算任意 Le m o 之间的差异-索引并建立与 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) ，但它更容易匹配。

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