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

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?

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.

I believe you've answered your own question. A module type in ocaml is an interface which you cannot look behind. Otherwise, there's no point. You cannot keep the generality of the interface while exposing details of the implementation. The only thing you can use is what's been exposed through the interface.

My answer to your question is yes, there might be something you can do to your definition of stack, that would make the type of a stack a little more complex, thereby making it match a different pattern than just a single value, like (val,val) for instance. However, you've got a fine definition of a stack to work with, and adding more type-fluff is probably a bad idea.

Some suggestions with regards to your definitions:

1. Rename the following functions: cons => push, head => peek, tail => pop_. I would also add a function val pop : 'a t -> 'a * 'a t, in order to combine head and tail into one function, as well as to mirror cons. Your current naming scheme seems to imply that a list is backing your stack, which is a mental leak of the implementation :D.
2. Why do eq, lt, and leq take a pair as the first parameter? In constraining the type of eq to be val eq : 'a t * 'a t -> 'a t, you're forcing the programmer that uses your interface to keep around one side of the equality predicate until they've got the other side, before finally applying the function. Unless you have a very good reason, I would use the default curried form of the function, since it provides a little more freedom to the user (val eq : 'a t -> 'a t -> 'a t). The freedom comes in that they can partially apply eq and pass the function around instead of the value and function together.