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.

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

Coq-like modules #522

Closed
fpvandoorn opened this issue Mar 31, 2015 · 4 comments

Comments

@fpvandoorn
Copy link
Contributor

commented Mar 31, 2015

@mikeshulman would like to have something similar to modules in Coq, or at least a way to do the following two things:

  • Have universe polymorphic assumptions. You might want to define something, which depends on a universe polymorphic argument, but without your definition being universe polymorphic in that variable. For example, in the Coq-HoTT library they define reflective subuniverses using modules (and give more explanation about modules in Coq and why you want to use them in this case)
  • Do empty-context tricks. I did not understand exactly how these work, but the idea is that you have some construction with rules which only work in the empty context. So you can model them as modules, but not as definitions. But maybe Mike can elaborate more on this.
@mikeshulman

This comment has been minimized.

Copy link

commented Apr 1, 2015

The idea is that semantically, there is some operation on types called e.g. flat which only applies to objects of the category and not to objects of any slice of the category. Thus, it can't be represented internally by a function Type -> Type, and similarly not by any usual sort of type constructor, since those can be applied in any context. However, since a module can only be defined at top-level, if we wrap a type in a module like so:

Module Type TypeM.
  Parameter m : Type2.
End TypeM.

then any actual instantiation of TypeM must be a type in the empty context. Thus, if we hypothesize an operation on modules like

Module Type FlatM (XM : TypeM) : TypeM.
Declare Module flat : FlatM

then we can only apply flat to types in the empty context. You can see how this works in practice at https://github.com/mikeshulman/HoTT/blob/comodalities/theories/Cohesion/Comodality.v.

Dan Licata has convinced me that a better way to do this is to have a type theory with two contexts, one for "flat types" and one for ordinary types, with the rule that flat can only be applied to types whose ordinary-context is empty. Apparently this is a common technique in modal type theory. So if there is a way to allow multiple kinds of context (cubical type theory also involves a separate context of "line variables") that would be awesome too.

By the way, the fact that modules can only be defined at top level is also essential for the consistency of the universe polymorphism. An operation that's defined at all universe levels is a "very large" gadget, not living in any universe itself, so hypothesizing such a thing is only possible "externally". Note that Agda's modules are different from Coq's --- in many ways, but one of them is that an Agda module-function can be parametrized by types and not just by modules, which breaks the TypeM trick.

@leodemoura leodemoura self-assigned this Apr 22, 2015
@maximedenes

This comment has been minimized.

Copy link

commented Jun 11, 2015

The introduction of modules has proved in retrospect to be a very invasive change to Coq's kernel, and many of us (Coq developers) think today that an elaboration to dependent records would have been enough for most usages. So you may want to think twice before polluting Lean's nice and small kernel.

The tricky aspects of Coq's modules (and functors) are the handling of name substitutions (when applying a functor) and subtyping. They tend to complexify other parts of the kernel that are apparently orthogonal.

Also, from a more theoretical standpoint, I am not aware of any detailed proof explaining why the addition of modules and functors (and the restrictions Mike mentions, that they can only be defined at toplevel) to the whole formalism of Coq (including inductive types, universe polymorphism and impredicativity) preserves consistency and normalization.

@leodemoura

This comment has been minimized.

Copy link
Member

commented Jun 11, 2015

Dear Maxime,

Thank you very much for the feedback. It is very useful.

Best,
Leo

@leodemoura

This comment has been minimized.

Copy link
Member

commented Jun 13, 2015

@fpvandoorn I'm closing this issue based on Maxime's feedback.
Feel free to reopen it and/or suggest a different approach for doing what Mike wants.

@leodemoura leodemoura closed this Jun 13, 2015
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
4 participants
You can’t perform that action at this time.