natural_builder.ml

module type NATURAL = sig
  type t

  val build : ((t -> t) -> t -> t) -> t
end

module type BUILD_NATURAL = functor
  (M : sig
     type t

     val succ : t -> t
     val zero : t
   end)
  -> NATURAL with type t = M.t

module BuildNatural : BUILD_NATURAL =
functor
  (M : sig
     type t

     val succ : t -> t
     val zero : t
   end)
  ->
  struct
    type t = M.t

    let build f = M.(f succ zero)
  end

module NaturalInt : NATURAL with type t = int = BuildNatural (struct
  type t = int

  let succ n = n + 1
  let zero = 0
end)

type pad = [ `Void ]

module NaturalList : NATURAL with type t = pad list = BuildNatural (struct
  type t = pad list

  let succ l = `Void :: l
  let zero = []
end)

let nat (type a) (module M : NATURAL with type t = a) = M.build
let four m = m |> Fun.flip nat @@ fun s z -> z |> s |> s |> s |> s
let list_repr = (module NaturalList : NATURAL with type t = [ `Void ] list) |> four
let int_repr = (module NaturalInt : NATURAL with type t = int) |> four