从属类型：在归纳类型中强制执行全局属性
Dependent types: enforcing global properties in inductive types
我有以下归纳类型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 ::不知道这个事实。它将首先用 k = 1 构建一个 MyVec，然后用 2，最后用 3。这使得无法根据值的最终形状定义约束。
例如，我无法将值限制为严格小于 k。接受 Fin (S k) 的 Vect 而不是 Nat 的 Vect 会排除一些有效值，因为最后的向量（由 ctor 插入的第一个向量）会 "know" k 的较小值，因此更严格的约束。
或者，另一个例子，我不能强制执行以下约束：位置 i 的向量不能包含数字 i。因为向量在容器中的最终位置是 ctor 不知道的（如果知道 k 的最终值，它会自动知道）。
所以问题是，我如何强制执行此类全局属性？
有（至少）两种方法可以做到这一点，这两种方法都可能需要跟踪附加信息才能检查 属性。
强制执行 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]]
此解决方案的关键是在 MyVec 的定义中将向量类型与 k 分开，然后在顶层使用 [=16= 的“全局值” ] 来约束向量元素的类型。
位置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 定义以跟踪必要的信息。在这种情况下，我们想跟踪 final 值中的当前位置。我称之为 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)
我有以下归纳类型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 ::不知道这个事实。它将首先用 k = 1 构建一个 MyVec，然后用 2，最后用 3。这使得无法根据值的最终形状定义约束。
例如，我无法将值限制为严格小于 k。接受 Fin (S k) 的 Vect 而不是 Nat 的 Vect 会排除一些有效值，因为最后的向量（由 ctor 插入的第一个向量）会 "know" k 的较小值，因此更严格的约束。
或者，另一个例子，我不能强制执行以下约束：位置 i 的向量不能包含数字 i。因为向量在容器中的最终位置是 ctor 不知道的（如果知道 k 的最终值，它会自动知道）。
所以问题是，我如何强制执行此类全局属性？
有（至少）两种方法可以做到这一点，这两种方法都可能需要跟踪附加信息才能检查 属性。
强制执行 data 定义中的属性
强制所有元素< k
I cannot constrain the values to be strictly less than
k. AcceptingVects ofFin (S k)instead ofVects ofNatwould 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]]
此解决方案的关键是在 MyVec 的定义中将向量类型与 k 分开，然后在顶层使用 [=16= 的“全局值” ] 来约束向量元素的类型。
位置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 定义以跟踪必要的信息。在这种情况下，我们想跟踪 final 值中的当前位置。我称之为 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)