dependent-type - 从属类型:强制归纳类型的全局属性

我有以下归纳类型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)而不是Vect的Nat会排除一些有效值，因为最后一个矢量（由ctor插入的第一个）会“知道”一个较小的k值，因此有更严格的约束。

或者，另一个示例，我不能强制执行以下约束：位置i处的向量不能包含数字i。因为矢量在容器中的最终位置对于控制器来说是未知的（如果知道k的最终值，它将自动知道）。

所以问题是，我该如何强制这些全局属性？

最佳答案

有（至少）两种方法，两种方法都可能需要跟踪其他信息才能检查该属性。

在data定义中强制执行属性

强制所有元素< k


我不能将值限制为严格小于k。接受Vect的Fin (S k)而不是Vect的Nat会排除一些有效值...


没错，只是将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上的向量不能包含数字i，因为构造函数不知道容器中向量的最终位置。


同样，解决方案是对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)