AThe Implicit Calculus: A New Foundation for Generic Programming
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong
TOM SCHRIJVERS, Ghent University
WONTAE CHOI, Seoul National University
WONCHAN LEE, Seoul National University
KWANGKEUN YI, Seoul National University
PHILIP WADLER, University of Edinburgh

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 traditionof coupling implicit instantiation with a special type of interface. Instead, implicits provide only implicit
instantiation, which is generalized to work for any types. Scala implicits turn out to be quite powerful anduseful 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 topof it. A novelty of the calculus is its support for partial resolution and higher-order rules (a feature that has
been proposed before, but was never formalized or implemented). Ultimately, the implicit calculus provides
a formal model of implicits, which can be used by language designers to study and inform implementationsof similar mechanisms in their own languages.
Categories and Subject Descriptors: D.3.2 [Programming Languages]: Language Classifications—Functional Languages, Object-Oriented Languages; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs
General Terms: Languages
Additional Key Words and Phrases: Implicit parameters, type classes, C++ concepts, generic programming,
Haskell, Scala
ACM Reference Format:
Oliveira, B. C. d. S., Schrijvers, T., Choi, W., Lee, W., Yi, K., Wadler, P. 201?. The implicit calculus: a new
foundation for generic programming. ACM Trans. Program. Lang. Syst. V, N, Article A (January YYYY), 42
pages.
DOI = 10.1145/0000000.0000000 http://doi.acm.org/10.1145/0000000.0000000

1. INTRODUCTION

Generic programming (GP) [Musser and Stepanov 1988] is a programming stylethat decouples algorithms from the concrete types on which they operate. Decoupling is achieved through parametrization. Typical forms of parametrization include
parametrization by type (for example: parametric polymorphism, generics or templates)or parametrization by algebraic structures (such as a monoid or a group).
Author’s addresses: B. C. d. S. Oliveira, Department of Computer Science, Hong Kong University; T. Schrijvers, Department of Applied Mathematics and Computer Science, Ghent University; W. Choi and W. Lee
and K. Yi, . . . , Seoul National University; P. Wadler, . . . , University of Edinburgh.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted
without fee provided that copies are not made or distributed for profit or commercial advantage and that
copies show this notice on the first page or initial screen of a display along with the full citation. Copyrights
for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, to redistribute to lists, or to use any componentof this work in other works requires prior specific permission and/or a fee. Permissions may be requested
from Publications Dept., ACM, Inc., 2 Penn Plaza, Suite 701, New York, NY 10121-0701 USA, fax +1 (212)869-0481, or permissions@acm.org.
c YYYY ACM 0164-0925/YYYY/01-ARTA $15.00°
DOI 10.1145/0000000.0000000 http://doi.acm.org/10.1145/0000000.0000000
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:2

B. Oliveira et al.

A central idea in generic programming is implicit instantiation of generic parameters. Implicit instantiation means that, when generic algorithms are called with concrete arguments, the generic arguments (concrete types, algebraic structures, or someother form of generic parameters) are automatically determined by the compiler. The
benefit is that generic algorithms become as easy to use as specialized algorithms. To
illustrate implicit instantiation and its benefits consider a polymorphic sorting function:sort : ∀α.(α → α → Bool ) → List α → List αwith 3 parameters: the type of the elements in the list (α); the comparison operator;
and the list to be sorted. Instantiating all 3 parameters explicitly at every use of sortwould be quite tedious. It is likely that, for a given type, the sorting function is calledwith the same, explicitly passed, comparison function over and over again. Moreover it
is easy to infer the type parameter α. GP simplifies such calls further by also inferring
the comparison operator.
isort : ∀α.(α → α → Bool ) ⇒ List α → List α
By using ⇒ instead of →, the function isort declares that the comparison function is
implicit (that is: automatically inferable). The function is used as in:implicit cmpInt : Int → Int → Bool in
implicit cmpChar : Char → Char → Bool in
implicit cmpPair : ∀α β.(α → α → Bool , β → β → Bool ) ⇒ (α, β) → (α, β) → Bool in(isort [2, 1, 3], isort [(’b’, 1), (’b’, 0), (’c’, 2)])The two calls of isort each take only one explicit argument: the list to be sorted. Boththe type of the elements and the comparison operator are implicitly instantiated. The
element type parameter is automatically inferred from the type of the input list. For
example in the first isort call the element type call is Int, whereas in the second callthe element type is (Char , Int). More interestingly, the implicit comparison operator is
automatically determined in a process called resolution. Resolution is a type-directed
process that uses a set of rules, the implicit (or rule) environment, to find a value thatmatches the type required by the function call.
The implicit construct extends the implicit environment with new rules. In otherwords, implicit is a scoping construct for rules similar to a conventional let-binding.
In this example we introduce three rules into the implicit environment. Each ruleadds a previously defined function (here cmpInt, cmpChar and cmpPair ) to the implicit
environment.
To infer an implicit comparison function for isort, the resolution mechanism uses
the rules in the implicit environment to construct a value of the right type. In the firstcall of isort the function cmpInt can be used directly because it matches the type ofthe comparison operation needed for that call. In the second call of isort a comparison
function of type (Char , Int) → (Char , Int) → Bool is needed, but no function matches
this type directly. However it is possible to combine the polymorphic function cmpPair
with cmpInt and cmpChar to create a function of the desired type. The ability to compose functions in a type-directed manner illustrates the real power of the resolution
mechanism: a finite set of rules can be used to automatically create specific instancesat an infinite number of types.
1.1. Existing Approaches to Generic Programming

The two main strongholds of GP are the C++ and the functional programming (FP)communities. Many of the pillars of GP are based on the ideas promoted by Musser
and Stepanov [1988]. These ideas were used in C++ libraries such as the Standard
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:3

Template Library [Musser and Saini 1995] and Boost [Boost 2010]. In the FP community, Haskell type classes [Wadler and Blott 1989] have proven to be well suited
to GP, although their original design did not have that purpose. As years passed the
FP community created its own forms of GP [Jansson and Jeuring 1996; Gibbons 2003;
Lämmel and Jones 2005].
Garcia et al.’s [2003] comparative study of programming language support for GP
was an important milestone for both communities. According to that study many languages provide some support for GP. However, Haskell did particularly well, largely
due to type classes. A direct consequence of that work was to bring the two main lines
of work on GP closer together and promote cross-pollination of ideas. Haskell adopted
associated types [Chakravarty et al. 2005b; Chakravarty et al. 2005a], which was the
only weak point found in the original comparison. For the C++ community, type classes
presented an inspiration for developing language support for concepts [Musser andStepanov 1988; Gregor et al. 2006; Siek and Lumsdaine 2005a].
Several researchers started working on various approaches to concepts (see Siek’s
work [Siek 2011] for a historical overview). Some researchers focused on integrating
concepts into C++ [Dos Reis and Stroustrup 2006; Gregor et al. 2006], while others
focused on developing new languages with GP in mind. The work on System F G [Siekand Lumsdaine 2005a; 2011] is an example of the latter approach: Building on theexperience from the C++ generic programming community and some of the ideas oftype classes, Siek and Lumsdaine developed a simple core calculus based on System F
which integrates concepts and improves on type classes in several respects. In particular, System F G supports scoping of rules (in the context of C++ rules correspond tomodels or concept maps).
During the same period Scala emerged as new contender in the area of generic programming. Much like Haskell, Scala was not originally developed with generic programming in mind. However Scala included an alternative to type classes: implicits.
Implicits were initially viewed as a poor man’s type classes [Odersky 2006]. Yet, ultimately, they proved to be quite flexible and in some ways superior to type classes.
In fact Scala turns out to have fine support for generic programming [Oliveira andGibbons 2010; Oliveira et al. 2010].
A distinguishing feature of Scala implicits, and a reason for their power, is that
resolution works for any type. This allows Scala to simply reuse standard OO interfaces/classes (which are regular types) to model concepts, and avoids introducing another type of interface in the language. In contrast, with type classes, or the various
concept proposals, resolution is tightly coupled with the type class or concept-like interfaces.
1.2. Limitations of Existing Mechanisms

Twenty years of programming experience have given the FP community insights about
the limitations of type classes. Some of these limitations were addressed by concept
proposals and others by implicits. We list these limitations next. As far as we know,
no existing language or language proposal overcomes all limitations, as our proposal
does.
Global scoping. In Haskell, rules (in the context of Haskell rules correspond to typeclass instances) are global and there can be only a single rule for any given type [Kahland Scheffczyk 2001; Camarão and Figueiredo 1999; Dijkstra and Swierstra 2005;
Dreyer et al. 2007] in the entire program. Locally scoped rules are not available.
Several researchers have already proposed to fix this issue: with named rules [Kahland Scheffczyk 2001] or locally scoped ones [Camarão and Figueiredo 1999; Dijkstra
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:4

B. Oliveira et al.

and Swierstra 2005; Dreyer et al. 2007]. However none of those proposals have been
adopted.
Both proposals for concepts and Scala implicits offer scoping of rules and as such do
not suffer from this limitation.
Second class interfaces. Haskell type classes are second-class constructs compared toregular types: in Haskell, it is not possible to abstract over a type class [Hughes 1999].
Yet, the need for first-class type classes is real in practice. For example, Lämmel and
Peyton Jones [2005] desire the following type class for their GP approach:class (Typeable α, cxt α) ⇒ Data cxt α where
gmapQ :: (∀β.Data cxt β ⇒ β → r ) → α → [r ]In this type class, the intention is that the ctx variable abstracts over a concrete typeclass. Unfortunately, Haskell does not support type class abstraction. Proposals forconcepts inherit this limitation from type classes. Concepts and type classes are usually interpreted as predicates on types rather than types, and cannot be abstracted
over as regular types. In contrast, because in Scala concepts are modelled with types,
it is possible to abstract over concepts. Oliveira and Gibbons [2010] show how to encode
this example in Scala.
No higher-order rules. Finally type classes do not support higher-order rules. As
noted by Hinze and Peyton Jones [2001], non-regular Haskell datatypes like:data Perfect f α = Nil | Cons α (Perfect f (f α))
require type class instances such as:
instance (∀β.Show β ⇒ Show (f β), Show α) ⇒Show (Perfect f α)
which Haskell does not support, as it restricts instances (or rules) to be first-order.
This rule is higher-order because it assumes another rule, ∀β.Show β ⇒ Show (f β),that contains an assumption itself. Also note that this assumed rule is polymorphic inβ.
Both concept proposals and Scala implicits inherit the limitation of first-order rules.
1.3. Contributions

This paper presents λ? , a minimal and general core calculus for implicits and it shows
how to build a source language supporting implicit instantiation on top of it. Perhaps
surprisingly the core calculus itself does not provide implicit instantiation: instantiation of generic arguments is explicit. Instead λ? provides two key mechanisms forgeneric programming: 1) a type-directed resolution mechanism and 2) scoping constructs for rules. Implicit instantiation is then built as a convenience mechanism on
top of λ? by combining type-directed resolution with conventional type-inference. We
illustrate support for implicits with a simple source language.
The calculus is inspired by Scala implicits and it synthesizes core ideas of that mechanism formally. In particular, like Scala implicits, a key idea is that resolution and implicit instantiation work for any type. This allows those mechanisms to be more widely
useful and applicable, since they can be used with other types in the language. The
calculus is also closely related to System F G , in that rules available in the implicit
environment are lexically scoped and scopes can be nested.
A novelty of our calculus is its support for partial resolution and higher-order rules.
Although Hinze and Peyton Jones [2001] have discussed higher-order rules informallyand several other researchers noted their usefulness [Trifonov 2003; Rodriguez et al.
2008; Oliveira and Gibbons 2010], no existing language or calculus provides support
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:5

for them. Higher-order rules are just the analogue of higher-order functions in theimplicits world. They arise naturally once we take the view that resolution should work
for any type. Partial resolution adds additional expressive power and it is especially
useful in the presence of higher-order rules.
From the GP perspective λ? offers a new foundation for generic programming. The
relation between the implicit calculus and Scala implicits is comparable to the relation
between System F G and various concept proposals; or to the relation between formal
calculi of type classes and Haskell type classes: The implicit calculus is a minimal andgeneral model of implicits useful for language designers wishing to study and inform
implementations of similar GP mechanisms in their own languages.
In summary, our contributions are as follows.
— Our implicit calculus λ? provides a minimal formal model for implicits, which can beused for the study of implicits and GP.
— Our resolution mechanism is more expressive than existing mechanisms in the literature. It works for any type, supports local scoping, first-class interfaces, higherorder rules, as well as partial resolution. The mechanism is based on unification andresembles logic programming.
— We provide a semantics in the form of a translation from λ? to System F. We prove ourtranslation to be type-preserving, ensuring soundness. The translation also serves as
an effective implementation technique.
— We present a small source language built on top of λ? via a type-directed encoding,
to demonstrate how λ? supports implicit instantiation and can be used to model concepts with higher-order rules.
— Finally, both λ? and the source language have been implemented and the source codefor their implementation is available at http://i.cs.hku.hk/~bruno/implicit.
Organization. Section 2 presents an informal overview of our calculus. Section 3 describes a polymorphic type system that statically excludes ill-behaved programs. Section 4 provides the elaboration semantics of our calculus into System F and correctness
results. Section 5 presents the source language and its encoding into λ? . Section 6 discusses comparisons and related work. Section 7 concludes.
This paper is a rewrite and expansion of the conference paper by Oliveira et al.
[2012]. It has one additional author (Wadler), whose main contribution was to suggest
a simplification to the formulation of λ? in Section 3. The previous work had separate
syntactic classes for types (τ ) and type rules (ρ), and a complex construct ∀ᾱ.ρ̄ ⇒ τ that
abstracts over many types and rules at once; this paper unifies types and rules into asingle syntactic class (ρ) and has separate constructs ∀α.ρ and ρ1 ⇒ ρ2 that abstractover a single type or rule at a time.
The new formulation of λ? also differs from the conference version in that resolution is generalized further and made more expressive. Section 3 presents a discussion
about the differences in terms of expressivity. Furthermore, (also in Section 3) we now
include a treatment of termination and present an algorithm for resolution. Neitherof these were discussed in the conference version. Finally, our formalization is moredetailed, having several additional lemmas proving properties of the calculus; and wehave significantly expanded our discussion of related work.
2. OVERVIEW OF THE IMPLICIT CALCULUS λ?

