Skip to content

Instantly share code, notes, and snippets.

@PhotonQuantum
Last active October 21, 2023 11:51
Show Gist options
  • Save PhotonQuantum/9e0e319bc889f8630871ed25a3bb29a7 to your computer and use it in GitHub Desktop.
Save PhotonQuantum/9e0e319bc889f8630871ed25a3bb29a7 to your computer and use it in GitHub Desktop.
[@@@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'')
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment