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)