something with inductive types or whatever

Cygnus2.ml

type inhabited = Inhabited

module Hole = struct
  (* Discriminator for Done *)
  type 'ty value = Value of 'ty

  (* Discriminator for Falling *)
  type nonterm = Nonterm

  type 'value t =
    | Done : 'value -> 'value value t
    (* [Falling] normally has discrim syntactic parameter, but such
      thing is not expressible in OCaml. *)
    | Falling : nonterm t

  type ('left, 'right, 'result) tilde =
    | Id :
        ('left value t * 'right value t)
        -> ('left value t, 'right value t, inhabited value t) tilde
    | Dis : ('left t * 'right t) -> ('left t, 'right t, nonterm t) tilde

  let ( ~= ) : type left right result. (left t, right t, result) tilde -> result
    = function
    | Id (_, _) -> Done Inhabited
    | Dis (_, _) -> Falling
  ;;
end

module type EQUIVALENCE_UP_TO_ISOMORPHISM = sig
  type 'discrim t
  type ('left, 'right, 'result) tilde

  val ( ~= ) : 'left 'right 'result. ('left t, 'right t, 'result) tilde -> 'result
end

module type INDUCTIVE = sig
  type 'discrim t =
    | Epsilon : epsilon_d t
    | Phi : 'discrim t -> 'discrim phi_d t

  and epsilon_d
  and 'discrim phi_d = S : 'discrim t -> 'discrim t phi_d
end

module Add_equivalence (T : INDUCTIVE) :
  EQUIVALENCE_UP_TO_ISOMORPHISM with type 'discrim t = 'discrim T.t = struct
  include T

  type ('left, 'right, 'result) tilde =
    | Both_epsilon :
        (epsilon_d t * epsilon_d t)
        -> (epsilon_d t, epsilon_d t, inhabited Hole.value Hole.t) tilde
    | Both_phi_s :
        ('s phi_d t * 's phi_d t)
        -> ('s phi_d t, 's phi_d t, inhabited Hole.value Hole.t) tilde
    | Dis : ('left t * 'right t) -> ('left t, 'right t, Hole.nonterm Hole.t) tilde

  let ( ~= ) : type left right result. (left t, right t, result) tilde -> result
    = function
    | Both_epsilon (_, _) -> Hole.Done Inhabited
    | Both_phi_s (_, _) -> Hole.Done Inhabited
    | Dis (_, _) -> Hole.Falling
  ;;
end

module H_bool = struct
  type false_d
  type true_d

  type 'discrim t =
    | True : true_d t
    | False : false_d t

  type ('left, 'right, 'result) tilde =
    | And :
        (true_d t * true_d t)
        -> (true_d t, true_d t, inhabited Hole.value Hole.t) tilde
    | Nand :
        (false_d t * false_d t)
        -> (false_d t, false_d t, inhabited Hole.value Hole.t) tilde
    | Dis : ('left t * 'right t) -> ('left t, 'right t, Hole.nonterm Hole.t) tilde

  let ( ~= ) : type left right result. (left t, right t, result) tilde -> result
    = function
    | And (_, _) -> Hole.Done Inhabited
    | Nand (_, _) -> Hole.Done Inhabited
    | Dis (_, _) -> Hole.Falling
  ;;
end

open H_bool

let indeed = ~=(Nand (False, False))

let () =
  match indeed with
  | Done Inhabited -> print_endline "indeed, False ~ False"
;;

https://bsky.app/profile/qexat.com/post/3ljxopoqpi22x