Concepts
The Subsumption Rule
The Subtype Relation
Slide QA1
Record Subtyping…
row type
index? record impl as list
width/depth/permulation
- multiple step rules
Java
- class - no index (thinking about offset)
having both width/permulation subtyping make impl slow
- OOP - hmm
- ML has no permulation - for perf reason (static structure) as C
ML has depth?
- a little bit by equality
OCaml objection has all three
Slide QA2
Looking at Contravariant!
-
(2)
{i1:S,i2:T}→U <: {i1:S,i2:T,i3:V}→U -
(4)
{i1:T,i2:V,i3:V} <: {i1:S,i2:U} * {i3:V}is interesting:
the interesting thing is, why don’t we make some subtyping rules for that as well?
- there are definitely code can do that
- their runtime semantics are different tho they carry same information
- coercion can used for that
3 and 4. (5) …
A <: Top => Top -> A <: A -> A – contravariant
if we only care (A*T), can use T:Top
but to type the whole thing : A
Top -> A?
but noticed that we said \z:A.z
can we pass A -> A into Top -> A?
more specific more general
smallest -> most specific -> A -> A
largest -> most specific -> Top -> A
- “The type Bool has no proper subtypes.” (I.e., the only type smaller than Bool is Bool itself.) Ture unless we have Bottom
hmm seems like Bottom in subtyping is different with Empty/Void, which is closer to logical Bottom ⊥ since Bottom here is subtyping of everything..
OH they are the same: (nice)
- True
Inversion Lemmas for Subtyping
inversion doesn’t lose information, induction does.
auto rememeber?? — dependent induction hetergeous equaltiy
In soundness proof
- subtyping only affects Canonical Forms + T_Sub case in induction
Lemma: If Gamma ⊢ \x:S1.t2 ∈ T, then there is a type S2 such that x⊢>S1; Gamma ⊢ t2 ∈ S2 and S1 → S2 <: T.
why T not arrow? Top…
if including Bottom…many proof becomes hard, canonical form need to say…might be Bottom?
no, no value has type Bottom (Void)…
