I implemented a simple type system inside Agda and I'm trying to understand, how expressive it is. The system consists from a predicative hierarchy of universes in the style of Russell, natural numbers and bounded and unbounded dependent quantifiers (there were reasons to separate these two instead of just adding an alias for
∀ A <: Top -> ...). It also permits writing universe polymorphic code, for example it's possible to represent the following functions, written in Agda:
id : ∀ α -> (A : Set α) -> A -> A id _ _ x = x Set' : ∀ α -> Set (suc α) Set' α = Set α
Subtyping rules are
ℕ <: ℕ
α' ≤ α -> Type α' <: Type α
(∀ x -> B' x <: B x) -> Π A B' <: Π A B
The last rule holds for both bounded and unbounded quantifiers.
- the subtyping rule for product types is covariant only
- there is no the subsumption rule
x : A, A <: B -> x : B
- there is no the rule
∀ A -> A <: Top(
Topisn't presented at all)
- the subtyping relation is provably a preorder
What I'm looking for is some test cases for this variation of subtyping. Here is one example, taken from the "A calculus of constructions with explicit subtyping" paper:
It would be ideal to have a bunch of similar definitions. Examples that require contravariant subtyping for product types or the subsumption rule are good too, since I can define some coercions. It should also be easy to add sum types if needed, or at least to represent them in terms of product types.
Please note, that I'm not interested in applications of conservative extensions (like coercive subtyping and refinement types) of type systems without subtyping. Just basic dependent subtyping stuff.