Our calculus λ? combines standard scoping mechanisms (abstractions and applications) and types à la System F, with a logic-programming-style query language. At theheart of the language is a threefold interpretation of types:
types ∼
= propositions ∼= rules
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:6

B. Oliveira et al.

Firstly, types have their traditional meaning of classifying terms. Secondly, via the
Curry-Howard isomorphism, types can also be interpreted as propositions – in the context of GP, the type proposition denotes the availability in the implicit environment of avalue of the corresponding type. Thirdly, a type is interpreted as a logic-programmingstyle rule, i.e., a Prolog rule or Horn clause [Kowalski 1974]. Resolution [Kowalski
et al. 1971] connects rules and propositions: it is the means to show (the evidence) thata proposition is entailed by a set of rules.
Next we present the key features of λ? and how these features are used for GP.
For readability purposes we sometimes omit redundant type annotations and slightly
simplify the syntax.
Fetching values by types. A central construct in λ? is a query. Queries allow values
to be fetched by type, not by name. For example, in the following function call
foo ?Intthe query ?Int looks up a value of type Int in the implicit environment, to serve as an
actual argument.
Constructing values with type-directed rules. λ? constructs values, using
programmer-defined, type-directed rules (similar to functions). A rule (or rule
abstraction) defines how to compute, from implicit arguments, a value of a particular
type. For example, here is a rule that given an implicit Int value, adds one to thatvalue:
λ? Int.?Int + 1
The rule abstraction syntax resembles a traditional λ expression. However, instead of
having a variable as argument, a rule abstraction (λ? ) has a type as argument. The
type argument denotes the availability of a value of that type (in this case Int) in theimplicit environment inside the body of the rule abstraction. Thus, queries over therule abstraction type argument inside the rule body will succeed.
The type of the rule above is:Int ⇒ Int
This type denotes that the rule has type Int provided the availability of a value of typeInt in the implicit environment. The implicit environment is extended through rule
application (analogous to extending the environment with function applications). Rule
application is expressed as, for example:(λ? Int.?Int + 1) with 1
With syntactic sugar similar to a let-expression, a rule abstraction-application combination is more compactly denoted as:
implicit 1 in (?Int + 1)
Both expressions return 2.
Rule Currying. Like traditional lambdas, rule abstractions can be curried. Here is arule that computes an Int ×Bool pair from implicit Int and Bool values:
λ? Int.λ? Bool .(?Int + 1, ¬ ?Bool )In the body of the second rule abstraction, two implicit values (of type Int and Bool
respectively) are available in the implicit environment. The type of this rule is :Int ⇒ Bool ⇒ Int ×Bool
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:7

Using two rule applications it is possible to provide the implicit values to the two rule
abstractions. For example:
implicit 1 in
implicit True in(?Int + 1, ¬ ?Bool )which returns (2, False).
Higher-order rules. λ? supports higher-order rules. For example, the ruleλ? Int.λ? (Int ⇒ Int ×Int).?(Int ×Int)
when applied, will compute an integer pair given an integer and a rule to compute an
integer pair from an integer. This rule is higher-order because another rule (of type
Int ⇒ Int ×Int) is used as an argument. The following expression returns (3, 4):
implicit 3 inimplicit (λ? Int.(?Int, ?Int + 1)) in?(Int ×Int)
Recursive resolution. Note that resolving the query ?(Int × Int) above involves applying multiple rules. The current environment does not contain the required integer
pair. It does however contain the integer 3 and a rule λ? Int ⇒ Int×Int.(?Int, ?Int + 1) tocompute a pair from an integer. Hence, the query is resolved with (3, 4), the result ofapplying the pair-producing rule to 3.
Polymorphic rules and queries. λ? allows polymorphic rules. For example, the ruleΛα.(λ? α.(?α, ?α))abstracts over a type using standard type abstraction and then uses a rule abstraction
to provide a value of type α in the implicit environment of the rule body. This rule has
type∀α.α ⇒ α×α
and can be instantiated to multiple rules of monomorphic types
Int ⇒ Int ×Int, Bool ⇒ Bool ×Bool , . . .
Multiple monomorphic queries can be resolved by the same rule. The following expression returns ((3, 3), (True, True)):
implicit 3 inimplicit True in
implicit (Λα.(λ? α.(?α, ?α))) in(?(Int ×Int), ?(Bool ×Bool ))Polymorphic rules can also be used to resolve polymorphic queries:
implicit (Λα.(λ? α.(?α, ?α))) in?(∀α.α ⇒ α×α)
Combining higher-order and polymorphic rules. The ruleλ? Int.λ? (∀α.α ⇒ α×α).(?((Int ×Int)×(Int ×Int)))
prescribes how to build a pair of integer pairs, inductively from an integer value, byconsecutively applying the rule of type∀α.α ⇒ α×α
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:8

B. Oliveira et al.

twice: first to an integer, and again to the result (an integer pair). For example, thefollowing expression returns ((3, 3), (3, 3)):
implicit 3 inimplicit (Λα.(λ? α.(?α, ?α))) in?((Int ×Int)×(Int ×Int))
Locally and lexically scoped rules. Rules can be nested and resolution respects thelexical scope of rules. Consider the following program:
implicit 1 in
implicit True in
implicit (λ? Bool . if ?Bool then 2 else 0) in?Int
The query ?Int is not resolved with the integer value 1. Instead the rule that returns
an integer from a boolean is applied to the boolean True, because that rule can provide
an integer value and it is nearer to the query. So, the program returns 2 and not 1.
Overlapping rules. Two rules overlap if their return types intersect, i.e., when they
can both be used to resolve the same query. Overlapping rules are allowed in λ?
through nested scoping. The nearest matching rule takes priority over other matching rules. For example consider the following program:
implicit (Λα.(λx .x )) in
implicit (λn.n + 1) in?(Int → Int) 1
In this case λn.n +1 (of type Int → Int) is the lexically nearest match in the implicit environment and evaluating this program results in 2. However, if we have the following
program instead:
implicit (λn.n + 1) in
implicit (Λα.(λx .x )) in?(Int → Int) 1
Then the lexically nearest match is Λα.(λx .x ) (of type ∀α.α → α) and evaluating thisprogram results in 1.
3. THE λ? CALCULUS

This section formalizes the syntax and type system of λ? . In Section 4 (building on topof this type system) we will present the formalization of the type-directed translation
to System F. However, to avoid duplication and facilitate readability, we present therules of the type system and type-directed translation together. We use grey boxes toindicate parts of the rules which belong to the type-directed translation. These greyedparts will be explained in Section 4 and can be ignored in the remainder of this section.
3.1. Syntax

This is the syntax of the calculus:Typesρ ::= α | ρ1 → ρ2 | ∀α.ρ | ρ1 ⇒ ρ2
Expressions e ::= x | λ(x : ρ).e | e1 e2 | Λα.e | e ρ |?ρ | λ? ρ.e | e1 with e2
Types ρ comprise four constructs: type variables α; function types ρ1 → ρ2 ; typeabstraction ∀α.ρ; and the novel rule type ρ1 ⇒ ρ2 . In a rule type ρ1 ⇒ ρ2 , type ρ1 iscalled the context and type ρ2 the head.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:9

Expressions e include three abstraction-eliminination pairs. The binder λ(x : ρ).e
abstracts expression e over values of type ρ, is eliminated by application e1 e2 andrefers to the bound value with variable x. The binder Λα.e abstracts expression e overtypes, is eliminated by type application e ρ and refers to the bound type with typevariable α (but α itself is not a valid expression). The binder λ? ρ.e abstracts expression
e over implicit values of type ρ, is eliminated by implicit application e1 with e2 andrefers to the implicitly bound value with implicit query ?ρ. Without loss of generality
we assume that all variables x and type variables α in binders are distinct. If not, they
can be easily renamed apart to be so.
Using rule abstractions and applications we can build the implicit sugar that wehave used in Sections 1 and 2.
def

implicit e : ρ in e1 = (λ? ρ.e1 ) with e
The notation λ? ρ. is a shortform for λ? ρ1 . . . . λ? ρn .. Correspondingly, the notation
with e is a shortform for with e1 . . . with en .
For brevity, we have kept λ? small. Examples may use additional syntax such as
built-in integers, integer operators and boolean literals and types.
3.2. Type System

Figure 1 presents the static type system of λ? . The type system is based on the typesystem of System F, and every System F term is typeable in our system.
Well-Formed Types. The judgement Γ ` ρ denotes the well-formedness of types withrespect to type environment Γ. A type environment Γ records the type variables α andthe variables x with associated type ρ in scope:
Type Environments Γ ::= ² | Γ, x : ρ | Γ, αTypes ρ are well-formed iff their free type variables occur in the type environment(WF-VarTy).
Well-Typed Expressions. The typing judgment Γ | ∆ ` e : ρ means that expression e
has type ρ under type environment Γ and implicit environment ∆. The implicit environment ∆ is defined as:
Implicit Environments ∆ ::= ² | ∆, ρ ; x
Most of the rules are entirely standard; only three deserve special attention. Firstly,
rule (Ty-IAbs) extends the implicit environment with the type of an implicit value. The
side condition ² `unamb ρ states that the type ρ1 must be unambiguous; we explain thisconcept in Section 3.4. Secondly, rule (Ty-IApp) eliminates an implicit abstraction by
supplying a value of the required type. Finally, rule (Ty-Query) resolves a particularunambiguous type ρ against the implicit environment. It is defined in terms of theauxiliary judgement ∆ `r ρ, which is explained next.
3.3. Resolution

The underlying principle of resolution in λ? originates from resolution in logic. Intuitively, ∆ `r ρ holds if ∆ entails ρ, where the types in ∆ and ρ are read as propositions.
Following the Curry-Howard correspondence, we read α as a propositional variable,∀α.ρ as universal quantification, and rule types ρ1 ⇒ ρ2 as implication. We do not givea special interpretation to the function type ρ1 → ρ2 , treating it as an uninterpreted
predicate. Unlike traditional Curry-Howard, we have two forms of arrow, functions
and rules, and the important twist on the traditional correspondence is that we choose
to treat rules as implications, leaving functions as uninterpreted predicates.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:10

B. Oliveira et al.

Γ`ρ(WF-VarTy)

α∈Γ
Γ`α

(WF-FunTy)Γ ` ρ1Γ ` ρ2Γ ` ρ1 → ρ2

(WF-AbsTy)

Γ, α ` ρΓ ` ∀α.ρ

(WF-RulTy)Γ ` ρ1Γ ` ρ2Γ ` ρ1 ⇒ ρ2Γ|∆`e:ρ;E(Ty-Var)(x : ρ) ∈ ΓΓ|∆`x:ρ;x(Ty-Abs)Γ ` ρ1
Γ; x : ρ1 | ∆ ` e : ρ2 ; E
Γ | ∆ ` λx : ρ1 .e : ρ1 → ρ2 ; λx : |ρ1 |.E(Ty-App)Γ | ∆ ` e1 : ρ1 → ρ2 ; E1
Γ | ∆ ` e2 : ρ1 ; E2
Γ | ∆ ` e1 e2 : ρ2 ; E1 E2(Ty-TAbs)α 6∈ ∆
Γ, α | ∆ ` e : ρ ; E1
Γ | ∆ ` Λα.e : ∀α.ρ ; Λα.E1
Γ ` ρ1
Γ | ∆ ` e : ∀α.ρ2 ; E
Γ | ∆ ` e ρ1 : ρ2 [ρ1 /α] ; E |ρ1 |(Ty-TApp)Γ ` ρ1(Ty-IAbs)² `unamb ρ1

Γ | ∆, ρ1; x ` e : ρ2 ; E x freshΓ | ∆ ` λ? ρ1 .e : ρ1 ⇒ ρ2 ; λx : |ρ1 |.E
Γ | ∆ ` e1 : ρ2 ⇒ ρ1 ; E1
Γ | ∆ ` e2 : ρ2 ; E2
Γ | ∆ ` e1 with e2 : ρ1 ; E1 E2(Ty-IApp)(Ty-Query)Γ`ρ² `unamb ρ∆ `r ρ ; E
Γ | ∆ `?ρ : ρ ; Eᾱ `unamb ρ(UA-TAbs)ᾱ, α `unamb ρᾱ `unamb ∀α.ρ(UA-IAbs)(UA-Simp)² `unamb ρ1ᾱ `unamb ρ2ᾱ `unamb ρ1 ⇒ ρ2ᾱ ⊆ ftv (ρ)ᾱ `unamb ρ

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

