Jun 4 Seminar

A <=s B

"Semantic subtyping"

forall v in V[A], exists v',
v -->B v' and v' in V[B]


         T |= e => A
implies  T |= e : B => B  or equivalently,  T |= e <= B


T |= (e : B) => B
=def=
exists v, e : B --> v, s.t. v in V[B]
(e : B) --> (v' : B) -->B v


T |= e <= B
=def=
exists v, e --> v s.t. v in V[B]

e --> v' -->B v

Problem is the cast-arr rule

C <= A
B <= D
----------------
\... : A -> B
--> C->D
\... : A -> D

? simplify to functionals? can you do a syntactic proof in the v1 system

why cannot work? the proposed plan Page 17

Page 18: typing, splitlam derive the intersection reduction

T |= e ⇒ A A <: B T |= (e : B) ⇒ B

Motivation:

• consistency, no longer needed in soundness proof, generalized in LR
• runtime subtyping
• BCD (ongoing work)

---------------------------
vf --> C->D (vf: C -> D) 


reduction is independent from subtyping
=> enable easy definition of "semantic subtyping" (coercively)

FW1 & 2?

motivation of envrionment based semantics?

paramatricity? ←> bidirectional typing, preciseness v ->Top () is more correct than v ->Top v