I have been looking for a way to formulate the interfaces of container modules such as Map and Set in a way that allows clients to avoid recursive modules. I have not found an entirely satisfactory solution, and I wonder whether anyone has other ideas or type system tricks.
As an example, consider the manual’s recursive modules example:
module rec A : sig
type t = Leaf of string | Node of ASet.t
val compare : t -> t -> int
end = struct
type t = Leaf of string | Node of ASet.t
let compare t1 t2 =
match (t1, t2) with
| Leaf s1, Leaf s2 -> Stdlib.compare s1 s2
| Leaf _, Node _ -> 1
| Node _, Leaf _ -> -1
| Node n1, Node n2 -> ASet.compare n1 n2
end
and ASet : (Set.S with type elt = A.t) = Set.Make (A)
I would like to write such code, where the main type being defined A.t appears in the argument of a functor to define a type ASet.t that appears in the definition of A.t, without using recursive modules. Note that the motivation is not so much to avoid recursive modules, but to enable the compiler to statically resolve calls to functions whose definitions follow a cycle through the recursive modules. For example, A.compare is defined in terms of ASet.compare, which is itself defined in terms of A.compare. Previous discussion has revealed that recursive modules make this hard or impossible for the compiler.
Currently the best I have found is:
module A = struct
module T = struct
type compare
type t = Leaf of string | Node of aset
and aset = (t, compare) Set.t
let rec compare t1 t2 =
match (t1, t2) with
| Leaf s1, Leaf s2 -> Stdlib.compare s1 s2
| Leaf _, Node _ -> 1
| Node _, Leaf _ -> -1
| Node n1, Node n2 -> Set.compare compare n1 n2
end
include T
include Comparer.Counterfeit (T)
end
module ASet = Set.Make (A)
This uses an interface of the Set module where the type of sets is polymorphic in the element type as well as a phantom type parameter used as a singleton denoting the comparison function for elements.
module Set : sig
type ('elt, 'cmp) t
val compare : ('elt -> 'elt -> int) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> int
(* ... *)
end
The relationship between comparison functions and these phantom types uses a “Comparer” module:
module Comparer : sig
(** 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
type compare
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 : OrderedType) : S with type t = Ord.t
(* ... *)
end
The key is that applying the Comparer.Make functor is used ensure that the compare type in the result uniquely corresponds to the compare function given in the functor argument. This is very similar to the approach taken in Base with Comparators. Then a container such as a Set is built from a Comparer rather than just an OrderedType:
module Set : sig
module type S = sig
type elt
type t
include Comparer.S with type t := t
(* ... *)
end
module Make (Ord : Comparer.S) : S (* with type... *)
Crucial to avoiding recursive modules in the A-ASet example above is the ability to define the compare type and use it to instantiate Set.t without applying a functor that accepts the A.t type or the A.compare function. This is where Comparer.Counterfeit comes in:
module Comparer : sig
(* ... *)
(** [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
include OrderedType
type compare
end) : S with type t = Ord.t with type compare = Ord.compare
Counterfeit just trusts the caller that the given compare type is a singleton denoting only the given compare function. This enables writing this sort of code without recursive modules, and the compiler does optimize it better, but it opens a dissatisfying hole in the type system (although not as worrying as using Obj.magic would be). The situation is also not as bad as not distinguishing between different sets with the same element type at all, since the client code must explicitly apply Comparer.Counterfeit, but this is still not great.
So at some level, this approach does not really work. Does anyone know a better one?
For reference and clarity, here is code that is complete enough to type-check by itself:
module type OrderedType = sig
type t
val compare : t -> t -> int
end
(** Singleton types for compare functions *)
module Comparer : sig
(** 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
type compare
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 : OrderedType) : 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
include OrderedType
type compare
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
type 'compare_a compare
val compare :
('a -> 'a -> int) -> ('a, 'compare_a) t -> ('a, 'compare_a) t -> int
end)
(A : S) : sig
include OrderedType with type t = (A.t, A.compare) F.t
include S with type t := t with type compare = A.compare F.compare
end
end = struct
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
val comparer : (t, compare) comparer
end
module Make (Ord : OrderedType) = struct
type t = Ord.t
type compare
let comparer = Ord.compare
end
module Counterfeit (Ord : sig
include OrderedType
type compare
end) =
struct
type t = Ord.t
type compare = Ord.compare
let comparer = Ord.compare
end
module Apply (F : sig
type ('a, 'compare_a) t
val compare :
('a -> 'a -> int) -> ('a, 'compare_a) t -> ('a, 'compare_a) t -> int
type 'compare_a compare
end)
(A : S) =
struct
type t = (A.t, A.compare) F.t
let compare x y = F.compare A.comparer x y
type compare = A.compare F.compare
let comparer = compare
end
end
(** Set adapted to the Comparer interface *)
module Set : sig
module type S = sig
type elt
type t
include Comparer.S with type t := t
val empty : t
val mem : elt -> t -> bool
val add : elt -> t -> t
end
type ('elt, 'cmp) t
val compare :
('elt -> 'elt -> int) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> int
type 'compare_elt compare
module Make (Ord : Comparer.S) :
S
with type elt = Ord.t
with type t = (Ord.t, Ord.compare) t
with type compare = Ord.compare compare
end = struct
module type S = sig
type elt
type t
include Comparer.S with type t := t
val empty : t
val mem : elt -> t -> bool
val add : elt -> t -> t
end
module T = struct
type ('elt, 'cmp) t =
| Empty
| Node of {l: ('elt, 'cmp) t; v: 'elt; r: ('elt, 'cmp) t; h: int}
type ('elt, 'cmp) enumeration =
| End
| More of 'elt * ('elt, 'cmp) t * ('elt, 'cmp) enumeration
let rec cons_enum s e =
match s with
| Empty -> e
| Node {l; v; r} -> cons_enum l (More (v, r, e))
let compare compare_elt s1 s2 =
let rec compare_aux e1 e2 =
match (e1, e2) with
| End, End -> 0
| End, _ -> -1
| _, End -> 1
| More (v1, r1, e1), More (v2, r2, e2) ->
let c = compare_elt v1 v2 in
if c <> 0 then c
else compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
in
compare_aux (cons_enum s1 End) (cons_enum s2 End)
type 'compare_elt compare
end
include T
module Make (Cmp : Comparer.S) = struct
type elt = Cmp.t
include Comparer.Apply (T) (Cmp)
module Ord = struct
include Cmp
let compare = (comparer :> t -> t -> int)
end
let empty = Empty
let rec mem x = function
| Empty -> false
| Node {l; v; r} ->
let c = Ord.compare x v in
c = 0 || mem x (if c < 0 then l else r)
let add _ _ = failwith "omitted for brevity"
end
end
(* now without recursive modules *)
module A = struct
module T = struct
type compare
type t = Leaf of string | Node of aset
and aset = (t, compare) Set.t
let rec compare t1 t2 =
match (t1, t2) with
| Leaf s1, Leaf s2 -> Stdlib.compare s1 s2
| Leaf _, Node _ -> 1
| Node _, Leaf _ -> -1
| Node n1, Node n2 -> Set.compare compare n1 n2
end
include T
include Comparer.Counterfeit (T)
end
module ASet = Set.Make (A)
(* normal, nonrecursive, use *)
(** A normal use *)
module IncreasingInt = Comparer.Make (struct
type t = int
let compare = Int.compare
end)
module IncreasingIntSet = Set.Make (IncreasingInt)
(** Another normal use, with different compare function *)
module DecreasingInt = Comparer.Make (struct
type t = int
let compare x y = -Int.compare x y
end)
module DecreasingIntSet = Set.Make (DecreasingInt)
let () =
let s = IncreasingIntSet.add 1 IncreasingIntSet.empty in
let r = DecreasingIntSet.add 2 DecreasingIntSet.empty in
assert (IncreasingIntSet.mem 1 s) ;
(* IncreasingIntSet.t and DecreasingIntSet.t are incompatible, so the
following does not type-check *)
(* assert (DecreasingIntSet.mem 1 s) ; *)
()
(** Flies in the ointment:
It is up to the user of [Comparer.Counterfeit] to ensure that distinct
[compare] types are always used for distinct [compare] functions, the
type system does not check this.
For example, [Bad] below mixes the decreasing compare function with the
increasing compare type. This yields a set that is type-compatible with
[IncreasingIntSet] but uses the decreasing order internally. With this
definition, the type system cannot prevent operating on set values that
are in the "wrong" order, leading to invalid set values and completely
incorrect results. *)
module Bad : module type of IncreasingIntSet =
Set.Make (Comparer.Counterfeit (struct
type t = int
(* use the decreasing order *)
let compare x y = -Int.compare x y
(* lie that it is the function denoted by the increasing compare type *)
type compare = IncreasingInt.compare
end))