Gergely Buday (Jul 10 2025 at 12:13): Gergely Buday (Jul 10 2025 at 12:13):Haftmann and Wenzel writes this in their Constructive Type Classes in Isabelle paper:
Module systems (especially for theorem provers) provide a more general perspective on our work. Roughly speaking, the huge amount of existing approaches can be categorized as follows: (1) full / explicit module languages vs. (2) restricted / implicit structuring mechanisms. ML functors [16] and Coq modules [4, 5] represent the first kind, type classes in Haskell or Isabelle the second, more light-weight one.
What is a practical need for Coq modules' extended functionality that is not present in Isabelle's locales and type classes?
Christian Pardillo Laursen (Jul 10 2025 at 12:30):This answer might be helpful https://stackoverflow.com/questions/36927169/ml-modules-vs-haskell-type-classes
Christian Pardillo Laursen (Jul 10 2025 at 12:34):With Isabelle type classes, you're forced to pick one implementation of a typeclass per type, whereas with modules you can have several. You can circumvent this by using locales rather than typeclasses, though, but there may be other reasons why modules are more powerful.
Last updated: Jul 12 2025 at 12:41 UTC