cata.ml

[@@@warnerror "-unused-value-declaration"]

module type Functor = sig
  type ('p, 'fix) t

  val fmap : ('a -> 'b) -> ('p, 'a) t -> ('p, 'b) t
end

let ( <.> ) f g x = f (g x)

module Mu (M : sig
  type ('p, 'fix) t
end) =
struct
  (*
     Inductive type is only allowed if wrapped in a constructor.
     Haskell users can use newtype to avoid this.
  *)
  type 'p mu = In of ('p, 'p mu) M.t

  let inj (In x) = x (* mu -> f mu *)
  let prj x = In x (* f mu -> mu *)

  (* induction principle:
     P t := t -> a
     (P mu -> P (f mu)) -> P mu
  *)
  let rec ind f (In x) = f (ind f) x

  (* ... for two arguments *)
  let rec ind_oo f (In x) (In y) = f (ind_oo f) x y

  (* ... not all arguments must be of type mu *)
  let rec ind_xo f x (In y) = f (ind_xo f) x y
end

module Cata (M : Functor) = struct
  include Mu (M)

  let inj2 = M.fmap inj <.> inj (* mu -> f f mu *)
  let prj2 = prj <.> M.fmap prj (* f f mu -> mu *)

  (* (f a -> a) -> mu -> a *)
  let rec cata f x = f (M.fmap (cata f) (inj x))

  (* (f f a -> a) -> mu -> a *)
  let rec cata2 f x = f (M.fmap (M.fmap (cata2 f)) (inj2 x))

  (* strong induction
     (P mu -> P (f f mu)) -> P mu
  *)
  let rec ind2 f x = f (ind2 f) (inj2 x)
end

module MyList = struct
  module T = struct
    type ('p, 'fix) t = Nil | Cons of 'p * 'fix [@@deriving eq, ord, show]

    let fmap (f : 'a -> 'b) = function
      | Nil -> Nil
      | Cons (x, xs) -> Cons (x, f xs)
  end

  include T
  include Cata (T)

  (* Because of reasons mentioned above, we need to wrap Nil and Cons in `In`. *)
  let mNil = In Nil
  let mCons (x, y) = In (Cons (x, y))
  let to_list = cata (function Nil -> [] | Cons (x, xs) -> x :: xs)
  let len = cata (function Nil -> 0 | Cons (_, xs) -> 1 + xs)
  let equal eq = ind_oo (equal eq)
  let compare cmp = ind_oo (compare cmp)
  let pp p = ind_xo (pp p)
  let show p = Format.asprintf "%a" (pp p)

  let map f =
    prj <.> cata (function Nil -> Nil | Cons (x, xs) -> Cons (f x, In xs))
end

open MyList

let rec pp_std_list (fmt : Format.formatter) (l : int list) =
  match l with
  | [] -> ()
  | x :: xs ->
      Format.fprintf fmt "%d " x;
      pp_std_list fmt xs

let show_std_list (l : int list) = Format.asprintf "%a" pp_std_list l

(* Example for strong induction *)
let add2 =
  prj
  <.> cata2 (function
        | Nil -> Nil
        | Cons (x, Cons (y, xs)) -> Cons (x + y, In xs)
        | Cons (x, Nil) -> Cons (x, In Nil))

let () =
  let l : int mu = mCons (1, mCons (2, mCons (3, mNil))) in
  Printf.printf "len l: %d\n" (len l);
  Printf.printf "to_list l: %s\n" (show_std_list (to_list l));
  Printf.printf "show l: %s\n" (show Format.pp_print_int l);
  let l' : int mu = mCons (1, mCons (2, mCons (4, mNil))) in
  Printf.printf "compare l l': %d\n" (compare Int.compare l l');
  Printf.printf "equal l l': %b\n" (equal Int.equal l l');
  Printf.printf "add2 l' = %s\n" (show Format.pp_print_int (add2 l'));
  let l'' : float mu = map float_of_int l' in
  Printf.printf "show l'': %s\n" (show Format.pp_print_float l'')