P-HOAS + typed object language = higher-kinded parameter -- finally!

lambda.ml

open Higher

module F = struct

  module Id : Newtype1 with type 'a s = 'a =
    Newtype1 ( struct type 'a t = 'a end )

  module Const (T : sig type t end) : Newtype1 with type 'a s = T.t =
    Newtype1 ( struct type 'a t = T.t end )
end

module Lang = struct

  type ('a, 'v) k = ('a, 'v) app Lazy.t

  type (_, _) t =
    | Var : ('a, 'v) k -> ('a, 'v) t
    | App : ('a -> 'b, 'v) t * ('a, 'v) t -> ('b, 'v) t
    | Lam : (('a, 'v) k -> ('b, 'v) t) -> ('a -> 'b, 'v) t
    | Fix : (('a, 'v) k -> ('a, 'v) t) -> ('a, 'v) t
    | K   : 'a -> ('a, 'v) t

  type 'a term = { t : 'v. ('a, 'v) t }

  let eval { t } =
    let rec ev' : type a. (a, F.Id.t) t -> a = function
      | Var (lazy x) -> F.Id.prj x
      | App (f, a)   -> ev' f (ev' a)
      | Lam f        -> fun x -> ev' (f @@ lazy F.Id.(inj x))
      | K a          -> a
      | Fix f as e   ->
          let rec x = lazy (ev' @@ f (lazy F.Id.(inj @@ Lazy.force x))) in
          Lazy.force x
    in
    ev' t


  module Ident = struct
    type t = int
    let initial = 0
    let next id =
      let s = String.create 1 in
      s.[0] <- Char.chr (id mod 25 + 97) ; (s, succ id)
  end

  let format fmt { t } =

    let module K = F.Const (struct type t = string end) in
    let open Format in

    let rec f1 : type a. Ident.t -> formatter -> (a, K.t) t -> unit =
      fun id fmt -> function
      | Var (lazy x) -> fprintf fmt "@[%s@]" (K.prj x)
      | App (e1, e2) -> fprintf fmt "@[%a@ %a@]" (f1 id) e1 (f2 id) e2
      | Lam fe ->
          let (v, id) = Ident.next id in
          fprintf fmt "@[<3>\206\187%s.%a@]" v (f2 id) (fe @@ lazy K.(inj v))
      | Fix fe ->
          let (v, id) = Ident.next id in
          fprintf fmt "@[<3>Y%s.%a@]" v (f2 id) (fe @@ lazy K.(inj v))
      | K x    -> fprintf fmt "K"

    and f2 : type a. Ident.t -> formatter -> (a, K.t) t -> unit =
      fun id fmt -> function
      | App _ as e -> fprintf fmt "@[<1>(%a)@]" (f1 id) e
      | e          -> f1 id fmt e
    in
    fprintf fmt "@[%a@]" (f1 Ident.initial) t


  let lam  f = Lam (fun x -> f (Var x))
  and lam2 f = Lam (fun x -> Lam (fun y -> f (Var x) (Var y)))
  and lam3 f = Lam (fun x -> Lam (fun y -> Lam (fun z -> f (Var x) (Var y) (Var z))))
  and app  a b     = App (a, b)
  and app2 a b c   = App (App (a, b), c)
  and app3 a b c d = App (App (App (a, b), c), d)
  and var v = Var v


  module Church = struct

    let t = {t=Lam (fun x -> Lam (fun y -> Var x))}
    and f = {t=Lam (fun x -> Lam (fun y -> Var y))}

    let zero = {t=Lam (fun _ -> Lam (fun z -> Var z))}
    and succ = {t=Lam (fun x -> lam2 @@ fun f z -> app f (app2 (var x) f z))}
    and pred = {t=
      Lam (fun x ->
        lam2 @@ fun f z ->
          app3 (var x) (lam2 @@ fun g h -> app h (app g f))
               (lam @@ fun _ -> z)
               (lam @@ fun u -> u)) }


    let one   = {t=App (succ.t, zero.t)}
    let two   = {t=App (succ.t, one.t )}
    let three = {t=App (succ.t, two.t )}

    let null = {t=Lam (fun n -> app2 (var n) (lam @@ fun _ -> f.t) t.t)}

    let add = {t=
      Lam (fun m -> lam3 @@ fun n f z -> app2 (var m) f (app2 n f z)) }
    let mul = {t=
      Lam (fun m -> lam3 @@ fun n f z -> app2 (var m) (app n f) z) }

  end

end

#install_printer Lang.format ;;