Are types in Coq mutually exclusive?

3
votes

Question:

Are types in Coq mutually exclusive?

For example in the accepted answer for this question: What exactly is a Set in COQ
it is mentioned that "Set <= Type_0". (Does it mean that anything of type Set is also of type Type?)

On the other hand in the accepted answer for this question: Making and comparing Sets in Coq
it is mentioned that "each valid element of the language has exactly one type".

My motivation:

Relations in Coq (in Relations: Coq.Relations.Relation_Definitions) are defined as:

Variable A : Type.
Definition relation := A -> A -> Prop.

My intention was to express a restriction of a relation to some "smaller" B. If the types are mutually exclusive then it may make no sense.

1
coq

1 Answers

1
votes

In the sense asked, yes, types are exclusive.

You cannot express a restriction to some smaller B, at least not between sorts like Set/Prop/Type(0) - everything contained in one sort is also contained in larger sorts.

Subtyping in Coq is a little different from traditional languages. Set <= Type(0) means anything of type Set can be promoted to having type Type(0), not that it always has Type(0). Subtyping between sorts is explained in CIC/Sorts section of the Coq Manual.

However, if you are using Type Classes, you can define restriction of relations on subclasses! For example, you can define a type class which has the "+" operator and define a subclass where the "+" operator is associative.