Programs for Free: Towards the Formalization of Implicit Resolution in Scala

Implicit resolution has been part of the Scala language for a while, but the formal system it constitutes and its properties have not been formalized. Oliveira et al. were the first to formalize a calculus of implicits λ⇒ based on the ideas of implicits in Scala. We propose a stronger calculus λS⇒ , extending their results and closing the gap with the maximum achievable expressiveness of resolution on top of System F. We believe that the strengthened results provide new insights into implicit resolution and are a big step towards a formalization that is entirely faithful to Scala. We give a partial algorithm for λS⇒ and use a proof-technique proposed by Abel & Altenkirch to establish its soundness and partial completeness independent of termination. To ensure that our results are correct and that it can be extended in the future, we made the language and proofs precise in the Agda dependently typed language.Electrical Engineering, Mathematics and Computer ScienceComputer ScienceProgramming Languages Grou