Help to understand the module declaration

Learning
1 
module Make_Set (Elt : EQ) : SET with type elt = Elt.t = struct
  type elt = Elt.t
  type t = elt list

  let empty = []

  let rec is_element i set =
    match set with [] -> false | x :: xs -> Elt.eq x i || is_element i xs

  let add i set = if is_element i set then set else i :: set
end

I couldn’t understand the SET with type elt = Elt.t , I can’t find in official documentation about sth like with type

2

manual and course (the keyword to google is ‘type constraint’)

1 Like
3

Hi, @george_hu! This is no replacement for the resources @n4323 shared, but it might help.

Simplifying to a minimal example, a module declaration

module M : S with 
  type t = u 
= <structure>

declares that the module identifier M is bound to a structure that must satisfy the interface S, with the additional constraint that the the type t in S is equal to the type u (whatever u may be)

This can be used to establish type equalities that preserve information about types that would otherwise be abstract (and so remain totally opaque).

Here is a concrete example from the standard library, illustrated in utop:

(* Note how the type `t` in this module type is abstract: 
   we have no info about how it is constructed or deconstructed: *)
# #show Set.OrderedType;;
module type OrderedType = sig type t val compare : t -> t -> int end

(* This shows that the module `Int` can implement the  `Set.OrderedType` interface, 
   and we are binding  that implementation to the module identifier `IntEx`.
   Note how the module type of `IntEx` is just `Set.OrderedType`, 
   and we still have no additional information. *) 
# module IntEx : Set.OrderedType = Int;;
module IntEx : Set.OrderedType


(* In particular, we cannot call `compare`  on values of type `Int.t`, 
   because from the outside we don't know that `IntEx.t = Int.t = int`: *)
# IntEx.compare 2 3;;
Error: This expression has type int but an expression was expected of type
         IntEx.t

(* Now, instead, we use a type constraint when we bind `IntEx`.
   Note how we now get visibility into the structure of `type t` now: *)
# module IntEx : Set.OrderedType with type t = Int.t = Int;;
module IntEx : sig type t = int val compare : t -> t -> t end

(* Since we now know, from outside the module, that `IntEx.t = Int.t`
   we can apply `IntEx.compare` on values of type `Int.t`: *)
# IntEx.compare 2 3;;
- : int = -1

In the context of your code example, the with type constraint shares the stated type equality with whoever uses the Make_Set functor, allowing code to know that the type of set elements elt in the resulting implementation of SET are the same as the type Elt.t over which the equality relation specified in EQ is defined. To help drive the point home, you could try removing that constraint and then seeing what you can and can’t do with implementations of SET constructed using Make_Set.

5 Likes
4

I see, thanks a lot!

1 Like