From 7cf6e1740396d66db6b96179e913bb2115bbbae4 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 21 Feb 2021 13:16:58 -0800 Subject: [PATCH] [sledge] Add Comparer: type-indexed compare functions Summary: A comparer `('a, 'compare_a) t` for type `'a` is a "compare" function of type `'a -> 'a -> int` tagged with a phantom type `'compare_a` acting as a singleton type denoting an individual compare function. The point of these is to enable writing type definitions of containers that depend on a compare function prior to applying a functor. For example, a type of sorted lists could be exposed as: ``` type elt type (elt, 'compare_elt) t = private elt list ``` and the operations manipulating sorted lists would be defined by a functor that accepts a `Comparer.S` and implements the operations using ``` let compare = (comparer :> elt -> elt -> int) ``` Reviewed By: ngorogiannis Differential Revision: D26250528 fbshipit-source-id: ea61844ec --- sledge/nonstdlib/NS.ml | 1 + sledge/nonstdlib/NS.mli | 1 + sledge/nonstdlib/comparer.ml | 86 +++++++++++++++++++++++++++++++++++ sledge/nonstdlib/comparer.mli | 86 +++++++++++++++++++++++++++++++++++ 4 files changed, 174 insertions(+) create mode 100644 sledge/nonstdlib/comparer.ml create mode 100644 sledge/nonstdlib/comparer.mli diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml index dacbfd770..54acea421 100644 --- a/sledge/nonstdlib/NS.ml +++ b/sledge/nonstdlib/NS.ml @@ -30,6 +30,7 @@ let mapN f e cons xs = let xs' = Array.map_endo ~f xs in if xs' == xs then e else cons xs' +module Comparer = Comparer module Array = Array module Float = Float module HashSet = HashSet diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index a5132404e..604ab765d 100644 --- a/sledge/nonstdlib/NS.mli +++ b/sledge/nonstdlib/NS.mli @@ -146,6 +146,7 @@ include module type of Iter.Import (** Containers *) +module Comparer = Comparer module Option = Option include module type of Option.Import diff --git a/sledge/nonstdlib/comparer.ml b/sledge/nonstdlib/comparer.ml new file mode 100644 index 000000000..651e26adb --- /dev/null +++ b/sledge/nonstdlib/comparer.ml @@ -0,0 +1,86 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Singleton types for compare functions *) + +type ('a, 'compare_a) t = 'a -> 'a -> int + +module type S = sig + type ('a, 'compare_a) comparer := ('a, 'compare_a) t + type t + type compare [@@deriving compare, equal, sexp] + + val comparer : (t, compare) comparer +end + +module type S1 = sig + type ('a, 'compare_a) comparer := ('a, 'compare_a) t + type 'a t + type 'compare_a compare [@@deriving compare, equal, sexp] + + val comparer : + ('a, 'compare_a) comparer -> ('a t, 'compare_a compare) comparer +end + +module Make (Ord : sig + type t [@@deriving compare] +end) = +struct + include Ord + + type compare [@@deriving compare, equal, sexp] + + let comparer = Ord.compare +end + +module Counterfeit (Ord : sig + type t [@@deriving compare] + type compare [@@deriving compare, equal, sexp] +end) = +struct + include Ord + + let comparer = Ord.compare +end + +module Apply (F : sig + type ('a, 'compare_a) t [@@deriving compare] + type 'compare_a compare [@@deriving compare, equal, sexp] +end) +(A : S) = +struct + module A = struct + include A + + let compare = comparer + end + + type t = (A.t, A.compare) F.t [@@deriving compare] + type compare = A.compare F.compare [@@deriving compare, equal, sexp] + + let comparer = compare +end + +module Apply1 (F : sig + type ('a, 'b, 'compare_a) t [@@deriving compare] + type ('compare_a, 'compare_b) compare [@@deriving compare, equal, sexp] +end) +(A : S) = +struct + module A = struct + include A + + let compare = comparer + end + + type 'b t = (A.t, 'b, A.compare) F.t [@@deriving compare] + + type 'b compare = (A.compare, 'b) F.compare + [@@deriving compare, equal, sexp] + + let comparer = compare +end diff --git a/sledge/nonstdlib/comparer.mli b/sledge/nonstdlib/comparer.mli new file mode 100644 index 000000000..ddc76d072 --- /dev/null +++ b/sledge/nonstdlib/comparer.mli @@ -0,0 +1,86 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Singleton types for compare functions *) + +(** A comparer [('a, 'compare_a) t] for type ['a] is a "compare" function of + type ['a -> 'a -> int] tagged with a phantom type ['compare_a] acting as + a singleton type denoting an individual compare function. *) +type ('a, 'compare_a) t = private 'a -> 'a -> int + +module type S = sig + type ('a, 'compare_a) comparer := ('a, 'compare_a) t + type t + + (** [compare] types are equipped with functions to support use of + [@@deriving compare, equal, sexp] on types parameterized by such + singleton types for compare functions. These derived functions are + never actually called, since the compare type parameters are phantom. *) + type compare [@@deriving compare, equal, sexp] + + val comparer : (t, compare) comparer +end + +(** [Make] takes a [compare] function, mints a fresh [compare] type to act + as a singleton type denoting that one compare function, and returns the + [compare] function at a type stamped with its singleton type. In this + way, [Make] applied to two different compare functions for the same type + of values yields comparers with incompatible types. *) +module Make (Ord : sig + type t [@@deriving compare] +end) : S with type t = Ord.t + +(** [Counterfeit] takes a compare function and type and yields a comparer + that asserts that the given [compare] type is a singleton for the given + [compare] function. This is not checked by the type system. It is the + client's responsibility to ensure that distinct types are provided for + distinct compare functions. If the same type is used for multiple + functions, then [Counterfeit] will produce type-compatible comparers + even though the wrapped compare functions differ. *) +module Counterfeit (Ord : sig + type t [@@deriving compare] + type compare [@@deriving compare, equal, sexp] +end) : S with type t = Ord.t with type compare = Ord.compare + +(** [Apply (F) (A)] takes a type [('a, 'compare_a) F.t] with a type + parameter ['a] and a compare type ['compare_a] for ['a], and a comparer + [A], and creates a comparer for [F.t] with ['a] instantiated to [A.t]. *) +module Apply (F : sig + type ('a, 'compare_a) t [@@deriving compare] + type 'compare_a compare [@@deriving compare, equal, sexp] +end) +(A : S) : sig + type t = (A.t, A.compare) F.t [@@deriving compare] + + include S with type t := t with type compare = A.compare F.compare +end + +module type S1 = sig + type ('a, 'compare_a) comparer := ('a, 'compare_a) t + type 'a t + type 'compare_a compare [@@deriving compare, equal, sexp] + + val comparer : + ('a, 'compare_a) comparer -> ('a t, 'compare_a compare) comparer +end + +(** [Apply1 (F) (A)] takes a type [('a, 'b, 'compare_a) F.t] with two type + parameters ['a], ['b] and a compare type ['compare_a] for ['a], and a + comparer [A], and creates a comparer for [F.t] with ['a] instantiated to + [A.t]. *) +module Apply1 (F : sig + type ('a, 'b, 'compare_a) t [@@deriving compare] + type ('compare_a, 'compare_b) compare [@@deriving compare, equal, sexp] +end) +(A : S) : sig + type 'b t = (A.t, 'b, A.compare) F.t [@@deriving compare] + + include + S1 + with type 'b t := 'b t + with type 'compare_b compare = (A.compare, 'compare_b) F.compare +end