Fig. 1. Type System and Type-directed Translation to System F

The Implicit Calculus: A New Foundation for Generic Programming

A:11∆ `r ρ ; E(R-TAbs)

α 6∈ ∆∆ `r ρ ; E∆ `r ∀α.ρ ; Λα.E

(R-IVar)ρ;x∈∆∆ `r ρ ; x(R-IApp)(R-IAbs)(R-TApp)∆ `r ∀α.ρ ; E∆ `r ρ[ρ0 /α] ; E |ρ0 |∆, ρ1 ; x `r ρ2 ; E

x fresh∆ `r ρ1 ⇒ ρ2 ; λx : |ρ1 |.E∆ `r ρ1 ⇒ ρ2 ; E2
∆ `r ρ1 ; E1
∆ `r ρ2 ; E2 E1

Fig. 2. Ambiguous Resolution

Figure 2 provides a first (ambiguous) definition of the resolution judgement ∆ `r ρthat corresponds to the intuition of logical implication checking. However, it suffersfrom two problems:(1) The definition is not syntax-directed; several of the inference rules have overlapping conclusions. Hence, a deterministic resolution algorithm is non-obvious.
(2) More importantly, the definition is ambiguous: a derivation can be shown by multiple different derivations. For instance, there are two different derivations for
Int, Bool , Bool ⇒ Int `r Int:
Bool ∈ (Int, Bool , Bool ⇒ Int)Int ∈ (Int, Bool , Bool ⇒ Int)
Int, Bool , Bool ⇒ Int `r Bool
Int, Bool , Bool ⇒ Int `r Int
Int, Bool , Bool ⇒ Int `r Int
While this may seem harmless at the type-level, at the value-level each derivation
corresponds with a (possibly) different value. Hence, ambiguous resolution renders
the meaning of a program ambiguous.
3.4. Deterministic Resolution

To help defining deterministic resolution, we provide a variant of the syntax of thecalculus:
Simple Types τ ::= α | ρ1 → ρ2
Context Types ρ ::= ∀α.ρ | ρ1 ⇒ ρ2 | τThis variant of the syntax splits types into simple types and context types. Simple
types τ comprise two type constructs (type variables α and function types ρ1 → ρ2 ).
Context types ρ comprise the types which participate in the (recursive) resolution ofrules. The type abstraction ∀α.ρ as well as the novel rule types ρ1 ⇒ ρ2 are the main
constructs, while other (simple) types act as base cases in the resolution process. Expressions remain unchanged.
To solve the two problems Figure 3 shows a syntax-directed and unambiguous variant of resolution. The main judgement ∆ `r ρ is defined by mutual recursion with theauxiliary judgement ∆; ρ `↓ τ . The former judgement handles proper context types ρ inthe obvious way and delegates to the latter judgement for simple types τ . Note that thestratification of types into context and simple types makes all rules syntax-directed.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:12

B. Oliveira et al.

∆ `r ρ ; E(R-IAbs)∆, ρ1 ; x `r ρ2 ; E

x fresh(R-TAbs)∆ `r ρ1 ⇒ ρ2 ; λx : |ρ1 |.E(R-Simp)α 6∈ ∆∆ `r ρ ; E∆ `r ∀α.ρ ; Λα.E∆hτ i = ρ ; x∆; ρ ; x `↓ τ ; E∆ `r τ ; E∆; ρ ; E1 `↓ τ ; E2
(I-IAbs)(I-Simp)∆ `r ρ1 ; E2∆; ρ2 ; E1 E2 `↓ τ ; E3∆; ρ1 ⇒ ρ2 ; E1 `↓ τ ; E3
(I-TAbs)∆; τ ; E `↓ τ ; E∆; ρ[ρ0 /α] ; E1 |ρ0 | `↓ τ ; E2∆; ∀α.ρ ; E1 `↓ τ ; E2∆hτ i = ρ ; x(L-Head)ρτ(∆, ρ ; x)hτ i = ρ ; x(L-Tail)

ρ1 
6 τ∆hτ i = ρ2 ; y(∆, ρ1 ; x)hτ i = ρ2 ; yρτ(M-Simp)τ τ

(M-TAbs)

ρ[ρ0 /α]  τ∀α.ρ  τ(M-IAbs)ρ0  τρ ⇒ ρ0  τ
00Fig. 3. Deterministic Resolution and Translation to System F

Rule types ρ1 ⇒ ρ2 are resolved by pushing ρ1 to the implicit environment and thenresolving ρ2 under that environment (R-TAbs). Type abstractions ∀α.ρ are resolved bypeeling off the universal quantifier and then resolving ρ against the implicit environment (R-IAbs). A simple type τ is resolved in terms of the first matching context type
ρ found in the implicit environment (R-Simp). The bias towards the first avoids ambiguity when there are multiple matching context type.
The partial function ∆hτ i returns the first matching context type found in the implicit environment. Whether a context type ρ matches a simple type τ is defined byρ  τ . In essence, a context type matches a simple type if the simple type is an instanceof its right-most head.
The judgement ∆; ρ `↓ τ is defined by three rules that mirror the three rules of thejudgement ρ  τ . These rules peal off from left to right the universal quantifiers andrule contexts until the target simple type is obtained:
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:13— Universal quantifiers are eliminated by means of appropriate instantiation(I-TAbs). Note that thanks to the well-formedness condition on types, the type instantiation is unambiguous.
— Contexts are eliminated by means of recursive resolution (I-IAbs).
Note that while the rules (I-TAbs) and (M-TAbs) do not explain how the substitution[ρ0 /α] should be obtained, there is in fact no ambiguity here. Indeed, there is at mostone substitution for which the judgement holds. Consider the case of matching ∀α.α →Int with the simple type Int → Int. Here the type ρ0 is determined to be Int by the needfor (α → Int)[ρ0 /α] to be equal to Int → Int.
However, for the context type ∀α.Int ambiguity arises. When we match the head of
this type Int with the simple type Int, the matching succeeds without actually determining how the type variable α should be instantiated. In fact, the matching succeeds
under any possible substitution of α. In this particular case the ambiguity is harmless,because it does not affect the semantics. Yet, it is not so harmless in other cases. Takefor instance the context type ∀α.(α → String) ⇒ (String → α) ⇒ (String → String).1
Again the choice of α is ambiguous when matching against the simple type String →String. Yet, now the choice is critical for two reasons. Firstly, if we guess the wrong instantiation ρ for α, then it may not be possible to recursively resolve (String → α)[α/ρ]or (α → String)[α/ρ], while with a lucky guess both can be resolved. Secondly, for different choices of ρ the types (String → α)[α/ρ] and (α → String)[α/ρ] can be resolved incompletely different ways.
In order to avoid any problems, we conservatively forbid all ambiguous context types
in the implicit environment with the ² `unamb ρ1 side-condition in rule (Ty-IAbs) of
Figure 1.2 The definition of ᾱ `unamb is also given in Figure 1. Rule (UA-TAbs) takes careof accumulating the bound type variables ᾱ before the head. Rule (UA-IAbs) skips overany contexts on the way to the head, but also recursively requires that these contexts
are unambiguous. When the head is reached, the central rule (UA-Simp) checks whether
all bound type variables ᾱ occur in that type.
Finally, the unambiguity condition is also imposed on the queried type ρ in rule
(Ty-Query) because this type too may extend the implicit environment in rule (R-IAbs).
3.5. Power of Resolution

The rules for deterministic resolution presented in this paper support all the examples
described in Section 2. They are strictly more powerful than the rules presented in theconference version of the paper [Oliveira et al. 2012]. In other words, strictly morequeries resolve with this article’s rules than with the rules of the previous paper. For
example, the query:
Char ⇒ Bool , Bool ⇒ Int `r Char ⇒ Int
does not resolve under the deterministic resolution rules of the conference paper. In
order to resolve such rule types, it is necessary to add the rule type’s context to theimplicit environment in the course of the resolution process:Char ⇒ Bool , Bool ⇒ Int, Char `r Int
1 This type encodes the well-known ambiguous Haskell type ∀α.(Show α, Read α) ⇒ String → String of theexpression read ◦ show .
2 An alternative design to avoid such ambiguity would instantiate unused type variables to a dummy type,
like GHC’s GHC.Prim.Any, which is only used for this purpose.

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:14

B. Oliveira et al.

but this was not supported by our previous set of rules. The new set of resolution
rules do support this by means of rule (RIAbs), and queries like the above can now be
resolved.
3.6. Algorithm

Figure 4 contains an algorithm that implements the non-algorithmic deterministic
resolution rules of Figure 3. It differs from the latter in two important ways: 1) it
computes rather than guesses type substitutions, and 2) it traverses a context type atmost once per matching.
The toplevel relation of the algorithm is ∆ `alg ρ; it implements the non-algorithmic∆ `r ρ relation. The relation is defined in a syntax-directed manner, with one rule foreach of the three possible forms of ρ. The first two of these three rules are essentially
identical to the corresponding two rules of `r .
The last rule, for the form τ , differs significantly in the algorithm. Essentially, it
captures the two relations ∆hτ i = ρ and ∆; ρ `↓ τ into the single ∆ `match1st τ ,→ ρ̄.
The two traversals of the intermediate rule type ρ are thereby replaced by a single
traversal. This avoids the need to compute the instantiation of the context type ρ twice.
The other major change is that recursive invocations of `r are no longer performed
where the recursive contexts ρ̄ are encountered in the auxiliary relation. Instead, theρ̄ involved are accumulated and returnd by `match1st , to be resolved afterwards. In asense, we change from a post-order to a pre-order traversal of the conceptual resolution
tree. This change in schedule is an outflow of the change from guessing to computing
context type instantiations, which is explained below.
The two rules for the ∆ `match1st τ ,→ ρ̄ are similar to those of ∆hτ i = ρ: they are set
up to commit to the first matching ρ in the environment ∆. They are defined in termsof the auxiliary relation ρ; ρ̄; ᾱ `match τ → ρ̄0 . The latter relation is the algorithmic
counterpart that combines ρ  τ and ∆; ρ `↓ τ . As already indicated, the part notincluded in this relation are the recursive invocations ∆ `r ρi (ρi ∈ ρ̄0 ). Instead ρ̄ is an
accumulating parameter for the ρi so they can be returned in ρ̄0 .
Essentially, the relation `match peals off the universal quantifiers and rule contexts
from the ruletype ρ until it hits the simple type τ 0 . The algorithm proceeds in thisway because it can compute (rather than guess) the necessary type instantiation for
the universal quantifiers by matching the context type’s head τ 0 against the target
simple type τ . This explains why type instantiation is postponed, and, since recursive
resolution depends on type instantiation, also why recursive resolution is postponedeven further.
Example 3.1. Consider for instance the matching of simple type Int → Int against
context type ∀α.α ⇒ (α → α). Just by looking at the outer quantifier ∀α we do notknow what α should be. Hence, we peal off the quantifier, postpone α’s instantiationand proceed with α ⇒ (α → α). At this point, we cannot recursively resolve the context
α because we have not determined α yet. Hence, we must postpone its resolution andproceed with α → α. Now we can determine the substitution θ = [α/Int] by performing a matching unification with the target simple type Int → Int. This substitution θ
enables the postponed recursive resolution of αθ = Int.
The above informal description is formalized as follows. There is one rule for each of
the three cases: pealing off a context, pealing off a universal quantifier and handlingthe simple type τ 0 :(1) As already said, the contexts are collected in the accumulating parameter ρ̄ and be
returned in ρ̄0
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:15(2) In the ∀α rule of `match we find the main difference between the algorithmic andthe non-algorithmic definitions. The non-algorithmic definition guesses an appropriate instantiation ρ0 for the type variable α, while the algorithmic definition computes this instantiation. This computation does not happen in the ∀α rule; that rule
only accumulates the type variables in the parameter ᾱ of the relation.
(3) The simple type rule checks whether the target type τ matches the simple type τ 0 .
Matching means that the rules checks whether there is a most general unifier θ0(see below) of τ and τ 0 whose domain consists only of the accumulated type variables ᾱ. The rule returns the accumulated contexts ρ̄, but is careful to apply theunifier θ to them in order to take the matching into account.
Matching Unification. Figure 5 lists the algorithm for computing the most generalmatching unifier. For θ = mgu ᾱ (ρ1 , ρ2 ) we have that ρ1 = ρ2 θ and dom(θ) ⊆ ᾱ. Moreover, θ subsumes any other matching unifier. The algorithm itself is fairly straightforward and needs little explanation. Only rule (UAbs) deserves two notes. Firstly, we
assume that α-renaming is used implicitly to use the same name β for both bound typevariables. Secondly, we have to be careful that β does not escape its scope through θ,which could happen when computing for example mgu α (∀β.β, ∀β.α).
3.7. Termination of Resolution

