Can I avoid committing to particular types in a module type and still get pattern matching?

Question

I have two module types:

module type ORDERED =
    sig
        type t
        val eq  : t * t -> bool
        val lt  : t * t -> bool
        val leq : t * t -> bool
    end
module type STACK =
    sig
        exception Empty 
        type 'a t
        val empty   : 'a t
        val isEmpty : 'a t -> bool  
        val cons        : 'a * 'a t -> 'a t
        val head        : 'a t -> 'a
        val tail        : 'a t -> 'a t
        val length  : 'a t -> int
    end

I want to write a functor which "lifts" the order relation from the basic ORDERED type to STACKs of that type. That can be done by saying that, for example, two stacks of elements will be equal if all its individual elements are equal. And that stacks s1 and s2 are s.t. s1 < s2 if the first of each of their elements, e1 and e2, are also s.t. e1 < e2, etc.

Now, if don't commit to explicitly defining the type in the module type, I will have to write something like this (or won't I?):

module StackLift (O : ORDERED) (S : STACK) : ORDERED =  
  struct
    type t = O.t S.t
    let rec eq (x,y) =
      if S.isEmpty x
        then if S.isEmpty y
        then true
            else false
    else if S.isEmpty y
        then false
        else if O.eq (S.head x,S.head y)
            then eq (S.tail x, S.tail y)
            else false
     (*  etc for lt and leq  *)
  end

which is a very clumsy way of doing what pattern matching serves so well. An alternative would be to impose the definition of type STACK.t using explicit constructors, but that would tie my general module somewhat to a particular implementation, which I don't want to do.

Question: can I define something different above so that I can still use pattern matching while at the same time keeping the generality of the module types?

I agree with axle, your ORDERED is a bit weird. One other thing though, if you had STACK a functor, then STACK itself could have a eq,lt,.. functions, and can be directly used as an ORDERED module; no need for a third module, or a secondary data-type to create a comparison function. As long as a subset of the functions in a module match a module used for a functor, it can be used in that functor. — nlucaroni
It's a bit off-topic, but rather than three boolean functions, I would rather use a type order = Lt | Eq | Gt and compare : 't -> t -> order. It's even a good idea to have it internally, as it allows more code factoring that three separate and often redundant lt/eq/gt functions. — gasche
@Gasche, wouldn't implementing compare : t -> t -> int be more productive? — nlucaroni
@nlucaroni: would certainly be compatible with most comparison-related standard library functions (such as sorts). — Victor Nicollet
@gasche Yes, it makes sense to me. Thanks for the suggestion. — Surikator

antonakos antonakos · Accepted Answer · 2011-02-17T15:59:46

As an alternative or supplement to the other access functions, the module can provide a view function that returns a variant type to use in pattern matching.

type ('a, 's) stack_view = Nil | Cons of 'a * 's

module type STACK =
sig
  val view : 'a t -> ('a , 'a t) stack_view
  ...
end

module StackLift (O : ORDERED) (S : STACK) : ORDERED =
struct
  let rec eq (x, y) =
    match S.view x, S.view y with
        Cons (x, xs), Cons (y, ys) -> O.eq (x, y) && eq (xs, ys)
      | Nil, Nil -> true
      | _ -> false
  ...
end

Any stack with a head and tail function can have a view function too, regardless of the underlying data structure.

Can I avoid committing to particular types in a module type and still get pattern matching?

2 Answers