代码之家 › 专栏 › 技术社区 › lodo

依赖类型:在归纳类型中强制全局属性

idris dependent-type

lodo · 技术社区 · 7 年前

我有以下归纳类型 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]]

问题是, val k = 3 ( k 是一个 :: 不知道这个事实。它将首先构建一个 MyVec公司 k = 1 2 ,最后 3

例如,我不能将值严格限制为小于 k Vect 第页,共页 Fin (S k) 而不是 Vect Nat 将排除一些有效值,因为最后一个向量(由ctor插入的第一个向量)“知道”的值较小因此是一个更严格的限制。

或者,另一个例子是,我无法强制执行以下约束: 位置i处的向量不能包含数字i . 因为向量在容器中的最终位置对于向量变换器来说是未知的(如果k的最终值已知,则会自动知道)。

1 回复 | 直到 7 年前

James Wilcox 7 年前

有(至少)两种方法,这两种方法都可能需要跟踪其他信息以检查属性。

在中强制执行属性 `data` 释义

强制执行所有元素 `< k`

我不能将值严格限制为小于 k Vect 第页,共页 Fin (S k) Vect Nat 将排除一些有效值。。。

你是对的,仅仅改变 MyVect 拥有 Vect n (Fin (S k)) 这是不对的。

多态性,如下所示。

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 约束向量元素的类型。

在位置强制向量 `i` `一、`

我不能强制位置I处的向量不能包含数字I,因为构造函数不知道向量在容器中的最终位置。

数据 跟踪必要信息的定义。在这种情况下,我们希望跟踪当前位置在 最终的 价值将为。我称之为 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)]]

事后强制执行属性

另一种有时更简单的方法是立即强制执行定义,但在事实之后写一个谓词。

强制执行所有元素 `<`

例如,我们可以编写一个谓词来检查是否所有向量的所有元素都是 <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)

`一、` 不包含 `一、`

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)

依赖类型:在归纳类型中强制全局属性

在中强制执行属性 data 释义

强制执行所有元素 < k

在位置强制向量 i 一、