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一個更具限制性的超類型，而不是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). 

Answer 2

我想我有一個解決了這個：

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

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

然而，現在看來似乎會更好，只是可以說更多的東西一樣Inductive wtree (A : WType) ...，避免與大量的「Wtype A」搞亂了定義」在整個定義中。