如何返回正确的依赖类型？

问题描述 投票：0回答：1

研究依赖类型的应用，我发现了以下依赖向量的定义。

Inductive vector(A: Type): nat -> Type :=
  empty_vector: vector A 0
  | nonempty_vector: forall (n: nat), A -> vector A n -> vector A (S n).

我希望编写返回与输入向量相同类型向量的函数。 这个非常简单的效果很好：

Definition fnc1(n: nat) (v: vector bool n): Type :=
vector bool n.

但是，将返回类型指定为 

vector bool n
会产生错误：

Definition fnc2(n: nat) (v: vector bool n): vector bool n :=
vector bool n.

In environment
n : nat
v : vector bool n
The term "vector bool n" has type "Set"
while it is expected to have type "vector bool n".

现在这个也可以了：

Definition fnc3(n: nat) (v: vector bool n): vector bool n :=
v.

fnc2 有什么问题吗？

谢谢你。

coq
1个回答
0
投票

正如评论中提到的：罪魁祸首是你的 

:= vector bool n
代码，因为你不能同时使用 
vector bool n
作为返回类型和返回值。更一般地说，对于相同的表达式 
T : T
，我们不能使用 
T
。

如果你想构建一个具有

vector bool n
类型的值（这是一个带有两个构造函数的归纳类型），你可以只使用构造函数:

Definition example1 := @nonempty_vector bool 1 true (@nonempty_vector bool 0 true (@empty_vector bool)).

您还可以在另一种归纳类型（例如

nat
）上使用模式匹配+固定点（递归函数）来构建例如一个“常数向量”。

即：

Set Implicit Arguments.

Inductive vector(A: Type): nat -> Type :=
  empty_vector: vector A 0
| nonempty_vector: forall (n: nat), A -> vector A n -> vector A (S n).

Fixpoint const_n (b : bool) (n : nat) : vector bool n :=
  match n with
  | 0 => empty_vector bool
  | S p => nonempty_vector b (const_n b p)
  end.

Eval compute in const_n true 2.
(* = nonempty_vector true (nonempty_vector true (empty_vector bool))
   : vector bool 2
 *)

免责声明：虽然以这种方式定义的向量是开始学习依赖类型的简单/有用的示例，但实际上不建议在生产中使用它们，因为在 Coq 中有更成功的方法可以将它们形式化。参见例如评论于：

最新问题
© www.soinside.com 2019 - 2024. All rights reserved.