2
$\begingroup$

The paper Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism provides examples for checking if one function type is a subtype of another, which I think demonstrates checking constructors with parameters which are covariant or contravariant.

I can not see an example of the subtype rule for type constructors with type parameters which are invariant.

For example consider some impure, mutable stack type:

type Stack : * -> *

push : forall a. Stack a -> a -> ()
pop : forall a. Stack a -> a

The type parameter on Stack represents a type that can be inputted and outputted from the stack, which makes it neither covariant nor contravariant.

To implement the subtyping rule for two Stack types could I simply apply the subtyping rule twice? Something like:

C1 |- a <: b -| C2    C2 |- b <: a -| C3
----------------------------------------
     C1 |- Stack a <: Stack b -| C3
|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ Your Stack type is actually covariant. You want an example that either has mutable/IO operations in its type or contains both data and codata. $\endgroup$ – Aaron Rotenberg Dec 13 '19 at 17:05

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.