Conversion from applicative general form to applicative normal form

convert.ml

(* by Jeremy Yallop *)


(** The applicative interface *)
module type APPLICATIVE =
sig
  type +'a t
  val pure : 'a -> 'a t
  val (<*>) : ('a -> 'b) t -> 'a t -> 'b t
end

(** Applicative normal form *)
module type APPLICATIVE_NORMAL =
sig
  type +'a carrier
  (** The underlying applicative type *)

  type +'a t =
      Pure : 'a -> 'a t
    | Apply : ('a -> 'b) t * 'a carrier -> 'b t
  (** The normal form *)

  include APPLICATIVE with type 'a t := 'a t
  (** Pull in pure and <*> *)

  val lift : 'a carrier -> 'a t
  (** Lift a primitive computation from the underlying applicative *)

  val run : 'a t -> 'a carrier
  (** Translate a computation from normal form back into the
      underlying applicative *)
end

(** Conversion to applicative normal form *)
module Normal(A: APPLICATIVE)
  : APPLICATIVE_NORMAL with type 'a carrier = 'a A.t =
struct
  type 'a carrier = 'a A.t

  let compose f g x = f (g x)
  let id x = x

  type +'a t =
      Pure : 'a -> 'a t
    | Apply : ('a -> 'b) t * 'a carrier -> 'b t

  let pure v = Pure v

  let rec (<*>) : type a b. (a -> b) t -> a t -> b t =
    fun f p -> match f, p with
        Pure f, Pure v -> Pure (f v)                           
        (*homomorphism law *)
      | u, Apply (v, w) -> Apply (Pure compose <*> u <*> v, w) 
        (*composition law *)
      | u, Pure x -> Pure ((|>)x) <*> u
        (*interchange law *)

  let lift : type a. a A.t -> a t =
    fun i -> Apply (Pure id, i) 
    (* identity law *)

  let rec run : type a. a t -> a carrier = function
      Pure v -> A.pure v                (* first morphism law *)
    | Apply (f, t) -> A.(<*>) (run f) t (* second morphism law *)
end