Last active
October 21, 2023 11:51
-
-
Save PhotonQuantum/9e0e319bc889f8630871ed25a3bb29a7 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[@@@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