rules.ott

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% METAVARIABLES

metavar typevar, X , Y ::= {{ repr-locally-nameless }}
  
metavar I, J, h, i, j, n, m ::= {{ coq nat }}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% GRAMMAR (LNgen portion)

grammar

l, k :: 'lbl_' ::=
  | i ::  :: TagIndex
  | tleft :: :: TagLeft {{ tex \mathrm{left} }}
  | tright :: :: TagRight {{ tex \mathrm{right} }}
  

typ, A , B , C, V, Aneg :: 't_' ::= {{ com type }}
  | X                                ::  :: tvar
  | In l A                           ::  :: rcd      {{ tex \tytag{[[l]]}{[[A]]} }}
  | A1 & A2                          ::  :: and
  | A1 | A2                          ::  :: or
  | A -> B                           ::  :: arrow
  | forall X . B                     ::  :: forall   (+ bind X in B +)
  | Top                              ::  :: top
  | Empty                            ::  :: bot
  | ( A )                            :: S:: paren    {{ icho [[A]] }}
  | A [ X ~> B ]                     :: M:: tsubst   {{ coq (open_typ_wrt_typ [[X A]][[B]]) }}


Fty {{ tex \hat{A} }}, FVty {{ tex \hat{V} }}, Ftyalt {{ tex \hat{B} }} :: 'fty_' ::= {{ com elimination type }}
  | A       :: :: StackArg
  | [ A ]   :: :: StackTyArg


substitutions
  single typ X   :: typsubst

freevars
  typ X      :: typefv
  
parsing
  t_arrow <= t_and
  t_forall <= t_and
  t_arrow <= t_or
  t_forall <= t_or
  t_arrow right t_arrow
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% GRAMMAR  (non LNgen portion)

grammar

tctx, D {{ tex \Delta }} :: 'tctx_' ::= {{ com type context }} {{ coq list ( atom * typ ) }}
  | []           ::  :: empty      {{ coq nil }}
                                   {{ tex \cdot }}
  | D , X        ::  :: cons       {{ coq (cons ([[X]],t_top) [[D]]) }}

terminals :: 'terminals_' ::=
  | [-]          ::    :: hole      {{ tex \hole }}
  | &            ::    :: intersect {{ tex \sqcap }}
  | |            ::    :: union     {{ tex \sqcup }}
  | forall       ::    :: forall    {{ tex \forall }}
  | exists       ::    :: exists    {{ tex \exists }}
  | nil          ::    :: nil       {{ tex \kw{*} }}
  | notin        ::    :: notin     {{ tex \notin }}
  | Top          ::    :: topty     {{ tex \tytop }}
  | Empty        ::    :: emptyty   {{ tex \tyempty }}
  | <:           ::    :: decsub    {{ tex \subtype }}
  | <a           ::    :: algsub    {{ tex \subtype_a }}
  | <p           ::    :: possub    {{ tex \subtype_+ }}
  | <n           ::    :: negsub    {{ tex \subtype_- }}

