Final tagless interpreters in terms of effects and handlers

tagless_effects_interp.ml

(* Encoding tagless interpreters with effects and handlers.
   TODOs:
   - do more examples from the tagless papers, especially with phantom types
   - examples of "higher order transformations", e.g., index-based definitions and index conversions
*)

module NumAlg = struct
  (* New symantics instances should extend this. Having this GADT makes it not
     truly "tagless". However, many other advantages of the final tagless style 
     carry over still. Perhaps one could try to improve the theory of effect handlers/handling
     to eliminate the need for such GADTs. 
     *)
  type _ key = ..
  (* key-indexed effect operations = symantic ops *)
  effect Lit: ('a key * int) -> 'a
  let lit k n = perform (Lit (k, n))
  effect Add: ('a key * 'a * 'a) -> 'a
  let add k n1 n2 = perform (Add (k, n1, n2))
end

(* Standard interpretation *)
module IntInterp = struct
  type _ NumAlg.key += Key: int NumAlg.key
  let handler action =
    try action Key with
    | effect (NumAlg.Lit (Key,n)) k -> continue k n
    | effect (NumAlg.Add (Key,n1,n2)) k -> continue k (n1+n2)
end

(* String Interp *)
module StringifyNum = struct
  type _ NumAlg.key += Key: string NumAlg.key
  let handler action =
    try action Key with
    | effect (NumAlg.Lit (Key,n)) k -> continue k (string_of_int n)
    | effect (NumAlg.Add (Key,n1,n2)) k -> continue k (Printf.sprintf "(%s + %s)" n1 n2)
end

(* Advantage: Expressions are first class and not clunky second class functors *)
let exp1 k =
  let open NumAlg in
  (* Here, we have to keep k explicitly to get the type of exp1 right, i.e. 'a NumAlg.key -> 'a.
     In language with proper effect types, we could leave parameter k implicit and inject via effects.
     exp1's type would then become unit -> <inject<'a>, lit,add> 'a. If Koka had only GADTs... *)
  add k (lit k 5) (add k (lit k 10) (add k (lit k 0) (lit k 2)))
  
 let test = IntInterp.handler exp1  
 let test2 = StringifyNum.handler exp1