namespace http://cds.omdoc.org/examples❚

fixmeta ur:?LF❚

/T Multi-adjunctive meta-language (MAM), following the paper "On the Expressive Power of user-defined effects".
   Formalized during Florian Rabe's visit to Matija Pretnar in June 2019❚

theory MAM =
  # Types❙
  
  vtp : type❙
  eff : type❙
  ctp : eff ⟶ type❙
  
  unit : vtp❙
  vprod : vtp ⟶ vtp ⟶ vtp❘# 1 × 2 prec 30❙
  sum  : vtp ⟶ vtp ⟶ vtp❘# 1 + 2 prec 30❙
  Thunk : {e} ctp e ⟶ vtp❘# U 2 prec 30❙
  
  Ret : {e} vtp ⟶ ctp e❘# F 1 2❙
  fun : {e} vtp ⟶ ctp e ⟶ ctp e❘# 2 → 3 prec 30❙
  cprod : {e} ctp e ⟶ ctp e ⟶ ctp e❘# 2 & 3 prec 30❙
  
  # Terms❙
  
  vtm : vtp ⟶ type❘# vtm 1 prec -5❙
  ctm : {e} ctp e ⟶ type❘# ctm 2 prec -5❙
  
  empty : eff❘# ∅❙
  
  unitterm : vtm unit❘# O❙

  pair : {A,B} vtm A ⟶ vtm B ⟶ vtm A × B❘# 3 , 4❙
  pcase : {A,B,e,C: ctp e} vtm A×B ⟶ (vtm A ⟶ vtm B ⟶ ctm C) ⟶ ctm C❙
  
  inj1 : {A,B} vtm A ⟶ vtm A + B❙
  inj2 : {A,B} vtm B ⟶ vtm A + B❙
  scase : {A,B,e,C: ctp e} vtm A+B ⟶ (vtm A ⟶ ctm C) ⟶ (vtm B ⟶ ctm C) ⟶ ctm C❙
  
  thunk : {e, C: ctp e} ctm C ⟶ vtm U C❘# T{ 3 } prec -10❙
  
  force : {e, C: ctp e} vtm U C ⟶ ctm C❘# 3 ! prec 50❙
  ret : {A, e} vtm A ⟶ ctm F e A❙
  
  bind : {A, e, C: ctp e} ctm F e A ⟶ (vtm A ⟶ ctm C) ⟶ ctm C❘# 4 ; 5❙
  
  lambda : {A,e,C: ctp e} (vtm A ⟶ ctm C) ⟶ ctm A → C❘# λ 4❙
  apply : {A,e,C: ctp e} ctm A → C ⟶ vtm A ⟶ ctm C❘# 4 @ 5❙
  
  cpair : {e,C,D: ctp e} ctm C ⟶ ctm D ⟶ ctm C & D❘# 4 ,, 5❙
  prj1 : {e,C,D:ctp e} ctm C & D ⟶ ctm C❙
  prj2 : {e,C,D:ctp e} ctm C & D ⟶ ctm D❙
❚

theory EFF =
  include ?MAM❙
  
  Op : type❙
  Opeff : type❙
  opeff : Op ⟶ vtp ⟶ vtp ⟶ Opeff❘# 1 2 ⇒ 3❙
  opcons : Opeff ⟶ eff ⟶ eff❘# 1 ⊎ 2❙
  
  handler : vtp ⟶ eff ⟶ {e:eff} ctp e ⟶ type❘# 1 2 ⟹ 4❙  
  rethandler : {A,e,C: ctp e} (vtm A ⟶ ctm C) ⟶ A ∅ ⟹ C❘# hret 4❙
  ophandler  : {o,A1,A2,B,e,f,C: ctp f}
               B e ⟹ C ⟶
               (vtm A1 ⟶ vtm U (A2 → C) ⟶ ctm C) ⟶
               B ((o A1 ⇒ A2) ⊎ e) ⟹ C❘
               # hop 8 9❙
  
  subsumed : Opeff ⟶ eff ⟶ type❘# 1 ∈ 2❙
  
  op : {o, A, B, e} (o A ⇒ B) ∈ e ⟶ vtm A ⟶ ctm F e B❘# op 4 5❙
  handle : {A, e, f, C: ctp f} ctm F e A ⟶ A e ⟹ C ⟶ ctm C❘# handle 5 with 6❙
❚

theory Monads =
  include ?MAM❙
  Monad : {e} (vtp ⟶ ctp e) ⟶ type❙
  
  monad : {e, C: vtp ⟶ ctp e}
              ({a:vtp} vtm a ⟶ ctm C a) ⟶
              ({a,b} vtm U (C a) ⟶ vtm U (a → C b) ⟶ ctm C b) ⟶
              Monad e C❘# where 3 ; 4❙
  moncons : {e,C} Monad e C ⟶ eff❘# 1 ≺ 3❙
  refl : {A, e, C, M: Monad e C}
         ctm (C A) ⟶
         ctm F (e ≺ M) A❘# μ 5❙
  reify : {A,e,C,M: Monad e C} ctm F (e ≺ M) A ⟶ ctm (C A)❘# reify 4 5❙
❚

theory DelimitedContinuations =
  include ?MAM❙
  dccons : {e} ctp e ⟶ eff❙
  
  shift : {A, e, C: ctp e} (vtm U (A → C) ⟶ ctm C) ⟶
                           ctm F (dccons e C) A❘# S0 4❙  
  reset : {A, e, C: ctp e} ctm F e A ⟶ (vtm A ⟶ ctm C) ⟶ ctm C❘# 4 | 5❙ 
❚

theory ContinuationMonad =
  include ?Monads❙
  cont : {e, C: ctp e} vtp ⟶ ctp e❘= [e,C,a] (U (a → C)) → C❘# cont 2 3❙
  contmon : {e, C: ctp e} Monad e [a] cont C a❘
          = [e,C] where ([a,x] λ[c] c! @ x) ;
               [a,b,m,f] λ[c] m! @ T{λ[y] f! @ y @ c}❘# contmon 2❙ 
❚

view delMon : ?DelimitedContinuations -> ?ContinuationMonad =
  include ?MAM❙
  dccons = [e,C] e ≺ contmon C❙
  shift = [A,e,C,p] μ λ p❙
  /T The next declarations has a typing error:
     We have p: ctm F e A, but we need
     ctm F (e ≺ contmon C) A.
     (Here ≪T≫ denotes a missing term of type T.)
  ❙
  reset = [A,e,C,p: ctm F e A,r]
    (reify (contmon C) ≪ctm F (e ≺ contmon C) A≫) @ T{λ r}❙
❚