- repair :reload
define a = b as a <= b and b <= a. This is useful to capture more equalities between meet and joins. Must be careful with recursive cases.
The subtyping rule for functions is: A ⊑ A’ B ⊑ B’
A’ -> B ⊑ A -> B’
Let’s say that the (->) type constructor keeps track of polarity of occurences modalities ⊕ and ⊝:
(->) : ⊝Type -> ⊕Type -> Type
Furthermore, the system can be arranged such that, for every f : ⊕Type -> Type, then
A ⊑ A’
f A ⊑ f A’
(and symmetrically for ⊝)
Then we can internalise the notion of subtyping:
Subtype A B = (P : (x : ⊕Type) -> Type) -> P A -> P B
And, whenever B ⊑ A:
sub :: Subtype A B sub P x = x
We also get a coercion function from subtyping:
coerce : Subtype A B -> A -> B coerce q = q (\x -> x)
(((We could also capture subtypes as follows: Subtype’ A B = [f : A -> B; p : f x = x] But = must be heterogeneous. This is a bit tricky.)))