CODEWITHSUNDEEP
coq
Mei Zhang
Mei Zhang

Reputation: 1714

define a "dependently typed" module functor

How can I make a dependently typed functor (for lack of a better term) ? I want to do something like the following:

Module Type Element.
  ...
End Element.

Module Wrapper (E : Element).
  ...
End Wrapper.

Module DepentlyTypedFunctor (E : Element) (W : Wrapper E).
  ...
End DepentlyTypedFunctor.

The last definition doesn't work, and I guess I'm looking for the correct syntax, if possible at all. My motivation for this kind of definition is to define theorems inside DependentlyTypedFunctor that work for all Wrappers that contain any instance of Element, similar to how one could define a theorem for vectors, forall (E : Element) (W : Wrapper E), some_proposition E W.

Upvotes: 1

Views: 63

Answers (1)

Tej Chajed
Tej Chajed

Reputation: 3948

I think you just meant to make Wrapper a Module Type. If it's not a module type, there's only one such module and you can just write DependentlyTypedFunctor over E. This might not be sufficient if you have opaque implementations of Element, though, in which case different instantiations of Wrapper might not be equal to each other.

If this is a problem, you might just want to use records instead of modules.

Upvotes: 3

Related Questions