Extended Report: The Implicit Calculus
Bruno C. d. S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee,, Kwangkeun Yi

TL;DR
This paper introduces the implicit calculus, a formal core language model that captures the key ideas of Scala implicits, supporting partial resolution and higher-order rules to advance generic programming mechanisms.
Contribution
It formalizes implicits in a minimal calculus, enabling better understanding and implementation of implicit instantiation in programming languages.
Findings
Supports partial resolution of rules
Allows higher-order rules in implicit resolution
Provides a formal foundation for implicits in language design
Abstract
Generic programming (GP) is an increasingly important trend in programming languages. Well-known GP mechanisms, such as type classes and the C++0x concepts proposal, usually combine two features: 1) a special type of interfaces; and 2) implicit instantiation of implementations of those interfaces. Scala implicits are a GP language mechanism, inspired by type classes, that break with the tradition of coupling implicit instantiation with a special type of interface. Instead, implicits provide only implicit instantiation, which is generalized to work for any types. This turns out to be quite powerful and useful to address many limitations that show up in other GP mechanisms. This paper synthesizes the key ideas of implicits formally in a minimal and general core calculus called the implicit calculus, and it shows how to build source languages supporting implicit instantiation on top of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · semigroups and automata theory
