dependent-type - 依赖类型 : enforcing global properties in inductive types

Question

我有以下感应式MyVec :

import Data.Vect

data MyVec: {k: Nat} -> Vect k Nat -> Type where
  Nil: MyVec []
  (::): {k, n: Nat} -> {v: Vect k Nat} -> Vect n Nat -> MyVec v -> MyVec (n :: v)

-- example:
val: MyVec [3,2,3]
val = [[2,1,2], [0,2], [1,1,0]]

也就是说，类型指定了 MyVec 中所有向量的长度。 .

问题是， val将有 k = 3 ( k 是 MyVec 内的向量数)，但ctor ::不知道这个事实。它将首先构建一个 MyVec与 k = 1 ，然后用 2 ，最后是 3 .这使得无法根据值的最终形状定义约束。

例如，我不能限制这些值严格小于 k .接受 Vect Fin (S k)的s而不是 Vect Nat的s会排除一些有效值，因为最后一个向量(构造函数插入的第一个向量)会“知道”较小的值 k ，因此有更严格的约束。

或者，另一个例子，我不能强制执行以下约束:位置 i 处的向量不能包含数字 i。因为 ctor 不知道容器中向量的最终位置(如果知道 k 的最终值，它将自动知道)。

所以问题是，我怎样才能强制执行这样的全局属性？

Answer 1

有(至少)两种方法可以做到，这两种方法都可能需要跟踪附加信息以检查属性(property)。

强制执行 data 中的属性定义

强制执行所有元素 < k

I cannot constrain the values to be strictly less than k. Accepting Vects of Fin (S k) instead of Vects of Nat would rule out some valid values...

您是对的，只需更改 MyVect 的定义即可。有 Vect n (Fin (S k))在它不会是正确的。

然而，通过概括 MyVect 来解决这个问题并不太难。是多态的，如下。

data MyVec: (A : Type) -> {k: Nat} -> Vect k Nat -> Type where
  Nil: {A : Type} -> MyVec A []
  (::): {A : Type} -> {k, n: Nat} -> {v: Vect k Nat} -> Vect n A -> MyVec A v -> MyVec A (n :: v)

val : MyVec (Fin 3) [3,2,3]
val = [[2,1,2], [0,2], [1,1,0]]

此解决方案的关键是将向量的类型与 k 分开。在 MyVec的定义中，然后在顶层，使用“全局值 k”来约束向量元素的类型。

在位置执行向量 i不包含 i

I cannot enforce that the vector at position i cannot contain the number i because the final position of a vector in the container is not known to the constructor.

同样，解决方案是概括 data定义以跟踪必要的信息。在这种情况下，我们希望跟踪最终值中的当前位置。我叫这个 index .然后我概括 A传递当前索引。最后，在顶层，我传入一个谓词，强制该值不等于索引。

data MyVec': (A : Nat -> Type) -> (index : Nat) -> {k: Nat} -> Vect k Nat -> Type where
  Nil: {A : Nat -> Type} -> {index : Nat} -> MyVec' A index []
  (::): {A : Nat -> Type} -> {k, n, index: Nat} -> {v: Vect k Nat} ->
        Vect n (A index) -> MyVec' A (S index) v -> MyVec' A index (n :: v)

val : MyVec' (\n => (m : Nat ** (n == m = False))) 0 [3,2,3]
val = [[(2 ** Refl),(1 ** Refl),(2 ** Refl)], [(0 ** Refl),(2 ** Refl)], [(1 ** Refl),(1 ** Refl),(0 ** Refl)]]

事后强制执行属性

另一种有时更简单的方法是不立即在 data 中强制执行该属性。定义，而是在事后写一个谓词。

强制执行所有元素 < k
例如，我们可以编写一个谓词来检查所有向量的所有元素是否都是 < k ，然后断言我们的值具有这个属性。

wf : (final_length : Nat) -> {k : Nat} -> {v : Vect k Nat} -> MyVec v -> Bool
wf final_length [] = True
wf final_length (v :: mv) = isNothing (find (\x => x >= final_length) v) && wf final_length mv

val : (mv : MyVec [3,2,3] ** wf 3 mv = True)
val = ([[2,1,2], [0,2], [1,1,0]] ** Refl)

在位置执行向量 i不包含 i
同样，我们可以通过检查属性来表达属性，然后断言该值具有该属性。

wf : (index : Nat) -> {k : Nat} -> {v : Vect k Nat} -> MyVec v -> Bool
wf index [] = True
wf index (v :: mv) = isNothing (find (\x => x == index) v) && wf (S index) mv

val : (mv : MyVec [3,2,3] ** wf 0 mv = True)
val = ([[2,1,2], [0,2], [1,1,0]] ** Refl)