If we are not careful about which rules are added to the implicit environment, thenthe resolution process may not terminate. This section describes how to impose a setof modular syntactic restrictions that prevents non-termination.
As an example of non-termination consider
Char ⇒ Int, Int ⇒ Char `r Int
which loops, using alternatively the first and second rule in the implicit environment.
The source of this non-termination are the mutually recursive definitions of the `r and`↓ relations: a type is resolved in terms of a rule type whose head it matches, but thisrequires further resolution of the rule type’s body.
3.7.1. Termination Condition. The problem of non-termination has been widely studied
in the context of Haskell’s type classes, and a set of modular syntactic restrictions
has been imposed on type class instances to avoid non-termination [Sulzmann et al.
2007]. Adapting these restrictions to our setting, we obtain the termination judgement`term ρ defined in Figure 6.
This judgement recursively constrains rule types ρ1 ⇒ ρ2 to guarantee that therecursive resolution process is well-founded. In particular, it defines a size measurekρk for type terms ρ and makes sure that the size of the resolved head type decreases
steadily with each recursive resolution step.
One potential problem is that the size measure does not properly take into accountuniversally quantified type variables. It assigns them size 1 but ignores the fact thatthe size may increase dramatically when the type variable is instantiated with a large
type. The rule (TermRule) makes up for this problem by requiring a size decrease forall possible instantiations of free type variables. However, rather than to specify thisproperty non-constructively as∀ρ̄.k[ᾱ 7→ ρ̄]τ1 k < k[ᾱ 7→ ρ̄]τ2 k
it provides a more practical means to verify this condition by way of free variableoccurrences. The number of occurrences occ α (τ1 ) of free variable α in type τ1 shouldbe less than the number of occurrences occ α (τ2 ) in τ2 . It is easy to see that the nonconstructive property follows from this requirement.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:16

B. Oliveira et al.

∆ `alg ρ ; E(Alg-TAbs)

α 6∈ ∆ ∆ `alg ρ ; E∆ `alg ∀α.ρ ; Λα.E∆, ρ1 ; x `alg ρ2 ; E(Alg-IAbs)∆ `alg ρ1 ⇒ ρ2 ; λ(x : |ρ1 |).E

∆ `match1st τ ,→ ρ̄; ω̄; E(Alg-Simp)x fresh∆ `alg ρi ; Ei(∀ρi ∈ ρ̄)∆ `alg τ ; E[ω̄/Ē]∆ `match1st τ ,→ ρ̄; ω̄; E(M1-Head)ρ; ²; ²; ²; x `match τ ,→ ρ̄; ω̄ 0 ; E 0∆, ρ ; x `match1st τ ,→ ρ̄; ω̄ 0 ; E 0
ρ; ²; ²; ²; x 6`match τ ,→ ρ̄0; ω̄ 0 ; E 0(M1-Tail)∆ `match1st τ ,→ ρ̄; ω̄ 00 ; E 00∆, ρ ; x `match1st τ ,→ ρ̄; ω̄ 00 ; E 00

ρ; ρ̄; ᾱ; ω̄; E `match τ ,→ ρ̄0; ω̄ 0 ; E 0(MTC-TAbs)(MTC-IAbs)

ρ; ρ̄; ᾱ, α; ω̄; E α `match τ ,→ ρ̄0; ω̄ 0 ; E 0∀α.ρ; ρ̄; ᾱ; ω̄; E `match τ ,→ ρ̄0; ω̄ 0 ; E 0

ρ2 ; ρ̄, ρ1 ; ᾱ; ω̄, ω; E ω `match τ ,→ ρ̄0; ω̄ 0 ; E 0(MTC-Simp)0ω fresh0

ρ1 ⇒ ρ2 ; ρ̄; ᾱ; ω̄; E `match τ ,→ ρ̄ ; ω̄ ; E

0

θ = mguᾱ (τ, τ 0 )τ 0 ; ρ̄; ᾱ; ω̄; E `match τ ,→ ρ̄θ; ω̄; E|θ|Fig. 4. Resolution Algorithm

3.7.2. Integration in the Type System. There are various ways to integrate the termination condition in the type system. The most generic approach is to require that all
types satisfy the termination condition. This can be done by making the condition partof the well-formedness relation for types.
4. TYPE-DIRECTED TRANSLATION TO SYSTEM F

In this section we explain the dynamic semantics of λ? in terms of System F’s dynamic
semantics, by means of a type-directed translation. This translation turns implicit
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:17

θ = mgu ᾱ (ρ1 , ρ2 )(UInst)α ∈ ᾱ
[α/ρ] = mgu ᾱ (ρ, α)(UVar)∅ = mgu ᾱ (β, β)(UFun)

θ1 = mgu ᾱ (ρ1,1 , ρ2,1 )θ2 = mgu ᾱ (ρ1,2 , ρ2,2 θ1 )
θ2 · θ1 = mgu ᾱ (ρ1,1 → ρ1,2 , ρ2,1 → ρ2,2 )(URul)

θ1 = mgu ᾱ (ρ1,1 , ρ2,1 )θ2 = mgu ᾱ (ρ1,2 , ρ2,2 θ1 )
θ2 · θ1 = mgu ᾱ (ρ1,1 ⇒ ρ1,2 , ρ2,1 ⇒ ρ2,2 )(UAbs)

θ = mgu ᾱ (ρ1 , ρ2 )β 6∈ ftv (θ)θ = mgu ᾱ (∀β.ρ1 , ∀β.ρ2 )Fig. 5. Most General Matching Unifier`term ρ(TermSimp)(TermRule)`term τ(TermForall)`term ρ`term ∀α.ρ`term ρ1`term ρ2
ρ1  τ1ρ2  τ2kτ1 k < kτ2 k∀α ∈ ftv (ρ1 ) ∪ ftv (ρ2 ) : occ α (τ1 ) 6 occ α (τ2 )`term ρ1 ⇒ ρ2
occ α (Int) = 0½
1
occ α (β) =0(α = β)(α 6= β)occ α (ρ1 → ρ2 ) = occ α (ρ1 ) + occ α (ρ2 )occ α (ρ1 ⇒ ρ2 ) = occ α (ρ1 ) + occ α (ρ2 )occ α (∀β.ρ) = occ α (ρ)
kIntk = 1kαk = 1kρ1 → ρ2 k = 1 + kρ1 k + kρ2 k
kρ1 ⇒ ρ2 k = 1 + kρ1 k + kρ2 kk∀α.ρk = kρkFig. 6. Termination Condition

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:18

B. Oliveira et al.

contexts into explicit parameters and statically resolves all queries, much like Wadler
and Blott’s dictionary passing translation for type classes [Wadler and Blott 1989]. The
advantage of this approach is that we simultaneously provide a meaning to well-typed
λ? programs and an effective implementation that resolves all queries statically.
The translation follows the type system presented in Section 3. The additional machinery that is necessary (on top of the type system) corresponds to the grayed partsof Figures 1, 2 and 3.
4.1. Type-Directed Translation

Figure 1 presents the translation rules that convert λ? expressions into ones of System
F. The gray parts of the figure essentially extend the type system with the necessary
information for the translation.
The syntax of System F is as follows:Types
T ::= α | T → T | ∀α.T
Expressions E ::= x | λ(x : T ).E | E E | Λα.E | E T

With respect to the type system the type environments Γ remain the same. However, implicit environments ∆ need to be extended with evidence information for thetranslation, thus becoming translation environments:
Translation Environments ∆ ::= ² | ∆, ρ ; E

The main translation judgment, which adapts the typing judgment, isΓ|∆`e:ρ;EThis judgment states that the translation of λ? expression e with type ρ is System F
expression E, with respect to type environment Γ and translation environment ∆. The
translation environment ∆ relates each rule type in the earlier implicit environment
to a System F variable x; this variable serves as explicit value-level evidence for the
implicit rule. Lookup in the translation environment is defined similarly to lookup in
the implicit environment, except that the lookup now returns a pair of a rule type andan evidence variable.
The function | · | takes λ? types ρ to System F types T:|α| = α|ρ1 → ρ2 | = |ρ1 | → |ρ2 ||∀α.ρ| = ∀α.|ρ||ρ1 ⇒ ρ2 | = |ρ1 | → |ρ2 |Variables, lambda abstractions and applications are translated straightforwardly.
Perhaps the only noteworthy rule is (Ty-IAbs). This rule associates the type ρ1 withthe fresh variable x in the translation environment (∆). This creates the necessary
evidence that can be used by resolutions in the body of the rule abstraction to construct
System F terms of type |ρ1 |.
Resolution. The more interesting part of the translation happens when resolving
queries. Queries are translated by rule (Ty-Query) using the auxiliary resolution judgment `r :∆ `r ρ ; E
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:19

which is shown, in deterministic form, in Figure 3. The translation of resolution basically extends the type-checking process with simultaenously building System F evidence terms. The mechanism that builds evidence dualizes the process of peeling off
abstractions and universal quantifiers. The rule (R-IAbs) wraps a lambda binder witha fresh variable x around a System F expression E, which is generated from the resolution for the head of the rule (ρ2 ). The rule (R-TAbs) wraps a type lambda binder aroundthe System F expression resulting from the resolution of ρ. For simple types (R-Simp),
evidence E1 is retrieved from matching τ and then used in the resolution process ofthe simple type τ with rule `↓ :∆; ρ ; E1 `↓ τ ; E2
The rules (I-IAbs) and (I-TAbs) are the most interesting in the translation. In rule
(I-IAbs) we need evidence for ρ2 to build evidence for τ , but all we have is evidence E1
for ρ1 ⇒ ρ2 . However, we can construct evidence for ρ2 , by generating evidence E2 forρ1 and then simply applying E1 to E2 . Rule (I-TAbs) is similar: we need evidence for ρ,
but all we have is evidence E1 for ∀α.ρ. To create evidence for ρ we can substitute α bysome type ρ0 in ρ and generate a term which is the type application of E1 to |ρ0 |.
Finally, matching (∆hτ i) also needs to be extended with evidence generation, but
this extension is straightforward.
T HEOREM 4.1 (T YPE - PRESERVING TRANSLATION). Let e be a λ? expression, ρ be a
type and E be a System F expression. If ² | ² ` e : ρ ; E, then ² ` E : |ρ|.
P ROOF. (Sketch) We first prove3 the more general lemma “if Γ | ∆ ` e : ρ ; E,
then |Γ|, |∆| ` E : |ρ|” by induction on the derivation of translation. Then, the theorem
trivially follows.
An important lemma in the theorem’s proof is the type preservation of resolution.
L EMMA 4.2 (T YPE -P RESERVING R ESOLUTION). Let ∆ be an implicit environment,ρ be a type and E be a System F expression. If ∆ `r ρ ; E, then |∆| ` E : |ρ|.
Moreover, we can express two key properties of Figure 3’s definition of resolution interms of the generated evidence.
L EMMA 4.3 (D ETERMINACY). The generated evidence of resolution is uniquely determined.
∀∆, ρ, E1 , E2 :∆ `r ρ ; E1 ∧ ∆ `r ρ ; E2⇒

E1 = E2

L EMMA 4.4 (S OUNDNESS). Figure 3’s definition of resolution (here denoted `3r ) issound (but incomplete) with respect to Figure 2’s definition (here denoted `2r ).
∀∆, ρ, E :∆ `3r ρ ; E⇒∆ `2r ρ ; E

4.2. Evidence Generation in the Algorithm

The evidence generation in Figure 4 is largely similar to that in the deterministic
specification of resolution in Figure 3.
The main difference, and complication, is due to the fact that the evidence for typeinstantiation and recursive resolution is needed before these operations actually takeplace, as the algorithm has to postpone them. For this reason, the algorithm first produces placeholders that are later substituted for the actual evidence.
3 in the technical report

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:20

B. Oliveira et al.

The central relation is ρ; ρ̄; ᾱ; ω̄; E `match τ ,→ ρ̄0; ω̄ 0 ; E 0. It captures the matching
instantiation of context type ρ against simple type τ . The input evidence for ρ is E,
and the output evidence for the instantiation is E 0 . The accumulating parameters ᾱ
and ρ̄ denote that the instantiation of type variables ᾱ and the recursive resolution ofρ̄ have been postponed. We use the ᾱ themselves as convenient placeholders for the
instantiating types, and we use the synthetic ω̄ as placeholders for the evidence ofthe ρ̄. The rules (MTC-Abs) and (MTC-Abs) introduce these two kinds of placeholders in
the evidence. The former kind, ᾱ, are substituted in rule (MTC-Simp) where the actual
type instantiatons θ̄ are computed. The latter kind, ω̄, are substituted later in rule
(Alg-Simp) where the recursive resolutions take place.
Now we can state the correctness of the algorithm.
T HEOREM 4.5 (PARTIAL C ORRECTNESS). Let ∆ be an implicit environment, ρ bea type and E be a System F expression. Assume that ² `unamb ρ and also ∀ρi ∈ ∆ :² `unamb ρi . Then ∆ `r ρ ; E if and only if ∆ `alg ρ ; E, provided that the algorithm
terminates.
4.3. Dynamic Semantics

Finally, we define the dynamic semantics of λ? as the composition of the type-directedtranslation and System F’s dynamic semantics. Following Siek’s notation [Siek andLumsdaine 2005a], this dynamic semantics is:eval (e) = V

where ² | ² ` e : ρ ; E and E →∗ V

with →∗ the reflexive, transitive closure of System F’s standard single-step call-byvalue reduction relation (see [Pierce 2002, Chapter 23]).
Now we can state the conventional type safety theorem for λ? :T HEOREM 4.6 (T YPE S AFETY). If ² | ² ` e : ρ, then eval (e) = V for some System F
value V .
The proof follows trivially from Theorem 4.1.
5. SOURCE LANGUAGES AND IMPLICIT INSTANTIATION

Languages like Haskell and Scala provide a lot more programmer convenience thanλ? (which is a low level core language) because of higher-level GP constructs, interfaces and implicit instantiation. This section illustrates how to build a simple source
language on top of λ? to add the expected convenience. We should note that unlike
Haskell this language supports local and nested scoping, and unlike both Haskell and
Scala it supports higher-order rules. We present the type-directed translation from thesource to λ? .
5.1. Type-directed Translation to λ?

The full syntax of the source language is presented in Figure 8. Its use is illustrated in
the program of Figure 7, which comprises an encoding of Haskell’s equality type class
Eq. The example shows that the source language features a simple type of interface I T̄(basically records), which are used to encode simple forms of type classes. Note that
we follow Haskell’s conventions for records: field names u are unique and they aremodelled as regular functions taking a record as the first argument. So a field u with
type T in an interface declaration I ᾱ actually has type ∀ᾱ.² ⇒ I ᾱ → T . The language
also has other conventional programming constructs (such as let expressions, lambdas
and primitive types).
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:21

interface Eq α = {eq : α → α → Bool }let (≡) : ∀α. {Eq α} ⇒ α → α → Bool = eq ? inlet eqInt1 : Eq Int = Eq {eq = primEqInt } inlet eqInt2 : Eq Int = Eq {eq = λx y.isEven x ∧ isEven y } inlet eqBool : Eq Bool = Eq {eq = primEqBool } inlet eqPair : ∀α β. {Eq α, Eq β } ⇒ Eq (α, β) =Eq {eq = λx y.fst x ≡ fst y ∧ snd x ≡ snd y } inlet p1 : (Int, Bool ) = (4, True) in
let p2 : (Int, Bool ) = (8, True) in
implicit {eqInt1 , eqBool , eqPair } in(p1 ≡ p2 , implicit {eqInt2 } in p1 ≡ p2 )Fig. 7. Encoding the Equality Type ClassInterface Declarations
interface I ᾱ = u : T
Types
T ::= αType Variables| I T̄
Interface Type
| T →T
Function
σ ::= ∀α. σ ⇒ T Rule Type
Expressions
E ::= xLambda Variable| λx.E
Abstraction| E1 E2
Application| u
Let Variable| let u : σ = E1 in E2 Let| implicit u in E2
Implicit Scoping| ?
Implicit Lookup| Iu=EInterface Implementation
Fig. 8. Syntax of Source Language

Unlike the core language, we strongly differentiate between simple types T and typeschemes σ in order to facilitate type inference. The source language also distinguishes
simply typed variables x from let-bound variables u with polymorphic type σ.
Figure 9 presents the type-directed translation G ` E : T ; e of source language
expressions E of type T to core expressions e, with respect to type environment G.
The type environment collects both simple and polymorphic variable typings. The connection between source types T and σ on the one hand and core types τ and ρ on theother hand is captured in the auxiliary function J·K. We should also remark that while
the type system in Figure 9 (the non-grey parts) is sufficient to allow the type-directedtranslation, it is incomplete as it does not check whether queries can be resolved or not.
Performing such checks at the level of the source language is possible, but requires repeating some of the infrastructure in Figures 1 and 3. For simplicity reasons, and since
we are mainly interested in the type-directed translation, we have avoided that extra
machinery here. For the translation of records, we assume that λ? is extended likewisewith records. Like in λ? , we also assume the existence of primitive types like integers,
booleans and pairs for the sake of examples.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:22

B. Oliveira et al.

Type Environments G ::= ² | G, u : σ | G, x : T

G`E:T ;eG(x) = TG`x:T ;x

(Ty-Var)(Ty-Abs)

G, x : T1 ` E ; e
G ` λx.E : T1 → T2 ; λx : JT1 K.e
G ` E1 : T1 → T2 ; e1
G ` E2 : T1 ; e2
G ` E1 E2 : T2 ; e1 e2(Ty-App)

G(u) = ∀α. σ ⇒ T2
θ = [α 7→ T ] T1 = θT2
qi = ?Jθσi K (∀σi ∈ σ)

(TyLVar)G ` u : T1 ; u JT K with q
σ1 = ∀α.σ2 ⇒ T1
G ` E1 : T1 ; e1G, u : σ1 ` E2 : T2 ; e2

(TyLet)G ` let u : σ1 = E1 in E2 : T2 ; (λu : Jσ1 K.e2 ) (Λα. λ? σ2 .e1 )G`E:T ;eG(ui ) = σi (∀ui ∈ u)

(TyImp)G ` implicit u in E : T ; (λ? JσK.e) with u(TyIVar)G `? : T ; ?JT K((TyRec)∀i :G(ui ) = ∀ᾱ.² ⇒ I ᾱ → Ti
G ` Ei : θTi ; e θ = [ᾱ 7→ T̄ ]G ` I u = E : I T̄ ; I u = e

JαK = αJT1 → T2 K = JT1 K → JT2 K
JI T̄ K = I JT̄ K
J∀α.σ ⇒ T K = ∀JᾱK.JσK ⇒ JT K
Fig. 9. Type-directed Encoding of Source Language in λ?

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:23

let and let-bound variables. The rule (TyLet) in Figure 9 shows the type-directedtranslation for let expressions. This translation binds the variable u using a regular
lambda abstraction in an expression e2 , which is the result of the translation of the
body of the let construct (E2 ). This lambda abstraction is then applied to an expression
which has type ∀α.σ2 ⇒ T1 . When both α and σ2 are empty that expression is simply an
expression e1 , resulting from the translation of the expression E1 . Otherwise, for each
α in α and for each σ in σ2 , corresponding type and rule binders are created aroundthe expression e1 .
The source language provides convenience to the user by inferring type arguments
and implicit values automatically. This inference happens in rule (TyLVar), i.e., theuse of let-bound variables. That rule recovers the type scheme of variable u from theenvironment G. Then it instantiates the type scheme and fires the necessary queries
to resolve the context.
Queries. The source language also includes a query operator (?). Unlike λ? this query
operator does not explicitly state the type; that information is provided implicitly
through type inference. For example, instead of using p1 ≡ p2 in Figure 7, we could
have directly used the field eq as follows:
eq ? p1 p2
When used in this way, the query acts like a placeholder for a value. The type of theplaceholder value can be determined using type-inference. Once the type system knows
the type of the placeholder it automatically synthesizes a value of the of the right typefrom the implicit context.
The translation of source language queries, given by the rule (TyIVar), is trivial.
To simplify type-inference, the query is limited to types, and does not support partial
resolution.
Implicit scoping. The implicit construct is the core scoping construct of the source
language. It is first used in our example to make eqInt1 , eqBool and eqPair available forresolution at the expression(p1 ≡ p2 , implicit {eqInt2 } in p1 ≡ p2 )Within this expression there is a second occurrence of implicit, which introduces anoverlapping rule (eqInt2 ) that takes priority over eqInt1 for the subexpression p1 ≡ p2 .
The translation rule (TyImp) of implicit into λ? also exploits type-information to
avoid redundant type annotations. It is not necessary to annotate the let-bound variables used in the rule set u since that information is recovered from the environment G.
Higher-order rules and implicit instantiation for any type. The following example
illustrates higher-order rules and implicit instantiation working for any type in thesource language.
let show : ∀α. {α → String } ⇒ α → String = ? inlet showInt : Int → String = . . . inlet comma : ∀α. {α → String } ⇒ [α] → String = . . . inlet space : ∀α. {α → String } ⇒ [α] → String = . . . inlet o : {Int → String, {Int → String } ⇒ [Int ] → String }⇒ String = show [1, 2, 3] in
implicit showInt in(implicit comma in o, implicit space in o)
For brevity, we have omitted the implementations of showInt, comma and space;but showInt renders an Int as a String in the conventional way, while comma and
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:24

B. Oliveira et al.

space provide two ways for rendering lists. Evaluation of the expression yields("1,2,3", "1 2 3"). Thanks to the implicit rule parameters, the contexts of the twocalls to o control how the lists are rendered.
This example differs from that in Figure 7 in that instead of using a nominal interface type like Eq, it uses standard functions to model a simple concept for pretty
printing values. The use of functions as implicit values is similar to structural matching of concepts, since only the type of the function matters for resolution.
5.2. Extensions

The goal of our work is to present a minimal and general framework for implicits. As
such we have avoided making assumptions about extensions that would be useful forsome languages, but not others.
In this section we briefly discuss some extensions that would be useful in the context
of particular languages and the implications that they would have in our framework.
Full-blown Concepts. The most noticeable feature that was not discussed is a fullblown notion of concepts. One reason not to commit to a particular notion of concepts
is that there is no general agreement on what the right notion of concepts is. For example, following Haskell type classes, the C++0x concept proposal [Gregor et al. 2006]
is based on a nominal approach with explicit concept refinement, while Stroustrup
favors a structural approach with implicit concept refinement because that would be
more familiar to C++ programmers [Stroustrup 2009]. Moreover, various other proposals for GP mechanisms have their own notion of interface: Scala uses standard OO
hierarchies; Dreyer et al. use ML-modules [Dreyer et al. 2007]; and in dependently
typed systems (dependent) record types are used [Sozeau and Oury 2008; Devriese
and Piessens 2011].
An advantage of λ? is that no particular notion of interface is imposed on source
language designers. Instead, language designers are free to use the one they prefer. In
our source language, for simplicity, we opted to add a very simple (and limited) typeof interface. But existing language designs [Oliveira et al. 2010; Dreyer et al. 2007;
Sozeau and Oury 2008; Devriese and Piessens 2011] offer evidence that more sophisticated types of interfaces, including some form of refinement or associated types, canbe built on top of λ? .
Type Constructor Polymorphism and Higher-order Rules. Type constructor polymorphism is an advanced, but highly powerful GP feature available in Haskell and Scala,among others. It allows abstracting container types like List and Tree with a type variable f ; and applying the abstracted container type to different element types, e.g., f Int
and f Bool .
This type constructor polymorphism leads to a need for higher-order rules: rules forcontainers of elements that depend on rules for the elements. The instance for showing
values of type Perfect f α in Section 1, is a typical example of this need.
Extending λ? with type constructor polymorphism is not hard. Basically, we needto add a kind system and move from a System F -like language to a System Fω -likelanguage.
Subtyping. Languages like Scala or C++ have subtyping. Subtyping would requiresignificant adaptations to λ? . Essentially, instead of targetting System F, we would
have to target a version of System F with subtyping. In addition, the notion of matchingin the lookup function ∆hτ i would have to be adjusted. While subtyping is a usefulfeature, some language designs do not support it because it makes the system more
complex and interferes with type-inference.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:25

Type-inference. Languages without subtyping (like Haskell or ML) make it easier tosupport better type-inference. Since we do not use subtyping, it is possible to improve
support for type-inference in our source language. In particular, we currently require a
type annotation for let expressions, but it should be possible to make that annotation
optional, by building on existing work for the GHC Haskell compiler [Schrijvers et al.
2009; Vytiniotis et al. 2011].
6. RELATED WORKThis section discusses related work.
The goal of our work is to formalize a core language (λ? ) with the essential featuresof a type-directed implicit parameter passing mechanism equipped with recursive resolution. There have been several other proposals for core calculi which contain someform of implicit parameter passing and/or recursive resolution. However none of these
allows for both implicit parameter passing for any types of values and recursive resolution. Furthermore, although there have been some informal proposals for higher-orderrules, the implicit calculus is the first system providing a full formalization of thisfeature.
6.1. Type Classes

Several core calculi and refinements have been proposed in the context of type-classes.
As already discussed in detail in Section 1, there are a number of design choices that
(Haskell-style) type classes take that are different from the implicit calculus. Most
prominently, type classes make a strong differentiation between types and type classes,
and they use global scoping instead of local scoping for the rule environment. Thesedesign choices can be traced back to Wadler and Blott’s [1989] original paper on typeclasses. In that paper the authors argue that the inspiration for type classes camefrom Standard ML’s eqtype variables. Eqtype variables were used to provide overloaded
equality, by allowing type variables which range only over types that admit equality.
Wadler and Blott generalized that idea by allowing arbitrary predicates over types tobe defined as type classes. This lead to type classes being viewed as predicates overtypes rather than types, and languages with types classes making a syntactic distinction between type classes and types. Implementations of type classes (that is, typeclass instances) are implicitly passed, whereas regular values implementing types are
explicitly passed.
The reason for global scoping is also motivated by Wadler and Blott. They wanted toextend Hindley-Milner type-inference [Hindley 1969; Milner 1978; Damas and Milner
1982] and discovered that local instances resulted in the loss of principal types. In boththe implicit calculus and our source language there are sufficient type annotations thatthe problem does not arise. However, the problem would indeed arise in the source
language if there were no top-level type annotations for a program. For example, if we
could write:
implicit eqInt : Eq Int in
implicit eqChar : Eq Char ineq(assuming the existence of values eqInt and eqChar ) then, without further annotations, the meaning of this program would be ambiguous. In a language that strives
for Hindley-Milner type-inference and principal types, this kind of ambiguity would beviewed as a serious problem. However, there are many languages with type-class likemechanisms (including Scala, Coq, Agda and Isabelle) that have more modest goals interms of type-inference. In these languages there are usually enough type annotations
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:26

B. Oliveira et al.

that such ambiguity is avoided, and there is indeed added expressive power because
type annotations drive the resolution process.
There are three possible behaviors here, which can all be accounted for by our source
language given a suitable type annotation for the program:— With the type annotation Int → Int → Bool resolution picks the eqInt instance.
— With the type annotation Char → Char → Bool would pick eqChar instead.
— With the type annotation ∀a.Eq a ⇒ a → a → Bool , a third implicit rule of type Eq awould have to be available in the implicit environment and resolution would pickthat rule instead.
In other words, type annotations allow the user to control the resolution processaccording to the intended semantics.
There is a wide range of work that builds on the original type classes proposal [Wadler and Blott 1989]. Jones’s work on qualified types [Jones 1995] provides
a particularly elegant framework that captures type classes and other forms of predicates on types. Like type classes, qualified types too make a strong distinction between
types and predicates over types, and scoping is global. There have been some proposals for addressing the limitations that arise from global scoping [Kahl and Scheffczyk
2001; Dijkstra and Swierstra 2005]. However in those designs, type classes are still
second-class and resolution only works for type classes. The GHC Haskell compiler
supports overlapping instances [Jones et al. 1997], that live in the same global scope.
This allows some relief for the lack of local scoping. A lot of recent work on type classes
is focused on increasingly more powerful “type class” interfaces. Functional dependencies [Jones 2000], associated types [Chakravarty et al. 2005b; Chakravarty et al.
2005a] and type families [Schrijvers et al. 2008] are all examples of this trend. Thisline of work is orthogonal to our own.
Our calculus has a different approach to overlapping compared to instancechains [Morris and Jones 2010]. With instance chains the programmer imposes anorder on a set of overlapping type class instances. All instance chains for a type classhave global scope and are expected not to overlap. This makes the scope of overlapping
closed within a chain. In our calculus, we make our local scope closed, thus overlap
only happens within one nested scope. More recently, there has been a proposal for
closed type families with overlapping equations [Eisenberg et al. 2014]. This proposal
allows the declaration of a type family and a (closed) set of instances. After this declaration no more instances can be added. In contrast our notion of scoping is closed ata particular resolution point, but the scopes can still be extended in other resolution
points.
6.2. Local Scoping

Implicit parameters [Lewis et al. 2000] are a proposal for a name-based implicit parameter passing mechanism with local scoping. Lewis et al. formalized a small corelanguage with the mechanism and there is also a GHC Haskell implementation. Implicit parameters allow named arguments to be passed implicitly, and these arguments
can be of any type. Using implicit parameters4 we could for example, write the following program:data EqD a = EqD {eq 0 :: a → a → Bool }eq :: (?eqD :: EqD a) ⇒ a → a → Booleq = eq 0 (?eqD)
4 Here we use the implementation available in the GHC Haskell compiler. The reader should note that thesyntax used in GHC differs from the syntax used in the original paper [Lewis et al. 2000].

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

eqInt:: EqD Int
eqMaybe :: (?eqD :: EqD a) ⇒ EqD (Maybe a)p1 = let ?eqD = eqInt in eq 3 4

A:27-- Definition omitted-- Definition omitted

Here the intention is to model something similar to Haskell’s Eq type class or thecode in Figure 7. The definitions eqInt and eqMaybe play the role of the rules. The implicit parameters are named, so that later they can be resolved from a local scope thatbinds named arguments. This resolution process is illustrated in program p1 : the eqInt
dictionary is brought into the local scope (bound to the variable eqD) and used in theexpression eq 3 4. In this case, the use of implicit parameters does not look too different
from the implicit calculus. However, implicit parameters do not support recursive resolution, so for most use-cases of type-classes they require composing rules manually,
instead of relying on the recursive resolution mechanism to do this automatically. For
example, the program:
p2 = let ?eqD = (let ?eqD = (let ?eqD = eqInt in eqMaybe) in eqMaybe)in eq (Just (Just 3)) (Just (Just 4))
illustrates a situation where we would like to compare two expressions (Just (Just 3))and (Just (Just 4)). This can be done by using the rule eqMaybe twice and using therule eqInt once. While in the implicit calculus recursive resolution would automaticallycompose these rules, with implicit parameters the rules have to be manually composed.
System F G . System F G [Siek and Lumsdaine 2005b] also offers an implicit parameter passing mechanism with local scoping, which is used for concept-based generic
programming. Instead of a name-based approach, a type-directed approach is used for
passing implicit parameters. This is closer to the implicit calculus. Program p1 could
be modelled as follows in System F G :concept Eqhti {eq : fn (t, t) → Bool ;} inlet p1 = model Eqhinti {. . .} in eq [int ] 3 4
The concept declaration provides the interface for Eqhti concepts, whereas the model
declaration provides the corresponding implementation of the concept. A difference tothe implicit calculus is that declaring a model automatically adds that model to theimplicit environment. In program p1 we must both provide the model and add it to
the implicit environment in a single step. In the implicit calculus, these two aspects
are decoupled. A more important difference to the implicit calculus is that, like typeclasses, there is a strong differentiation between types and concepts in System F G :concepts cannot be used as types; and types cannot be used as concepts. As a consequence, models implementing concepts can only be passed as implicit parameters, andregular values can only be passed as explicit parameters.
In contrast to λ? , System F G has both a notion of concepts and implicit instantiationof concepts5 built-in. This has the advantage that language designers can just reusethat infrastructure, instead of having to implement it (as we did in Section 5). The
language G [Siek and Lumsdaine 2011] is based on System F G and it makes gooduse of these built-in mechanisms. However, System F G also imposes important design
5 Note that instantiation of type variables is still explicit.

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:28

B. Oliveira et al.

trait A {implicit def id [a ] : a ⇒ a = x ⇒ x
def ?[a ] (implicit x : a) = x}
object B extends A {implicit def succ : Int ⇒ Int = x ⇒ x + 1
val v1 = (?[Int ⇒ Int ]).apply (3)//evaluates to 4
val v2 = (?[Char ⇒ Char ]).apply (’a’)//evaluates to ’a’}
Fig. 10. Nested Scoping with Overlapping Rules in Scalachoices, such the use of a notion of concepts that is built-in to the calculus. In contrast
λ? offers a freedom of choice (see also the discussion in Section 5.2).
Finally System F G only formalizes a very simple type of resolution, which does notsupport recursive resolution. To create program p2 a model:
model EqhMaybe [Maybe [Int ]]i {. . .}that manually composes rules must first be created in System F G .
Modular type classes [Dreyer et al. 2007] are a language design that uses MLmodules to model type classes. The main novelty of this design is that, in addition
to explicit instantiation of modules, implicit instantiation is also supported. In thisdesign local scoping is allowed. However, unlike λ? (and also System F G and implicit
parameters) the local scopes cannot be nested. Furthermore, implicit instantiation islimited to modules (that is other regular values cannot be implicitly passed and automatically resolved).

6.3. Scala Implicits

The main inspiration for our work comes from Scala implicits [Oliveira et al. 2010;
Odersky 2010]. Like our work Scala implicits allow implicit parameters of any typesof values and recursive resolution is supported. Prior to our work, there was no small
core calculus or any other form of formalization for this style of implicit parameters.
The main objective of our work was the formalize the essence of the ideas behind Scala
implicits. What we promote on this work is that the key idea of implicits is a typedirected implicit parameter passing mechanism that works for all types of values andsupports local scoping with recursive resolution. However, we should note that our goal
is not to have a faithful formalization of Scala implicits, since many other orthogonal
aspects of the mechanism are tailored for the particularities of the Scala language.
Therefore there are noteworthy differences between λ? and Scala implicits. In contrast to λ? , Scala has subtyping. We do not think that subtyping is essential, and it
complicates the formalization: as discussed in Section 5.2 subtyping would requireconsiderable adaptations to our calculus. Therefore we have omitted subtyping here.
Although Scala also provides local and nested scoping, nested scoping can only happen through subclassing and the rules for resolution in the presence of overlapping
instances are quite ad-hoc. Figure 10 illustrates the idea of nested scoping in Scala.
Note that Scala implicits do not natively support the query expressions (?), but wecan easily encode this functionality. In Scala each trait/class declaration introduces ascope and trait/class extension allows extending that scope. Thus in trait A an implicit
rule for type ∀a.a → a is introduced. In object B the scope of A is extended and a new,
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:29

overlapping, rule (succ) of type Int → Int is added6 . Like the implicit calculus the later
rule takes priority when a query of type Int → Int is required. However, in Scala therules of scoping are more complicated than in the implicit calculus. If more than one
implicit value has the right type, there must be a single most specific one according toan ordering. Informally this ordering states that a rule A is more specific than a rule
B if the relative weight of A over B is greater than the relative weight of B over A. The
relative weight is a score between 0 and 2, where A gets a point over B for being as
specific as B, and another if it is defined in a class (or in its companion object) which isderived from the class that defines B, or whose companion object defines B. Roughly, amethod is as specific as a member that is applicable to the same arguments, a polymorphic method is compared to another member after stripping its type parameters, and a
non-method member is as specific as a method that takes arguments or type parameters. In other words Scala’s scoring system attempts to account for both nested scoping
through subclassing and the most specific type, whereas in the implicit calculus only
the lexical scope is considered. Finally, Scala has no (first-class) rule abstractions andconsequently no support for higher-order rules. Rather, implicit arguments can only be
used in definitions.
6.4. Type Classes, Theorem Proving and Dependent Types

A number of dependently typed languages also include several mechanisms inspired bytype classes. Although such mechanisms have been implemented and they are actively
used, there is little work on formalization.
Isabelle Type Classes. The first type-class mechanism in a theorem prover was in
Isabelle [Haftmann. and Wenzel 2006]. The mechanism was largely influenced by
Haskell type classes and shares many of the same design choices. The introductionof axiomatic type classes [Wenzel and Mnchen 2000] showed how theorem proving canbenefit from type classes to model not only the operations in type classes, but also thecorresponding algebraic laws.
Coq’s Canonical Structures And Type Classes. The Coq theorem prover has
two mechanisms that allow modelling type-class like structures: canonical structures [Gonthier et al. 2011] and type classes [Sozeau and Oury 2008]. The two mechanisms have quite a bit of overlap in terms of functionality. In both mechanisms theidea is to use dependent records to model type-class-like structures, and pass instancesof such records implicitly. Both mechanisms support recursive resolution to automatically build suitable records and they follow Haskell type classes model of global scoping. Furthermore, because Coq is dependently typed an additional feature of the two
mechanisms is that they can also model value classes [Gonthier et al. 2011] (that isclasses parametrized by values, rather than by types). This functionality is not available in the implicit calculus, due to the lack of dependent types. Another differenceis that recursive resolution is allowed to backtrack in canonical structures and typeclasses, whereas the implicit calculus forbids this. The reason for forbidding backtracking in the implicit calculus (and also Haskell type classes) is justified by the useof the mechanism for programming purposes, and the need for users to easily predict
which instances are used. In a theorem proving context, backtracking makes more
sense since, due to proof irrelevance, which instances get picked in a proof is not soimportant, as long as the proof is completed.
A key difference to our work is that both canonical structures and Coq’s type classes
focus on the implementation of a concrete mechanism, whereas we focus on the formal6 Note that introducing this rule directly in A would result in an ambiguity problem, since two overlapping

rules are not allowed within the same trait/class.

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:30

B. Oliveira et al.

ization of a general mechanism. Neither canonical structures nor Coq’s type classes
have been formally specified. It could be that a generalization of the implicit calculus
with dependent types (and allowing backtracking) would be able to provide a suitablespecification for these mechanisms. Generalizing the implicit calculus with Coq styledependent types poses considerable challenges, because computation can happen during type-checking.
Instance arguments [Devriese and Piessens 2011] are an Agda extension that isclosely related to implicits. Like the implicit calculus, instance arguments use a special
arrow for introducing implicit arguments. However, unlike most other mechanisms,
implicit rules are not declared explicitly. Instead rules are drawn directly from thetype-environment, and any previously defined declaration can be used as a rule. Furthermore resolution is limited in its expressive power, to avoid introducing a different
computational model in Agda. This design differs significantly from λ? , where resolution is very expressive and the scoping mechanisms allow explicit rule declarations.
6.5. Other Related Work

Resolution with Higher-order Rules. Resolution in λ? is significantly more expressive than in other systems. Notably resolution supports higher-order rule types andqueries, as well as queries for polymorphic types. A closely related design sketch isthat of higher-order predicates by Hinze and Peyton Jones [2001]; no other IP system
has adopted a similar extension.
As Hinze and Peyton Jones show, higher-order predicates are specially importantwhen dealing with types that involve type constructor polymorphism. In order to simplify presentation, our formalization of the implicit calculus does not include type constructor polymorphism.
Our work is the first to study the meta-theory of higher-order rules as part of alanguage. Hinze and Peyton Jones only list a system of inference rules, but do notstudy any of its properties.
Type Classes and Logic Programming. The connection between Haskell type classes
and Prolog is folklore. Neubauer et. al. [2002] also explore the connection with Functional Logic Programming and consider different evaluation strategies to deal withoverlapping rules. With Constraint Handling Rules, Stuckey and Sulzmann [2002] use
Constraint Logic Programming to implement type classes.
7. CONCLUSION

Our main contribution is the development of the implicit calculus λ? . This calculus
isolates and formalizes the key ideas of Scala implicits and provides a simple model
for language designers interested in developing similar mechanisms for their own languages. In addition, λ? supports higher-order rules and partial resolution, which add
considerable expressiveness to the calculus.
Implicits provide an interesting alternative to conventional GP mechanisms liketype classes or concepts. By decoupling resolution from a particular type of interfaces,
implicits make resolution more powerful and general. Furthermore, this decouplinghas other benefits too. For example, by modeling concept interfaces as conventional
types, those interfaces can be abstracted as any other types, avoiding the issue of second class interfaces that arise with type classes or concepts.
Ultimately, all the expressiveness offered by λ? offers a wide-range of possibilities
for new generic programming applications.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:31

APPENDIXELECTRONIC APPENDIX

The electronic appendix for this article can be accessed in the ACM Digital Library.
ACKNOWLEDGMENTS
We are grateful to Ben Delaware, Derek Dreyer, Jeremy Gibbons, Scott Kilpatrick, eta Ziliani, the membersof ROPAS and the anonymous reviewers for their comments and suggestions. This work was partially supported by Korea Ministry of Education, Science and Technology/Korea Science and Enginering Foundation’s
ERC grant R11-2008-007-01002-0, Brain Korea 21, Mid-career Research Program 2010-0022061, and by
Singapore Ministry of Education research grant MOE2010-T2-2-073.

REFERENCES
Boost 2010. The Boost C++ libraries. http://www.boost.org/.
C AMAR ÃO, C. AND F IGUEIREDO, L. 1999. Type inference for overloading without restrictions, declarations
or annotations. In FLOPS.
C HAKRAVARTY, M., K ELLER , G., AND J ONES, S. L. P. 2005a. Associated type synonyms. In ICFP.
C HAKRAVARTY, M., K ELLER , G., J ONES, S. L. P., AND M ARLOW, S. 2005b. Associated types with class. In
POPL.
D AMAS, L. AND M ILNER , R. 1982. Principal type-schemes for functional programs. In POPL. 207–212.
D EVRIESE , D. AND P IESSENS, F. 2011. On the bright side of type classes: Instance arguments in agda. In
ICFP.
D IJKSTRA , A. AND S WIERSTRA , S. D. 2005. Making implicit parameters explicit. Tech. rep., Utrecht University.
D OS R EIS, G. AND S TROUSTRUP, B. 2006. Specifying C++ concepts. In POPL ’06. 295–308.
D REYER , D., H ARPER , R., C HAKRAVARTY, M., AND K ELLER , G. 2007. Modular type classes. In POPL.
E ISENBERG, R. A., V YTINIOTIS, D., P EYTON J ONES , S., AND W EIRICH , S. 2014. Closed type families withoverlapping equations. In POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. San Diego, CA, USA.
G ARCIA , R., J ARVI , J., L UMSDAINE , A., S IEK , J., AND W ILLCOCK , J. 2003. A comparative study of language
support for generic programming. In OOPSLA.
G IBBONS, J. 2003. Patterns in datatype-generic programming. In The Fun of Programming, Cornerstones in
Computing. Palgrave.
G ONTHIER , G., Z ILIANI , B., N ANEVSKI , A., AND D REYER , D. 2011. How to make ad hoc proof automation less ad hoc. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional
Programming. ICFP ’11. 163–175.
G REGOR , D., J ÄRVI , J., S IEK , J. G., S TROUSTRUP, B., R EIS, G. D., AND L UMSDAINE , A. 2006. Concepts:
linguistic support for generic programming in c++. In OOPSLA.
H AFTMANN., F. AND W ENZEL , M. 2006. Constructive type classes in Isabelle. In TYPES.
H INDLEY, J. R. 1969. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146, 29–60.
H INZE , R. AND J ONES, S. L. P. 2001. Derivable type classes. Electronic Notes in Theoretical Computer
Science 41, 1, 5 – 35.
H UGHES, J. 1999. Restricted data types in Haskell. In Haskell.
J ANSSON, P. AND J EURING, J. 1996. Polytypic programming. In AFP. Springer-Verlag.
J ONES, M. P. 1995. Simplifying and improving qualified types. In FPCA.
J ONES, M. P. 2000. Type classes with functional dependencies. In ESOP.
J ONES, S. L. P., J ONES, M. P., AND M EIJER , E. 1997. Type classes: exploring the design space. In Haskell
Workshop.
K AHL , W. AND S CHEFFCZYK , J. 2001. Named instances for Haskell type classes. In Haskell Workshop.
K OWALSKI , R. 1974. Predicate logic as a programming language. In Proceedings of IFIP Congress.
K OWALSKI , R., D ONALD, AND K UEHNER. 1971. Linear resolution with selection function. Artificial Intelligence 2.
L ÄMMEL , R. AND J ONES, S. L. P. 2005. Scrap your boilerplate with class: extensible generic functions. In
ICFP.

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:32

B. Oliveira et al.

L EWIS, J., L AUNCHBURY, J., M EIJER , E., AND S HIELDS, M. 2000. Implicit parameters: dynamic scopingwith static types. In POPL.
M ILNER , R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 3, 348–375.
M ORRIS, J. G. AND J ONES, M. P. 2010. Instance chains: type class programming without overlapping instances. In ICFP.
M USSER , D. AND S TEPANOV, A. 1988. Generic programming. In Symbolic and algebraic computation: ISSAC 88. Springer, 13–25.
M USSER , D. R. AND S AINI , A. 1995. The STL Tutorial and Reference Guide: C++ Programming with theStandard Template Library. Addison Wesley Longman Publishing Co., Inc.
N EUBAUER , M., T HIEMANN, P., G ASBICHLER , M., AND S PERBER , M. 2002. Functional logic overloading.
In POPL.
O DERSKY, M. 2006. Poor man’s type classes. http://lamp.epfl.ch/~odersky/talks/wg2.8-boston06.pdf.
O DERSKY, M. 2010. The Scala language specification, version 2.8.
O LIVEIRA , B. C. D. S. AND G IBBONS, J. 2010. Scala for generic programmers. Journal of Functional Programming 20.
O LIVEIRA , B. C. D. S., M OORS, A., AND O DERSKY, M. 2010. Type classes as objects and implicits. In OOPSLA.
O LIVEIRA , B. C. D. S., S CHRIJVERS, T., C HOI , W., L EE , W., AND Y I , K. 2012. Extended report: The implicit
calculus. http://arxiv.org/abs/1203.4499.
P IERCE , B. C. 2002. Types and programming languages. MIT Press, Cambridge, MA, USA.
R ODRIGUEZ , A., J EURING, J., J ANSSON, P., G ERDES, A., K ISELYOV, O., AND O LIVEIRA , B. C. D. S. 2008.
Comparing libraries for generic programming in haskell. In Haskell.
S CHRIJVERS, T., J ONES, S. L. P., C HAKRAVARTY, M., AND S ULZMANN, M. 2008. Type checking with open
type functions. In ICFP.
S CHRIJVERS, T., J ONES, S. L. P., S ULZMANN, M., AND V YTINIOTIS, D. 2009. Complete and decidable type
inference for GADTs. In ICFP.
S IEK , J. 2011. The C++0x Concepts Effort. http://ecee.colorado.edu/~siek/concepts_effort.pdf.
S IEK , J. G. AND L UMSDAINE , A. 2005a. Essential language support for generic programming. In PLDI.
S IEK , J. G. AND L UMSDAINE , A. 2005b. Essential language support for generic programming. In PLDI.
S IEK , J. G. AND L UMSDAINE , A. 2011. A language for generic programming in the large. Science of Computer Programming 76(5).
S OZEAU, M. AND O URY, N. 2008. First-class type classes. In TPHOLs.
S TROUSTRUP, B. 2009. Simplifying the use of concepts. Tech. rep., Technical Report N2906, ISO/IEC JTC 1
SC22 WG21.
S TUCKEY, P. J. AND S ULZMANN, M. 2002. A theory of overloading. In ICFP.
S ULZMANN, M., D UCK , G., J ONES, S. L. P., AND S TUCKEY, P. J. 2007. Understanding functional dependencies via Constraint Handling Rules. Journal of Functional Programming 17.
T RIFONOV, V. 2003. Simulating quantified class constraints. In Haskell.
V YTINIOTIS, D., J ONES, S. L. P., S CHRIJVERS, T., AND S ULZMANN, M. 2011. O UTSIDE I N(x): Modular type
inference with local assumptions. Journal of Functional Programming 21, 4–5, 333–412.
WADLER , P. L. AND B LOTT, S. 1989. How to make ad-hoc polymorphism less ad hoc. In POPL.
W ENZEL , M. AND M NCHEN, T. 2000. Using axiomatic type classes in isabelle.

A. PROOFS

Throughout the proofs we refer to the type system rules of System F listed in Figure 11.

A.1. Type Preservation

Lemma A.1 states that the translation of expressions to System F preserves types. Its
proof relies on Lemma A.2, which states that the translation of resolution preserves
types.
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming(F-Var)(x : T ) ∈ ΓΓ`x:T(F-Abs)Γ, x : T1 ` E : T2
Γ ` λx : T1 .E : T1 → T2

(F-App)Γ ` E1 : T2 → T1
Γ ` E2 : T2
Γ ` E1 E2 : T1

(F-TApp)Γ ` E : ∀α.T2
Γ ` E T1 : T2 [T1 /α](F-TAbs)

Γ, α ` E : TΓ ` Λα.E : ∀α.T

A:33

Fig. 11. System F Type System

L EMMA A.1. IfΓ|∆ ` e : ρ ; E
then|Γ|, |∆| ` E : |ρ|P ROOF. By structural induction on the expression and corresponding inference rule.
(Ty-Var)Γ|∆ ` x : ρ ; x.

It follows from (Ty-Var) that
(x : ρ) ∈ Γ
Based on the definition of | · | it follows(x : |ρ|) ∈ |Γ|Thus we have by (F-Var) that|Γ|, |∆| ` x : |τ |(Ty-Abs)Γ|∆ ` λx : ρ1 .e : ρ1 → ρ2 ; λx : |ρ1 |.E.

It follows from (Ty-Abs) that
Γ; x : ρ1 |∆ ` e : ρ2 ; E
and by the indution hypothesis that|Γ|, x : |ρ1 |, |∆| ` E : |ρ2 |ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:34

B. Oliveira et al.

As all variables are renamed unique, it is easy to verify that this also holds:|Γ|, |∆|, x : |ρ1 | ` E : |ρ2 |Hence, by (F-Abs) we have|Γ|, |∆| ` λx : |ρ1 |.E : |ρ1 → ρ2 |(Ty-App)Γ|∆ ` e1 e2 : ρ1 ; E1 E2 .

By the induction hypothesis, we have:|Γ|, |∆| ` E1 : |ρ2 → ρ1 |and|Γ|, |∆| ` E2 : |ρ2 |Then it follows by (F-App) that|Γ|, |∆| ` E1 E2 : |ρ1 |(Ty-TAbs)Γ|∆ ` Λα.e : ∀α.ρ ; Λα.E.

Based on (Ty-TAbs) and the induction hypothesis, we have|Γ, α|, |∆|, ` E : |ρ|As α 6∈ ∆, it is easy to see that the above is equivalent to|Γ|, |∆|, α ` E : |ρ|Thus, based on (F-TAbs) we have|Γ|, |∆| ` Λα.E : ∀α.|ρ|or, using the definition of | · ||Γ|, |∆| ` Λα.E : |∀α.ρ|(Ty-TApp).

Γ|∆ ` e ρ1 : ρ2 [ρ1 /α] ; E |ρ1 |By (Ty-TApp) and the induction hypothesis, it follows that|Γ|, |∆| ` E : |∀α.ρ2 |From which we have by definition of | · ||Γ|, |∆| ` E : ∀∀α.|ρ2 |It follows from (F-TApp) that|Γ|, |∆| ` E |ρ1 | : |ρ2 |[|ρ1 |/α]which is easily seen to be equivalent to|Γ|, |∆| ` E |ρ1 | : |ρ2 [ρ1 /α]|
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming(Ty-IAbs)

A:35Γ|∆ ` λ? ρ1 .e : ρ1 ⇒ ρ2 ; λx : |ρ1 |.E.

Based on (Ty-IAbs) and the induction hypothesis, we have|Γ|, |∆, ρ1 ; x| ` E : |ρ2 |or, using the definition of | · ||Γ|, |∆|, x : |ρ1 | ` E : |ρ2 |Thus, based on (F-Abs) we have|Γ|, |∆| ` λx : |ρ1 |.E : |ρ1 | → |ρ2 |or, using the definition of | · ||Γ|, |∆| ` λx : |ρ1 |.E : |ρ1 ⇒ ρ2 |(Ty-IApp)Γ|∆ ` e1 with e2 : ρ1 ; E1 E2 .

From (Ty-IApp) and the induction hypothesis we have:|Γ|, |∆| ` E1 : |ρ2 ⇒ ρ1 |and|Γ|, |∆| ` E2 : |ρ2 |Hence, based on the definition of | · |, the first of these means|Γ|, |∆| ` E1 : |ρ2 | → |ρ1 |Hence, based on (F-App) we know
|Γ|, |∆| ` E1 E2 : |ρ1 |(Ty-Query)Γ|∆ `?ρ : ρ ; E.

From (Ty-Query) we have∆ `r ρ ; E
Based on Lemma A.2 we then know|∆| ` E : |ρ|Hence, because all variables are unique|Γ|, |∆| ` E : |ρ|L EMMA A.2. If∆ `r ρ ; E
then|∆| ` E : |ρ|ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:36

B. Oliveira et al.

P ROOF.
By induction on the derivation.
(R-TAbs)∆ `r ∀α.ρ ; Λα.E.

From rule (R-TAbs) and the induction hypothesis, we have|∆, α| ` E : |ρ|or alternatively, based on the definition of | · |,|∆|, α ` E : |ρ|Then, rule (F-TAbs) allows us to conclude|∆| ` Λα.E : ∀α.|ρ|or, again based on the definition of | · |,|∆| ` Λα.E : |∀α.ρ|(R-TApp).

00∆ `r ρ[ρ /α] ; E |ρ |From rule (R-TApp) and the induction hypothesis, we have|∆| ` E : |∀α.ρ|or alternatively, based on the definition of | · |,|∆| ` E : ∀α.|ρ|Then, rule (F-TApp) allows us to conclude|∆| ` E |ρ0 | : |ρ|[|ρ0 |/α]or, again based on the definition of | · |,|∆| ` E |ρ0 | : |ρ[ρ0 /α]|(R-IVar).

∆ `r ρ ; x

From rule (R-IVar) we have(ρ ; x) ∈ ∆Hence, based on the definition of | · |, we have
(x : |ρ|) ∈ |∆|Thus, using rule (F-Var), we can conclude|∆| ` x : |ρ|(R-IAbs).

∆ `r ρ1 ⇒ ρ2 ; λx : |ρ1 |.E

From rule (R-IAbs) and the induction hypothesis, we have|∆, ρ1 ; x| ` E : |ρ2 |or alternatively, based on the definition of | · |,|∆|, x : |ρ1 | ` E : |ρ2 |Then, rule (F-Abs) allows us to conclude|∆| ` λx : |ρ1 |.E : |ρ1 | → |ρ2 |ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:37

or, again based on the definition of | · |,|∆| ` λx : |ρ1 |.E : |ρ1 ⇒ ρ2 |(R-IApp).

∆ `r ρ2 ; E2 E1

From rule (R-IAbs) and the induction hypothesis, we have|∆| ` E1 : |ρ1 |and|∆| ` E2 : |ρ1 ⇒ ρ2 |or alternatively, based on the definition of | · |,|∆| ` E2 : |ρ1 | → |ρ2 |Then, rule (F-App) allows us to conclude|∆| ` E2 E1 : |ρ2 |A.2. Soundness of Deterministic Resolution

Lemma A.5 states that deterministic resolution is sound with respect to nondeterministic resolution. Its proof relies on Lemma A.3, which states that ∆hτ i returns
an element in the environment.
The proof of Lemma A.5 also proceeds by mutual induction with the proof of
Lemma A.4. The latter lemma states that the auxiliary `↓ relation is sound with respect to non-deterministic resolution.
L EMMA A.3. If∆hτ i = ρ ; xthen(ρ ; x) ∈ ∆The proof is trivial.
L EMMA A.4. If∆; ρ ; E1 `↓ τ ; E2and∆ `2r ρ ; E1then
∆ `2r τ ; E2
P ROOF. The proof proceeds by induction on the derivation of the `↓ assumption.
(I-Simp).
∆; τ ; E `↓ τ ; E
The conclusion follows trivially.
(I-IAbs).
∆; ρ1 ⇒ ρ2 ; E1 `↓ τ ; E3
From the (I-IAbs) rule and the next lemma, it follows that∆ `2r ρ1 ; E2
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:38

B. Oliveira et al.

Given the above, as well as the assumption ∆ `2r ρ1 ⇒ ρ2 ; E1 , it follows from rule
(R-IAbs) that∆ `2r ρ2 ; E1 E2
From the (I-IAbs) rule and the induction hypothesis, we then have∆ `2r τ ; E3
(I-TAbs).

∆; ∀α.ρ ; E1 `↓ τ ; E2

From the assumption ∆ `2r ∀α.ρ ; E1 and rule (R-TApp) it follows that∆ `2r ρ[ρ0 /α] ; E1 |ρ0 |From that, the (I-TAbs) rule and the induction hypothesis, we then have∆ `2r τ ; E2

L EMMA A.5. If∆ `3r ρ ; Ethen∆ `2r ρ ; E
P ROOF. The proof proceeds by induction on the derivation.
(R-IAbs)3 . ∆ `3r ρ1 ⇒ ρ2 ; λx : |ρ1 |.E
From rule (R-IAbs)3 and the induction hypothesis, we have∆, x : ρ1 `2r ρ2 ; E
Hence, from rule (R-IAbs)2 it follows that∆ `2r ρ1 ⇒ ρ2 ; λx : |ρ1 |.E(R-TAbs)3 . ∆ `3r ∀α.ρ ; Λα.E
From rule (R-TAbs)3 and the induction hypothesis, we have∆ `2r ρ ; E
Hence, from rule (R-TAbs)2 it follows that∆ `2r ∀α.ρ ; Λα.E
(R-Simp)3 .

∆ `3r τ ; E

From the (R-Simp) rule and the lemma, it follows that(ρ ; x) ∈ ∆or, following rule (R-IVar), that∆ `2r ρ ; x
From the (R-Simp) rule and the other lemma, we also have that∆ `2r ρ ; x⇒∆ `2r τ ; E

Combining both observations, yields the desired result∆ `2r τ ; E

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:39

A.3. Correctness of the Resolution Algorithm

Lemma A.8 states that the resolution algorithm `alg is sound with respect to the deterministic resolution specification `r .
Its proof relies on Lemma A.7, which states that the auxiliary relation `match1st
is sound, whose proof in turn relies on Lemma A.6 which states that the auxiliary
relation `match is sound.
The completeness proof proceeds in a similar fashion.
L EMMA A.6. If
ρ; ρ̄; ᾱ; ω̄; E `match τ ,→ ρ̄0 ; ω̄ 0 ; E 0then there exist ρ̄00 withρ̄θ ⊆ ρ̄0where θ = [ρ¯00 /ᾱ],andω̄ ⊆ ω̄ 0such that forall ∆ and Ē 00 :if
∆ `r ρ0i ; Ei00(∀ρ0i ∈ ρ̄0 )thenρθ  τ
and∆; ρθ ; E|θ|η `↓ τ ; E 0 η
where η = [Ē 00 /ω̄ 0 ]P ROOF. The proof proceeds by induction on the derivation.
(MTC-Simp). τ 0 ; ρ̄; ᾱ; ω̄; E `match τ ,→ ρ̄θ; ω̄; E|θ|Obviously, we have thatω̄ ⊆ ω̄andρ̄θ ⊆ ρ̄θ
From rule (MTC-Simp) we have
θ = mgu ᾱ (τ, τ 0 )This meansτ 0θ = τHence, from rule (M-Simp) it follows that
τ 0θ  τ
Also, from rule (I-Simp) it follows that∆; τ ; E|θ|η `↓ τ ; E|θ|η
or, equivalently,∆; τ 0 θ ; E|θ|η `↓ τ ; E|θ|η
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:40(MTC-IAbs).

B. Oliveira et al.

ρ1 ⇒ ρ2 ; ρ̄; ᾱ; ω̄; E `match τ ,→ ρ̄0 ; ω̄; E 0

From the rule (MTC-IAbs) and the induction hypothesis, it follows thatω̄, ω ⊆ ω̄ 0Hence,ω̄ ⊆ ω̄ 0
Similarly, it follows that(ρ̄, ρ1 )θ ⊆ ρ̄0Hence,ρ̄θ ⊆ ρ̄0
Also, from the rule (MTC-IAbs) and the induction hypothesis, it follows that
ρ2 θ  τ
and, by rule (M-IAbs), we hence have
ρ1 θ ⇒ ρ2 θ  τor, more succinctly,(ρ1 ⇒ ρ2 )θ  τFinally, from the rule (MTC-IAbs) and the induction hypothesis, it follows that∆; ρ2 θ ; (E ω)|θ|η `↓ τ ; E 0 ηor∆; ρ2 θ ; (Eθη) (ωη) `↓ τ ; E 0 η
Using rule (I-IAbs) we may then conclude∆; ρ1 θ ⇒ ρ2 θ ; Eθη `↓ τ ; E 0 ηor, equivalently,∆; (ρ1 ⇒ ρ2 )θ ; Eθη `↓ τ ; E 0 η(MTC-TAbs).

∀α.ρ; ρ̄; ᾱ; ω̄; E `match τ ,→ ρ̄0 ; ω̄; E 0

From the rule (MTC-TAbs) and the induction hypothesis, it follows thatω̄ ⊆ ω̄ 0
Similarly, it follows thatρ̄θ ⊆ ρ̄0
Also it follows thatρθ  τ
or, equivalently,ρ[ᾱθ/ᾱ][αθ/α]  τHence, following rule (MTC-TAbs), we have that∀α.(ρ[ᾱθ/ᾱ])  τ
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

The Implicit Calculus: A New Foundation for Generic Programming

A:41

or, equivalently,(∀α.ρ)[ᾱθ/ᾱ]  τFinally, from the rule (MTC-TAbs) and the induction hypothesis, it follows that∆; ρθ ; (E α)|θ|η `↓ τ ; E 0 ηor, equivalently,∆; ρθ ; (E|θ|[α|θ|/α]η) (α|θ|) `↓ τ ; E 0 η
Hence, following rule (I-TAbs), we get∆; (∀α.ρ)θ ; E|θ|η `↓ τ ; E 0 η

L EMMA A.7. If∆ `match1st τ ,→ ρ̄0 ; ω̄; Ethen there exist ρ and x such that∆hτ i = ρ ; x
and for all ∆0 ⊇ ∆ and for all Ē 0 such that∆0 `r ρ0i ; Ei0(∀ρ0i ∈ ρ̄0 )we have that
∆0 ; ρ ; x `↓ τ ; Eη
where η = [Ē 0 /ω̄].
P ROOF. The proof proceeds by induction on the derivation.
(M1-Head).
∆, ρ ; x `match1st τ ,→ ρ̄; ω̄; E
From rule (M1-Head) and the previous lemma, we then have thatρτ
Using rule (L-Head) we can conclude that(∆, ρ ; x)hτ i = ρ ; x
Similarly, we have that
∆0 ; ρ ; xη `↓ τ ; Eη
which simplifies to∆0 ; ρ ; x `↓ τ ; Eη
(M1-Tail).
∆, ρ ; x `match1st τ ,→ ρ̄; ω̄; E
From rule (M1-Tail) and the induction hypothesis, we then have that there exist ρ0
and x0 such that∆hτ i = ρ0 ; x0
Also from rule (M1-Tail) and a previous lemma, we have thatρ
6 τ
ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

A:42

B. Oliveira et al.

Hence, using rule (L-Tail) we can conclude that(∆, ρ ; x)hτ i = ρ0 ; x0
From rule (M1-Tail) and the induction hypothesis, we also have that
∆0 ; ρ0 ; x0 `↓ τ ; Eηfor ∆0 ⊇ (∆, ρ ; x).

L EMMA A.8. If∆ `alg ρ ; Ethen∆ `r ρ ; E
P ROOF. The proof proceeds by induction on the derivation.
(Alg-TAbs). ∆ `alg ∀α.ρ ; Λα.E
From rule (Alg-TAbs) and the induction hypothesis, it follows that∆ `r ρ ; E
Using rule (R-TAbs), we then get∆ `r ∀α.ρ ; Λα.E
(Alg-IAbs). ∆ `alg ρ1 ⇒ ρ2 ; λ(x : |ρ1 |).E
From rule (Alg-IAbs) and the induction hypothesis, it follows that∆, ρ1 ; x `r ρ2 ; E
Using rule (R-IAbs), we then get∆ `r ρ1 ⇒ ρ2 ; λ(x : |ρ1 |).E
(Alg-Simp). ∆ `alg τ ; E[ω̄/Ē]
From rule (Alg-Simp) and the previous lemma it follows that∆hτ i = ρ ; x
and∆; ρ ; x `↓ τ ; E[ω̄/Ē]
Hence, using rule (R-Simp), we conclude∆ `r τ ; E[ω̄/Ē]

ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY.