package type_eq

  1. Overview
  2. Docs
Type equality proofs for OCaml 4

Install

Dune Dependency

Authors

Maintainers

Sources

type_eq-0.0.1.tbz
sha256=7855592497d4ea17dbf2f28d5ce64b67570772c0ddcc551eadb87645906dd199
sha512=b54629c3eca93c820156d5d4cf1a71fdef3fba07321a8ac068869d7e900e056944d8a02770dd21e4c2bbdcb5376036ddb61b83b33afe7bb355ac59b9b4bb0d63

README.md.html

type_eq

What does this library do?

type_eq provides a simple mechanism for constructing a type proof -- i.e. a binding which knows that two types are the same, even if they are opaque. Here's a short example:

module A : sig
  (* These types are opaque outside of the [A] module. *)
  type a
  type b

  (* This type is not the same as [a] or [b]. *)
  type c

  val a_b_proof : (a, b) Type_eq.t
  (** [a_b_proof] proves that [a] and [b] are the same type -- otherwise a type
      error will be thrown during its construction! *)

  val a_c_proof : (a, c) Type_eq.t
  (** [a_c_proof] proves that [a] and [c] are the same type.

      Unfortunately, [a] and [c] are _not_ the same type, so this cannot be constructed! *)
end = struct
  (* These types are indeed the same! *)
  type a = string
  type b = string
  type c = int

  let a_b_proof = Type_eq.Eq
  let a_c_proof = Type_eq.Eq
  (* This fails with a type error:

     Error: Signature mismatch:
        ...
        Values do not match:
          val a_c_proof : ('a, 'a) Type_eq.t
        is not included in
          val a_c_proof : (b, c) Type_eq.t
        The type (b, b) Type_eq.t is not compatible with the type
          (b, c) Type_eq.t
        Type b is not compatible with type c
  *)
end

Why is this library useful?

Sometimes you'll be working with types which are opaque -- as in the example above. This utility can be used to determine if two opaque types are indeed equal, which can allow you to cast between them, among other operations.

See the .mli file for a fully-documented interface.

Note that a stripped-down version of this utility is included as Type.eq in OCaml 5+: https://github.com/ocaml/ocaml/blob/c2d00ef67b4af1e6ba90e77e4106770bbdd88a01/stdlib/type.ml#L18

OCaml

Innovation. Community. Security.