Sigma Pi monad

sigma-pi-monad.ml

(* See https://github.com/snowleopard/selective/blob/master/src/Control/Selective/Multi.hs *)

module Sigma (T : sig
  type 'a t
end) =
struct
  type t = Sigma : 'a T.t * 'a -> t
end

module type T = sig
  type t
end

module Two (A : T) (B : T) = struct
  type 'a t =
    | A : A.t t
    | B : B.t t
end

module Many (A : T) = struct
  type 'a t = Many : A.t -> unit t
end

module Either (A : T) (B : T) = Sigma (Two (A) (B))

let from_result : (int, string) result -> Either(Int)(String).t = function
  | Ok i -> Sigma (A, i)
  | Error s -> Sigma (B, s)

let to_result : Either(Int)(String).t -> (int, string) result = function
  | Sigma (A, i) -> Ok i
  | Sigma (B, s) -> Error s

module type Monad = sig
  type 'a f

  val map : 'a f -> f:('a -> 'b) -> 'b f

  module Case (T : sig
    type 'a t
  end) : sig
    type 'a pi = { run : 'x. 'x T.t -> ('x -> 'a) f }

    val case : Sigma(T).t f -> 'a pi -> 'a f
  end
end

module Bind (M : Monad) = struct
  open M

  let bind (type a b) (x : a f) (f : a -> b f) : b f =
    let module A = struct
      type t = a
    end in
    let module Case = Case (Many (A)) in
    let sigma = map x ~f:(fun a -> (Sigma (Many a, ()) : Sigma(Many(A)).t)) in
    let pi : b Case.pi =
      { run =
          (fun (type x) ->
            ( function
              | Many a -> map (f a) ~f:(fun b () -> b)
              : x Many(A).t -> (x -> b) f ))
      }
    in
    Case.case sigma pi
end