Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment