ML Advend Clendar 2017

basic_fc.ml

(** basic definition **)

module type ExpSYM = sig
  type repr
  val lit : int -> repr
  val neg : repr -> repr
  val add : repr -> repr -> repr  
end

module ExpSYMInt : ExpSYM with type repr = int = struct
  type repr = int
  let lit n = n
  let neg e = - e
  let add e1 e2 = e1 + e2
end

module ExpSYMString : ExpSYM with type repr = string = struct
  type repr = string
  let lit n = string_of_int n
  let neg e = "-" ^ e
  let add e1 e2 = "(" ^ e1 ^ "+" ^ e2 ^ ")"
end

(* let tf1 (type a) (module S : ExpSYM with type repr = a) =
let open S in
add (lit 8) (neg (add (lit 1) (lit 2))) *)

let tf1 (type a) (module S : ExpSYM with type repr = a) =
  let open S in
  add (lit 8) (neg (add (lit 1) (lit 2)))

module ModuleStyle (S : ExpSYM) = struct
  let tf1 = S.(add (lit 8) (neg (add (lit 1) (lit 2))))
end

let tf1_1 = let module M = ModuleStyle(ExpSYMInt) in M.tf1

let tf12 : type a. (module ExpSYM with type repr = a) -> a =
fun (module S : ExpSYM with type repr = a) ->
let open S in
add (lit 8) (neg (add (lit 1) (lit 2)))

(* utop # tf1 (module ExpSYMInt);;
- : int = 5 *)

(* utop # tf1 (module ExpSYMString);;
- : string = "(8+-(1+2))" *)


(** extension with mul **)

module type MulSYM = sig
  type repr
  val mul : repr -> repr -> repr
end

module MulSYMInt : MulSYM with type repr = int = struct
  type repr = int
  let mul e1 e2 = e1 * e2
end

module MulSYMString : MulSYM with type repr = string = struct
  type repr = string
  let mul e1 e2 = "(" ^ e1 ^ "*" ^ e2 ^ ")"
end


let tfm1 (type a) (module S1 : ExpSYM with type repr = a) (module S2 : MulSYM with type repr = a) = 
  let open S1 in
  let open S2 in
  add (lit 7) (neg (mul (lit 1) (lit 2)))


(* utop # tfm1 (module ExpSYMInt) (module MulSYMInt);;
- : int = 5 *)

(* utop # tfm1 (module ExpSYMString) (module MulSYMString);;
- : string = "(7+-(1*2))" *)


(** serialization **)

type tree = Leaf of string | Node of string * (tree list)

module ExpSYMTree : ExpSYM with type repr = tree = struct
  type repr = tree
  let lit n = Node ("Lit", [Leaf (string_of_int n)])
  let neg e = Node ("Neg", [e])
  let add e1 e2 = Node ("Add", [e1; e2])
end

(* utop # tf1 (module ExpSYMTree);;
- : tree =
Node ("Add",    
 [Node ("Lit", [Leaf "8"]);
  Node ("Neg",
   [Node ("Add", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])])
*)

module MulSYMTree : MulSYM with type repr = tree = struct
  type repr = tree
  let mul e1 e2 = Node ("Mul", [e1; e2])
end

(* 
# tfm1 (module ExpSYMTree) (module MulSYMTree);;
- : tree =
Node ("Add",
 [Node ("Lit", [Leaf "7"]);
  Node ("Neg",
   [Node ("Mul", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])])
*)

(* let safeRead s= match s with
| [(x, "")] -> Right x
| _ -> Left ("Read error: " ^ s) *)
type ctx = Pos | Neg

module ExpSYMneg (S : ExpSYM) : (ExpSYM with type repr = ctx -> S.repr) = struct
  type repr = ctx -> S.repr
  let lit n = function Pos -> S.lit n | Neg -> S.neg (S.lit n)
  let neg e = function Pos -> e Neg | Neg -> e Pos
  let add e1 e2 ctx = S.add (e1 ctx) (e2 ctx)
end


(** relation between initial and final expressions **)

type exp = Lit of int | Neg of exp | Add of exp * exp

module ExpSYMExp : ExpSYM with type repr = exp = struct 
  type repr = exp
  let lit n = Lit n
  let neg e = Neg e
  let add e1 e2 = Add (e1, e2)
end

let rec finalize : type a. (module ExpSYM with type repr = a) -> exp -> a =
fun (module S : ExpSYM with type repr = a) x ->
  let open S in match x with
    | Lit n -> lit n
    | Neg e -> neg (finalize (module S : ExpSYM with type repr = a) e)
    | Add (e1, e2) -> add (finalize (module S : ExpSYM with type repr = a) e1) (finalize (module S : ExpSYM with type repr = a) e2)

(*
utop # tf1 (module ExpSYMExp) |> finalize (module ExpSYMInt);;
- : int = 5
utop # tf1 (module ExpSYMExp) |> finalize (module ExpSYMString);;
- : bytes = "(8+-(1+2))"
*)

basic_mi.ml

(** basic definition **)

module type ExpSYM = sig
  type repr
  val lit : int -> repr
  val neg : repr -> repr
  val add : repr -> repr -> repr  
end

implicit module ExpSYMInt : ExpSYM with type repr = int = struct
  type repr = int
  let lit n = n
  let neg e = - e
  let add e1 e2 = e1 + e2
end


implicit module ExpSYMString : ExpSYM with type repr = string = struct
  type repr = string
  let lit n = string_of_int n
  let neg e = "-" ^ e
  let add e1 e2 = "(" ^ e1 ^ "+" ^ e2 ^ ")"
end

let eval : int -> int = fun x -> x
let show : string -> string = fun x -> x

let tf1 {S : ExpSYM} ctx =
let open S in
add (lit 8) (neg (add (lit 1) (lit 2)))
|> ctx

(*
# tf1 eval;;
- : int = 5
# tf1 show;;
- : string = "(8+-(1+2))" 
*)


(** extension with mul **)

module type MulSYM = sig
  type repr
  val mul : repr -> repr -> repr
end

implicit module MulSYMInt : MulSYM with type repr = int = struct
  type repr = int
  let mul e1 e2 = e1 * e2
end

implicit module MulSYMString : MulSYM with type repr = string = struct
  type repr = string
  let mul e1 e2 = "(" ^ e1 ^ "*" ^ e2 ^ ")"
end

let tfm1 (type a) {S1 : ExpSYM with type repr = a} {S2 : MulSYM with type repr = a} (ctx : a -> a) = 
  let open S1 in
  let open S2 in
  add (lit 7) (neg (mul (lit 1) (lit 2)))
  |> ctx

(*
# tfm1 eval;;
- : int = 5
# tfm1 show;;
- : string = "(7+-(1*2))" 
*)


(** serialization **)

type tree = Leaf of string | Node of string * (tree list)

implicit module ExpSYMTree : ExpSYM with type repr = tree = struct
  type repr = tree
  let lit n = Node ("Lit", [Leaf (string_of_int n)])
  let neg e = Node ("Neg", [e])
  let add e1 e2 = Node ("Add", [e1; e2])
end

let toTree : tree -> tree = fun x -> x

(* 
# tf1 toTree;;
- : tree =
Node ("Add",
 [Node ("Lit", [Leaf "8"]);
  Node ("Neg",
   [Node ("Add", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])
*)

implicit module MulSYMTree : MulSYM with type repr = tree = struct
  type repr = tree
  let mul e1 e2 = Node ("Mul", [e1; e2])
end

(* 
# tfm1 toTree;;
- : tree =
Node ("Add",
 [Node ("Lit", [Leaf "7"]);
  Node ("Neg",
   [Node ("Mul", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])])
*)


(** pattern-matching **)

type ctx = Pos | Neg

implicit module ExpSYMneg {S : ExpSYM} : (ExpSYM with type repr = ctx -> S.repr) = struct
  type repr = ctx -> S.repr
  let lit n = function Pos -> S.lit n | Neg -> S.neg (S.lit n)
  let neg e = function Pos -> e Neg | Neg -> e Pos
  let add e1 e2 ctx = S.add (e1 ctx) (e2 ctx)
end

let push_neg (type a) (f : a -> a) : (ctx -> a) -> (ctx -> a) = fun e -> e

(* 
# tf1 (push_neg eval) Pos;;
- : int = 5
# tf1 (push_neg show) Pos;;
- : string = "(8+(-1+-2))"
*)

implicit module MulSYMneg {S : MulSYM} : (MulSYM with type repr = ctx -> S.repr) = struct
  type repr = ctx -> S.repr
  let mul e1 e2 ctx = S.mul (e1 ctx) (e2 ctx)
end

(* 
# tfm1 (push_neg show) Pos;;
- : string = "(7+(-1*-2))"
# tfm1 (push_neg eval) Pos;;a
- : int = 9 
*)


(** relation **)

type exp = Lit of int | Neg of exp | Add of exp * exp

implicit module ExpSYMExp : ExpSYM with type repr = exp = struct 
  type repr = exp
  let lit n = Lit n
  let neg e = Neg e
  let add e1 e2 = Add (e1, e2)
end

let initialize : exp -> exp = fun e -> e

let rec finalize : type a. {S : ExpSYM with type repr = a} -> exp -> a =
fun {S : ExpSYM with type repr = a} x ->
  let open S in match x with
    | Lit n -> lit n
    | Neg e -> neg (finalize e)
    | Add (e1, e2) -> add (finalize e1) (finalize e2)

let finalize : type a. {S : ExpSYM with type repr = a} -> (a -> a) -> exp -> a = fun {S : ExpSYM with type repr = a} f x ->
  let rec aux : type a. {S : ExpSYM with type repr = a} -> exp -> a =
    fun {S : ExpSYM with type repr = a} x ->
      let open S in match x with
        | Lit n -> lit n
        | Neg e -> neg (aux e)
        | Add (e1, e2) -> add (aux e1) (aux e2) in
  aux x |> f


(*
# tf1 initialize;;
  - : exp = Add (Lit 8, Neg (Add (Lit 1, Lit 2))) 
*)

(* 
# tf1 initialize |> (finalize eval);;
- : int = 5
# tf1 initialize |> (finalize show);;
- : string = "(8+-(1+2))"
# tf1 initialize |> (finalize toTree);;
- : tree =
Node ("Add",
 [Node ("Lit", [Leaf "8"]);
   Node ("Neg",
    [Node ("Add", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])])
 *)

tagless_final_hoas_mi.ml

(** tagless final with hoas **)

module type Symantics = sig
  type 'a repr
  val int : int -> int repr
  val add : int repr -> int repr -> int repr
  val lam : ('a repr -> 'b repr) -> ('a -> 'b) repr
  val app : ('a -> 'b) repr -> 'a repr -> 'b repr
end

type 'a r = R of 'a
let unR = function R x -> x

implicit module SymanticR : Symantics with type 'a repr = 'a r = struct
  type 'a repr = 'a r
  let int x = R x
  let add e1 e2 = R (unR e1 + unR e2)
  let lam f = R (fun x -> R x |> f |> unR)
  let app e1 e2 = R (unR e1 (unR e2))
end

(* type varCounter = int *)
(* type 'a s = S of (varCounter -> string) *)
type 'a s = S of (int -> string)
let unS = function S x -> x

implicit module SymanticS : Symantics with type 'a repr = 'a s = struct
  type 'a repr = 'a s
  let int x = S (fun _ -> string_of_int x)
  let add e1 e2 = S (fun h -> "(" ^ unS e1 h ^ "+" ^ unS e2 h ^ ")")
  let lam e = S (fun h -> let x = "x" ^ string_of_int h in
                          "("^x^" -> "^ (unS (e (S (fun _ ->x)))) (h+1) ^")")
  let app e1 e2 = S (fun h -> "(" ^ unS e1 h ^ " " ^ unS e2 h ^ ")")
end

let th1 {M : Symantics} f = 
  M.(app (lam (fun x -> add x x)) (int 21)) |> f

let eval = unR
let show x = unS x 0

(*
# th1 eval;;
- : int = 42
# th1 show;;
- : string = "((x0 -> (x0+x0)) 21)"
*)

tagless_final_mi.ml

(** tagless final **)

module type Symantics = sig
  type ('a, 'b) repr
  val int : int -> ('h, int) repr
  val add : ('h, int) repr -> ('h, int) repr -> ('h, int) repr
  val z : (('a * 'h), 'a) repr
  val s : ('h, 'a) repr -> ('any * 'h, 'a) repr 
  val lam : ('a * 'h, 'b) repr -> ('h, 'a -> 'b) repr
  val app : ('h, 'a -> 'b) repr -> ('h, 'a) repr -> ('h, 'b) repr
end

type ('h, 'a) r = R of ('h -> 'a)
let unR = function R f -> f

implicit module SymanticsR : Symantics with type ('a, 'b) repr = ('a, 'b) r = struct
  type ('a, 'b) repr = ('a, 'b) r
  let int x = R (fun _ -> x)
  let add e1 e2 = R (fun h -> unR e1 h + unR e2 h)
  let z = R (fun (x, _) -> x)
  let s v = R (fun (_, h) -> unR v h)
  let lam e = R (fun h x -> unR e (x, h))
  let app e1 e2 = R (fun h -> (unR e1 h) (unR e2 h))
end

type ('h, 'a) s = S of (int -> string)
let unS = function S f -> f

implicit module SymanticsS : Symantics with type ('a, 'b) repr = ('a, 'b) s = struct
  type ('a, 'b) repr = ('a, 'b) s
  let int x = S (fun _ -> string_of_int x)
  let add e1 e2 = S (fun h -> "(" ^ unS e1 h ^ "+" ^ unS e2 h ^ ")")
  let z = S (fun h -> "x" ^ string_of_int (h-1))
  let s v = S (fun h -> unS v (h-1))
  let lam e = S (fun h ->
                  let x = "x" ^ string_of_int h in
                  "(\\" ^ x ^ " -> " ^ unS e (h+1) ^ ")")
  let app e1 e2 = S (fun h -> "(" ^ unS e1 h ^ " " ^ unS e2 h ^ ")")
end

let th1 {M : Symantics} f = 
  M.(app (lam (add z z)) (int 21)) |> f

let eval x = unR x ()
let show x = unS x 0

(*
# th1 eval;;
- : int = 42
# th1 show;;
- : string = "((\\x0 -> (x0+x0)) 21)"
*)