formula :: formula_ ::=  
   | judgement                       ::   :: judgement
   | l != l'                         ::   :: labNeq
     {{ coq [[l]] <> [[l']] }}
   | l = l'                          ::   :: labEq
   | X in D                          ::   :: inD
    {{ coq binds [[X]]t_top[[D]] }}
   | lc_typ A                        ::   :: lcTyp
     {{ tex }}
     {{ coq lc_typ [[A]] }}
   | ( formula )                     :: M :: formulaParen
    {{ coq [[formula]] }}
   | not formula                     :: M :: not
    {{ tex \neg [[formula]] }}
    {{ coq not ([[formula]]) }}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% subtyping & positive / negative subtyping
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
DSub :: '' ::=

  defn
  A <: B
  :: :: declarative_subtyping :: DSub_
  {{ com Declarative subtyping }}
  by


  ----------- :: Refl
  A <: A

  A1 <: A2
  A2 <: A3
  ------------- :: Trans
  A1 <: A3

  A <: B
  -------------------- :: CovIn
  In l A <: In l B

  A <: B
  -------------------- :: CovArr
  C -> A <: C -> B

  A <: B
  --------------------------- :: CovAll
  forall X. A <: forall X. B

  A2 <: A1
  -------------------- :: FunCon
  A1 -> B <: A2 -> B

  ------------------------------------- :: CovDistIIn
  (In l A) & (In l B) <: In l (A & B)

  ------------------------------------- :: CovDistIArr
  (C -> A) & (C -> B) <: (C -> A & B)

  ------------------------------------------------------ :: CovDistIAll
  (forall X. A) & (forall X. B) <: (forall X. A & B)  

  ------------------------------------- :: CovDistUIn
  In l (A | B) <: (In l A) | (In l B)

  ------------------------------------------------------ :: CovDistUAll
  forall X. (A | B) <: (forall X. A) | (forall X. B)

  ------------------------------------- :: CovDistUInterL
  (A | B) & C <: (A & C) | (B & C)

  ------------------------------------------------- :: FunDistI
  (A1 -> B) & (A2 -> B) <: (A1 | A2) -> B 

  A1 <: B
  ----------------- :: InterLL
  A1 & A2 <: B

  A2 <: B
  ----------------- :: InterLR
  A1 & A2 <: B

  A <: B1
  A <: B2
  ----------------- :: InterR
  A <: B1 & B2

  A1 <: B
  A2 <: B
  ------------ :: UnionL
  A1 | A2 <: B

  A <: B1
  ------------ :: UnionRL
  A <: B1 | B2

  A <: B2
  ------------ :: UnionRR
  A <: B1 | B2

  ---------- :: Empty
  Empty <: B

  --------- :: Top
  A <: Top
  

defns
NegTyp :: '' ::=

  defn
  neg Aneg
  :: :: isNegTyp :: NTyp
  {{ com Negative Types }}
  by

  ---------------- :: Fun
  neg A -> B

  % ------------------ :: Rec
  % neg (In l Top)->A

  ------------------ :: Forall
  neg forall X . A

  neg A
  neg B
  ------------------ :: Intersection
  neg A & B

  neg A
  neg B
  ------------------ :: Union
  neg A | B

  ------------------ :: Top
  neg Top
  

defns
ValTyp :: '' ::=

  defn
  val V
  :: :: isValTyp :: VTyp
  {{ com Value Types }}
  by
  
  val V
  ---------------- :: In
  val In l V

  neg A
  ------------------ :: Neg
  val A


defns
ValFty :: '' ::=

  defn
  valF FVty
  :: :: isValFty :: VFty
  {{ com value elimination types }}
  by
  
  ---------------- :: TypArg
  valF [A]

  val V
  ---------------- :: Arg
  valF V


defns
PSub :: '' ::=

  defn
  V <p A
  :: :: PositiveSubtyping :: PSub_
  {{ com Positive Subtyping }}
  by

  val V
  V <p A
  ---------------- :: In
  In l V <p In l A 

  val V
  V <p A
  ---------- :: UnionL
  V <p A | B

  val V
  V <p B
  ---------- :: UnionR
  V <p A | B

  val V
  V <p A
  V <p B
  ---------- :: Intersect
  V <p A & B

  val V
  neg Aneg
  --------- :: Neg
  V <p Aneg


defns
NSub :: '' ::=

  defn
  Aneg <n Fty
  :: :: NegativeSubtyping :: NSub_
  {{ com Negative Subtyping }}
  by

  val V
  V <p A
  ----------- :: Fun
  A -> B <n V

  ------------------- :: TyFun
  forall X . A <n [B]

  Aneg1 <n Ftyalt
  Aneg2 <n Ftyalt
  -------------------- :: Union
  Aneg1 | Aneg2 <n Ftyalt

  Aneg1 <n Ftyalt
  -------------------- :: IntersectL
  Aneg1 & Aneg2 <n Ftyalt

  Aneg2 <n Ftyalt
  -------------------- :: IntersectR
  Aneg1 & Aneg2 <n Ftyalt


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% algorithmic subtyping
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
Ordinary :: '' ::=

  defn ordinaryU A :: :: ordu :: OrdU_
  by

  ------------- :: var
  ordinaryU X
  
  ------------- :: top
  ordinaryU Top

  --------------- :: bot
  ordinaryU Empty

  ---------------- :: arrow
  ordinaryU A -> B

  ordinaryU A
  ordinaryU B
  --------------- :: and
  ordinaryU A & B

  ordinaryU A
  ---------------- :: rcd
  ordinaryU In l A

  ordinaryU A
  ---------------------- :: forall
  ordinaryU forall X . A


  defn ordinaryI A :: :: ordi :: OrdI_
  by

  ------------- :: var
  ordinaryI X

  ------------- :: top
  ordinaryI Top

  --------------- :: bot
  ordinaryI Empty

  ordinaryU A
  ordinaryI B
  ---------------- :: arrow
  ordinaryI A -> B

  ordinaryI A
  ordinaryI B
  --------------- :: or
  ordinaryI A | B

  ordinaryI A
  ---------------- :: rcd
  ordinaryI In l A

  ordinaryI A
  ---------------------- :: forall
  ordinaryI forall X . A


defns
Split :: '' ::=

  defn splitI A = B1 & B2 :: :: spli :: SpI_
  by

  -------------------- :: and
  splitI A & B = A & B

  splitI A = A1 & A2
  ---------------------------------- :: orl
  splitI A | B = A1 | B & A2 | B

  ordinaryI A
  splitI B = B1 & B2
  ---------------------------------- :: orr
  splitI A | B = A | B1 & A | B2

  splitI B = B1 & B2
  --------------------------------- :: arrow
  splitI A -> B = A -> B1 & A -> B2

  ordinaryI B
  splitU A = A1 | A2
  --------------------------------- :: arrowUnion
  splitI A -> B = A1 -> B & A2 -> B

  splitI A = A1 & A2
  --------------------------------------------------- :: forall
  splitI forall X . A = forall X . A1 & forall X . A2

  splitI A = A1 & A2 
  --------------------------------- :: in
  splitI In l A = In l A1 & In l A2


  defn splitU A = B1 | B2 :: :: splu :: SpU_
  by

  -------------------- :: or
  splitU A | B = A | B

  splitU A = A1 | A2
  ------------------------------ :: andl
  splitU A & B = A1 & B | A2 & B

  ordinaryU A
  splitU B = B1 | B2
  ------------------------------ :: andr
  splitU A & B = A & B1 | A & B2

  splitU A = A1 | A2
  --------------------------------------------------- :: forall
  splitU forall X . A = forall X . A1 | forall X . A2

 splitU A = A1 | A2 
 --------------------------------- :: in
 splitU In l A = In l A1 | In l A2


defns
AlgorithmicSubtyping :: '' ::=

  defn
  A <a B  :: :: algo_sub :: ASub_
  {{ com Algorithmic Subtyping }}
  by
  
  ---------------------- :: refl
  A <a A
  
  ---------------------- :: top
  A <a Top
  
  ---------------------- :: bot
  Empty <a  A

  B1 <a A1
  A2 <a B2
  ------------------------ :: arrow
  A1 -> A2 <a B1 -> B2
  
  A <a B
  ---------------------------- :: forall
  forall X. A <a forall X. B

  A <a B
  ------------------------ :: rcd
  In l A <a In l B

  splitI B = B1 & B2
  A <a B1
  A <a B2
  --------------- :: and
  A <a B
  
  splitI A = A1 & A2
  A1 <a B
  ------------------------- :: andl
  A <a B

  splitI A = A1 & A2
  A2 <a B
  ------------------------- :: andr
  A <a B

  splitU A = A1 | A2
  A1 <a B
  A2 <a B
  --------------- :: or
  A <a B  
  
  splitU B = B1 | B2
  A <a B1
  ------------------------- :: orl
  A <a B
  
  splitU B = B1 | B2
  A <a B2
  ------------------------- :: orr
  A <a B


defns
OrduFty :: '' ::=

  defn ordinaryUFty Fty :: :: UnionOrdinaryFty :: ''
  {{ tex \nsplitu{[[Fty]]} }}
  by

  ordinaryU A
  -------------- :: OrdUArg
  ordinaryUFty A

  ---------------- :: OrdUTypeArg
  ordinaryUFty [A]


defns
Appty :: '' ::=

  defn
  apply ( A , Fty ) => B
  :: :: ApplyTy :: ''
  {{ tex \applyty{[[ A ]]}{[[ Fty ]]}{[[ B ]]} }}
  {{ com type-level dispatch }}
  by

  ordinaryUFty Fty
  -------------------------- :: ApplyTyEmpty
  apply(Empty, Fty) => Empty

  ------------------------------------ :: ApplyFunTy
  apply(forall X . A, [B]) => A[X~>B]

  ordinaryUFty B
  B <: A
  ----------------------- :: ApplyTyFun
  apply(A -> A', B) => A'

  ordinaryUFty Fty
  apply(A1, Fty) => A1'
  apply(A2, Fty) => A2'
  -------------------------------- :: ApplyTyUnion
  apply(A1 | A2, Fty) => A1' | A2'

  splitU B = B1 | B2
  apply(A, B1) => B1'
  apply(A, B2) => B2'
  ------------------------ :: ApplyTyUnionArg
  apply(A, B) => B1' | B2'

  ordinaryUFty Fty
  apply(A1, Fty) => A1'
  apply(A2, Fty) =/>
  ------------------------------ :: ApplyTyInterL
  apply(A1 & A2, Fty) => A1'

  ordinaryUFty Fty
  apply(A1, Fty) =/>
  apply(A2, Fty) => A2'
  ------------------------------ :: ApplyTyInterR
  apply(A1 & A2, Fty) => A2'

  ordinaryUFty Fty
  apply(A1, Fty) => A1'
  apply(A2, Fty) => A2'
  ------------------------------ :: ApplyTyInterBoth
  apply(A1 & A2, Fty) => A1' & A2'


  defn
  apply ( A , Fty ) =/>
  :: :: NApplyTy :: ''
  {{ tex \napplyty{[[ A ]]}{[[ Fty ]]} }}
  by

  ---------------------------------- :: NApplyTyTop
  apply(Top, Fty) =/>
  
  ---------------------------------- :: NApplyTyVar
  apply(X, Fty) =/>
  
  ---------------------------------- :: NApplyTyIn
  apply(In l A, Fty) =/>
  
  ---------------------------------- :: NApplyTyAll
  apply(forall X . A, B) =/>

  lc_typ A 
  ordinaryUFty B
  not (B <: A)
  ----------------------- :: NApplyTyFun
  apply(A -> A', B) =/>

  ----------------------- :: NApplyTyFunFty
  apply(A -> A', [B]) =/>

  ordinaryUFty Fty
  apply(A1, Fty) =/>
  -------------------------------- :: NApplyTyUnionL
  apply(A1 | A2, Fty) =/>

  ordinaryUFty Fty
  apply(A2, Fty) =/>
  -------------------------------- :: NApplyTyUnionR
  apply(A1 | A2, Fty) =/>
  
  splitU B = B1 | B2
  apply(A, B1) =/>
  ------------------------ :: NApplyTyUnionArgL
  apply(A, B) =/>
  
  splitU B = B1 | B2
  apply(A, B2) =/>
  ------------------------ :: NApplyTyUnionArgR
  apply(A, B) =/>

  ordinaryUFty Fty
  apply(A1, Fty) =/>
  apply(A2, Fty) =/>
  ------------------------------ :: NApplyTyInter
  apply(A1 & A2, Fty) =/>

  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% alternative non-deterministic definition
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
NewSplit :: '' ::=

  defn
  splitI A ~ B1 & B2 :: :: new_spli :: NSpI_
  by

  -------------------- :: and
  splitI A & B ~ A & B

  splitI A ~ A1 & A2
  ---------------------------------- :: orl
  splitI A | B ~ A1 | B & A2 | B

  splitI B ~ B1 & B2
  ---------------------------------- :: orr
  splitI A | B ~ A | B1 & A | B2

  splitI B ~ B1 & B2
  --------------------------------- :: arrow
  splitI A -> B ~ A -> B1 & A -> B2

  splitU A ~ A1 | A2
  --------------------------------- :: arrowUnion
  splitI A -> B ~ A1 -> B & A2 -> B

  splitI A ~ A1 & A2
  --------------------------------------------------- :: forall
  splitI forall X . A ~ forall X . A1 & forall X . A2

  splitI A ~ A1 & A2 
  --------------------------------- :: in
  splitI In l A ~ In l A1 & In l A2


  defn
  splitU A ~ B1 | B2 :: :: new_splu :: NSpU_
  by

  -------------------- :: or
  splitU A | B ~ A | B

  splitU A ~ A1 | A2
  ------------------------------ :: andl
  splitU A & B ~ A1 & B | A2 & B

  splitU B ~ B1 | B2
  ------------------------------ :: andr
  splitU A & B ~ A & B1 | A & B2

  splitU A ~ A1 | A2
  --------------------------------------------------- :: forall
  splitU forall X . A ~ forall X . A1 | forall X . A2

  splitU A ~ A1 | A2 
  --------------------------------- :: in
  splitU In l A ~ In l A1 | In l A2


defns
NewAlgorithmicSubtyping :: '' ::=

  defn
  A <na B  :: :: new_sub :: NSub_
  {{ com New Algorithmic Subtyping }}
  by
  
  ---------------------- :: refl
  A <na A
  
  ---------------------- :: top
  A <na Top
  
  ---------------------- :: bot
  Empty <na  A

  B1 <na A1
  A2 <na B2
  ------------------------ :: arrow
  A1 -> A2 <na B1 -> B2
  
  A <na B
  ---------------------------- :: forall
  forall X. A <na forall X. B

  A <na B
  ------------------------ :: rcd
  In l A <na In l B

  splitI B ~ B1 & B2
  A <na B1
  A <na B2
  --------------- :: and
  A <na B
  
  splitI A ~ A1 & A2
  A1 <na B
  ------------------------- :: andl
  A <na B

  splitI A ~ A1 & A2
  A2 <na B
  ------------------------- :: andr
  A <na B

  splitU A ~ A1 | A2
  A1 <na B
  A2 <na B
  --------------- :: or
  A <na B  
  
  splitU B ~ B1 | B2
  A <na B1
  ------------------------- :: orl
  A <na B
  
  splitU B ~ B1 | B2
  A <na B2
  ------------------------- :: orr
  A <na B

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Disjointness: distinguishability and mergeabililty
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
DistinguishabilityAx :: '' ::=

  defn
  |-ax A <> B
  :: :: DistinguishabilityAx :: 'DistAx'
  {{ tex \distax{[[A]]}{[[B]]} }}
  by

  l1 != l2
  ------------------ :: In
  |-ax In l1 A <> In l2 B

  ------------------ :: EmptyL
  |-ax Empty <> B

  ------------------ :: EmptyR
  |-ax A <> Empty


defns
Distinguishability :: '' ::=

  defn
  |- A <> B
  :: :: Distinguishability :: 'Dist'
  {{ tex \dist{[[A]]}{[[B]]} }}
  by

  |-ax A <> B
  ----------- :: Ax
  |- A <> B

  |- A <> B
  --------------------- :: In
  |- In l A <> In l B

  splitU A = A1 | A2
  |- A1 <> B
  |- A2 <> B
  ---------------- :: Union
  |- A <> B

  splitU A = A1 | A2
  |- B <> A1
  |- B <> A2
  ---------------- :: UnionSym
  |- B <> A

  |- A <> B
  ---------------- :: IntersectL
  |- A & A' <> B

  |- A' <> B
  ---------------- :: IntersectR
  |- A & A' <> B

  |- B <> A
  ---------------- :: IntersectLSym
  |- B <> A & A'

  |- B <> A'
  ---------------- :: IntersectRSym
  |- B <> A & A'


defns
DistinguishabilityAx_Dec :: '' ::=

  defn
  ||-ax A <> B
  :: :: DistinguishabilityAx_Dec :: 'DistAxDec'
  {{ tex \distax{[[A]]}{[[B]]} }}
  {{ com the definition on the paper }}
  by

  l1 != l2
  ------------------ :: In
  ||-ax In l1 A <> In l2 B

  ------------------ :: Empty
  ||-ax Empty <> B


defns
Distinguishability_Dec :: '' ::=

  defn
  ||- A <> B
  :: :: Distinguishability_Dec :: 'DistDec'
  {{ tex \dist{[[A]]}{[[B]]} }}
  {{ com declarative formulation of distinguishability }}
  by

  ||- A <> B
  --------------------- :: In
  ||- In l A <> In l B

  ||- A1 <> B
  ||- A2 <> B
  ---------------- :: Union
  ||- A1|A2 <> B

  ||-ax A <> B
  ----------- :: Ax
  ||- A <> B

  ||- B <> A
  ----------- :: Sym
  ||- A <> B

  ||- A <> B'
  B <: B'
  ----------- :: Sub
  ||- A <> B


defns
MergeabilityAx :: '' ::=
  
  defn
  |-ax A >< B
  :: :: MergeabilityAx :: ''
  {{ tex \mergeableax{[[ A ]]}{[[ B ]]} }}
  by

  -------- :: MergeAxTopL
  |-ax Top >< B
  
  ----------------------------- :: MergeAxFunTyp
  |-ax A -> A' >< forall X . B


defns
Mergeability :: '' ::=

  defn
  |- A >< B
  :: :: Mergeability :: ''
  {{ tex \judgmerg{[[A]]}{[[B]]} }}
  by
  
  |- A <> B
  ----------------------- :: MergeFunL
  |- A -> A' >< B -> B'

  |- B >< B'
  ----------------------- :: MergeFunR
  |- A -> B >< A -> B'

  |- A >< B
  --------------------------------- :: MergeForall
  |- forall X . A >< forall X . B

  |- A  >< B
  |- A' >< B
  ---------------- :: MergeIntersect
  |- A & A' >< B

  |- B >< A
  |- B >< A'
  ---------------- :: MergeIntersectSym
  |- B >< A & A'
  
  |- A  >< B
  |- A' >< B
  ---------------- :: MergeUnion
  |- A | A' >< B
  
  |- B >< A
  |- B >< A'
  ---------------- :: MergeUnionSym
  |- B >< A | A'
  
  |-ax A >< B
  ----------- :: MergeAx
  |- A >< B
  
  |-ax B >< A
  ----------- :: MergeAxSym
  |- A >< B

defns
TypeWellformedness :: '' ::=

  defn
  D |- A
  :: :: TypeWF :: ''
  {{ com well-formed types }}
  by

  X in D
  --------- :: TyWfVar
  D |- X

  D |- A
  ----------- :: TyWfIn
  D |- In l A
  
  D |- A1
  D |- A2
  |- A1 >< A2
  ------------ :: TyWfInter
  D |- A1 & A2

  D |- A1
  D |- A2
  ------------ :: TyWfUnion
  D |- A1 | A2

  D |- A
  D |- B
  ----------- :: TyWfFun
  D |- A -> B

  D, X |- B
  ----------------- :: TyWfTyFun
  D |- forall X . B

  -------- :: TyWfTop
  D |- Top

  ---------- :: TyWfEmpty
  D |- Empty


defns
Similarity :: '' ::=

  defn
  V1 ~ V2
  :: :: sim :: Sim_
  {{ com Similar Types }}
  by

  neg A
  neg B
  ----------------------- :: Neg
  A ~ B

  V1 ~ V2
  ----------------------- :: In
  In l V1 ~ In l V2