Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

A few propositions about the module system #58

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

A few propositions about the module system #58

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 78 additions & 0 deletions text/modules.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
- Title: Addressing a few limitations of the module system

- Author: Hugo Herbelin

----

# Summary

The module system of Coq has several roles:
- name space management and visibility (`Module`, `Import`, `Export`, qualified names)
- modular development of theories (modules parametric over module specifications, `:`, `<:`)
- building of large theories by combination (`with`, `<+`, `Include`)
- sealing of an implementation under an interface for the purpose of extraction towards the OCaml module system (`Module M:T:=S`)

Though inherited from the OCaml module system, it differs from the latter by the absence of syntactic differences between interfaces and implementations. In Coq, types are terms, interfaces can have arbitrary kinds of definitions, and implementations can have axioms.

This CEP tries to address a few limitations of the module system:
1. identifying modules canonically defined by their implementation and modules canonically defined by their interface
2. giving direct access to implementations sealed behind interfaces without going through extraction
3. integrating ideas inherited from OCaml's module system
4. providing more algebraic combinators to build theories

# Propositions

## Towards identifying modules canonically defined by their implementation and modules canonically defined by their interface

Despite the absence of syntactic differences between interfaces and implementations, Coq maintains a somehow artificial distinction between a (so-called) "declared" module, that is a module characterized by its interface and whose implementation is canonically defined to be the same as the interface, and a "defined" module, that is a module characterized by its implementation and whose interface is canonically defined to be the same as the implementation. Here are examples showing the limitation:
- In extraction:
```coq
Require Import Extraction.

Module M. Definition a:=0. End M.
Extraction M. (* ok *)

Module Type T. Definition a:=0. End T.
Declare Module N : T.
Fail Extraction N. (* currently unsupported *)
```
- In module definitions:
```coq
Module M. Axiom a:nat. End M.
Fail Module N := M with Definition a:=0. (* "with" not allowed for modules *)

Module Type T. Axiom a:nat. End T.
Fail Module N := T with Definition a:=0. (* T not a module *)

Declare Module N : T with Definition a:=0. (* ok *)
```
even though all three declarations basically build the same module.

Note: the syntactic limitation of the first case is addressed in [#11897](https://github.com/coq/coq/pull/11897).

In the implementation, these limitations come from the difference between `MExpr(params,expr,None)` (= a module with interface canonically identified with the implementation) and `MType(params,expr)` (= a module with implementation canonically identified with the interface). This difference goes to `module_body` by giving either the value `FullStruct` or the value `Abstract` to the field `mod_expr`.

Both issues would be solved by identifying the two constructions (i.e. rebinding `MType(params,expr)` to `MExpr(params,expr,None)`) and identifying `FullStruct` and `Abstract`.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@herbelin Are you proposing mixin modules, a bit like in Scala or MixML? I’ve often wanted them, and I’ve actually spent a couple of years studying the Scala case.

Here’s a small example:

Module Type Base.
  Axiom a : nat.
  Definition b := 1 + a.
End Base.

Module Derived1 <: Base.
  Definition a : nat := 0.
  Include Base.
  (* Include should _merge_ the axiom `a` with the `Definition `` as long as the definition is a subtype of the interface — if Coq satisfies the usual metatheory of subtyping, definitions using `a` should still typecheck and need not be rechecked, except for universe constraints since those are not modular. *)
End Derived1.

Module Derived2 <: Base.
  Include Base.
  Fail Definition a : nat := b. (* This creates a new kind of infinite loop, which must be forbidden. *)
  Definition a : nat := 0.
  (* Such things work in Scala but is harder, since we have to _replace_ a definition; rejecting this might be fine here, but not so well with FancyBase below. To make this work, we could replace [Include] by some other “inheritance” mechanism. *)
End Derived2.

Module FancyBase.
  Include Base.
  Axiom c : Fin b.
  Definition d := (c, c).
End FancyBase.

Module FancyDerived1 <: FancyBase.
  Definition a : nat := 0.
  Definition c : Fin 1 := Fin.FZ. (* We cannot write [Fin b], and we might be unable to write this definition at all. *)
  Include FancyBase.
End FancyDerived1.

Module FancyDerived2 <: Base.
  Include FancyBase.
  (* Now we can fill in the axioms *)
  Definition a : nat := 0.
  Definition c : Fin b := Fin.FZ.
End FancyDerived2. (* *)

This code can be translated to avoid mixing modules — Coq’s numerical hierarchy shows how. But the encoding is pretty annoying, since you can never mix axioms and definitions if the axioms are to be later instantiated.

I also realize that working out the details is not trivial; but I am not sure what you get if you stop short of mixin modules.


## Giving direct access to implementations sealed behind interfaces without going through extraction

In Coq, only the interface of a module is relevant for typing a development dependent on a module. In particular, sealing implementations behind interfaces definitely prevents being able to access the contents of an implementation. The latter is then be seen only by extraction which can export the implementation to a programming language, such as OCaml, Haskell, Scheme, etc.

But the implementation is still there!

The proposal is to provide a command `Magic Eval reduction in term` which evaluates `term` by referring to the implementation of the modules mentioned in `term` rather than to their interface. For instance, in:
```coq
Module Type T. Axiom f:nat->nat. End T.
Module N:T. Definition f:=Nat.pred. End N.
```
calling `Magic Eval compute in N.f 1.` would produce `0`.

## Ideas inherited from OCaml's module system

OCaml has two module system features which Coq does not have:
- Private inductive types
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Don't we have private inductive types in coq?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but it does not mean the same and it's not a kernel feature (read: it's a broken hack).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ocaml private is used to enforce guarantees about the values in the type.
In Coq this is can done by explicitly manipulating proofs about the values in the type, so there seems to be no need to for ocaml-style private.
Also I'm not sure how it would work, consider

Module Import SortedList.

Private(ocaml) Inductive t := Nil | Cons : nat -> t -> t.

Definition nil := Nil.
Definition cons x l := (* add x to l keeping it sorted *).
End SortedList.
Compute nil. (* Nil : t ??? *)

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suppose opaque types would have abstract values, as in OCaml: <abstract> : t.

- Axiomatic variant of `Module Type` providing a polymorphically-typed module system
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can this lead to a type-in-type inconsistency?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could this proposal be clarified? Is this Declare Module Type Foo. where Foo is then an abstract signature?


## Providing more algebraic combinators to build theories
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Have you got any more combinators in mind?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not really. I was mostly thinking at the oppportunity to integrate Include and the quite powerful <+ in the kernel.


A force of the module system is to build new theories by combination, resulting in virtually very large theories. I wonder whether modules should not internally be kept as algebraically as possible. Functor application and updating with `with` are kept algebraically, but shouldn't `Include` and `<+` be kept also algebraically and their expansion into a pair of structures (i.e the pair of the expansion of the implementation and of the expansion of the interface) being done lazily.