3
$\begingroup$

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.

So

  • 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 (Top isn'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: example

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.

$\endgroup$
  • 1
    $\begingroup$ It's a bit weird that you don't have a subsumption rule; is it at least admissible? $\endgroup$ – cody Dec 30 '14 at 21:16
  • 1
    $\begingroup$ @cody, there is no sumsumption rule in the "Structural Subtyping and the Notion of Power Type" paper and other similar papers by Luca Cardelli, so I don't think it's weird (but power types are more expressive, than just bounded dependent quantification). I can (at least I could in one of the previous versions of the code) define explicit coercions like x : A', le : A' <: A -> coerce x : Coerce le A among with the uncoerce function pretty much in the style of Agda's Lift, lift and lower, but this explicitness quickly becomes cumbersome. $\endgroup$ – user3237465 Dec 30 '14 at 21:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.