disjunction funsies with GADTs

Or_gadt.ml

type left = private Left_tag
type right = private Right_tag

type ('ctr, 'left, 'right) t =
  | Left : 'a 'b. 'a -> (left, 'a, 'b) t
  | Right : 'a 'b. 'b -> (right, 'a, 'b) t

let introduction_left : type a b. a -> (left, a, b) t =
  fun a -> Left a

let introduction_right : type a b. b -> (right, a, b) t =
  fun b -> Right b

let elimination
  : type ctr a b c. (a -> c) -> (b -> c) -> (ctr, a, b) t -> c
  =
  fun left_elimination right_elimination -> function
  | Left a -> left_elimination a
  | Right b -> right_elimination b

module Reflexivity = struct
  type ('ctr, 'ty) witness =
    | To_left : 'a. (left, 'a, 'a) t -> (left, 'a) witness
    | To_right : 'b. (right, 'b, 'b) t -> (right, 'b) witness

  let witness_elimination
    : type ctr a. (ctr, a) witness -> (ctr, a, a) t
    = function
    | To_left (Left a) -> Left a
    | To_right (Right b) -> Right b

  type 'ty t =
    | Reflexivity : 'ctr 'a. ('ctr, 'a) witness -> 'a t

  let introduction : type a. a -> a t =
    fun x -> Reflexivity (To_left (Left x))
end

module Symmetry = struct
  type ('ctr, 'a, 'b) witness =
    | From_left :
        'a 'b.
        (left, 'a, 'b) t
        -> (right, 'a, 'b) witness
    | From_right :
        'a 'b.
        (right, 'a, 'b) t
        -> (left, 'a, 'b) witness

  let witness_elimination
    : type ctr a b. (ctr, a, b) witness -> (ctr, b, a) t
    = function
    | From_left (Left a) -> Right a
    | From_right (Right b) -> Left b

  type ('a, 'b) _t =
    | Symmetry :
        'ctr 'a 'b.
        ('ctr, 'a, 'b) witness
        -> ('a, 'b) _t

  let introduction : type ctr a b. (ctr, a, b) t -> (a, b) _t
    = function
    | Left a -> Symmetry (From_left (Left a))
    | Right b -> Symmetry (From_right (Right b))

  type ('a, 'b) t = ('a, 'b) _t
end

let identity_left : type ctr b. (ctr, False.t, b) t -> b
  = function
  | Right b -> b

let identity_right : type ctr a. (ctr, a, False.t) t -> a
  = function
  | Left a -> a