当参数表明结果不应该存在时的依赖型设计

Question

这是的后续。

我定义了一个矩阵类型，其中dims中的每个自然定义了对应维度的大小。例如，对于某些类型 A，matrix A [3; 5; 2] 是一个 3x5x2 矩阵：

Require Import Coq.Unicode.Utf8.
Require Export Vector.
Import VectorNotations.
Require Import List.
Import ListNotations.

Fixpoint matrix (A: Type) (dims: list nat) :=
  match dims with
  | [] => A
  | head::tail => Vector.t (matrix A tail) head
  end.

我还定义了一个 get 函数，它在指定所有索引时访问矩阵的元素：

Fixpoint get {A: Type} {dims: list nat} (m: matrix A dims) (indexes: list nat): option A :=
  if Nat.eqb (length dims) (length indexes)
  then match dims, indexes return matrix A dims → option A with
       | [], [] => λ a, Some a
       | dimh::dimt, idxh::idxt => λ m',
           match Fin.of_nat (idxh - 1) dimh with
           | inleft H => @get A dimt (Vector.nth m' H) idxt
           | _ => None
           end
       | _, _ => λ _, None
       end m
  else None.

现在我想支持 MATLAB 风格的索引器，其中索引是标量或范围；特殊范围 : 表示“该维度中的所有对应元素”。此函数不需要处理 MATLAB 仅指定某些索引的能力；我们将假设提供了所有索引。一些例子：

>> A = rand(3,5,2)

A(:,:,1) =

    0.8147    0.9134    0.2785    0.9649    0.9572
    0.9058    0.6324    0.5469    0.1576    0.4854
    0.1270    0.0975    0.9575    0.9706    0.8003


A(:,:,2) =

    0.1419    0.7922    0.0357    0.6787    0.3922
    0.4218    0.9595    0.8491    0.7577    0.6555
    0.9157    0.6557    0.9340    0.7431    0.1712

>> size(A)

ans =

     3     5     2

>> A(1,1,1)

ans =

    0.8147

>> A(1,1,:)       

ans(:,:,1) =

    0.8147


ans(:,:,2) =

    0.1419

>> A(1,2:4,:)

ans(:,:,1) =

    0.9134    0.2785    0.9649


ans(:,:,2) =

    0.7922    0.0357    0.6787

我可以定义代表索引器的类型：

Inductive range: Type :=
  | Scalar: nat → range
  | Subrange: nat → nat → range
  | Fullrange.

但我遇到的困难是计算函数的结果类型。我最初的想法是定义一个函数 range_dimensions: list nat -> list range -> list nat ，范围列表中的每个标量给出一个维度 1 ，每个子范围给出子范围大小的维度，并且每个完整-range给出维度列表对应大小的一个维度（第一个参数）。

但是，当列表大小不同，或者子范围的一部分超出范围时（例如，Subrange 3 5 表示大小为 4 的维度），return没有好结果——换句话说，我更愿意有range_dimensions: list nat -> list range -> option (list nat)。但这提出了如何处理实际索引功能的问题：

Fixpoint get_range {A: Type} {dims: list nat} (m: matrix A dims) (indexes: list range): matrix A (range_dimensions dims indexes)

这行不通，因为类型不一致。我真正想要的是 return 一个 option (matrix A (range_dimensions dims indexes))，即当尺寸计算失败时 None，否则 Some …，但我看不到这样做的方法。当维度列表为 None:

时，option (matrix A …) 没有可输入的类型

Axiom range_dimensions_ex: option (list nat)
Check match range_dimensions_ex with
      | Some dims => matrix nat dims
      | None => option (matrix nat ???)
      end.

我认为这意味着我坚持使用我在 Certified Programming with Dependent Types 中看到的东西，即使用类似

的东西

Fixpoint get_range {A: Type} {dims: list nat} (m: matrix A dims) (indexes: list range):
match (range_dimensions dims indexes) with
| None => unit
| Some dims' => matrix A dims'
end

这似乎很难处理，特别是考虑到到目前为止我的其他矩阵函数 return option (matrix A …) 来指示索引失败，而不是 tt.

我是不是找错人了？是否有更准确地反映我的目标的设计？请注意，这是为了进入 MATLAB 语义的（非常小的）子集的表达式求值函数——如果我坚持使用 unit，我如何才能与 [=62] 的函数集成=]ing option?

Answer 1

在 Coq 中编程的一种通用方法是将依赖类型限制在规范中，而不是在程序中使用它们。

例如，矩阵可以表示为嵌套递归类型中的一对维度和内容

Inductive matrix_ :=
| Scalar : scalar -> matrix_
| Matrix : list matrix_ -> matrix_
.

Record matrix :=
  { dim : list nat
  ; contents : matrix_
  }.

然后您需要一些谓词来指定矩阵何时“合式”：

Definition well_formed : matrix -> Prop := ...

操作将具有简单类型：

Definition submatrix : matrix -> range -> matrix := ...

所有的复杂性都进入了规范：

Theorem submatrix_wf (m : matrix) (r : range)
  : well_formed m -> valid_range m r -> well_formed (submatrix m r).

Theorem submatrix_dim (m : matrix) (r : range)
  : well_formed m -> valid_range m r -> dim (submatrix m r) = dim_range r.

(* etc. *)

这是一个简单的表示
对于格式错误的输入，您可以简单地 return 垃圾而不显式 option（而对于更结构化的表示，甚至可能没有“垃圾”的空间）；如果您验证您的程序，就会发现错误。
您仍然可以获得静态类型的许多好处：不能混淆矩阵、标量、布尔值、维度...

主要的权衡是使用依赖类型的丰富表示免费提供格式良好的证明，但让程序进行类型检查可能是一项任意困难的任务。使用愚蠢的表示，您只能从程序本身获得最基本的健全性检查（仍然比实际的 MATLAB 多）。但是，通过自动化可以在很大程度上减轻单独证明的繁琐。

当参数表明结果不应该存在时的依赖型设计

Dependent-type design when the parameters indicate the result should not exist

matlab

matrix

optional

coq

dependent-type