types - Coq 中的子类型多态性

Question

我想定义一个带有可变扇出的加权树，它是类型上的多态。我想出了这个:

(* Weighted tree with topological ordering on the nodes. *)
Inductive wtree (A : Type) : Type :=
  LNode : A->wtree A
| INode : A->list (R*wtree A) -> wtree A.

但是，我更愿意将重量存储在一种类型中，例如:

Inductive Wtype (A : Type) : Type := W : R->A->Wtype A.
Inductive wtree (A : Wtype) : Type :=
  LNode : A->wtree A
| INode : A->list (wtree A) -> wtree A.

哪里 R是标准库中的实数集。

这不起作用，因为 Wtype是 Type->Type ，不是 Type ，但我不知道如何做到这一点。不幸的是，我仍然生活在面向对象的领域，我真的只想给 A 一个更严格的父类(super class)型。比 Type ，但就是不知道如何在 Coq 中做到这一点。

Answer 1

问题是Wtype是 Type -> Type是吗？既然我们不能不应用它，我们需要给它某种论证。所以我们需要把它应用到一些论证上。一个简单的解决方案可能只是

Inductive wtree' (A : Type) : Type :=
| LNode : A -> wtree' A
| INode : A -> list (wtree' A) -> wtree A.

Inductive Wtype (A : Type) : Type := W : R -> A -> Wtype A.

Definition wtree (A : Type) := wtree' (Wtype A).