Instance arguments

[brendanzab]

Once we get dependent records in #2 it would be nice to then be able to use them to implement typeclasses/modules. Instance arguments would give us the ability to automatically pass instances to functions. I think this might actually be easier to implement than implicit arguments (see #8).

Resources:

• Agda Docs: Instance Arguments
• On the Bright Side of Type Classes: Instance Arguments in Agda
• Modular Type Classes
• modular type classes SMLFamily/Successor-ML#18
• Modular Implicits

[brendanzab]

Interesting paper on open type classes: Improving Typeclass Relations by Being Open - this seems to solve one of my annoyances with type class hierarchies, namely how to evolve them over time. It would be interesting to see whether it would still work in a non-coherent world. 🤔

[brendanzab]

@theindigamer has posted this nice article describing some of the design space of implicit module systems: Principled ad-hoc polymorphism.

[brendanzab]

@buggymcbugfix also points to Named Instances - this seems to be a similar solution to the others posted here, but with a view towards retrofitting it onto Haskell.