package octez-proto-libs

  1. Overview
  2. Docs
package octez-proto-libs
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module provides support for type equalities and runtime type identifiers.

For two types a and b, (a, b) eq is a witness that a = b. This is a standard generalized algebraic datatype on top of which type-level programming techniques can be implemented.

Given a type a, an inhabitant of a t is a dynamic identifier for a. Identifiers can be compared for equality. They are also equipped with a hash function.

WARNING: the hash function changes at every run. Therefore, the result of the hash function should never be stored.

Notice that dynamic identifiers are not unique: two identifiers for a can have distinct hash and can be physically distinct. Hence, only eq can decide if two type identifiers correspond to the same type.

type (_, _) eq =
  1. | Refl : ('a, 'a) eq

A proof witness that two types are equal.

type 'a t

A dynamic representation for 'a.

val make : unit -> 'a t

make () is a dynamic representation for 'a. A fresh identifier is returned each time make () is evaluated.

val eq : 'a t -> 'b t -> ('a, 'b) eq option

eq ida idb returns a proof that a = b if ida and idb identify the same type.

val hash : 'a t -> int

hash id returns a hash for id.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct