> Hindley-Milner type systems to the rescue!
You're implying that all type-systems derived from HM have a form of bounded polymorphism. They're not, for example OCaml does not have type classes (you could probably encode a lot into objects, though).
You're implying that all type-systems derived from HM have a form of bounded polymorphism. They're not, for example OCaml does not have type classes (you could probably encode a lot into objects, though).
I believe they're experimental in Coq.
Yeup, some folks did show the functors + modules \equiv type classes in some sense, for system F or a variant thereof. Theres also an oleg approach too I think.