A projectional editor for implicit arguments
Many languages have different forms of implicit arguments: types in languages with Hindley-Milner type inference, type classes in Haskell, implicit and instance arguments in Agda, … Instead of inferring and re-inferring implicit arguments, we could make them part of the source language but have editor support for inserting them automatically and hiding them from the user. This would allow an easy way to display the implicit arguments with a toggle, and to set them to an explicit value if the inference fails or infers an undesired value.
Contacts for the project
- Jesper Cockx (TU Delft)
Supervisor(s): Jesper Cockx
Posted: October 25, 2022