当参数指示结果不应存在时，依赖类型设计

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风格的索引器，其中索引是标量或范围；特殊范围CCD_ 5表示"；该维度中的所有对应元素"此函数不需要处理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的维度，每个子范围都给出子范围大小的维度，而每个完整范围都给出维度列表相应大小的维度(第一个参数(。

然而，当列表的大小不同时，或者当子范围的一部分超出界限时(例如，对于大小为4的维度，Subrange 3 5(，没有好的结果返回——换句话说，我更喜欢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)

这行不通，因为类型不一致。我真正想要的是在维度计算失败时返回一个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.

我认为这意味着我在使用依赖类型的认证编程中看到了一些问题，那就是使用之类的东西

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

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

我是不是找错树了？有没有一种设计能更准确地反映我的目标？请注意，这是为了进入MATLAB语义的(非常小的(子集的表达式评估函数——如果我被unit卡住了，我怎么能与返回option的函数集成呢？

Answer 1

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

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

Inductive matrix_ :=
| Scalar : scalar -> matrix_
| Matrix : list matrix_ -> matrix_
.
Record matrix :=
{ dim : list nat
; contents : matrix_
}.

然后，您需要一些谓词来指定矩阵何时为"0"；形成良好的"：

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. *)

• 这是一个简单的表示
• 对于格式错误的输入，您可以简单地在没有显式option的情况下返回垃圾(而对于更结构化的表示，甚至可能没有"垃圾"的空间(；如果你验证你的程序，就会发现错误
• 静态类型仍然有很多好处：不能混淆矩阵、标量、布尔值、维度

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