2
$\begingroup$

Say I have a (more general) module type Collection that specifies some operations like read and write and now I want to create (more specialized) module types like Stack & Queue.

Stack for example, should have all operations that Collection has, so we want to save time by including Collection in Stack. However, with stacks, the "write" operation is typically called "push". What is the best way for Stack to reuse Collection while being able to do this renaming?

In the example below, any opaque usage of Stack will only expose wr but not the name push, as in ListStack

Module Type TypElt.
  Parameter t elt : Type.
End TypElt.

Module Type Collection (Import T: TypElt).

  (* Parameter rd : t -> (option elt * t). *)
  Parameter wr : elt -> t -> t.

End Collection.


Module Type Elt .
  Parameter elt : Type.
End Elt.

Module Type Stack (E: Elt).

  Definition elt := E.elt.
  Parameter t : Type.
  Include Collection.

  (* Notation pop := rd. *)
  Notation push := wr. (* <- doesn't achieve what I want *)
  (* Parameter peek : t -> option elt. *)
End Stack.

Module ListStack (E: Elt) <: Stack E.
  
  Definition elt := E.elt.
  Definition t := list elt.
  
  Definition push := @cons elt.

  (* In order to satisfy the Module Type Stack, we must provide an operation, wr *)

  Definition wr := push.

End ListStack.
$\endgroup$
13
  • $\begingroup$ I find your question quite confused/confusing: besides that the example doesn't match the question (you should at least edit that and make it more to the point): you can "reuse" a module, not a module type... That said and fixed, the simple answer here might end up just being: do not Include, rather Import and wrap around it... no? $\endgroup$ Jan 28 at 13:52
  • $\begingroup$ @JulioDiEgidio I'm... not sure which part doesn't match? Nor do I understand you point about module type reuse. That Include works for module types would be evidence for their reuse no? No... I don't see that Importing would give me the behaviour I want, which is to rename a parameter $\endgroup$
    – C.E.Sally
    Jan 29 at 6:59
  • $\begingroup$ Importing for wrapping: and you cannot import a module type. I am a bit perplexed about the example code as e.g. I don't understand why you have a ListStack there, but especially I don't understand why Elt vs a totally unrelated TypElt for what looks like the Key/Value types. Anyway, the point is the only approach for renaming that I can think of is by wrapping around the original module (and that per se cannot be a module type): I am not terribly an expert with Coq, but considering also that nobody else is chiming in, I might just put together an answer along those lines. $\endgroup$ Jan 29 at 10:24
  • $\begingroup$ Indeed, the thing that confuses me most is how you expect to go from (apparently) a keyed collection to a stack, where pop and push only apply to the top-most element, by... just renaming? I mean, to use that code, even just to answer the present question, I'd have to completely ignore what the naming suggests. $\endgroup$ Jan 29 at 11:43
  • $\begingroup$ @JulioDiEgidio: Ah I see. I've used your feedback to hopefully make the question clearer. However, I think you are confused by some of the Coq-isms going on here. TypElt has a type of elements, and collections. t is meant to be abstract type of the collection (This is pretty typical in the stdlib which is why I didn't explain that). This is why t is defined (rather than a parameter) in Stack, while elt is still (ultimately -- via E) a parameter. ListStack is a negative/unsatisfactory example, and illustrates why I want to do the renaming in the module type and not the module. $\endgroup$
    – C.E.Sally
    Jan 30 at 1:12

1 Answer 1

0
$\begingroup$

Notation are not part of the module type. So you need to make it a definition. But if you put a definition in a module type then you must comply to it exactly in the module. So the definition of push must be exactly Definition push := wr.

  Module Type Stack (E: Elt).
    Definition elt := E.elt.
    Parameter t : Type.
    Include Collection.
    Definition push := wr. (* <- push must be exactly wr in any module of type Stack *)
  End Stack.

  Module ListStack (E: Elt) <: Stack E.
    Definition elt := E.elt.
    Definition t := list elt.
    (* In order to satisfy the Module Type Stack, we must provide an operation, wr and rd *)
    (* Definition push := @cons elt. Won't be accepted, cf above *)
    Definition wr := @cons elt. (* complying *)
    Definition rd (l:t) :=
    match l with
      nil => (None,l)
    | cons e l' => (Some e, l')
    end.
    Definition push := wr.
    Definition pop := rd.
  End ListStack.

If you want to avoid polluting Stack with rd and wr you have no choice but to define Stack independently from Collection (except a possible common sub-interface, but here you don't have one). Rule of thumb: use Include Foo only if you want to include the whole Foo. Otherwise split Foo into WantedFoo and NotWantedFoo and include only the former.

Below an adaptation of your code although I am still not sure why you want TypElt instead of only Elt.

Module Type TypElt.
  Parameter t elt : Type.
End TypElt.

Module Type Collection (Import T: TypElt).

  Parameter rd : t -> (option elt * t).
  Parameter wr : elt -> t -> t.

End Collection.


Module Type Elt .
  Parameter elt : Type.
End Elt.

Module Type Stack (E: Elt).

  Definition elt := E.elt.
  Parameter t: Type.

  (* Module Col := Collection E. *)

  Parameter pop : t -> (option elt * t).
  Parameter push : elt -> t -> t.

End Stack.

Module ListStack (E: Elt) <: Stack E.
  
  Definition elt := E.elt.
  Definition t := list elt.
  
  Definition push := @cons elt.
  Definition pop (l:t) :=
    match l with
      nil => (None,l)
    | cons e l' => (Some e, l')
    end.
End ListStack.

Module Type TypEltList <: TypElt.
  Parameter elt : Type.
  Definition t := list elt.
End TypEltList.

(* Collection with list *)
Module ListCollec (E: TypEltList) <: Collection E.
  (* Include E. *)
  Import E.                     (* Include pointless here *)
  Definition t := list elt.
  Definition wr := @cons elt.
  Definition rd (l:E.t) :=
    match l with
      nil => (None,l)
    | cons e l' => (Some e, l')
    end.
End ListCollec.

(* Function from one to the other *)
Module MakeStack (E:TypElt) (Col: Collection E) <: Stack E.
  Definition elt := E.elt.
  Definition t := E.t.
  Definition pop := Col.rd.
  Definition push := Col.wr. 
  (* Parameter peek : t -> option elt. *)
End MakeStack.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.