Types.ott

grammar
valtyp,A,B :: 'vt_' ::= {{ com value types }}
  | 1       :: :: Unit
  | A1 * A2 :: :: Pair
  | 0       :: :: Empty
  | A1 + A2 :: :: Sum
  | U E C   :: :: Thunk {{ tex [[U]]_[[E]] [[C]] }}

comptyp,C :: 'ct_' ::= {{ com computation types }}
  | F A     :: :: ValueReturning
  | A -> C  :: :: Function
  | TT      :: :: Unit
  | C1 & C2 :: :: Pair

effsig,E :: 'ef_' ::= {{ com effect signatures }}
  | E + { oper : A -> B }  :: :: Oper
  | 0                      :: :: Nil

handtyp,R :: 'r_' ::= {{ com handlers }}
  | A E => E' C :: :: Handler

env,G :: 'env_' ::= {{ com environments }}
  | 0         :: :: Nil
  | G , x : A :: :: Cons

defns
Env :: '' ::=

 defn
 x : A in G :: ::Env::'' {{ tex [[x]]:[[A]] \in [[G]] }} by

  ------------ :: EnvHere
  x:A in G,x:A

  x <> x'
  x:A in G
  -------------- :: EnvLater
  x:A in G,x':A'

defns
EffSig :: '' ::=

 defn
 ( oper : A -> B ) in E :: ::eff::''
  {{ tex ([[oper]]:[[A]]\rightarrow[[B]]) \in [[E]] }} by

  -------------------------------------- :: OperHere
  (oper : A -> B) in E + {oper : A -> B}

  oper <> oper'
  (oper : A -> B) in E
  ----------------------------------------- :: OperLater
  (oper : A -> B) in E + {oper' : A' -> B'}

defns
Typing :: '' ::=

 defn
 G |- v : A :: ::vtyp::'' by

  x:A in G
  -------- :: Var
  G |- x:A

  --------- :: UnitVal
  G |- ():1

  G |- v1 : A1
  G |- v2 : A2
  ---------------------- :: PairVal
  G |- (v1,v2) : A1 * A2

  G |- v : A1
  -------------------- :: InL
  G |- inl v : A1 + A2

  G |- v : A2
  -------------------- :: InR
  G |- inr v : A1 + A2

  G |-E m : C
  ---------------- :: Thunk
  G |- {m} : U E C

 defn
 G |- E m : C :: ::ctyp::'' {{ tex [[G]] \vdash_{[[E]]} [[m]]:[[C]] }} by

% The order for context extension is rather awkward here
  G |- v : A1 * A2
  G, x2:A2, x1:A1 |-E m : C
  -------------------------- :: Split
  G |-E split(v,x1,x2,m) : C

  G |- v : 0
  ------------------ :: CaseNil
  G |-E case0(v) : C

  G |- v : A1 + A2
  G, x1:A1 |-E m1 : C
  G, x2:A2 |-E m2 : C
  ----------------------------- :: Case
  G |-E case(v,x1,m1,x2,m2) : C

  G |- v : U E C
  -------------- :: Force
  G |-E v! : C

  G |- v : A
  -------------------- :: Return
  G |-E return v : F A

  G |-E m : F A
  G, x:A |-E m' : C
  -------------------------- :: Let
  G |-E let x <- m in m' : C

  G, x:A |-E m : C
  ------------------- :: Lambda
  G |-E \x.m : A -> C

  G |-E m : A -> C
  G |- v : A
  ---------------- :: App
  G |-E m v : C

  ------------- :: UnitComp
  G |-E <> : TT

  G |-E m1 : C1
  G |-E m2 : C2
  ----------------------- :: PairComp
  G |-E <m1,m2> : C1 & C2

  G |-E m : C1 & C2
  ------------------ :: ProjL
  G |-E prjl m : C1

  G |-E m : C1 & C2
  ------------------ :: ProjR
  G |-E prjr m : C2

  (oper : A -> B) in E
  G |- v : A
  G, x:B |-E m : C
  --------------------- :: Oper
  G |-E oper v (\x.m) : C

  G |-E m : F A
  G |- h : A E => E' C
  -------------------------- :: Handle
  G |-E' handle m with h : C

 defn
 G |- h : A E => E' C :: ::handle::''
  {{ tex [[G]] \vdash [[h]] : [[A]] {}^{[[E]]}\!\!\Rightarrow^{[[E']]} [[C]] }} by

% These two rules are a single rule in the paper, with comprehensions.

  G,x:A |-E' m : C
  ------------------------------------ :: HandleR
  G |- { return x -> m } : A 0 => E' C

  G |- h : A E => E' C
  G, k:U E' B -> C, p:A' |-E' m : C
  ------------------------------------------------------------ :: HandleOp
  G |- h + { oper p k -> m } : A E + { oper : A' -> B } => E' C


defns
Canonical :: '' ::=

 defn
 canonical m :: ::canonical::'C_' by

 ------------------ :: Value
 canonical return v

 -------------- :: Lambda
 canonical \x.m

 ------------ :: Unit
 canonical <>

 ----------------- :: Pair
 canonical <m1,m2>

 ----------------------- :: Oper
 canonical oper v (\x.m)