Modules for comodalities?

[mikeshulman]

I just had the thought that one of the aspects of modules that was annoying while using them for modalities --- namely, the fact that modules can't be parametrized over types, and all modules must be defined at toplevel --- might enable them to be used for something else that I haven't yet found a satisfactory way to formalize, namely comonadic modalities like the cohesive "flat".

To recap for those who may not be familiar with it, the problem with a naive formulation of these like

Axiom flat : Type -> Type

is that such an axiom can then be applied in any context. For instance, we could define

Definition oops (A : Type) (B : A -> Type) : A -> Type
  := fun a => flat (B a).

whereas this sort of thing is not (as far as we know) justified by the models we have in mind: flat is a coreflection on the category itself, but not "locally" on slice categories. In type-theoretic language, this means that we should only be allowed to apply flat to closed types.

However, what if instead of the above we wrote this:

Module Type TypeM.
  Parameter X : Type.
End TypeM.

Module Flat (XM : TypeM).
  Axiom flatX : Type.
End Flat.

Now if we want to apply flat to some specific closed type, like nat, we can say

Module natM <: TypeM.
  Definition X := nat.
End natM.

Module Flat_Nat := Flat natM.
Definition flat_nat := Flat_Nat.flatX.

But because modules can't be parametrized over types, defined in sections, etc., there is no obvious way to define a function like oops. If A and B are closed, we can try to say something like

Module Type AM.
  Parameter a : A.
End AM.

Module Flat_BM (aM : AM).
  Module BM <: TypeM.
    Definition X := B aM.a.
  End BM.

  Module FBM := Flat BM.

  Definition flat_B := FBM.flatX.
End Flat_BM.

but it seems that in order to actually get any instance of flat_B, one would have to have a closed element a:A in order to define a particular instantiation of AM to which one could apply the module functor Flat_BM, and in this case the type B a is closed and thus unproblematic to apply flat to.

So my question is, for people who know more about modules than I do, would this be justified? I expect it would be too much to ask for a categorical semantics of Coq modules, but at least is there some obvious trick or workaround I'm missing that would enable one to extract something like oops from the module Flat?

[JasonGross]

It is commonly believed that turning a parameterized module definition into a lambda abstration is impossible (though I know of no attempt at a formal proof), and my understanding of the universe algorithm is that such a transformation unsound, given how universes are implemented. (Of course, there could be a bug somewhere, given how complicated the implementation of modules and functors is.) I suspect Bob Harper might be the right person to ask; I seem to recall that he's a strong proponent of the ML module system (which Coq's is very closely modeled on), and so presumably knows a lot about it.

[JasonGross]

I've asked Bob if he has ideas/answers on Twitter.

[mikeshulman]

I'm curious: why twitter?

[JasonGross]

Because I don't have his handle on any other public forum, and was in the "ask publicly" mode since this discussion is public.

[mikeshulman]

Ok. (-: Let me know if you get an answer (I don't twitter).

BTW, does this mean that what you said here about the restriction of modules parameters to be module types being "only syntactic" is not really correct?

[JasonGross]

BTW, does this mean that what you said here about the restriction of modules parameters to be module types being "only syntactic" is not really correct?

There's a purely syntactic transformation that takes any pseudo-valid syntax

Module Foo (bar : T).

to the valid syntax

Module Type TM.
  Parameter T_carrier : T.
End TM.
Module Foo (bar : TM).

I'd call this a purely syntactic restriction. It's going, approximately, the other way, that I think is impossible (from a parameterized module to a lambda or an unparameterized module), and which I understood this question to be about.

[mikeshulman]

Okay. I was thinking that if your pseudo-valid syntax were valid, then I would expect to also be able to apply Foo to elements of T, and that sort of thing can't be translated into valid syntax. But maybe your point is that this question is really about the restriction that all modules must be declared at top level (which would, I guess, also apply if the pseudo-valid syntax were valid), not about the restriction on parameters to be module types?

[JasonGross]

this question is really about the restriction that all modules must be declared at top level

Yes.

apply Foo to elements of T

Also fine (purely syntactic restriction), as long as you're only doing it at top level.

[mikeshulman]

Ok, thanks, I understand better now!

[mikeshulman]

Well, if Bob has something to add, that'd be great, but "everyone thinks it's probably impossible" is about the best answer I hoped for when I asked this question, and probably good enough for me to experiment with it.