CODEWITHSUNDEEP
typespolymorphismcoq
John
John

Reputation: 2042

Subtyping polymorphism in Coq

I want to define a weighted tree with variable fan-out which is polymorphic over types. I came up with this:

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

However, I would prefer to store the weight in a type, something like:

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.

where R is the set of real numbers from the standard library.

This doesn't work becuase Wtype is a Type->Type, not a Type, but I can't figure out how to do this. Unfortunately I still live in Object Oriented land and I really just want to give a more restrictive super type to A than Type, but just can't figure out how to do it in Coq.

Upvotes: 2

Views: 450

Answers (2)

daniel gratzer
daniel gratzer

Reputation: 53871

The problem is that Wtype is Type -> Type yes? Since we can't not apply it, we need to give it some sort of argument. So we need to apply it to some argument. A simple solution to this might be just

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

Upvotes: 2

John
John

Reputation: 2042

I guess i have solved this with: 

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.

However, it seems like it would be nicer to just be able to say something more like Inductive wtree (A : WType) ... and avoid cluttering up definition with lots of "Wtype A"'s all throughout the definition.

Upvotes: 1

Related Questions