In my project, I have the following structure and I am looking for the best way to encode it in Coq. Because Modules can only take Module Types as parameters and Module Types doesn’t allow to have defaults in them, I couldn’t find a easy way to structure it. High level overview of it is, I have list of stateful operations as a module type
Module Type Operation.
Parameter state : Type.
Parameter prog : Type -> Type.
Parameter exec: forall T, state -> prog T -> @Result state T -> Prop.
End Operation.
Then I define a module that takes an operation and adds a stateful computation monad to it. Because i can’t pass this as a parameter to another module, I made it an operation too. Ideally I would not to if possible.
Module Language (Op: Operation) <: Operation.
Import Op.
Definition state := Op.state.
Inductive prog : Type -> Type :=
| Op : forall T, Op.prog T -> prog T
| Ret : forall T, T -> prog T
| Bind : forall T T', prog T -> (T -> prog T') -> prog T'.
Then I define a Hoare Logic module on this language
Module HoareLogic (Ops: Operation).
Module Lang := Language Ops.
Import Ops Lang.
Export Lang.
This is where things start to get messy. To be able to have generic theorems about Bind and Ret, I need to have a language. But I can only pass an operation to it so I create a new language from it inside and then export it. This is fine for the most parts but I have this generic horizontal composer that takes to languages and creates another language that is composition of two. Then I pass this new composite language to HL module which redundantly wraps it in another layer of stateful computation monad. I also have other modules that suppose to take languages (That can only take operations right now and creates a new language). So more I chain these modules, more redundant layers are being added and because there is no subtyping, each of this layers adds a new constructor to the beginning.
I know I can get around this by defining different notations that implicitly add those constructors but it is not a sustainable solution and I wanted to know if there is a better way to structure this.
Perhaps the problem can be solved by creating a Module Type LANGUAGE which refines the Operation type by additionally requiring three functions: Op, Ret, and Bind (plus whatever equations). Then Module Language (Op:Operation) <: LANGUAGE by defining those functions as the three constructors. Do your generic reasoning over modules of type LANGUAGE.
If the purpose is to have generic theorems on the structure, it is probably better to encode the structures as Record (*), as in:
Record Operation := {
state : Type;
prog : Type -> Type;
exec : forall T, state -> prog T -> @Result state T -> Prop
}.
Then, objects of type Operation are first-class citizens that you can quantify over.
Functors over modules are more relevant when you have a few instances of a same theory that you want to share, but not really to reason about structures, as far as I can tell.
(*) The keyword Structure can also be used, it is a synonym to Record.
But behavior of Bind and Ret should be predefined and Module Types doesn’t allow that. Therefore I can’t do generic reasoning over 'LANGUAGE with their default semantics.
Module Types can contain definitions, but those cannot be overridden. The suggestion by @herbelin is likely a good one.
This is confusing: you can apply functors to modules of the appropriate type, but if this is not an operation, what is it? What’s the interface it does satisfy?
Module Type A.
End A.
Module Type B (a: A).`
Definition foo := 0.
Inductive bar := Bar.
Ltac id := idtac.
Theorem t : True. exact I. Qed.
End B.
Module a <: A.
End a.
(* Works *)
Module b <: B a.
Definition foo := 0.
Inductive bar := Bar.
Theorem t : True. exact I. Qed.
End b.
(* Doesn't work *)
Module b' <: B a.
End b'.
System forces me to redefine those definitions exactly the same way if I wanted to create a module of that type. This defeats entire purpose of having a Module with predefined objects. It doesn’t properly eliminate code duplication.
I tried to write an “instantiator” that can take a module (a: A) and returns a module of type (B a) so that at least I can encapsulate the duplication into a single function but couldn’t do it. I guess I can do it if I change A to a record but when I have another module type that depends on B, then it becomes impossible again because I can’t turn B into a record.
First, the recommendation is still the one by @herbelin: use records. You are correct that you cannot turn modules into records — hence, that means you should probably use only records.
On “inheritance” using modules, it can be done, and it’s done in the stdlib for number types, but it’s subtle. Your Module b can Include the a module type — here, you could Include (b a). (or maybe Module M := (b a). Include M.), avoiding the duplication. One caveat is that such Module Type cannot also contain assumptions to fill in — those belong in a separate Module Type, otherwise you’ll get conflicts.
Can you give me an example of how can I turn Module Type B into a record? I don’t know how to have concrete definitions in records except writing an instantiator and only using it to create a record of that type.
Precisely; Operation becomes a record type, and most Module Types become record types, except their concrete definition move into concrete records or functions creating them, so B becomes a concrete record I guess; if you want more interfaces, you can create more record types; I’m not sure I see anything wrong with what you describe in your examples.