substruct.ml

(* -*- Interfaces -*- *)

module type ORDERED = sig
  type ('a, 'b) t
end

module type LINEAR = sig
  include ORDERED

  val exchange : 'a 'b. ('a, 'b) t -> ('b, 'a) t
end

module type AFFINE = sig
  include LINEAR

  val weakening : 'a 'b. ('a, 'b) t -> 'a
end

module type RELEVANT = sig
  include LINEAR

  val contraction : 'a 'b. 'a -> ('a, 'a) t
end

module type NORMAL = sig
  include AFFINE
  include RELEVANT with type ('a, 'b) t := ('a, 'b) t
end

(* -*- Impls -*- *)

module Pair : NORMAL = struct
  type ('a, 'b) t = 'a * 'b

  let exchange (a, b) = (b, a)
  let weakening (a, _) = a
  let contraction a = (a, a)
end

module Relevant_pair : RELEVANT = Pair
module Affine_pair : AFFINE = Pair
module Linear_pair : LINEAR = Pair
module Ordered_pair : ORDERED = Pair

module Eq : NORMAL = struct
  type (_, _) t = Refl : 'a. 'a -> ('a, 'a) t

  let exchange : type a b. (a, b) t -> (b, a) t = function
    | Refl a -> Refl a

  let weakening : type a b. (a, b) t -> a = function
    | Refl a -> a

  let contraction : type a. a -> (a, a) t = function
    | a -> Refl a
end

module Partial_eq : AFFINE = Eq
module Eq_without_J : RELEVANT = Eq
module Partial_eq_without_J : LINEAR = Eq
module Preorder_without_J : ORDERED = Eq