Stream: Coq users

Topic: indexed modules


view this post on Zulip Quinn (Nov 10 2022 at 19:27):

Is there a literature on something like

Module F (X : Type).
   ...
End F.
Module Fb := F bool.
Module Fn := F nat.

?

Using full "functors" (Module Type) is clunkier than needed for a lot of usecases. I know I can express a lot with Section but I'm really curious about this.

view this post on Zulip Paolo Giarrusso (Nov 10 2022 at 20:14):

Sections + typeclasses are often a convenient encoding. Otherwise, Agda shows an implementation of this pattern. You could probably implement this as syntactic sugar over Coq modules but there might be some details that need care (I suspect you'd want a module type with a Parameter Inline to make the encoding accurate)


Last updated: Jan 27 2023 at 00:03 UTC