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.
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