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