ZU064-05-FPR

Main

7 December 2018

10:26

Under consideration for publication in J. Functional Programming

1

C OCHIS: Stable and Coherent Implicits
TOM SCHRIJVERSKU Leuven, Belgium
BRUNO C.D.S. OLIVEIRAThe University of Hong Kong
PHILIP WADLER
University of Edinburgh, UK
KOAR MARNTIROSIANKU Leuven, Belgium

Abstract
Implicit Progamming (IP) mechanisms infer values by type-directed resolution, making programs
more compact and easier to read. Examples of IP mechanisms include Haskell’s type classes, Scala’s
implicits, Agda’s instance arguments, Coq’s type classes, and Rust’s traits. The design of IP mechanisms has led to heated debate: proponents of one school argue for the desirability of strong reasoning
properties; while proponents of another school argue for the power and flexibility of local scopingor overlapping instances. The current state of affairs seems to indicate that the two goals are at odds
with one another and cannot easily be reconciled.
This paper presents C OCHIS, the Calculus Of CoHerent ImplicitS, an improved variant of theimplicit calculus that offers flexibility while preserving two key properties: coherence and stabilityof type substitutions. C OCHIS supports polymorphism, local scoping, overlapping instances, firstclass instances, and higher-order rules, while remaining type safe, coherent and stable under type
substitution.
We introduce a logical formulation of how to resolve implicits, which is simple but ambiguous andincoherent, and a second formulation, which is less simple but unambiguous, coherent and stable.
Every resolution of the second formulation is also a resolution of the first, but not conversely. Partsof the second formulation bear a close resemblance to a standard technique for proof search calledfocusing. Moreover, key for its coherence is a rigorous enforcement of determinism.

1 Introduction
Programming language design is usually guided by two, often conflicting, goals: flexibility and ease of reasoning. Many programming languages aim at providing powerful,flexible language constructs that allow programmers to achieve reuse, and develop programs rapidly and concisely. Other programming languages aim at easy reasoning aboutprograms, as well as at avoiding programming pitfalls. Often the two goals are at odds
with each other, since highly flexible programming mechanisms make reasoning harder.
Arguably the art of programming language design is to reconcile both goals.
A concrete case where this issue manifests itself is in the design of Implicit Programming(IP) mechanisms. Implicit programming denotes a class of language mechanisms which
infer values by using type information. Examples of IP mechanisms include Haskell’s type

ZU064-05-FPR

Main

2

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosianclasses (Wadler & Blott, 1989), C++’s concepts (Gregor et al., 2006), JavaGI’s generalized interfaces (Wehr et al., 2007), Coq’s type classes (Sozeau & Oury, 2008), Scala’s
implicits (Odersky, 2010), Agda’s instance arguments (Devriese & Piessens, 2011), Rust’s
traits (Mozilla Research, 2017), and OCaml’s modular implicits (White et al., 2014). IP canalso be viewed as a form of (type-directed) program synthesis (Manna & Waldinger, 1980).
The programming is said to be implicit, because expressions (e.g., function arguments) canbe omitted by the programmer. Instead the necessary values are provided automatically via
a type-directed resolution process. These implicit values are either fetched by type fromthe current (implicit) environment or constructed by type-directed rules.
Currently there are two main schools of thought regarding the design of IP mechanisms.
Haskell’s type classes (Wadler & Blott, 1989) embody the first school of thought, whichis guided by the ease of reasoning qualities of pure functional languages, and the predictability of programs. To ensure these goals the semantics of the language should satisfy
a number of properties. One of those properties is coherence (Reynolds, 1991; Jones,
1992). The original definition of coherence in the literature is that any valid program musthave exactly one meaning (that is, the semantics is not ambiguous). In fact Haskell typeclasses are supposed to support an even stronger property, the so-called global uniquenessof instances (Zhang, 2014). Global uniqueness ensures that at any point in a program, andindependently of the context the type-directed resolution process always returns the samevalue for the same resolved type. This is a consequence of Haskell having a restriction ofat most one instance of a type class per type in a program.
While both coherence and global uniqueness of instances are preserved in Haskell, thiscomes at a cost. Since the first implementations of type classes, Haskell imposes several restrictions to guarantee those properties. Various past work has indicated limitations of typeclasses (Kahl & Scheffczyk, 2001; Camarão & Figueiredo, 1999; Dijkstra & Swierstra,
2005; Dreyer et al., 2007; Garcia et al., 2007; Oliveira et al., 2010; Morris & Jones, 2010;
Oliveira et al., 2012). In particular, type classes allow at most one instance per type (orseverely restrict overlapping instances) to exist in a program. That is, all instances must be
visible globally and local scoping of instances is not allowed. This form of global scoping
goes against modularity. Other restrictions of type classes are that they are not first-classvalues and that the type-directed rules cannot be higher-order (Oliveira et al., 2012).
Advanced features of type classes, such as overlapping instances (GHC, 2017), also posesevere problems, since they go against the principle of one instance per type. One issue isthat “when more specific overlapping instances are added, the proofs of some predicateswill change to use the new instances” (Morris & Jones, 2010). In essence special care(via restrictions) is needed to preserve coherence in the presence of overlapping instances.
Another important property that is broken in the presence of overlapping instances (ifspecial care is not taken) is the so-called stability of type substitutions. The issue is thatthe behaviour of resolution for an expression e can change if e gets a more specific type,leading to a different evaluation result. This is problematic because seemingly harmless
inlinings will actually have a different semantics before and after the inlining. Becauseof this problem, the design of Haskell type classes significantly restricts the set of valid
overlapping instances to ensure that stability holds, and the meaning of an expression does
not change simply due to a more specific type. In other words, resolution should resolve
implicit values using the same rules before and after instantiation of type variables.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

3

As an orthogonal remark, in the Haskell community, the term coherence is often colloquially used to encompass several different properties, including global uniqueness, stability and the original coherence definition by Reynolds (Reynolds, 1991). In the context
of an elaboration semantics (which the standard semantics style for IP mechanisms), thedefinition of coherence that follows from Reynolds one is that all possible elaborations fora program possess the same meaning. However such a definition of coherence is narrower
than the colloquial term usually used in the Haskell community. It is important to notethat the three properties are distinct. For example global uniqueness implies coherence,but not the converse. Furthermore it is also possible to have coherence, but not stability.
In this paper we will use coherence in Reynolds’ sense, and be precise about the different
properties under discussion.
An alternative school of thought in the design of IP mechanisms favours flexibility.
For example, Scala’s implicits and Agda’s instance arguments do not impose all of thetype class restrictions. Scala supports local scoping of instances, which allows distinct
instances to exist for the same type in different scopes of the same program. Scala also
allows a powerful form of overlapping implicits (Oliveira et al., 2010). The essence of
this style of implicit programming is modelled by the implicit calculus (Oliveira et al.,2012) or the more recent SI calculus (Odersky et al., 2017). The implicit calculus supports
a number of features that are not supported by type classes. Besides local scoping, in theimplicit calculus any type can have an implicit value. In contrast Haskell’s type class model
only allows instances of classes (which can be viewed as a special kind of record) tobe passed implicitly. Finally the implicit calculus supports higher-order instances/rules:
that is rules whose requirements can themselves be other rules. The implicit calculus has
been shown to be type-safe, and it also ensures coherence, but it lacks stability. The SI
calculus lacks both coherence and stability, but the authors present a simply-typed subsetthat is coherent1 . Unfortunately, while both the implicit/SI calculus and the various existinglanguage mechanisms embody flexibility, the lack of important properties such as stability
makes reasoning about the semantics of programs harder, and can prevent refactorings andcompiler optimizations such as inlining.
The design of IP mechanisms has led to heated debate (Hulley, 2009; Zhang, 2014;
Kmett, 2015) about the pros and cons of each school of thought: ease of reasoning versus
flexibility. Proponents of the Haskell school of thought argue that coherence, stability anduniqueness of instances are extremely desirable, and flexibility should not come at the costof those properties. Proponents of flexible IP mechanisms argue that flexibility is more
important, and that uniqueness of instances goes against modularity. As far as we are aware
there are no current designs that support local scoping, overlapping instances and first-classand higher-order rules, while at the same time ensuring both coherence and stability.
This paper presents C OCHIS: the Calculus Of CoHerent ImplicitS. C OCHIS is an improved variant of the implicit calculus that guarantees coherence and stability. C OCHIS
supports local scoping, overlapping instances, first-class instances and higher-order rules.
Yet, in contrast to most previous work that supports these features, the calculus is not

1

It makes no sense to talk about stability of type substitutions in a simply typed calculus, since thisis a property that is only relevant for polymorphic calculi.

ZU064-05-FPR

Main

4

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

only type-safe, but also stable and coherent. Naturally, the unrestricted calculus does notsupport global uniqueness of instances, since this property depends on the global scoping
restriction. Nevertheless, if retaining global uniqueness is desired, that can be modeled by
the subset of C OCHIS without local declarations. In fact, based on the resolution algorithmof an early version of C OCHIS, GHC has been recently extended with quantified classconstraints (Bottu et al., 2017; GHC, 2017). Quantified class constraints enable higherorder rules in a setting with global scoping.
Ensuring coherence and stability in the presence of C OCHIS’s overlapping and higherorder rules is particularly challenging. We introduce a logical formulation of how to resolve
implicits, which is simple but ambiguous and incoherent, and a second formulation, whichis less simple but unambiguous and coherent. Every resolution of the second formulationis also a resolution of the first, but not conversely. Parts of the second formulation bear aclose resemblance to a standard technique for proof search in logic called focusing (Andreoli, 1992; Miller et al., 1991; Liang & Miller, 2009). However, unlike focused proof
search, which is still essentially non-deterministic, C OCHIS’s resolution employs additional techniques to be entirely deterministic and thus obviously coherent. In particular,
unlike focused proof search, our resolution uses a stack discipline to prioritize implicits,
and removes any recursive resolutions from matching decisions. Moreover, further restrictions are needed to obtain stability.
In summary, our contributions are as follows:• We present C OCHIS, a coherent, stable and type-safe formal model for implicit
programming that supports local scoping, overlapping implicits, first-class implicits
and higher-order rules.
• We significantly improve the design of resolution over the existing work on theimplicit calculus by Oliveira et al. (2012). The new design for resolution is more
powerful and expressive; it is closely based on principles of logic and the idea of
propositions as types (Wadler, 2015); and is related to the idea of focusing in proof
search.
• C OCHIS comes with a semantics in the form of a type-directed elaboration to System F.
• We provide a unification-based algorithm as an executable form of the declarative
specification of resolution. A prototype implementation of this algorithm and of
C OCHIS is available at https://bitbucket.org/tom schrijvers/cochis/.
• We establish key meta-theoretic properties of our system:— The elaboration is type-preserving.
— Resolution is deterministic and thus obviously coherent.
— Resolution is stable under type substitution, and type-directed elaboration ispreserved by reduction of type application.
— Our algorithm is sound and complete with respect to its declarative specification.
The proofs are available in the appendix and at https://bitbucket.org/KlaraMar/cochiscoq
Organization Section 2 presents an informal overview of our calculus. Section 3 describes a polymorphic type system that statically excludes ill-behaved programs. Section 5

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

5

provides the elaboration semantics of our calculus into System F and correctness results.
Section 6 discusses several of our design choices as well as some alternatives. Section 7
discusses related work and Section 8 concludes.

2 Overview
This section summarises the relevant background on type classes, IP and coherence, andintroduces the key features of C OCHIS. We first discuss Haskell type classes, the oldest andmost well-established IP mechanism, then compare them to Scala implicits, and finally we
introduce the approach taken in C OCHIS.

2.1 Type Classes and Implicit Programming
Type classes enable the declaration of overloaded functions like comparison.
class Ord α where(6) :: α → α → BoolA type class declaration consists of: a class name, such as Ord; a type parameter, such asα; and a set of method declarations, such as (6). Each of the methods in the type classdeclaration should have at least one occurrence of the type parameter α in their signature.
Instances and Type-Directed Rules Instances implement type classes. For example, Ord
instances for integers, characters, and pairs can be defined as follows:
instance Ord Int wherex 6 y = primIntLe x yinstance Ord Char wherex 6 y = primCharLe x yinstance (Ord α, Ord β ) ⇒ Ord (α, β ) where(x, x0 ) 6 (y, y0 ) = x 6 y ∧ (¬ (y 6 x) ∨ x0 6 y0 )The first two instances provide the implementation of ordering for integers and characters,
in terms of primitive functions. The third instance is more interesting, and provides theimplementation of lexicographic ordering for pairs. In this case, the ordering instance itself
requires an ordering instance for both components of the pair. These requirements areresolved by the compiler using the existing set of instances in a process called resolution.
Using Ord we can define a generic sorting function
sort :: Ord α ⇒ [α ] → [α ]that takes a list of elements of an arbitrary type α and returns a list of the same type, aslong as ordering is supported for type α 2 .

2Note that, in Haskell, the single arrow (→) denotes a function type constructor, whereas the doublearrow (⇒) denotes a type with type class constraints (on the left of the arrow). In the sort function,for example, Ord α are the constraints.

ZU064-05-FPR

Main

6

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Implicit Programming Type classes are an implicit programming mechanism because
implementations of type class operations are automatically computed from the set of instances during the resolution process. For example, a call to sort only type checks if asuitable type class instance can be found. Other than that, the caller does not need toworry about the type class context, as shown in the following interaction with a Haskell
interpreter:
Prelude > sort [(3, ’a’), (2, ’c’), (3, ’b’)][(2, ’c’), (3, ’a’), (3, ’b’)]
In this example, the resolution process combines the three Ord instances to find a suitable
implementation for Ord (Int, Char). The declarations given are sufficient to resolve an
infinite number of other instances, such as Ord (Char, (Int, Int)) and the like.
One Instance Per Type A characteristic of (Haskell) type classes is that only one instanceis allowed for a given type. For example, it is forbidden to include the alternative orderingmodel for pairs
instance (Ord α, Ord β ) ⇒ Ord (α, β ) where(xa, xb) 6 (ya, yb) = xa 6 ya ∧ xb 6 yb
in the same program as the previous instance because the compiler automatically picks theright type class instance based on the type parameter of the type class. If there are two typeclass instances for the same type, the compiler does not know which of the two to choose.
2.2 Coherence in Type Classes
An IP design is coherent if any valid program has exactly one meaning (that is, the semantics is not ambiguous). Haskell imposes restrictions to guarantee coherence. For example,
Haskell rejects the expression:
show (read "3") ≡ "3"
due to ambiguity of type class resolution (Jones, 1992). The functions show and read print
and parse values of any type α that implements the classes Show and Read:class Show α whereshow :: α → Stringclass Read α whereread :: String → α
The program is rejected because there is more that one possible choice for α. For example
α can be instantiated to Int, Float, or Char. Choosing α = Float leads to False, since
showing the float 3 would result in "3.0", while choosing α = Int leads to True. In otherwords if this expression was accepted then it could have multiple possible semantics. To
ensure coherence instead of making an arbitrary choice Haskell rejects such programs.
Overlapping Instances Advanced features of type classes, such as overlapping instances,
require additional restrictions to ensure coherence. The following program illustrates someof the issues:

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

7class Trans α where trans :: α → αinstance Trans α where trans x = x
instance Trans Int where trans x = x + 1
This program declares a type class Trans α for defining transformations on some type α.
The first instance provides a default implementation for any type, the identity transformation. The second instance defines a transformation for integers only.
An important question here is what happens if we write an expression like trans 3.
Shall we pick the first or the second instance? Ideally this question should be answeredby the language specification. One possible choice for the specification (not the Haskell
choice) would be to allow any matching instance to be used, but this choice would leadto incoherence, since trans 3 could then both evaluate to 3 or 4. Instead, for overlapping
instances, the GHC documentation (GHC, 2017) makes a different choice and declares thatthe most specific instance should be chosen. For the expression trans 3, the most specificinstance is Trans Int and the expression evaluates to 4.
For the particular program trans 3, the Haskell specification manages to avoid incoherence by using the most specific instance, which ensures an unambiguous semantics. Thus,
Haskell preserves coherence in the presence of a certain kind of overlapping instances, butthere are other problematic overlapping instances that threaten the coherence property.

Incoherent Instances With overlapping instances, it is not always the case that a most
specific instance exists. Consider the following type class and instance declarations:class C α β wherem :: α → β → Bool
instance C Bool α where
mxy=x
instance C α Bool where
mxy=y
If we write the following program
incoherent :: Boolincoherent = m True False-- rejected without IncoherentInstances extension

then there is no most specific instance: both instances are equally specific. In this case,even with the overlapping instances extension activated, Haskell rejects the program.
However, Haskell also supports an additional extension, called IncoherentInstances,
for allowing a more general kind of overlapping instances. With IncoherentInstances
activated, Haskell accepts the incoherent definition. The (informal) language specification (GHC, 2017) for IncoherentInstances essentially says that in such a situation any
matching instance could be picked. Thus, either of the two instances above can be picked,
producing different evaluation results for the expression. Thus, as the name indicates, theexpression incoherent leads to incoherence.

ZU064-05-FPR

Main

8

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian
2.3 Stability in Type Classes

Another important property that is closely related to coherence is stability. Informally, stability ensures that instantiation of type variables does not affect resolution. Unfortunately
overlapping instances threaten this property. Consider the following declaration, that uses
the trans method from the type class Trans and the two instances declared previously:
bad :: α → α
bad x = trans x-- unstable definition!

Note here that the type of bad is α → α instead of Trans α ⇒ α → α. In Haskell bothsignatures can be accepted, but they are not equivalent. With Trans α ⇒ α → α resolution
is deferred to the call site of bad, allowing the instance of Trans α to be selected when α has
been instantiated to a (potentially) more precise type. By contrast, with α → α resolution
is applied eagerly, and an instance must be selected at the definition site. If Haskell were toaccept this definition, it would have to implement trans using the first instance, since transis applied at the arbitrary type α. Unfortunately this would mean that bad 3 returns 3 but
trans 3 returns 4, even though bad and trans are defined to be equal, a nasty impedimentto equational reasoning!
For this reason Haskell rejects the program by default. A programmer who really wants
such behaviour can enable the IncoherentInstances compiler flag, which allows the
program to type check.
Note that even though to allow bad we need the IncoherentInstances extension,
which is suggestive of the definition breaking coherence, the issue here is not really coherence but rather stability. That is, type instantiation affects type class instantiation. As thisexample illustrates, instability is actually observable from a compiler implementation like
GHC: we can observe that bad 3 and trans 3 behave differently. In contrast (in)coherence
is not really observable from a compiler implementation: we need a language specification
to understand whether there is incoherence or not. More concretely, with a single compiler
implementation we can only observe the result of one possible elaboration of a program,but we cannot observe all the other possible elaborations allowed by the specification forthat program. Therefore, we cannot observe incoherence.
The IncoherentInstances extension is understood to be highly problematic among
Haskell programmers, since it can break both stability and coherence. Thus its use is greatly
discouraged.

2.4 Global Uniqueness in Type Classes
A consequence of having at most one instance of a type class per type in a program is
global uniqueness of instances (Zhang, 2014). That is, at any point in the program typeclass resolution for a particular type always resolves to the same value. Global uniquenessis a simple way to guarantee coherence, but it offers more than just coherence. The usefulness of this property is illustrated by a library that provides a datatype for sets that ispolymorphic in the elements along with a union operation:
union :: Ord α ⇒ Set α → Set α → Set αZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

9For efficiency reasons the sets are represented by a data structure that orders the elements
in a particular way. It is natural to rely on the Ord type class to deal with ordering forthe particular type α. To preserve the correct invariant, it is crucial that the ordering ofelements in the set is always the same. The global uniqueness property guarantees this.
If two distinct instances of Ord could be used in different parts of the program for thesame type, then it would be possible to construct within the same program two sets using
two different orderings (say ascending and descending order), and then break the ordering
invariant by union-ing those two sets.
However, although global uniqueness is, in principle, a property that should hold in
Haskell programs, Haskell implementations actually violate this property in various circumstances (nponeccop, 2012). In fact, it is acknowledged that providing a global uniqueness check is quite challenging for Haskell implementations (Marlow, 2012).

2.5 Scala Implicits and Stability
Scala implicits (Oliveira et al., 2010) are an interesting alternative IP design. Unlike typeclasses, implicits are locally scoped. Consequently, Scala does not have the global uniqueness property, since different “instances” may exist for the same type in different scopes.
Another important difference between implicits and type classes is that implicit parameters
can be of any type, and there are no special constructs analogous to type class or instancedeclarations. Instead, implicits are modelled with ordinary types. They can be abstracted
over and do not suffer from the second-class nature of type classes. These features meanthat Scala implicits have a wider range of applications than type classes. Unlike Haskell
type classes, however, with Scala implicits there is no way to enforce stability.
Modelling Type Classes with Implicits In Scala there is no special construct for defining
the interface of a type class. Instead we can use regular interfaces to model type classinterfaces. Scala models OO interfaces with traits (Scharli et al., 2003). For example, the3 interfaces presented in Section 2.1 can be modelled as:
trait Ord [T ] {def le (x : T, y : T) : Boolean}
trait Show [T ] {def show (x : T) : String}trait Read [T ] {def read (x : String) : T }Of course, by declaring traits like this, we still require explicit objects to call the methods
on. To be able to use methods in the same way as Haskell type classes, the object (ordictionary) should be passed implicitly. This can be achieved by using Scala’s implicits
feature:def cmp [A] (x : A, y : A) (implicit ordD : Ord [A]) : Boolean = ordD.le (x, y)
The Scala definition of cmp plays the same role as 6 in Haskell. The type of cmp statesthat cmp is parametrized in a type A, takes two (explicit) arguments of type A, and one
implicit parameter (ordD). This is similar to a Haskell signature Ord α ⇒ α → α → Bool,
except that the implicit argument comes last. Additionally, unlike Haskell, at call sites it ispossible to pass the implicit argument explicitly, if desired.

ZU064-05-FPR

Main

10

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. MarntirosianContext Bounds and Queries For the purposes of this paper we will, however, present
cmp using context bounds: an alternative way to declare functions with constraints (orimplicit arguments), supported in Scala. Context bounds are a simple syntactic sugar built
on top of implicit parameters. With context bounds, the cmp definition is rewritten into:
def cmp [A : Ord ] (x : A, y : A) : Boolean = ?[Ord [A]].le (x, y)
The notation A : Ord is the so-called context bound. This notation enables us to declare aconstraint on the type A. Namely, the type A should be an “instance” of Ord [A]. In the
background the Scala compiler rewrites definitions with context bounds into definitions
with implicit arguments. In the body of cmp an additional mechanism, called an implicit
query, is now necessary to query the environment for a value of type Ord [A]. This querymechanism in Scala is nothing more than a simple function taking an implicit argument.
The (slightly simplified) definition of the query operator is:3
def ? [T ] (implicit w : T) : T = w
The operator ? takes a single implicit argument of type T and returns that value. Hence
operationally it is just the identity function. The key point is that, when used, the implicit
argument is filled in automatically by the compiler. In the definition of cmp, the expression?[Ord [A]] triggers the compiler to look for a value of type Ord [A] in the implicit environment. The implicit environment collects values that are declared to be implicit, and usable
for automatic implicit resolution.
Implicit values, which correspond to type class instances in Haskell, are declared byusing the implicit keyword. The following three examples capture the “instances” for Ord:
implicit val OrdInt = new Ord [Int ] {def le (x : Int, y : Int) = primIntLe (x, y)}
implicit val OrdChar = new Ord [Char ] {def le (x : Char, y : Char) = primCharLe (x, y)}
implicit def OrdPair [A : Ord, B : Ord ] = new Ord [(A, B)] {def le (x : (A, B), y : (A, B)) =cmp (fst (x), fst (y)) ∧ (!(cmp (fst (y), fst (x))) ∨ cmp (snd (x), snd (y)))}
With those definitions it is now possible to declare functions, such as sort, that require
Ord instances:
def sort [A : Ord ] (x : List [A]) = ...
This Scala sort function can be used in a similar way to the corresponding Haskell function.
For example the call sort (List ((3, ’a’), (2, ’c’), (3, ’b’))) is valid and does not require
an explicit argument of type Ord [(Int, Char)]. Instead this argument is computed from theimplicit definitions for Ord.
3

In Scala the operator is known by the longer name implicitly.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

11

Wider Range of Applications for Implicits Scala implicits do allow for a wider range ofapplications than type classes. One example where implicits naturally address a problem
that type classes do not address well is the problem of implicit configurations (Kiselyov &Shan, 2004). The following example, adapted from Kiselyov and Shan, illustrates this:def add (x : Int, y : Int) (implicit modulus : Int) = (x + y) % modulus
def mul (x : Int, y : Int) (implicit modulus : Int) = (x ∗ y) % modulus
implicit val defMod : Int = 4
def test = add (mul (3, 3), mul (5, 5)) // returns 2
Here the idea is to model modular arithmetic, where numbers that differ by multiples of agiven modulus are treated as identical. For example 3 * 3 = 1 (mod 4) because 9 and 1 differ
by a multiple of 4. The code shows the definition of addition and multiplication in modular
arithmetic, where in Scala % is modulo division. Both addition and multiplication include
a third (implicit) parameter, which is the modulus of the division. Although the modulus
could be passed explicitly this would be extremely cumbersome. Instead it is desirable
that the modulus is passed implicitly. Scala implicits allow this, by simply marking themodulus parameter in add and mul with the implicit keyword. The third line shows how to
set up an implicit value for the modulus. Adding implicit before val signals that the value
being defined is available for synthesising values of type Int. Finally, test illustrates how
expressions doing modular arithmetic can be defined using the implicit modulus. Because
Scala also has local scoping, different modulus values can be used in different scopes.
Several other examples of applications that can be covered by implicits, but are harderto achieve with type classes are found in the existing literature (Oliveira et al., 2010;
Oliveira et al., 2012; Odersky et al., 2017). In particular, in a recent paper Odersky et al.
(2017) introduce implicit function types, which are a generalization of the original Scala
implicits (Oliveira et al., 2010), and demonstrate several interesting use cases for implicits.
Instability in Scala Although Scala allows nested local scoping and overlapping implicits, stability is not guaranteed. Figure 1 illustrates the issue briefly, based on the example
from Section 2.2. Line (1) defines a function id with type parameter α, which is simply theidentity function of type α ⇒ α 4 . The implicit keyword in the declaration specifies that
this value may be used to synthesise an implicit argument. Line (2) defines a function transwith type parameter α, which takes an implicit argument f of type α ⇒ α and returns
f (x). Here the implicit keyword specifies that the actual argument should not be given
explicitly; instead argument of the appropriate type will be synthesised from the available
implicit declarations.
In the nested scope, line (3) defines function succ of type Int ⇒ Int that takes argument
x and returns x + 1. Again, the implicit keyword in the declaration specifies that succ
may be used to synthesise implicit arguments. Line (4) defines a function bad with typeparameter α which takes an argument x of type α and returns the value of function transapplied at type α to argument x. Line (5) shows that, as in the earlier example and for thesame reason, bad (3) returns 3. As with the Haskell example, accepting this definition is

4

Note that the α ⇒ β notation in Scala represents a function type, rather than a rule type.

ZU064-05-FPR

Main

7 December 2018

12

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian
trait A {implicit def id [α ] : α ⇒ α = x ⇒ x// (1)
def trans [α ] (x : α) (implicit f : α ⇒ α) = f (x) // (2)}object B extends A {implicit def succ : Int ⇒ Int = x ⇒ x + 1// (3)
def bad [α ] (x : α) : α = trans [α ] (x)// (4) unstable definition !
val v1 = bad [Int ] (3)// (5) evaluates to 3// val v2 = trans [Int ] (3)// (6) substituting bad by trans is rejected}

Fig. 1. Nested Scoping with Overlapping Rules in Scalaan equally nasty impediment to equational reasoning, since performing simple equational
reasoning would lead to a different result. However unlike in Haskell, it is the intended
behaviour: it is enabled by default and cannot be disabled. Interestingly the expression inline (6), which is accepted in Haskell, is actually rejected in Scala. Note that the expression
in line (6) is simply the unfolding of the expression in line (5) (which is accepted in Scala).
In the expression in line (6) the Scala compiler does detect two possible instances forInt ⇒ Int, but does not select the most specific one. In this case the call in line (6) is
considered ambiguous because Scala accounts for other factors, when deciding whether
there is ambiguity (Oliveira et al., 2010; Odersky et al., 2017). Rejecting line (6) has
another unfortunate effect. Not only is the semantics not preserved under unfolding, buttyping is not either: i.e. going from line (5) to line (6) using a simple unfolding step makes
the program ill-typed! Clearly, satisfying desirable properties such as stability and typepreservation is a subtle matter in the presence of implicits and deserves careful study.
2.6 An Overview of C OCHIS
Like Haskell, our calculus C OCHIS guarantees stability and coherence and, like Scala, it
permits nested/overlapping declarations, and does not guarantee global uniqueness. C OCHIS
improves upon the implicit calculus (Oliveira et al., 2012) by having stability and a better, more expressive design for resolution. Like the implicit calculus, the primary goalof C OCHIS is to model implicit resolution and the scoping of implicit values used byresolution. Next we iterate over the key constructs and features of C OCHIS.
Fetching Values by Type A central construct in C OCHIS 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 actualargument. Note that queries in C OCHIS play the same role as the operator ? in Scala.
Constructing Values with Type-Directed Rules C OCHIS constructs values, using programmerdefined, 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 arule that given an implicit Int value, adds one to that value:

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

13

λ? 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 typeargument denotes the availability of a value of that type (in this case Int) in the implicit
environment inside the body of the rule abstraction. Thus, queries over the rule abstraction
type argument inside the rule body will succeed.
The type of the rule above is the rule type Int ⇒ Int. This type denotes that the rule has
type Int provided a value of type Int is available 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.
The analog to rule abstractions in Scala are functions with arguments marked with the
implicit keyword. However, in older versions of Scala, functions with implicit arguments
were not first class and could not be abstracted over. In particular in older versions of
Scala it was impossible to express the type of a function with an implicit argument. Recent
versions of Scala, partly inspired by the implicit calculus, generalize the mechanism of
implicits and make rule abstractions and types first class too, by what they call implicit
function types (Odersky et al., 2017).
Higher-Order Rules C OCHIS 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):(λ? Int.λ? (Int ⇒ Int×Int).?(Int×Int))
with 3
with (λ? Int.(?Int, ?Int + 1))
Recursive Resolution Note that resolving the query ?(Int×Int) above involves multiple
implicits. The current environment does not contain the required integer pair. It does however contain the integer 3 and a rule λ? Int.(?Int, ?Int + 1) to compute a pair from an integer.
Hence, the query is resolved with (3, 4), the result of applying the pair-producing rule to 3.
Polymorphic Implicits and Queries C OCHIS features explicit polymorphism. For example, the rule Λα.(λ? α.(?α, ?α)) abstracts over a type using standard type abstraction andthen uses a rule abstraction to provide a value of type α in the implicit environment of theZU064-05-FPR

Main

14

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

rule body. This rule has type ∀α.α ⇒ α ×α and can be instantiated to multiple rules ofmonomorphic types Int ⇒ Int×Int, Bool ⇒ Bool×Bool, . . ..
Multiple monomorphic queries can be resolved by the same polymorphic rule. The
following expression returns ((3, 3), (True, True)):
implicit 3 in implicit True in implicit (Λα.(λ? α.(?α, ?α))) in (?(Int×Int), ?(Bool×Bool))
Queries can be polymorphic too. For instance, the following example extracts the polymorphic implicit with a polymorphic query.
implicit (Λα.(λ? α.(?α, ?α))) in ?(∀β .β ⇒ (β ×β )))In practice, polymorphic queries are useful in combination with higher-kinded types where
they occur as recursive resolvents of polymorphic rules. We cannot illustrate this withC OCHIS as, to keep its definition small, it is not equipped with higher-kinded types. Theinterested reader can find examples in the work of Bottu et al. (2017).
Type-Directed Synthesis of Simple Programs One interesting feature of C OCHIS is thatit can synthesize simple programs of a given type. This feature can potentialy be usefulwhen there is at most one possible implementation of a program. For example a variant of
the polymorphic identity function could be synthesized with the following query:?(∀α.α ⇒ α)
We have not yet explored the usefulness of this feature for practical programming in depth,
but this seems to be related to programming with typed holes (Norell, 2008). Perhaps such a
feature (or some extension of it) can be useful to automatically synthesize implementations
for typed holes.
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 ∀α.α ⇒ α ×α twice: first to an integer, and again
to the result (an integer pair). For example, the following expression returns ((3, 3), (3, 3)):
implicit 3 in implicit (Λα.(λ? α.(?α, ?α))) in ?((Int×Int)×(Int×Int))
Locally and Lexically Scoped Implicits Implicits can be nested and resolution respects
their lexical scope. 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.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

15

Care with Reduction Observe that some care is required with the inlining of let-bindings
and other refactorings that perform variable substitutions. Consider for instance the following program.
implicit 1 inlet x = ?Int in
implicit 2 inx
One might inline x and obtain the following.
implicit 1 in
implicit 2 in? Int
But this would change its meaning: the first program returns 1, while the second returns
2. The solution is to never consider a term as a candidate for substitution until all of its
implicits have been resolved.
This situation is not much different from that of regular let-bindings. For example, if wenaively inline y in the following program:let x = 1 inlet y = x inlet x = 2 inywe getlet x = 1 inlet x = 2 inx
The second program clearly has a different meaning, since the variable x is now capturedby the second binder rather than the first. While this problem can be remedied by renaming
the second binder’s variable, there is no analogous solution for implicits.

2.6.1 Encoding Simple Type Classes in C OCHIS
A simple form of type classes can be encoded in C OCHIS similarly to how type classes
can be encoded in Scala. In this section we briefly (and informally) illustrate the encoding
using examples. The simple encoding presented here does not deal with superclasses. We
discuss superclasses in Section 6.
Next we illustrate how the encoding works on the examples from Section 2.1. To help
with readability we assume a few convenient source language features not available in
C OCHIS (which is designed as a formal core calculus rather than a full-fledged source language). In particular C OCHIS has no type-inference and requires explicit rule applications
and queries. The design of a source language that supports type-inference, implicit rule
applications, implicit polymorphism and that translates into a C OCHIS-like calculus was

ZU064-05-FPR

Main

16

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosianalready explored in our previous work on the implicit calculus (Oliveira et al., 2012). To
better illustrate some of our examples here we will assume such source language features.
Firstly we use type synonyms to allow us to give a short name to a type. Secondly we use
records. Using both of those constructs, the three type classes introduced in Sections 2.1
and 2.2 can be declared as:type Ord α = {le : α → α → Bool}type Show α = {show : α → String}type Read α = {read : String → α }Similarly to the Scala encoding we define a cmp function that makes the argument of type
Ord α implicit:
let cmp : ∀α.Ord α ⇒ α → α → Bool = (? : Ord α).le in
Here the query is annotated with a type Ord α triggering the resolution of a value of thattype. Once that value is computed, the field le can be extracted from it.
The “instances” of Ord can be defined as record values or rule types returning an Ord
record.
let ordInt : Ord Int = {le = λ x. λ y. primIntLe x y} in
let ordChar : Ord Char = {le = λ x. λ y. primCharLe x y} in
let ordPair : ∀α β . Ord α ⇒ Ord β ⇒ Ord (α, β ) = {le = λ x. λ y.
cmp (fst x) (fst y) ∧ ((¬ (cmp (fst y) (fst x))) ∨ cmp (snd x) (snd y))} in
Here the first two values denote instances for the base types Int and Char. The instance forpairs (ordPair) has two constraints (Ord α and Ord β ), and those constraints are implicitly
used by cmp.
Given a sort function:
let sort : ∀α.Ord α ⇒ List α → List α = ...
we can now use implicit to introduce the “instances” into the implicit scope and have theOrd (List Int) argument of the call sort [(3, ’a’), (2, ’c’), (3, ’b’)] automatically inferred:
implicit ordInt in
implicit ordChar in
implicit ordPair insort [(3, ’a’), (2, ’c’), (3, ’b’)]

2.7 Overlapping Implicits and Stability in C OCHISAs previously shown, the lexical scope imposes a natural precedence on implicits that
ensures coherence. This precedence means that the lexically nearest implicit is used toresolve a query, and not necessarily the most specific implicit. For instance, the following
C OCHIS variation on the running trans example from Section 2.2
implicit (λ n.n + 1 : Int → Int) in
implicit (λ x.x : ∀α.α → α) in?(Int → Int) 3

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

17yields the result 3 as the inner identity implicit has precedence over the more specificincrementation implicit in the outer scope. Yet, it is not always possible to statically selectthe nearest matching implicit. Consider the program fragment
let bad : ∀β .β → β =implicit (λ x.x : ∀α.α → α) in
implicit (λ n.n + 1 : Int → Int) in?(β → β )Here we cannot statically decide whether Int → Int matches β → β : it depends on whether
β is instantiated to Int or not.
One might consider to force the matter by picking the lexically nearest implicit thatmatches all possible instantiations of the query, e.g., ∀α.α → α in the example. While thisposes no threat to type safety, this approach is nevertheless undesirable for two reasons.
Firstly, it makes the behaviour of programs harder to predict, and, secondly, the behaviourof programs is not stable under inlining. Consider the call bad Int 3, which would yield theresult 3. If instead we inline the function definition of bad at the call site and substitute thetype argument, we obtain the specialised program
implicit (λ x.x : ∀α.α → α) in
implicit (λ n.n + 1 : Int → Int) in?(Int → Int) 3
Now Int → Int is the nearest lexical match and the program yields the result 4. Consequently, inlining definitions changes their behavior. To avoid this unpredictable behaviour,C OCHIS rejects such unstable matchings. Technically speaking the key property that C OCHIS
guarantees is stability of resolution (see also Section 5). Essentially this property ensuresthat type instantiation does not affect the resolution of queries. That is, if some typevariables appear free in a query that resolves, then, after instantiating any or all of thosetype variables, the query still resolves in the same way, i.e., using the same implicits.
If it cannot be statically guaranteed that resolution behaves in the same way for every
instantiation, then the program is rejected. The benefit of rejecting such potentially unstable
programs is that the principle of substituting equals for equals is not affected by theinteraction between resolution and instantiation. This makes reasoning about programs
and code refactoring more predictable.

3 The C OCHIS Calculus
This section formalizes the syntax and type system of C OCHIS, while Section 5 formalises
the type-directed translation to System F. To avoid duplication and ease reading, we present
the type system and type-directed translation together, using grey boxes to indicate whichparts of the rules belong to the type-directed translation. These greyed parts can be ignoredin this section and will be explained in the next.

ZU064-05-FPR

Main

18

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian
3.1 Syntax

Here is the syntax of the calculus:
Types
Monotypes
Expressions

ρσe::= α | ρ1 → ρ2 | ∀α.ρ | ρ1 ⇒ ρ2::= α | σ → σ::= x | λ (x : ρ).e | e1 e2 | Λα.e | e σ |?ρ | λ? ρ.e | e1 with e2

Types ρ comprise four constructs: type variables α; function types ρ1 → ρ2 ; universal
types ∀α.ρ; and the novel rule types ρ1 ⇒ ρ2 . In a rule type ρ1 ⇒ ρ2 , type ρ1 is called
the context and type ρ2 the head, following Haskell’s terminology for type class instances.
Observe that C OCHIS types are similar to Haskell’s type schemes with the exception that
contexts are types rather than type class constraints. We also define a subset of types, called
monotypes σ , which, like Haskell’s monotypes, do not contain universal quantifiers or rule
types.
Expressions e include three abstraction-elimination pairs. The form λ (x : ρ).e abstracts
over a value of type ρ in expression e, which can refer to it with variable x; the abstraction
is eliminated by application e1 e2 . Similarly, Λα.e abstracts over a type in expression e,
which can refer to it with type variable α; the abstraction is eliminated by predicative
type application e σ (see Section 3.5.1). Finally, λ? ρ.e abstracts over implicit values oftype ρ in expression e, which can refer to it with implicit query ?ρ; the abstraction iseliminated by implicit application e1 with e2 . For convenience we adopt the Barendregt
convention (Barendregt, 1981), that variables in binders are distinct, throughout this article.
Using implicit abstraction and implicit application we can build the implicit sugar usedin Section 2.
def

implicit e1 : ρ in e2 = (λ? ρ.e2 ) with e1
For brevity we have kept the C OCHIS calculus small. Examples may use additional
syntax such as built-in integers, integer operators, and boolean literals and types.

3.2 Type System
Figure 2 presents the static type system of C OCHIS. Our language is based on predicative
System F, which is included in our system.
As in predicative System F, a type environment Γ records type variables α and variables
x with associated types ρ that are in scope. New here is that it also records instances of
implicits ?ρ.
Type Environments Γ ::= ε | Γ, x : ρ | Γ, α | Γ, ?ρ ; x

A typing judgment Γ ` e : ρ holds if expression e has type ρ with respect to type environment Γ. The first five rules copy the corresponding predicative System F rules; only the last
three deserve special attention. Firstly, rule (T Y-IA BS) extends the implicit environment
with the type of an implicit instance. The side condition `unamb ρ1 states that the type ρ1
must be unambiguous; we explain this concept in Section 3.5. Secondly, rule (T Y-IA PP)
eliminates an implicit abstraction by supplying an instance of the required type. Finally,rule (T Y-Q UERY) resolves a given type ρ against the implicit environment. Again, a side-ZU064-05-FPR

Main

7 December 2018

10:26

19

Cochis: Stable and Coherent Implicits

Γ`e:ρ ;E
(T Y-VAR )(x : ρ) ∈ ΓΓ`x:ρ ;xΓ, x : ρ1 ` e : ρ2 ; E(T Y-A BS )

Γ ` λ x : ρ1 .e : ρ1 → ρ2 ; λ x : |ρ1 |.E(T Y-A PP )

Γ ` e1 : ρ1 → ρ2 ; E1

Γ ` e2 : ρ1 ; E2

Γ ` e1 e2 : ρ2 ; E1 E2
Γ, α ` e : ρ ; E1

(T Y-TA BS )Γ ` Λα.e : ∀α.ρ ; Λα.E1(T Y-TA PP )

Γ ` e : ∀α.ρ ; E

Γ ` e σ : ρ[σ /α] ; E |σ |(T Y-IA BS )Γ, ?ρ1 ; x ` e : ρ2 ; E`unamb ρ1

x freshΓ ` λ? ρ1 .e : ρ1 ⇒ ρ2 ; λ x : |ρ1 |.E(T Y-IA PP )

Γ ` e1 : ρ2 ⇒ ρ1 ; E1

(T Y-Q UERY )Γ ` e2 : ρ2 ; E2

Γ ` e1 with e2 : ρ1 ; E1 E2
Γ `ar ρ ; E`unamb ρΓ `?ρ : ρ ; E

Fig. 2. Type System and Type-directed Translation to System F
condition states that ρ must be unambiguous. Resolution is defined in terms of the auxiliary
judgment Γ `ar ρ, which is explained next.
3.3 Resolution
Figure 3 provides a first, ambiguous definition of the resolution judgment. Its underlying
principle is resolution in logic. Intuitively, Γ `ar ρ holds if Γ entails ρ, where the types inΓ and ρ are read as propositions, r stands for resolution and a for ambiguous. Following
the “Propositions as Types” correspondence (Wadler, 2015), we read α as a propositionalvariable and ∀α.ρ as universal quantification. Yet, unlike in the traditional interpretation oftypes as propositions, we have two forms of arrows, function types ρ1 → ρ2 and rule types
ρ1 ⇒ ρ2 , and the twist is that we choose to treat only rule types as implications, leaving
function types as uninterpreted predicates.
Unfortunately, the definition in Figure 3 suffers from two problems. Firstly, it is notsyntax-directed; several of the inference rules have overlapping conclusions. Hence, a

ZU064-05-FPR

Main

7 December 2018

20

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. MarntirosianΓ `ar ρ ; E(AR-IVAR )(AR-TA BS )(AR-TA PP )Γ, α `ar ρ ; E?ρ ; x ∈ ΓΓ `ar ρ ; x(AR-IA BS )Γ `ar ∀α.ρ ; Λα.EΓ `ar ∀α.ρ ; EΓ `ar ρ[σ /α] ; E |σ |(AR-IA PP )Γ, ?ρ1 ; x `ar ρ2 ; E

x freshΓ `ar ρ1 ⇒ ρ2 ; λ x : |ρ1 |.EΓ `ar ρ1 ⇒ ρ2 ; E2

Γ `ar ρ1 ; E1

Γ `ar ρ2 ; E2 E1

Fig. 3. Ambiguous Resolution

deterministic resolution algorithm is non-obvious. Secondly and more importantly, thedefinition is ambiguous: a type can be derived in multiple different ways. As an example
of both issues, consider that under the environment
Γ0 =?Int, ?Bool, ?(Bool ⇒ Int)
there are two different derivations for resolving Γ0 `ar Int:
(AR-IVAR )?Int ∈ Γ0Γ0 `ar Int

and(AR-IVAR )(AR-IA PP )?(Bool ⇒ Int) ∈ Γ0
Γ0 `ar Bool ⇒ Int(AR-IVAR )?Bool ∈ Γ0
Γ0 `ar Bool

Γ0 `ar Int

This example illustrates the first issue; in particular the inference rules (AR-IVAR) and(AR-IA PP) overlap as both can be used to conclude Γ0 `ar Int. It also shows the second
issue as there are two fully different derivation trees for Γ0 `ar Int. While this may seem
harmless at the type-level, at the value-level each derivation corresponds to a (possibly)
different value. Hence, ambiguous resolution may render the meaning of a program ambiguous. In other words, if both resolutions are allowed then the semantics is not coherent.
We next address these two issues one by one. Readers who are keen to see the end result
may wish to skip the gradual developments and jump straight to Section 3.5.5.

3.4 Type-Directed Resolution with Focusing
To obtain a type-directed formulation of resolution, we adopt a solution from proof search
known as focusing (Andreoli, 1992). This solution makes sure that only one inference rule
applies at any given point and thereby rules out gratuitous forms of nondeterminism.

ZU064-05-FPR

Main

7 December 2018

10:26

21

Cochis: Stable and Coherent Implicits

Σ ::= ε | ρ ; x , ΣΓ `fr [ρ] ; E(FR-TA BS )(FR-S IMP )Γ, α `fr [ρ] ; E(FR-IA BS )

Γ `fr [∀α.ρ] ; Λα.E

?ρ ; x ∈ ΓΓ, ?ρ1 ; x `fr [ρ2 ] ; E

x freshΓ `fr [ρ1 ⇒ ρ2 ] ; λ x : |ρ1 |.E

Γ; [ρ] ; x `fr ρ̄ 0 ; x̄0 ; τ ; EΓ `fr [ρ 0 ] ; E 0 (∀ρ 0 ∈ ρ̄ 0 )Γ; [ρ] ; E `fr Σ; τ ; E 0

MatchingΓ `fr [τ] ; E[Ē 0 /x̄0 ](FM-TA PP )(FM-IA PP )Fig. 4. Focusing Resolution

Focusing

Γ; [ρ[σ /α]] ; E |σ | `fr Σ; τ ; E 0
Γ; [∀α.ρ] ; E `fr Σ; τ ; E 0

Γ; [ρ2 ] ; E x `fr Σ; τ ; E 0

x freshΓ; [ρ1 ⇒ ρ2 ] ; E `fr ρ1 ; x , Σ; τ ; E 0(FM-S IMP ) Γ; [τ] ; E `fr ε; τ ; E

As an example of such gratuitous nondeterminism consider the following two ways ofresolving α given Γ = α, ?α ; x:
(AR-IVAR )versus(AR-IVAR )(AR-IA BS )(AR-IA PP )?α ; x ∈ ΓΓ `ar α ; x?α ; y ∈ (Γ, ?α ; y)Γ, ?α ; y `ar α ; yΓ `ar α ⇒ α ; λ y.yΓ `ar α ; (λ y.y) x(AR-IVAR )?α ; x ∈ ΓΓ `ar α ; x

While these are two different proofs, they use the information in the context Γ in essentially the same way. They are β -equivalent and infer System F expressions that are also
semantically equivalent. Hence, unlike the nondeterminism in the previous example at theend of Section 3.3, where the context provides two ways of resolving the query, this formof nondeterminism serves no purpose. We will see that focusing provides a straitjacket thateliminates the gratuitous nondeterminism and allows only the first and more direct of thesetwo proofs. In fact, it allows only derivations in β -reduced and η-expanded form.

ZU064-05-FPR

Main

22

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

The focusing approach refines the grammar of types to distinguish a special class of
simple types:
Context Types
Simple Typesρτ::= ∀α.ρ | ρ1 ⇒ ρ2 | τ::= α | ρ1 → ρ2

Observe that simple types τ are those types that do not have corresponding pairs of introduction and elimination rules in the ambiguous resolution judgment.
The definition of resolution with focusing that uses this refined grammar is given in Figure 4. The main focusing judgment Γ `fr [ρ] ; E is defined with the help of the auxiliary
matching judgment Γ; [ρ] ; E `fr Σ; τ ; E 0 . Both definitions are syntax-directed on thetype ρ enclosed in square brackets.
The focusing judgment Γ `fr [ρ] ; E focuses on the type ρ that is to be resolved –we call this type the “goal”. There are three rules, for the three possible syntactic formsof ρ. Rules (FR-IA BS) and (FR-TA BS) decompose the goal by applying implication andquantifier introductions respectively. Once the goal is stripped down to a simple type
τ, Rule (FR-S IMP) selects an implicit ρ from the environment Γ to discharge it. The
selected type must match the goal, a notion that is captured by the auxiliary judgment.
Matching gives rise to a sequence Σ of new (and hopefully simpler) goals that are resolved
recursively.
The matching judgment Γ; [ρ] ; E `fr Σ; τ ; E 0 focuses on the selected implicit ρand checks whether it matches the simple goal τ; informally it captures that ρ can beinstantiated to Σ ⇒ τ. Again, there are three rules for the three possible forms the rulecan take. Rule (FM-TA PP) handles universal quantification by instantiating the quantified
variable α in a way that recursively yields a match. Rule (FM-IA PP) handles a rule
type ρ1 ⇒ ρ2 by recursively checking whether ρ2 matches the goal. At the same time
it yields a new goal ρ1 which needs to be resolved in order for the rule to apply. Finally,rule (FM-S IMP) expresses the base case where the axiom is identical to the goal and there
are no new goals.
This type-directed formulation of entailment reduces the number of proofs for a given
goal. For instance, for the example above there is only one proof:(FR-S IMP )?α ; x ∈ Γ(FM-S IMP ) Γ; [α] ; x `fr ε; α ; xΓ `fr [α] ; x

3.5 Deterministic and Stable Resolution
While focusing provides a syntax-directed definition of resolution, it does not make resolution entirely deterministic. There are still two sources of nondeterminism: 1) the ambiguous
instantiation of type variable α with a monotype σ in rule (FM-TA PP), and 2) nondeterministic selection of an implicit ρ from the type environment Γ in rule (FR-S IMP). Thissection eradicates those two remaining sources of nondeterminism to obtain an entirely
deterministic formulation of resolution. On top of that, it imposes an additional stability
condition to make resolution “super”-deterministic: resolution is preserved under type
substitution. First, though, we point out that our choice for predicative instantiation has
pre-emptively avoided a further source of nondeterminism.

ZU064-05-FPR

Main

7 December 2018

10:26

23

Cochis: Stable and Coherent Implicits
3.5.1 Predicative Instantiation

We have restricted C OCHIS to predicative instantiation, i.e., type variables can only be
instantiated with monotypes σ . Impredicativity is a known source of nondeterminism inother settings like type inference for the polymorphic λ -calculus (Boehm, 1985; Pfenning,1993). It causes similar problems for C OCHIS, in the rules (AR-TA PP) and (FM-TA PP)
for ambiguous and focusing resolution that choose an instantiation of a type variable.
To see why the impredicative instantiation in those rules causes nondeterminism, consider two ways resolving Γ1 `ar Int ⇒ Int against the environment Γ1 =?(∀α.α ⇒ α):5
(AR-IVAR )(AR-TA PP )?(∀α.α ⇒ α) ∈ Γ1
Γ1 `ar ∀α.α ⇒ αΓ1 `ar Int ⇒ Int

and(AR-IVAR )(AR-TA PP )?(∀α.α ⇒ α) ∈ Γ1
Γ1 `ar ∀α.α ⇒ α(AR-IVAR )Γ1 `ar (∀β .β ⇒ β ) ⇒ (∀β .β ⇒ β )(AR-IA PP )
Γ1 `ar ∀β .β ⇒ β(AR-TA PP )
Γ1 `ar Int ⇒ Int?(∀β .β ⇒ β ) ∈ Γ1
Γ1 `ar ∀β .β ⇒ βThe first proof only involves the instantiation of α with Int. Yet, the second proof contains
an impredicative instantiation of α with ∀β .β ⇒ β .
We have adopted the standard solution from the outset, which only allows predicative
instantiation and thus only accepts the first of the two derivations above.
Observe that we not only forbid instantiation with universally quantified types ∀α.ρ,but also with rule types ρ1 ⇒ ρ2 . The latter are also a source of ambiguity. Consider for
instance resolving Int in the environment Γ2 =?(∀α.(α → α) ⇒ α), ?Bool, ?((Bool ⇒Int) → (Bool → Int)), ?(Int → Int). There is one derivation that involves instantiating thefirst entry’s α with a monotype, namely with Int:
(AR-IVAR )(AR-TA PP )(AR-IA PP )?(∀α.(α → α) ⇒ α) ∈ Γ2
Γ2 `ar ∀α.(α → α) ⇒ α
Γ2 `ar (Int → Int) ⇒ Int(AR-IVAR )?(Int → Int) ∈ Γ2
Γ2 `ar Int → IntΓ2 `ar Int

However, instantiation with the non-monotype Bool ⇒ Int also yields a derivation; for thesake of conciseness, we have abbreviated Bool and Int to B and I respectively.

5

For the sake of compactness the example uses the ambiguous definition of resolution. Similarly
problematic examples can be created for the focusing-based definition.

ZU064-05-FPR

Main

7 December 2018

24

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian(AR-IVAR )(AR-TA PP )?(∀α.(α→α)⇒α)∈Γ2(AR-IVAR )Γ2 `ar ∀α.(α→α)⇒α?((B⇒I)→(B⇒I))∈Γ2(AR-IVAR )Γ2 `ar (B⇒I)→(B⇒I)?B∈Γ2Γ2 `ar ((B⇒I)→(B⇒I))⇒(B⇒I)(AR-IA PP )
Γ2 `ar B⇒I(AR-IA PP )

Γ2 `ar BΓ2 `ar I

By restricting ourselves to instantiation with monotypes, we disallow the second derivationand thus avoid this source of ambiguity.
3.5.2 Non-Ambiguity Constraints
Rule (FM-TA PP) does not explain how the predicative substitution [σ /α] for the type∀α.ρ should be obtained. At first sight it seems that the choice of σ is free and thus a sourceof nondeterminism. However, in many cases the choice is not free at all, but is instead determined fully by the simple type τ that we want to match. However, the choice is not always
forced by the matching. Take for instance the context type ∀α.(α → String) ⇒ (String →α) ⇒ (String → String). This type encodes the Haskell type ∀α.(Show α, Read α) ⇒String → String of the ambiguous expression read ◦ show discussed in Section 2.2. The
choice of α is ambiguous when matching against the simple type String → String. Yet, thechoice is critical for two reasons. Firstly, if we guess the wrong instantiation σ for α, thenit may not be possible to recursively resolve (String → α)[σ /α] or (α → String)[σ /α],while with a lucky guess both can be resolved. Secondly, for different choices of σ ,(String → α)[σ /α] and (α → String)[σ /α] can be resolved in completely 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 (T Y-IA BS) of Figure 2.6
This judgment is defined in Figure 5 in terms of the auxiliary judgment ᾱ `unamb ρ whichtakes an additional sequence of type variables α that is initially empty.
This auxiliary judgment expresses that all type variables ᾱ are resolved when matching
against ρ. Its base case, rule (UA-S IMP), expresses that fixing the simple type τ fixes its
free type variables ᾱ. The inductive rule (UA-TA BS) accumulates the bound type variablesᾱ before the head. Rule (UA-IA BS) skips over any contexts on the way to the head, but also
recursively requires that these contexts are unambiguous. The latter is necessary because
rule (FR-S IMP) resolves those contexts recursively when ρ matches the resolvent; asrecursive resolvents they add their contexts to the implicit environment in rule (FR-IA BS).
Finally, the unambiguity condition is imposed on the queried type ρ in rule (T Y-Q UERY)
because this type too may extend the implicit environment in rule (FR-IA BS).
Note that the definition rules out harmless ambiguity, such as that in the type ∀α.Int.
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. Here the6

A more permissive design would allow quantified type variables that are not mentioned anywhere,
such as α in ∀α.Int ⇒ Int, and instantiate them to a dummy type, like GHC’s GHC.Prim.Any,
which is only used for this purpose. As such unused type variables serve little purpose, we have
opted not to make an exception for them.

ZU064-05-FPR

Main

7 December 2018

10:26

25

Cochis: Stable and Coherent Implicits`unamb ρ(UA-S IMP )ᾱ `unamb ρ(UA-TA BS )ε `unamb ρ(UA-M AIN )`unamb ρ

ᾱ, α `unamb ρ(UA-IA BS )ᾱ `unamb ∀α.ρᾱ ⊆ ftv(τ)ᾱ `unamb τ`unamb ρ1ᾱ `unamb ρ2ᾱ `unamb ρ1 ⇒ ρ2

Fig. 5. Unambiguous Context Types
ambiguity is harmless, because it does not affect the semantics. Yet, to keep the meta-theory
simple, we have opted to not differentiate between harmless and harmful ambiguity.
3.5.3 Committed Choice
The other remaining source of nondeterminism is the nondeterministic choice ?ρ ∈ Γthat appears in rule (FR-S IMP) of the focusing judgment. Consider the trivial example
of resolving the goal Int against the environment Γ =?Int ; x, ?Int ; y. Both implicits inthe environment match the goal and yield different, i.e., incoherent, elaborations.
Our solution is to replace the nondeterministic relation ?ρ ∈ Γ by a deterministic one that
selects the first matching implicit in the environment and commits to it. In fact, we encapsulate all three hypotheses of rule (FR-S IMP) in a new lookup judgment Γ; [Γ0 ] `r τ ; E
which resolves τ with the first matching implicit in the environment Γ0 and performs any
recursive resolutions against the environment Γ. Of course, the modified rule (FR-S IMP ’)
invokes this lookup judgment with two copies of the same environment, i.e., Γ and Γ0 are
identical.
Γ; [Γ] `r τ ; E(FR-S IMP ’)Γ `fr [τ] ; E
The (still preliminary) definition of the judgment itself is syntax-directed with respect tothe type environment Γ0 :Γ; [Γ0 ] `r τ ; E(DL-M ATCH )Γ; [ρ] ; x `fr ρ 0 ; x; τ ; EΓ `fr [ρ 0 ] ; E 0(∀ρ 0 ∈ ρ 0 )Γ; [Γ0 , ?ρ ; x] `r τ ; E[Ē 0 /x̄]

(DL-N O M ATCH )(DL-VAR )Lookup

6 ∃E, Σ : Γ; [ρ] ; x `fr Σ; τ ; E

Γ; [Γ0 ] `r τ ; E

Γ; [Γ0 ] `r τ ; E 0

Γ; [Γ0 , ?ρ ; x] `r τ ; E 0

Γ; [Γ0 , x : ρ] `r τ ; E(DL-T Y VAR )Γ; [Γ0 ] `r τ ; E

Γ; [Γ0 , α] `r τ ; E

ZU064-05-FPR

Main

26

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Rule (DL-M ATCH) concerns the case where the first entry in the environment matches
the goal. Its behavior is the same as in the original definition of rule (FR-S IMP).
Rule (DL-N O M ATCH) is mutually exclusive with the above rule: it skips the first entry
in the environment only iff it does not match to look for a matching implicit deeper in theenvironment. This implements the committed choice semantics: the first matching implicit
is committed to and further implicits are not considered.
Finally, rules (DL-VAR) and (DL-T Y VAR) skip the irrelevant non-implicit entries in thetype environment.
It is not difficult to see that with the above definition there is only one way to resolve thegoal Int against the environment Γ =?Int ; x, ?Int ; y. The first matching entry, which
elaborates to y, is committed to and the second entry is not considered.
3.5.4 Stability
While the above committed-choice formulation of resolution is deterministic, it is a rather
fragile, or unstable, notion of resolution. Consider for example resolving the goal Int
against the environment Γ =?Int ; x, α, ?α ; y. This scenario arises for instance whentype checking the expression e = λ? Int.(Λα.λ? α.?Int) Int. Our definition of resolution
skips the first entry in the environment because α does not match Int, commits to thesecond entry because Int trivially matches Int, and elaborates to x.
However, this resolution is not stable. Consider what happens when we apply a seemingly innocuous refactoring to the expression e by β -reducing the type application. This
yields the new, and supposedly equivalent, expression e0 = λ? Int.λ? Int.?Int. The direct
impact of this refactoring on the resolution problem is to substitute Int for the type variable
α. As a consequence the resolution commits now to the first entry and elaborates toy instead of x. Hence, more generally, the above definition of resolution is not stable
under type substitution. This is problematic because it defies the common expectation that
simple refactorings like the reduction of type application above do not change a program’s
behavior.
To avoid this problem and obtain stability under type substitution, we tighten the requirement of rule (DL-N O M ATCH): an implicit in the environment can only be skipped
iff it does not match under any possible substitution of type variables. With this tightened
requirement the scenario above simply does not resolve: unstable resolutions are invalid.
(DL-N O M ATCH ’)

stable(Γ; ρ ; x; τ)

Γ; [Γ0 ] `r τ ; E 0

Γ; [Γ0 , ?ρ ; x] `r τ ; E 0

where a first stab at a formalisation of the stability condition is:stable(Γ; ρ ; x; τ)(S TABLE ’)

6 ∃θ , E , Σ : θ (Γ); [θ (ρ)] ; x `r Σ; θ (τ) ; E
stable(Γ; ρ ; x; τ)The above formulation of the condition is a bit too lax; we have to be more precise about
the domain and range of the substitution θ . Indeed, substitution does not make sense forZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

27

every type variable in the environment. Consider for example resolving the type ∀β .β → βagainst the environment Γ0 =?(∀γ.γ → γ) ; x, α, ?(α → α) ; y. We would like thisresolution of ∀β .β → β to succeed against ?(∀γ.γ → γ).
Unfortunately, the above formulation of stability unnecessarily throws a spanner inthe works. Consider what happens: Using Rule (FR-TA BS), we would recursively resolve β → β against the extended environment Γ1 = Γ0 , β . Next we get stuck as neither
rule (DL-M ATCH) nor rule (DL-N O M ATCH ’) applies. The former does not apply because
α → α does not match β → β . Also the latter does not apply because there are two
substitutions such that θ (α → α) matches θ (β → β ) and hence skipping α → α is deemed
unstable.
However, if we look more closely at these substitutions, we see that none of them makesense. Essentially, there are two groups of substitutions:• Those substitutions that instantiate β , of which θ = [α/β ] is a prominent example.
These substitutions do not make sense because code inlining cannot result in β being
instantiated to α or to any other type, because β is not in scope at the point in thecode where the query happens (i.e., β does not appear in Γ0 ). Hence, considering
substitutions of β does not make sense.
Figure 7, which puts all the measures together to obtain a type-directed, deterministic and stable resolution, addresses the issue as follows. It introduces a top-level
main judgment Γ `r ρ ; E to handle a query that delegates to the focusing-based
judgments we have described above. The only contribution of the main judgment,
which is defined by the single rule (R-M AIN), is to gather the type variables ᾱthat appear in the environment at the point of the query by means of the function
tyvars(Γ), and to pass them on through the auxiliary judgments to the point where
the stability check is performed. Hence, the auxiliary judgments ᾱ; Γ `r [ρ] ; E(focusing), ᾱ; Γ; [Γ0 ] `r τ ; E (lookup) and stable(ᾱ; Γ; ρ ; x; τ) now all feature
an additional argument ᾱ of type variables that can be substituted.
• The substitution θ 0 = [β /α] also generates a match. However, this substitution does
not make sense either because code inlining can only result in substitutions of α bytypes that are well-scoped in the prefix of the environment before α. In the caseof the example this means that we can only consider substitutions [σ /α] where?(∀γ.γ → γ) ; x ` σ . In other words, σ cannot have any free type variables. Thereis no such σ that matches β .
In summary, Figure 6 formalises our notion of valid substitutions with the judgment
ᾱ; Γ ` θ . Rule (S-E MPTY) covers the base case and states that the empty substitution
ε is trivially valid. Rule (S-C ONS) covers the inductive case [σ /α] · θ . It says that thesingle variable substitution [σ /α] is valid if α appears in the sequence of substitutable
type variables, expressed by the structural pattern ᾱ, α, ᾱ 0 . Moreover, α must appear in thetype environment, expressed by a similar structural pattern Γ, α, Γ0 . Lastly, the type σ must
be well-scoped with respect to the environment prefix Γ. In addition, the remainder θ must
be valid with respect to the remaining type variables ᾱ, ᾱ 0 and the type environment after
substitution of α.

ZU064-05-FPR

Main

28

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosianθ ::= ε | [σ /α] · θᾱ; Γ ` θ
(S-E MPTY ) ᾱ; Γ ` ε(S-C ONS )Γ`σᾱ, ᾱ 0 ; Γ, θ (Γ0 ) ` θᾱ, α, ᾱ 0 ; Γ, α, Γ0 ` [σ /α] · θ

Fig. 6. Valid Substitutions

3.5.5 Summary
Figure 7 puts all the above measures together in our unambiguous, deterministic and stabledefinition of resolution.
The main judgment Γ `r ρ ; E resolves the query ρ against the type environment Γ. It
is defined by a single rule, (R-M AIN), which delegates the task to the auxiliary focusing
judgment ᾱ; Γ `r [ρ] ; E .
The focusing judgment has one more index than the main judgment, namely the typevariables ᾱ that are recorded in the type environment, which are retrieved by the function
tyvars(Γ) in rule (R-M AIN). Three rules define the focusing judgment. The first two,
(R-IA BS) and (R-TA BS), strip the query type ρ until only a simple type τ remains,which is handled by rule (R-S IMP). Rule (R-IA BS) strips the context ρ1 from a rule type
ρ1 ⇒ ρ2 , adds it to the type environment as a new implicit and then recursively processes
the head ρ1 . Rule (R-TA BS) strips the quantifier from a universally quantified type ∀α.ρand adds the type variable α to the type environment in which ρ is processed. Finally,rule (R-S IMP) delegates the job of processing the simple type τ to the auxiliary lookup
judgment ᾱ; Γ; [Γ0 ] `r τ ; E .
The lookup judgment takes an additional index, the type environment Γ0 , which is
initialised to Γ in rule (R-S IMP). It pops entries from Γ0 until it finds an implicit thatmatches the simple query type τ. Rule (L-M ATCH) first uses the auxiliary matching judgment Γ; [ρ] ; x `r ρ 0 ; x; τ ; E to establish that implicit ρ at the top of Γ0 matches thequery type τ and to receive new queries ρ 0 , which it resolves recursively against the typeenvironment Γ. Rule (L-N O M ATCH) skips the implicit at the top of the environment when
it is stable to do so according to the auxiliary stability judgment stable(ᾱ; Γ; ρ ; x; τ).
Rules (L-VAR) and (L-T Y VAR) skip term and type variable entries.
Three rules define the matching judgment. In the first one, (M-S IMP), the implicit isa simple type τ that is identical to query type; there are no remaining queries. When theimplicit is a rule type ρ1 ⇒ ρ2 , rule (M-IA PP) defers querying ρ1 and first checks whether
ρ2 matches the query τ. When the implicit is a universally quantified type ∀α.ρ, rule
(M-TA PP) instantiates it appropriately to match the query τ.
Finally, the stability judgment is defined by a single rule, (S TABLE), which makes surethat there is no substitution θ of the type variables ᾱ for which θ (ρ) matches θ (τ).

ZU064-05-FPR

Main

7 December 2018

10:26

29

Cochis: Stable and Coherent Implicits

Σ ::= ε | ρ ; x , ΣΓ `r ρ ; E(R-M AIN )tyvars(ε)
tyvars(Γ, x : ρ)

=
=

Main

tyvars(Γ); Γ `r [ρ] ; EΓ `r ρ ; E

tyvars(Γ, α)tyvars(Γ, ?ρ ; x )εtyvars(Γ)==

tyvars(Γ), αtyvars(Γ)ᾱ; Γ `r [ρ] ; E(R-IA BS )ᾱ; Γ, ?ρ1 ; x `r [ρ2 ] ; E

Focusing

x fresh(R-TA BS )ᾱ; Γ `r [ρ1 ⇒ ρ2 ] ; λ x : |ρ1 |.E(R-S IMP )ᾱ; Γ, α `r [ρ] ; E

ᾱ; Γ `r [∀α.ρ] ; Λα.E

ᾱ; Γ; [Γ] `r τ ; E
ᾱ; Γ `r [τ] ; E

ᾱ; Γ; [Γ0 ] `r τ ; E(L-M ATCH )ᾱ; Γ `r [ρ 0 ] ; E 0

Γ; [ρ] ; x `r ρ 0 ; x ; τ ; E(∀ρ 0 ∈ ρ 0 )ᾱ; Γ; [Γ0 , ?ρ ; x ] `r τ ; E[Ē 0 /x̄]

(L-N O M ATCH )(L-VAR )Lookupstable(ᾱ; Γ; ρ ; x ; τ)ᾱ; Γ; [Γ0 ] `r τ ; E

ᾱ; Γ; [Γ0 ] `r τ ; E 0ᾱ; Γ; [Γ0 , ?ρ ; x ] `r τ ; E 0ᾱ; Γ; [Γ0 , x : ρ] `r τ ; E(L-T Y VAR )ᾱ; Γ; [Γ0 ] `r τ ; E

ᾱ; Γ; [Γ0 , α] `r τ ; E

Γ; [ρ] ; E `r Σ; τ ; E 0

Matching(M-S IMP ) Γ; [τ] ; E `r ε; τ ; E(M-IA PP )Γ, ?ρ1 ; x ; [ρ2 ] ; E x `r Σ; τ ; E 0(M-TA PP )x freshΓ; [ρ1 ⇒ ρ2 ] ; E `r ρ1 ; x , Σ; τ ; E 0

Γ; [ρ[σ /α]] ; E |σ | `r Σ; τ ; E 0

Γ; [∀α.ρ] ; E `r Σ; τ ; EΓ`σ0stable(ᾱ; Γ; ρ ; x; τ)(S TABLE )6 ∃θ , E, Σ : ᾱ; Γ ` θ

θ (Γ); [θ (ρ)] ; x `r Σ; θ (τ) ; E

stable(ᾱ; Γ; ρ ; x ; τ)Fig. 7. Deterministic Resolution and Translation to System F

Stability

ZU064-05-FPR

Main

30

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian
4 Resolution Algorithm

This section presents an algorithm that implements the deterministic resolution rules of
Figure 7. It differs from the latter in two important ways: firstly, it computes rather thanguesses type substitutions in rule (M-TA PP); and secondly, it replaces explicit quantification over all substitutions θ in rule (S TABLE) with a tractable approach to stability
checking.
The definition of the algorithm, in Figure 8, is structured in the same way as the declarative specification: with one main judgment and three auxiliary ones that have similar roles(focusing, lookup, and matching). In fact, since the differences are not situated in the mainand focusing judgment, these are actually identical.
4.1 Deferred Variable Instantiation
The first difference is situated in the matching judgment ᾱ; Γ; [ρ] ; E ; Σ `alg Σ0 ; τ ; E 0 .
While its declarative counterpart immediately instantiates the quantified type variable inrule (M-TA PP), this algorithmic formulation defers the instantiation to the point wherea deterministic choice can be made. As long as the type variables ᾱ have not been instantiated, the judgment keeps track of them in its first argument. The actual instantiation
happens in the base case, rule (A LG -M-S IMP). This last rule performs the deferred instantiation of type variables ᾱ by computing the most general unifier θ = unifyΓ;ᾱ (τ 0 , τ). The
unification algorithm, which we present below, computes a substitution θ that is valid (i.e.,ᾱ; Γ ` θ ) and that equates the two types (i.e., θ (τ) = θ (τ 0 )).
In order to subject the recursive goals to this substitution, the algorithmic judgment
makes use of an accumulating parameter Σ. This accumulator Σ represents all the goals
collected so far in which type variables have not been substituted yet. In contrast, Σ0 denotes
all obligations with type variables already substituted.
Finally, observe that rule (A LG -L-M ATCH) invokes the algorithmic judgment with anempty set of not-yet-instantiated type variables and an empty accumulator Σ.
The following example illustrates the differences between the declarative judgment:
Γ; [Int] ; x Int y `r ε; Int ; x Int y (M-S IMP )Γ; [Int ⇒ Int] ; x Int `r Int ; y; Int ; x Int yΓ; [∀α.α ⇒ α] ; x `r Int ; y; Int ; x Int y(M-IA PP )(M-TA PP )and its algorithmic counterpart:[Int/α] = unifyΓ;α (α, Int)α; Γ; [α] ; x α y; α ; y `alg ε; Int ; x Int y(A LG -M-S IMP )α; Γ; [α ⇒ α] ; x α ; ε `alg Int ; y; Int ; x Int yε; Γ; [∀α.α ⇒ α] ; x; ε `alg Int ; y; Int ; x Int y(A LG -M-IA PP )(A LG -M-TA PP )4.2 Algorithmic Stability Check
The second difference can be found in (A LG -L-N O M ATCH) of the lookup judgment.
Instead of using the stable(ᾱ; Γ; ρ ; x; τ) judgment, which quantifies over all valid sub-

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

31

stitutions, this rule uses the algorithmic judgment ᾱ; Γ; ρ `sta τ. This auxiliary judgment
checks algorithmically whether the type ρ matches τ under any possible instantiation of
the type variables ᾱ. We apply the same deferred-instantiation technique as with the firstdifference: Instead, of applying a substitution first and then checking whether the implicit
matches the goal, we defer the instantiation to the end where we can deterministically pick
one instantiation instead of considering all valid instantiations.
As a consequence of the similarity, in purpose and strategy, between the algorithmic
stability, ᾱ; Γ; ρ `sta τ, and the matching judgment, ᾱ; Γ; [ρ] ; E ; Σ `alg Σ0 ; τ ; E 0 , theformer is a variation of the latter, with two differences. Firstly, since the stability judgment is only concerned with matchability, no recursive resolvents Σ are collected nor
are any elaborations tracked. Secondly, since the stability check considers the substitution of the type variables ᾱ that occur in the environment at the point of the query, rule
(A LG -L-N O M ATCH) pre-populates the substitutable variables of the `sta judgment withthem. Contrast this with the matching judgment where only the implicit’s quantified variables are instantiated, as witnessed by rules (A LG -M-TA PP) and (A LG -M-S IMP).

4.3 Scope-Aware Unification
The unification algorithm θ = unifyΓ;ᾱ (ρ1 , ρ2 ) is a key component of the two algorithmicchanges explained above.
Figure 9 provides its definition, which is a hybrid between standard first-order unification (Martelli & Montanari, 1982) and polymorphic type instantiation (Dunfield & Krishnaswami, 2013) that is a restricted form of Miller’s mixed-prefix unification (Miller, 1992).
The domain restriction ᾱ denotes which type variables are to be treated as unification
variables; all other type variables are to be treated as constants. The returned substitution
is a unifier of ρ1 and ρ2 , i.e., θ (ρ1 ) = θ (ρ2 ).
Validity The differences with standard first-order unification arise because, like polymorphic type instantiation, the algorithm has to account for the scope of type variables.
Indeed, as we have already explained in Section 3.5, we expect that the returned substitution is valid, i.e., ᾱ; Γ ` θ . For instance, using standard first-order unification forunifyΓ;β (∀α.α → β , ∀α.α → α) would yield the invalid substitution [β /α]. The substitution is invalid because α is not in scope in Γ.
Most General Unifier Secondly, traditional unification computes the most general unifier,i.e., any other unifier can be expressed as its composition with another substitution. Yet,the most general unifier may not be a valid substitution, while more specific unifiers may
be valid. Consider for instance unifying α with β → β where Γ = α, β and both α and β
are unification variables. The most general unifier is [β → β /α]. However this unifier is
not valid, as α appears before β in the environment. In contrast, there are infinitely many
more specific unifiers that are valid, all of the form [ρ → ρ/α, ρ/β ] where ρ is a closed
type.
Fortunately, by a stroke of luck, the above is not a problem for either of our two use
cases:

ZU064-05-FPR

Main

32

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian• The first use case is that in rule (A LG -M-S IMP) where this is not a problem because
the scenario never arises. In unifyΓ;ᾱ (τ 0 , τ) only τ 0 contains unification variables
and hence the range of the substitution never contains any unification variables. As
a consequence the above example and others like it cannot occur.
• The second use case, in rule (S TA -S IMP), is only interested in the existence of a valid
substitution. We neither care which one it is nor whether it is the most general one.
Moreover, as illustrated above, whenever there is a most general substitution that isinvalid due to the relative position of unification variables in the environment, we
can always construct a more specific valid substitution by substituting the remaining
unification variables by closed types.

Definition With the above issues in mind we can consider the actual definition in Figure 8. The main unification judgment θ = unifyΓ;ᾱ (ρ1 , ρ2 ) is defined by rule (U-M AIN).
This rule computes the unifier in terms of the auxiliary judgment θ = unify0 ᾱ (ρ1 , ρ2 ),which is essentially standard unification, and then checks the above validity concerns.
Indeed, for any type variable β that appears in the image of a type variable α, either
β must appear before α in the environment Γ (regular validity), or β must itself be aunification variable (the exceptional case). The relative position of variables is checkedwith the auxiliary judgment β >Γ α whose one rule verifies that β appears before α inthe environment Γ;7 a similar check on relative positions can be found in Dunfield andKrishnaswami’s algorithm (Dunfield & Krishnaswami, 2013).
The auxiliary judgment unify0 ᾱ (ρ1 , ρ2 ) computes the actual unifier. Rule (U-VAR) is
the standard reflexivity rule for type variables. Rules (U-I NST L) and (U-I NST R) are twosymmetric base cases; they only create a substitution [σ /α] if α is one of the unification
variables and if α does not occur in σ , which is the well-known occurs-check. Rules(U-F UN), (U-RUL) and (U-U NIV) are standard congruence rules that combine the unification problems derived for their subterms.

4.4 Termination of Resolution
If we are not careful about which implicits are added to the environment, then the resolution
process may not terminate. This section describes how to impose a set of modular syntactic
restrictions that prevents non-termination. As an example of non-termination consider?(Char ⇒ Int), ?(Int ⇒ Char) `ar Int
which loops, using alternatively the first and second implicit in the environment. The sourceof this non-termination is the recursive nature of resolution: a simple type can be resolvedin terms of an implicit type whose head it matches, but this requires further resolution of
the implicit type’s context.
The problem of non-termination has been widely studied in the context of Haskell’s typeclasses, and a set of modular syntactic restrictions has been imposed on type class instances

7

If type variables are represented by de Bruijn indices, this can be done by checking whether one
index is greater than the other.

ZU064-05-FPR

Main

7 December 2018

10:26

33

Cochis: Stable and Coherent Implicits

Γ `alg ρ ; E

Main

tyvars(Γ); Γ `alg ρ ; E(A LG -R-M AIN )Γ `alg ρ ; E

ᾱ; Γ `alg ρ ; E(A LG -R-IA BS )Focusing

ᾱ; Γ, ?ρ1 ; x `alg ρ2 ; E

x freshᾱ; Γ `alg ρ1 ⇒ ρ2 ; λ (x : |ρ1 |).E

(A LG -R-TA BS )ᾱ; Γ, α `alg ρ ; E

ᾱ; Γ `alg ∀α.ρ ; Λα.E

(A LG -R-S IMP )ᾱ; Γ; [Γ] `alg τ ; E
ᾱ; Γ `alg τ ; E

ᾱ; Γ; [Γ0 ] `alg τ ; E(A LG -L-M ATCH )ε; Γ; [ρ] ; x ; ε `alg ρ̄ 0 ; x̄0 ; τ ; E

ᾱ; Γ `alg ρ 0 ; E 0 (∀ρ 0 ∈ ρ̄ 0 )ᾱ; Γ; [Γ0 , ?ρ ; x ] `alg τ ; E[Ē 0 /x̄0 ](A LG -L-N O M ATCH )(A LG -L-VAR )Lookupᾱ; Γ; [Γ0 ] `alg τ ; E 0ᾱ; Γ; ρ 6`sta τ

ᾱ; Γ; [Γ0 , ?ρ ; x ] `alg τ ; E 0ᾱ; Γ; [Γ0 ] `alg τ ; E
0ᾱ; Γ; [Γ , x : ρ] `alg τ ; E(A LG -L-T Y VAR )ᾱ; Γ; [Γ0 ] `alg τ ; E

ᾱ; Γ; [Γ0 , α] `alg τ ; E

ᾱ; Γ; [ρ] ; E ; Σ `alg Σ0 ; τ ; E 0

Matching

θ = unifyΓ;ᾱ (τ, τ 0 )(A LG -M-S IMP )0ᾱ; Γ; [τ ] ; E ; Σ `alg θ (Σ); τ ; |θ |(E)(A LG -M-IA PP )ᾱ; Γ, ?ρ1 ; x ; [ρ2 ] ; E x ; Σ, ρ1 ; x `alg Σ0 ; τ ; E 0

x freshᾱ; Γ; [ρ1 ⇒ ρ2 ] ; E ; Σ `alg Σ0 ; τ ; E 0(A LG -M-TA PP )ᾱ, α; Γ, α; [ρ] ; E α ; Σ `alg Σ0 ; τ ; E 0ᾱ; Γ; [∀α.ρ] ; E ; Σ `alg Σ0 ; τ ; E 0ᾱ; Γ; ρ `sta τ(S TA -TA PP )ᾱ, α; Γ, α; ρ `sta τ
ᾱ; Γ; ∀α.ρ `sta τ(S TA -S IMP )Fig. 8. Resolution Algorithm(S TA -IA PP )Stabilityᾱ; Γ; ρ2 `sta τ
ᾱ; Γ; ρ1 ⇒ ρ2 `sta τθ = unifyΓ;ᾱ (τ, τ 0 )ᾱ; Γ; τ 0 `sta τZU064-05-FPR

Main

7 December 2018

34

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosianθ = unifyΓ;ᾱ (ρ1 , ρ2 )(U-M AIN )θ = unify0 ᾱ (ρ1 , ρ2 )β ∈ ᾱ ∨ β >Γ α(∀[σ /α] ∈ θ , ∀β ∈ ftv(σ ))θ = unifyΓ;ᾱ (ρ1 , ρ2 )

θ = unify0 ᾱ (ρ1 , ρ2 )(U-VAR )(U-I NST L)

ε = unify0 ᾱ (β , β )α ∈ ᾱ
α 6∈ ftv(σ )α ∈ ᾱ

(U-I NST R)[σ /α] = unify0 ᾱ (α, σ )(U-F UN )(U-RUL )θ1 = unify0 ᾱ (ρ11 , ρ21 )α 6∈ ftv(σ )[σ /α] = unify0 ᾱ (σ , α)

θ2 = unify0 ᾱ (θ1 (ρ12 ), θ1 (ρ22 ))0θ2 · θ1 = unify ᾱ (ρ11 → ρ12 , ρ21 → ρ22 )θ1 = unify0 ᾱ (ρ11 , ρ21 )θ2 = unify0 ᾱ (θ1 (ρ12 ), θ1 (ρ22 ))0θ2 · θ1 = unify ᾱ (ρ11 ⇒ ρ12 , ρ21 ⇒ ρ22 )θ = unify0 ᾱ (ρ1 , ρ2 )(U-U NIV )θ = unify0 ᾱ (∀β .ρ1 , ∀β .ρ2 )β >Γ αβ >Γ1 ,β ,Γ2 ,α,Γ3 αFig. 9. Unification Algorithm
to avoid non-termination (Sulzmann et al., 2007). This paper adapts those restrictions tothe setting of C OCHIS.
Overall Approach We show termination by characterising the resolution process as a(resolution) tree with goals in the nodes. The initial goal sits at the root of the tree. A
multi-edge from a parent node to its children represents a rule type from the environmentthat matches the parent nodes goal; the node’s children are the recursive goals.
Resolution terminates if the tree is finite. Hence, if it does not terminate, there is an
infinite path from the root in the tree, that denotes an infinite sequence of matching rule
type applications. To show that there cannot be such an infinite path, we use a norm k · k(defined at the bottom of Figure 10) that maps the head of every goal ρ to a natural number,its size. While types like Int and Bool are not formally part of our calculus, we assume that
their size is 1. Similarly, the size of type constructor applications like List ρ is 1 + kρk.
If we can show that this size strictly decreases from any parent goal to its children, then
we know that, because the order on the natural numbers is well-founded, on any path fromthe root there is eventually a goal that has no children.
Termination Condition It is trivial to show that the size strictly decreases, if we requirethat every implicit binding in the environment makes it so. This requirement is formalised
as the termination condition `term ρ in Figure 10. This condition should be imposed on

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

35

every type added to the environment, namely to ρ1 in rule (T Y-IA BS) of Figure 2 andto ρ1 in rule (R-IA BS) of Figure 7. However, because the latter concerns only a part ofa resolved type, we feel that it is easier to follow for the programmer if we impose thecondition instead on the whole resolved type in rule (T Y-Q UERY) of Figure 2.
The judgment is defined by case analysis on the type ρ. Rule (T-S IMP) states that simple
types trivially satisfy the condition. Next, rule (T-F ORALL) is the congruence rule foruniversally quantified types. Finally, rule (T-RULE) enforces the actual condition on rule
types ρ1 ⇒ ρ2 , which requires that the head τ1 of ρ1 is strictly smaller than the head τ2 ofρ2 .
To account for polymorphism and the fact that the type variables in rule types can be instantiated, rule (T-RULE) ensures that the kτ1 k < kτ2 k property is stable under substitution.
Declaratively, we can formulate this stability under substitution as:∀θ .dom(θ ) ⊆ ftv(τ1 ) ∪ ( f tv)(τ2 ) : kθ (τ1 )k < kθ (τ2 )kConsider for instance the type ∀a.(a → a) ⇒ (a → Int → Int). In this example, thehead’s size 5 is strictly greater than the context constraint’s size 3. Yet, if we instantiate
α to (Int → Int → Int), then the head’s size becomes 9 while the context constraint’s size
becomes 11.
The declarative formulation above is not suitable in an algorithm because it enumerates
all possible substitutions. Rule (T-RULE) uses instead an equivalent algorithmic formulation which states that, in addition to kτ1 k < kτ2 k, the number of occurrences of any free
type variable α may not be larger in τ1 than in τ2 . The first condition expresses that for
the empty substitution, the size strictly decreases, say from kτ2 k = n to kτ1 k = m. If weinstantiate a type variable α to a type σ of size k, then the sizes change to k[σ /α]τ1 k =m + k × occα (τ1 ) and k[σ /α]τ2 k = n + k × occα (τ2 ) where the auxiliary function occα (ρ)
determines the number of occurrences of α in ρ. The second condition guarantees that k ×
occα (τ1 ) 6 k × occα (τ2 ) and thus that the strict decrease is preserved under substitution.
In our example above, we do have that kα → αk = 3 < 5 = kα → Int → Intk, the second
condition is not satisfied, i.e., occα (α → α) = 2 66 1 = occα (α → Int → Int).
Finally, as the types have a recursive structure whereby their components are themselves added to the environment, rule (T-RULE) also enforces the termination condition
recursively on the components.
Discussion Above we have adapted termination conditions for Haskell’s type class resolution to C OCHIS. While our adapted conditions are sufficient for termination, they are
not necessary. In fact, they can be rather restrictive. For instance, 6`term Int ⇒ Bool because
kIntk <
6 kBoolk. Indeed, resolving Bool in the context Γ1 =?(Bool ⇒ Int), ?(Int ⇒ Bool) is
problematic. Yet, it is not in the context Γ2 =?(Int), ?(Int ⇒ Bool). The problem is that theconditions are not context sensitive. We leave exploring more permissive, context-sensitive
conditions to future work.
5 Type-Directed Translation to System F
In this section we explain the dynamic semantics of C OCHIS in terms of System F’s
dynamic semantics, by means of a type-directed translation. This translation turns implicit

ZU064-05-FPR

Main

7 December 2018

36

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian`term ρ(T-RULE )(T-F ORALL )(T-S IMP ) `term τ`term ρ1kτ1 k < kτ2 k`term ρ`term ∀α.ρ`term ρ2
τ1 = hd(ρ1 )τ2 = hd(ρ2 )∀α ∈ ftv(ρ1 ) ∪ ftv(ρ2 ) : occα (τ1 ) 6 occα (τ2 )`term ρ1 ⇒ ρ2

hd(τ)

=

occα (β )=occα (ρ1 → ρ2 )=1
(α = β )0(α 6= β )occα (ρ1 ) + occα (ρ2 )kαkkρ1 → ρ2 k==

1
1 + kρ1 k + kρ2 kτhd(∀α.ρ)=hd(ρ)

hd(ρ1 ⇒ ρ2 )=hd(ρ2 )

occα (∀β .ρ)=

occα (ρ) (α 6= β )occα (ρ1 ⇒ ρ2 )=occα (ρ1 ) + occα (ρ2 )k∀α.ρkkρ1 ⇒ ρ2 k

=
=

kρk
1 + kρ1 k + kρ2 kFig. 10. Termination Condition
contexts into explicit parameters and statically resolves all queries, much like Wadler
and Blott’s dictionary passing translation for type classes (Wadler & Blott, 1989). The
advantage of this approach is that we simultaneously provide a meaning to well-typed
C OCHIS programs and an effective implementation that resolves all queries statically.
The translation follows the type system presented in Section 3. The additional machinerythat is necessary (on top of the type system) corresponds to the grayed parts of Figures 2,
3 and 7.
5.1 Type-Directed Translation
Figure 2 presents the translation rules that convert C OCHIS expressions into System F
expressions. The gray parts of the figure extend the type system with the necessary information for the translation.
The syntax of System F is as follows:
Types
Expressions

T
E

::=
::=

α | T → T | ∀α.Tx | λ (x : T ).E | E E | Λα.E | E T

The gray extension to the syntax of type environments annotates every implicit’s typewith explicit System F evidence in the form of a term variable x.
Translation of Types The function | · | takes C OCHIS types ρ to System F types T:|α| = α|ρ1 → ρ2 | = |ρ1 | → |ρ2 ||∀α.ρ| = ∀α.|ρ||ρ1 ⇒ ρ2 | = |ρ1 | → |ρ2 |It reveals that implicit C OCHIS arrows are translated to explicit System F function arrows.
Translation of Terms The type-directed translation judgment, which extends the typing
judgment, is

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

37

Γ`e:ρ ;E

This judgment states that the translation of C OCHIS expression e with type ρ is System F
expression E, with respect to type environment Γ.
Variables, lambda abstractions and applications are translated straightforwardly. Perhaps
the only noteworthy rule is (T Y-IA BS). This rule associates the type ρ1 with the fresh
variable x in the type environment. This creates the necessary evidence that can be used byresolutions 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 (T Y-Q UERY) using the auxiliary resolution judgment `r :
Γ `r ρ ; E

which is shown, in deterministic form, in Figure 7. The translation builds a System F term
as evidence for the resolution.
The mechanism that builds evidence dualizes the process of peeling off abstractions anduniversal quantifiers: Rule (R-IA BS) wraps a lambda binder with a fresh variable x arounda System F expression E, which is generated from the resolution for the head of the rule(ρ2 ). Similarly, rule (R-TA BS) wraps a type lambda binder around the System F expression
resulting from the resolution of ρ.
For simple types τ rule (R-S IMP) delegates the work of building evidence, when amatching implicit ρ is found in the environment, to rule (L-M ATCH). The evidence consistsof two parts: E is the evidence of matching τ against ρ. This match contains placeholders x̄ for the contexts whose resolution is postponed by rule (M-IA PP). It falls to rule
(L-M ATCH) to perform these postponed resolutions, obtain their evidence Ē and fill in theplaceholders.
Meta-Theory The type-directed translation of C OCHIS to System F exhibits a number ofdesirable properties.
Theorem 5.1 (Type-Preserving Translation). Let e be a C OCHIS expression, ρ be a type,Γ a type environment and E a System F expression. If Γ ` e : ρ ; E , then |Γ| `F E : |ρ|.
Here we define the translation of the type environment from C OCHIS to System F as:|ε| = ε|Γ, x : ρ| = |Γ|, x : |ρ||Γ, α| = |Γ|, α|Γ, ?ρ ; x| = |Γ|, x : |ρ|An important lemma in the theorem’s proof is the type preservation of resolution.
Lemma 5.1 (Type-Preserving Resolution). Let Γ be a type environment, ρ be a type andE be a System F expression. If Γ `ar ρ ; E , then |Γ| `F E : |ρ|.

Section A.1 of the Appendix points to the mechanized proofs of Theorem 5.1 andLemma 5.1 stated above.
In addition, we can express three key properties of Figure 7’s definition of resolution interms of the generated evidence. Firstly, the deterministic version of resolution is a soundvariation on the original ambiguous resolution.

ZU064-05-FPR

Main

38

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Theorem 5.2 (Soundness). Figure 7’s deterministic definition of resolution is sound (butincomplete) with respect to Figure 3’s ambiguous definition.
∀Γ, ρ, E :Γ `r ρ ; E⇒Γ `ar ρ ; E

Section A.3 of the Appendix points to the mechanized proof of the above theorem. Asa corollary (by use of this result with Lemma 5.1), the deterministic resolution process isalso type-preserving. Secondly, the deterministic resolution is effectively deterministic:
Theorem 5.3 (Determinacy). Let Γ be a type environment, ρ be a type and E1 , E2 besystem F expressions. Assume that `unamb ρ and ∀?ρi ∈ Γ, `unamb ρi . ThenΓ `r ρ ; E1 ∧ Γ `r ρ ; E2⇒

E1 = E2

A full proof of Theorem 5.3 can be found in Section A.4 of the Appendix.
It follows immediately that deterministic resolution is also coherent, which for ourelaboration-based setting is formulated, following Biernacki and Polesiuk (2018), in termsof contextual equivalence (Morris, 1969).
Corollary 5.1 (Coherence). Let Γ be a type environment, ρ be a type and E1 , E2 be system
F expressions. Assume that `unamb ρ and ∀?ρi ∈ Γ, `unamb ρi . ThenΓ `r ρ ; E1 ∧ Γ `r ρ ; E2⇒

|Γ| `F E1 'ctx E2 : |ρ|Here, the well-studied (Chong, 2017) contextual equivalence judgment Γ `F E1 'ctx E2 : T
captures that E1 and E2 behave the same in any well-typed program context. We do not givethe formal definition here as it is not required to prove the corollary; we only need to knowthat it is an equivalence relation, and, more specifically, that it is reflexive, i.e., any welltyped System F term is contextually equivalent to itself.
Thirdly, on top of the immediate coherence of deterministic resolution, an additional
stability property holds.
Lemma 5.2 (Stability of Resolution). Resolution is stable under monotype substitution.
∀Γ, α, Γ0 , σ , ρ, E : Γ, α, Γ0 `r ρ ; E ∧ Γ ` σ ⇒ Γ, Γ0 [σ /α] `r ρ[σ /α] ; E[|σ |/α]This is a key lemma to establish that static reduction of type application preserves typing
and elaboration.
Lemma 5.3 (Stability of Typing under Type Application Reduction). Static reduction oftype application preserves typing.
∀Γ, α, σ , ρ, E : Γ ` (Λα.e) σ : ρ ; (Λα.E) |σ | ⇒ Γ ` e[σ /α] : ρ ; E[|σ |/α]This, together with another property of System F’s contextual equivalence:∀Γ, α, E, T, T 0 : Γ `F (Λα.E) T : T 0 ⇒ Γ `F (Λα.E) T 'ctx E[T /α] : T 0
allows us to conclude the correctness of static reduction of type application.
Theorem 5.4 (Correctness of Type Application Reduction). If a type application and its
reduced form elaborate to two System F terms, those terms are contextually equivalent.
∀Γ, α, e, σ , E1, E2 : Γ ` (Λα.e) σ : ρ ; E1 ∧ Γ ` e[σ /α] : ρ ; E2 ⇒ |Γ| `F E1 'ctx E2 : |ρ|The stability Lemmas 5.2 and 5.3 are proved in Section A.5 of the Appendix.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

39

5.2 Evidence Generation in the Algorithm
The evidence generation in Figure 8 is largely similar to that in the deterministic specification of resolution in Figure 7. With the evidence we can state the correctness of thealgorithm.
Theorem 5.5 (Partial Correctness). Let Γ be a type environment, ρ be a type and E be
a System F expression. Assume that `unamb ρ and also `unamb ρi for all ?ρi ∈ Γ. ThenΓ `r ρ ; E if and only if Γ `alg ρ ; E .
The proof is split in two parts, one for each “direction” of the theorem. Section A.7
proves soundness of the algorithm with respect to deterministic resolution, while Section A.8 proves partial completeness. The latter correctness property is partial because
it does not hold without the additional termination conditions for the queried type and thetype environment, Γ.
5.3 Dynamic Semantics
Finally, we define the dynamic semantics of C OCHIS as the composition of the typedirected translation and System F’s dynamic semantics. Following Siek’s notation (Siek& Lumsdaine, 2005), 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-by-value
reduction relation (see Chapter 23 of (Pierce, 2002)).
Now we can state the conventional type safety theorem for C OCHIS:
Theorem 5.6 (Type Safety). If ε ` e : ρ, then eval(e) = V for some System F value V .
The proof follows from Theorem 5.1 and System F’s well-known normalization property.
6 Discussion
In this section we discuss and justify several of the design decisions made during thecreation of C OCHIS. Mostly, these choices are motivated by the design of Haskell typeclasses or Scala implicits.
6.1 Predicative Instantiation
System F is an impredicative calculus, allowing the instantiation of type variables with
arbitrary (polymorphic) types. In contrast C OCHIS is predicative: instantiation of typevariables only allows monotypes. Our reasons for departing from System F are threefold:• Impredicative instantiation in resolution leads to additional ambiguity. As discussed in Section 3, impredicative instantiations of type variables during resolution
can lead to ambiguity. The restriction to predicative instantiation removes this ambiguity, and we see no way that preserves impredicativity to achieve the same.

ZU064-05-FPR

Main

40

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian• Impredicativity is complex for implicit instantiation. While System F (where
all type instantiations are explicit) is simple, matters become much more complicated when some implicit instantiation is allowed. Indeed, the design of System
F-like calculi with implicit instantiation and/or some form of type-inference (Odersky & Läufer, 1996; Jones et al., 2007; Le Botlan & Rémy, 2003; Leijen, 2008;
Vytiniotis et al., 2008) is much more divided in terms of design choices regarding(im)predicativity. Notably, Rouvoet (2016) has shown that the ambiguous resolution
from the implicit calculus (Oliveira et al., 2012), which is the impredicative variantof our Figure 3, is undecidable. His proof proceeds by showing that the problem
is equivalent to the System F type inhabitation problem, which is known to be
undecidable (Barendregt et al., 2013).
• Predicative instantiation is not a big restriction in practice. Due to the above
complications brought by impredicativity, many practical languages with type-inference
only allow predicative instantiation. For example, the key algorithm for type-inference
currently employed by the GHC Haskell compiler is predicative (Jones et al., 2007;
Vytiniotis et al., 2011). Worth noting is that the original Hindley-Milner (HM) typesystem (Hindley, 1969; Milner, 1978) is where the predicativity restriction on polymorphic type systems with type-inference was first put into place. Since C OCHIS isintended as a target for languages with implicit polymorphism and type-inference,
which have predicativity restrictions, restricting the core language to allow only
predicative instantiation does not pose any problems.

Alternative Design Choices One alternative design choice worth mentioning for C OCHIS
would be to allow impredicative instantiation in explicit type applications, but still retain
the predicativity restriction during resolution. This design would be less restrictive than thedesign of C OCHIS, and we believe that it is a reasonable design. We decided against it for
two reasons. Firstly, as already mentioned, C OCHIS is aimed to be a target for source
languages with type-inference. As these source languages have predicative restrictions
anyway, there is little to be gained from having impredicative instantiation in the core.
Secondly, and more importantly, some of the meta-theory would be more involved if impredicative instantiation on type applications were allowed. In particular, Lemmas 5.2, 5.3
and 5.4 would need to be generalized to allow any types to be used in the substitution, rather
than just monotypes. This could be problematic since the impredicative instantiations of
the type variables could bring back the ambiguity issues discussed in Section 3. We expectthat additional restrictions would be needed at type applications to prevent instantiations
with problematic polymorphic types that would lead to ambiguity.
Allowing full impredicativity (both in type applications and resolution) seems more
complicated. We expect that such a design is possible, but necessarily more complicated if
ambiguity and undecidability are to be avoided. We expect that the work on impredicative
type-inference (Le Botlan & Rémy, 2003; Leijen, 2008; Vytiniotis et al., 2008) is relevant,and perhaps some of the design choices employed in those works would be helpful in thedesign of a system with full impredicativity.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

41

6.2 Committed Choice
C OCHIS commits to the first implicit whose head matches the query type. It has inherited
this committed choice approach from Haskell. Consider for instance the following Haskell
program with two overlapping instances:class C α wherem :: α → αinstance Eq α ⇒ C [α ] where . . .
instance Ord α ⇒ C [α ] where . . .
f :: StablePtr Int → [StablePtr Int ]f sp = m [sp]This code declares a type class C α and defines two instances. The first instance requires
Eq α, whereas the second instance requires Ord α. The function f takes a stable pointer(StablePtr) and returns a list of stable pointers. Unlike many other types, StablePtr only
supports equality, and not ordering. That is, there is an instance Eq (StablePtr α) but not
one for Ord (StablePtr α).
Should the above code type-check or not? In GHC Haskell the answer is no. Even though
there is no ambiguity in this program— resolution only succeeds with the first type classinstance— the program is nevertheless rejected. The reason is that Haskell’s resolution
only checks whether the instance heads match. As there are two equality specific matchingheads C [α ], the program is rejected.
Although this Haskell design choice is not very well documented in the research literature, the reason for not allowing backtracking is folklore among Haskell programmers andcan be found in various informal discussions (oleg, 2006; rHaskell, 2006; Bottu & simonpj,
2018). In essence there are two arguments for not allowing backtracking during resolution:• Reasoning: When reasoning about Haskell code that involves type classes, programmers have to understand which type class instance is used. This involves performing
the resolution algorithm mentally. The fact that only instance heads are needed
to determine whether an instance is committed to, makes this much easier thanperforming a full backtracking process.
• Performance: If backtracking is allowed, type-checking times of programs could
grow exponentially due to backtracking. Thus, by disallowing backtracking, GHC
eliminates a potential source of significant performance degradation in type-checking.
No Backtracking in C OCHIS Like in Haskell, our committed choice design for C OCHIS
also looks only at the heads of rule types, whereas a design with backtracking would need tolook at their contexts as well. In other words we commit to a matching rule type, even if its
recursive goals do not resolve. For instance, when resolving Char against the environment
Γ =?Bool, ?(Bool ⇒ Char), ?(Int ⇒ Char), we commit to ?(Int ⇒ Char) even though its
recursive goal Int cannot be resolved and thus the resolution of Char also fails. A more
permissive approach would be to backtrack when a recursive resolution fails and try thenext alternative matching implicit. That would allow Char to resolve.

ZU064-05-FPR

Main

42

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

In the design of C OCHIS, we have followed Haskell’s pragmatic reasons for committed
choice. Considering that Haskell’s 30 years of experience have shown that this works wellin practice, we believe that it is a reasonable choice.
Alternative Designs While there are advantages to committed choice, backtracking also
has its appeal and several systems have adopted it (White et al., 2014; Sozeau & Oury,
2008). In particular, backtracking accepts more queries, and would allow us to have asound and complete algorithm for C OCHIS (instead of just a sound one) with respect toFigure 4. Yet, the specification in Figure 4 does not guarantee stability or coherence. So
additional restrictions would be needed to have both properties.
OCaml’s modular implicits (White et al., 2014) suggest another alternative. When aquery is resolved, it exhaustively searches the implicit context for all possible solutions.
If more than one solution is found, then the program is rejected due to ambiguity. In thisway it is possible to have highly overlapping implicits in the type environment, that could
result in some queries being ambiguous. One advantage of this design is its flexibility,
since contexts can be more liberal and all queries that would be resolved in unambiguous
contexts with backtracking can, in principle, also be resolved with OCaml’s modular implicits. However the modular implicits approach is not formalized yet, and the fact that
contexts have to be searched exhaustively raises practical questions regarding performanceand ease of reasoning that have dictated the committed choice approach taken by Haskell
type classes.
Finally, in the context of theorem provers like Coq (Sozeau & Oury, 2008) where proof
irrelevance typically holds, backtracking seems to be the better choice. If type classes aresupplying proofs and it does not matter which proof is found, coherence is not relevant, andthe objection about the difficulty of reasoning is also not relevant. Moreover, in theorem
proving the expressiveness of search is often more important than having a very fast searchmethod, and thus worse performance is more tolerable.
6.3 Superclasses
Like Scala’s implicits design,8 C OCHIS does not directly support superclasses. While superclasses can be encoded in C OCHIS to a certain extent, there are several problems.
Superclasses in Haskell Haskell has supported superclasses since the introduction oftype classes. The Eq and Ord classes, with Eq a superclass of Ord, constitute a standard
example. The following simplified code shows the two classes, together with instances for
integers:
class Eq α where(≡) :: α → α → Boolclass Eq α ⇒ Ord α where(<) :: α → α → Bool
8

Note that, superclasses are often simulated in Scala with OO Subtyping and class hierarchies,
although there is no one-to-one correspondence between both.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

43

instance Eq Int where . . .
instance Ord Int where . . .
In the class context Eq α in the definition of the Ord class specifies that Eq α is a superclassof Ord α. Superclasses allow the use of methods from the superclasses, even if only the
subclass is part of the type class context. For example:
p :: Ord α ⇒ α → α → Boolp = (≡) -- accepted because Eq α is a superclass of Ord α
Here the signature of function p assumes that an instance for Ord α is available. In the bodyof p, the method (≡) of the class Eq α is used. This code is accepted in Haskell because
Eq α is a superclass of Ord α.
Superclasses, Determinism and Coherence In the presence of superclasses, Haskell’s
resolution is not deterministic. Consider this variant of p, defined only for integers:
p0 :: Int → Int → Boolp0 = (≡)
Haskell has two ways to resolve Eq Int to obtain the implementation of ≡ in p0 . The
first is to get the implementation of Eq Int directly from the Eq Int instance. The second
is to get an implementation of Eq Int as the superclass of Ord Int. The two elaborations are syntactically different, which makes elaboration with Haskell superclasses nondeterministic. Nonetheless the elaboration is still coherent, since both elaborations yield
the same semantics (they both execute the code of the one Eq Int instance).
A First Attempt at Encoding Superclasses We can try to encode the previous Haskell
definitions in the C OCHIS environment Γ =?(∀α.Ord α ⇒ Eq α) ; super , ?(Eq Int) ; x,?(Ord Int) ; y, whose implicit entries capture the superclass relation—super is a functionthat extracts the Eq dictionary out of an Ord dictionary— and the two instances9 . With respect to C OCHIS, the query ?(Eq Int) resolves deterministically by picking the second entryin Γ. Hence, C OCHIS’s explicit ordering of implicits avoids Haskell’s non-determinism.
While the ordering is beneficial for determinism, fewer queries may succeed due to an
unsuitable order of implicits. For example, suppose that we have instead the environmentΓ =?(Eq Int) ; x, ?(∀α.Ord α ⇒ Eq α) ; super , then resolving ?(Eq Int) fails because
the first entry matches and its requirement Ord Int cannot be satisfied. In this case thecommitted choice semantics prevents reaching the second entry, which would resolve
Eq Int directly.
Superclasses with Committed Choice The situation we just saw also arises in Haskell.
Treating superclass relations in the same way as type class instances does not work wellwith a committed choice strategy. That is why GHC treats superclass relations differently.

9Note that the proposed encoding does not satisfy our termination conditions, but we ignore this
aspect since there are other more pressing issues with the encoding.

ZU064-05-FPR

Main

44

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

In essence, whenever GHC adds a given type class constraint (e.g., from a programmersupplied type signature) to the type environment, it uses the superclass relation to also add
all of its ancestors. We believe that a similar strategy would be possible for C OCHIS. For
instance, in the last example, the type environment would be Γ =?Eq Int ; x, not containthe superclass relation and be able to resolve the query ?(Eq Int) with x. When adding an
Ord Int entry, we would also add its Eq Int superclass, yielding the modified environment
Γ =?Eq Int ; x, ?Ord Int ; y, ?Eq Int ; super y. Now, the query ?(Eq Int) is resolved
with super y, which is the superclass value of the new Ord Int entry.
Superclasses with Global Scoping and C OCHIS-style Resolution in GHC Haskell As
we have explained above, standard Haskell gets away with committed choice in the presence of superclasses without unnecessarily rejecting queries. Yet, this is no longer the casefor the recent extension with quantified class constraints (Bottu et al., 2017). Like C OCHIS,
quantified class constraints allow nested implications in type class instance contexts andas superclasses. The committed choice approach does not work with the latter. GHC hasdecided to retain its committed choice approach and to reject queries that would require
backtracking to explore the superclass relations.
6.4 Coherence
There are several ways to enforce coherence in a language design. For example, Haskell
guarantees coherence by ensuring that there is a unique instance of a type class per type. In
this way whenever code accesses a type class dictionary, it always returns the same (equal)
dictionary value. This is a very strict way to enforce coherence.
C OCHIS’s way to achieve coherence is more relaxed than Haskell’s. C OCHIS enforcesthat the elaboration and resolution are deterministic but, under different scopes the same
queries can resolve to different values (unlike Haskell).
While determinism is sufficient to ensure coherence, it is still a fairly strict way to ensure
coherence. A more relaxed and general notion of coherence is to allow elaboration andresolution to have multiple different (but observationally equivalent) terms for the same
expression. Our Corollary 5.1 provides a formal statement of coherence that is based oncontextual equivalence of two expressions:∀Γ, ρ, E1 , E2 :Γ `r ρ ; E1 ∧ Γ `r ρ ; E2⇒

|Γ| `F E1 'ctx E2 : |ρ|This statement is close to the usual definition of coherence in the literature (Reynolds,
1991; Jones, 1992; Breazu-Tannen et al., 1991). That is, E1 and E2 are not required to besyntactically equivalent, but they must be semantically equivalent. Many language designs
that are coherent are often not necessarily deterministic (unlike C OCHIS).
Alternative Designs We use determinism to establish coherence in C OCHIS, but a morerelaxed notion of coherence would also be possible. For example if, instead of committed
choice, we decided to allow for a more powerful resolution strategy (for example withbacktracking), then a more relaxed notion of coherence would be helpful. This could be
useful to deal with some situations that appear in superclasses. For example, consider again
the context Γ = ?(Eq Int), ?(∀α.Ord α ⇒ Eq α), ?(Ord Int). In this case the query ?(Eq Int)

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

45

can be resolved in two possible ways: either going via the superclass instance Ord Int; orby directly using the instance Eq Int. Even thought the two elaborations are syntacticallydifferent, their semantics is the same.

7 Related Work
The most closely related work can be divided into three strands: IP mechanisms that support local scoping with coherence and stability, but forbid overlapping implicits and lackother types of flexibility; IP mechanisms that have global scoping and preserve coherence
and stability; and IP mechanisms that are unstable and sometimes incoherent but offer
greater flexibility in terms of local scoping and/or overlapping implicits. C OCHIS is unique
in offering flexibility (local scoping with overlapping implicits, first-class implicits andhigher-order rules), while preserving coherence and stability.

7.1 Implicit Programming with Local Scoping, but no Overlapping Rules
Our work allows a very flexible model of implicits with first-class implicits, higher-orderrules and nested scoping with overlapping implicits while guaranteeing coherence andstability. Closest to our work in terms of combining additional flexibility with desirable
properties (such as coherence and stability) are modular type classes (Dreyer et al., 2007)
and System FG (Siek & Lumsdaine, 2005). Both works preserve coherence and stability
in the presence of local scoping, but (unlike C OCHIS) the local scopes forbid overlapping
implicits. The restriction of no overlapping implicits is an essential part of guaranteeing
coherence and stability. C OCHIS also has several other fundamental differences to both
modular type classes and System FG . Modular type classes (Dreyer et al., 2007) are alanguage design that uses ML-modules to model type classes. The main novelty of thisdesign is that, in addition to explicit instantiation of modules, implicit instantiation is
also supported. System FG (Siek & Lumsdaine, 2005) also offers an implicit parameter
passing mechanism with local scoping, which is used for concept-based generic programming (Siek, 2011). Both mechanisms are strongly influenced by type classes, and theypreserve some of the characteristics of type classes such as only allowing modules orconcepts to be implicitly passed. Moreover neither of those mechanisms support higherorder rules. In contrast C OCHIS follows the Scala implicits philosophy and allows valuesof any type to be implicit, and additionally higher-order rules are supported.
Implicit parameters (Lewis et al., 2000) are a proposal for a name-based implicit parameter passing mechanism with local scoping. Implicit parameters allow named arguments to
be passed implicitly, and these arguments can be of any type. However, implicit parameters
do not support recursive resolution, so for most use-cases of type-classes, including the
Ord instance for pairs in Section 2.1, implicit parameters would be very cumbersome.
They would require manual composition of rules instead of providing automatic recursive
resolution. This is in stark contrast with most other IP mechanisms, including C OCHIS,
where recursive resolution and the ability to compose rules automatically is a key featureand source of convenience.

ZU064-05-FPR

Main

46

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian
7.2 Implicit Programming with Local Scoping and Overlapping Implicits

The implicit calculus (Oliveira et al., 2012) is the main inspiration for the design of C OCHIS.
There are two major differences between C OCHIS and the implicit calculus. The firstdifference is that the implicit calculus, like Scala, does not enforce stability. Programs
similar to that in Figure 1 can be written in the implicit calculus and there is no way todetect instability. The second difference is in the design of resolution. Rules in the implicit
calculus have n-ary arguments, whereas in C OCHIS rules have single arguments and n-ary
arguments are simulated via multiple single argument rules. The resolution process with nary arguments in the implicit calculus is simple, but quite ad-hoc and forbids certain typesof resolution that are allowed in C OCHIS. For example, the query:?(Char ⇒ Bool), ?(Bool ⇒ Int) `ar Char ⇒ Int
does not resolve under the deterministic resolution rules of the implicit calculus, but it resolves in C OCHIS. Essentially resolving such query requires adding the rule type’s context
to the implicit environment in the course of the resolution process. But in the implicit
calculus the implicit environment never changes during resolution, which significantly
weakens the power of resolution.
S , which is a variation on the implicit calculus. The key
Rouvoet (2016) presents λ⇒feature of his calculus is the focusing resolution of Figure 4, although Rouvoet does notmake the connection with focusing in proof search. As we have already explained in
Section 3.5 this approach is both deterministic and unstable.
Scala implicits (Oliveira et al., 2010; Odersky, 2010) were themselves the inspiration
for the implicit calculus and, therefore, share various similarities with C OCHIS. In Scala
implicit arguments can be of any type, and local scoping (including overlapping implicits)
is supported. However the original model of Scala implicits did not allow higher-orderrules. Recently, following the implicit calculus and a preliminary version of C OCHIS,
Odersky et al. (2017) presented the SI calculus as a new basis for the Scala language’s
treatment of implicits. Prominently, SI features implicit function types T1 ?→ T2 , which
are akin to rule types T1 ⇒ T2 in C OCHIS, and implicit queries ?, which are akin to ?T in
C OCHIS. There are two main differences with C OCHIS. Firstly, like the Hindley-Milner
calculus SI is aimed at type inference and, e.g., does not feature explicit abstraction over
implicits λ? T.e or type application e T at the term level. In contrast, C OCHIS is more similar
to System F in this sense, making all abstractions and applications explicit.
Secondly, while C OCHIS aims to formalise and investigate the meta-theory of resolution,
the priority of Odersky et al. is not so much the SI calculus itself as the derived implementation of the Scala compiler. As a consequence, SI features a simplified type system thatis incoherent and unstable and a resolution algorithm that supports only monomorphic
types, while the compiler’s much more complex enforcement of coherence and support forpolymorphism are only discussed informally.
An interesting design of implicits has also been created in OCaml (White et al., 2014),
where the implicit entities are OCaml modules. Like C OCHIS, these implicits have local
scope, but, unlike C OCHIS, coherence is obtained by performing a backtracking search overall possible ways to resolve an implicit module signature, and fail if there is not exactly
one way. Hence, while introducing overlapping implicits is allowed, they are only usable

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

47

if only one leads to a full resolution. As far as we know, a partial prototype exists but theapproach has not been formalised yet.
7.3 Implicit Programming with Global Scoping
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 (Haskellstyle) type classes take that are different from C OCHIS. Most prominently, type classes
make a strong differentiation between types and type classes, and they use global scoping
instead of local scoping for instances/implicits. The design choice for global scoping can betraced back to Wadler and Blott’s (1989) original paper on type classes. They wanted to extend Hindley-Milner type-inference (Hindley, 1969; Milner, 1978; Damas & Milner, 1982)and discovered that local instances resulted in the loss of principal types. For Haskell-likelanguages the preservation of principal types is very important, so local instances werediscarded. However, there are many languages with IP mechanisms (including Scala, Coq,Agda, Idris or Isabelle) that have more modest goals in terms of type-inference. In theselanguages there are usually enough type annotations such that ambiguity introduced by
local instances is avoided.
There have been some proposals for addressing the limitations that arise from global
scoping (Kahl & Scheffczyk, 2001; Dijkstra & Swierstra, 2005) in the context of Haskell
type classes. Both named instances (Kahl & Scheffczyk, 2001) and Explicit Haskell (Dijkstra & Swierstra, 2005) preserve most design choices taken in type classes (including
global scoping), but allow instances that do not participate in the automatic resolution
process to be named. This enables the possibility of overriding the compiler’s default
resolution result with a user-defined choice.
Jones’s work on qualified types (Jones, 1995b) provides a particularly elegant frameworkthat captures type classes and other forms of predicates on types. Like type classes, qualified types make a strong distinction between types and predicates over types, and scopingis global. Jones (1995a) discusses the coherence of qualified types. The formal statementof determinacy in C OCHIS essentially guarantees a strong form of coherence similar to theone used in qualified types.
The GHC Haskell compiler supports overlapping instances (Peyton Jones et al., 1997)
that live in the same global scope. This allows some relief for the lack of local scoping. Yet,it still does not allow different instances for the same type to coexist in different scopes ofa program. Moreover, GHC only commits to an instance if it is the only one whose headmatches, and does not backtrack among multiple matching instances.
C OCHIS has a different approach to overlapping compared to instance chains (Morris& Jones, 2010). With instance chains the programmer imposes an order on a set of overlapping type class instances. All instance chains for a type class have a global scope andare expected not to overlap. This makes the scope of overlapping closed within a chain.
Instance chains can explicitly declare cases when resolution should fail, and these aredealt with by backtracking. 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 thedeclaration of a type family and a (closed) set of instances. After this declaration no more

ZU064-05-FPR

Main

48

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

instances can be added. In contrast our notion of scoping is closed at a particular resolution
point, but the scopes can still be extended at other resolution points.
Inspired by the focusing approach of C OCHIS Bottu et al. (2017) have extended Haskell’s
type class inference with quantified class constraints. This generalizes the syntax of Haskell’s
type class constraints to feature arbitrarily nested uses of universal quantification and implication. Their work differs from C OCHIS in that it does not support local instances. Moreover, they achieve coherence through requiring non-overlapping instances. Their algorithm
performs a backtracking search among these instances as well as any local assumptions(which themselves can ultimately only be satisfied by combinations of global instances),
rather than a linear committed-choice traversal of the environment.
IP Mechanisms in Dependently Typed Programming A number of dependently typed
languages also have IP mechanisms inspired by type classes. Coq’s type classes (Sozeau& Oury, 2008) and canonical structures (Gonthier et al., 2011), Agda’s instance arguments (Devriese & Piessens, 2011) and Idris type classes (Brady, 2015) all allow multiple
and/or highly overlapping implicits/instances that can be incoherent. The Coq theorem
prover has two mechanisms that allow modelling type-class like structures: canonicalstructures (Gonthier et al., 2011) and type classes (Sozeau & Oury, 2008). The two mechanisms have quite a bit of overlap in terms of functionality. In both mechanisms the idea
is to use dependent records to model type-class-like structures, and pass instances of suchrecords implicitly, but they still follow Haskell’s global scoping approach. Neverthelesshighly overlapping instances, which can be incoherent, are allowed and resolution performs
a backtracking search. Like implicits, the design of Idris type classes, known as interfaces,
allows for any type of value to be implicit. Thus type classes in Idris are first-class andcan be manipulated like any other values. The language distinguishes unnamed instances,which are used for resolution, and named instances which have to be applied explicitly. The
former cannot be overlapping, while there can be multiple (incoherent) named instances ofthe same type. The implicit resolution follows the committed choice strategy of Haskell,and ignores the fact that named instances can distinguish between alternative derivations.
Instance arguments (Devriese & Piessens, 2011) are an Agda extension that is closely
related to implicits. Like C OCHIS, instance arguments use a special arrow for introducing
implicit arguments. However, unlike most other mechanisms, implicits are not declared
explicitly. Instead they are drawn directly from the regular type environment, and any
previously defined declaration can be used as an implicit. The original design of instancearguments severely restricted the power of resolution by forbidding recursive resolution.
Since then, recursive resolution has been enabled in Agda. Like Coq’s and Idris’s typeclasses, instance arguments allow multiple incoherent implicits. Agda computes all possible resolutions and uses one of them only if all are equal.
7.4 Global Uniqueness and Same Instance Guarantee
Haskell type classes not only ensure coherence but also global uniqueness (Zhang, 2014)(due to global scoping), as discussed in Section 2.2. Unrestricted C OCHIS programs ensure
coherence only, as multiple implicits that match the same type can coexist in the same
program. We agree that for programs such as the Set example, it is highly desirable toZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

49

ensure that the same ordering instance is used consistently. C OCHIS is a core calculus,
meant to enable the design of source languages that utilize its power. An example are
Bottu et al.’s (2017) quantified class constraints for Haskell, which forbid local scoping
constructs and, instead, make all declared implicits visible in a single global environment.
This retains several of the benefits of C OCHIS (such as first-class implicits, higher-orderrules, and coherent overlapping implicits), while providing a form of global uniqueness.
However this design is still essentially non-modular, which is a key motivation for many
alternatives to type classes to provide local scoping instead.
Global uniqueness of instances is just a sufficient property to ensure consistent usesof the same instances for examples like Set. However, the important point is not to haveglobal uniqueness, but to consistently use the same instance. C OCHIS admittedly does notprovide a solution to enforce such consistency, but there is existing work with an alternative
solution to deal with the problem. Genus (Zhang et al., 2015) tracks the types of instances
to enforce their consistent use. For instance, in Genus two sets that use different orderings
have different types that reflect which Ord instance they use. As a consequence, taking
the union of those two sets is not possible. In contrast to C OCHIS Genus is focused onproviding a robust source language implementation for generic programming. Although the
Genus authors have proved some meta-theoretic results, neither type-safety nor coherence
have been proved for Genus. In dependently typed languages such as Agda and Idris, it
is possible to parametrize types by the instances they use (Brady, 2015). This achieves asimilar outcome to Genus’s approach to consistent usage of instances. Investigating theapplicability of a similar approach to C OCHIS is an interesting line of future work.

7.5 Focused Proof SearchPart of the syntax-directedness of our deterministic resolution is very similar to that obtained by focusing in proof search (Andreoli, 1992; Miller et al., 1991; Liang & Miller,2009). Both approaches alternate a phase that is syntax directed on a “query” formula (ourfocusing judgment), with a phase that is syntax directed on a given formula (our matching
judgment). This is as far as the correspondence goes though, as the choice of given formula
to focus on is typically not deterministic in focused proof search.

8 Conclusion
This paper presented C OCHIS, the Calculus Of CoHerent ImplicitS, a new calculus for
implicit programming that improves upon the implicit calculus and strikes a good balance between flexibility and desirable properties such as coherence and stability. C OCHIS
supports local scoping, overlapping implicits, first-class implicits, and higher-order rules,
while remaining type safe, coherent and stable. Interesting future work includes integrating
Genus’s solution for the instance coherence problem (Zhang et al., 2015) in C OCHIS;
and adding more features that show up in various IP mechanisms, such as associatedtypes (Chakravarty et al., 2005b; Chakravarty et al., 2005a) and type families (Schrijvers
et al., 2008).

ZU064-05-FPR

Main

50

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Acknowledgments We are very grateful for the feedback of the anonymous reviewers.
This work was partially supported by the the Hong Kong Research Grant Council projects
number 27200514 and 17258816, and by the Flemish Fund for Scientific Research (FWO).

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

51

References
Andreoli, Jean-marc. (1992). Logic programming with focusing proofs in linear logic. Journal of
logic and computation, 2, 297–347.
Barendregt, H. (1981). The lambda calculus: its syntax and semantics, volume 103 of studies in logic
and the foundations of mathematics. North-Holland.
Barendregt, Henk, Dekkers, Wil, & Statman, Richard. (2013). Lambda calculus with types.
Cambridge University Press.
Biernacki, Dariusz, & Polesiuk, Piotr. (2018). Logical relations for coherence of effect subtyping.
Logical methods in computer science, 14(1).
Boehm, Hans-J. (1985). Partial polymorphic type inference is undecidable. Pages 339–345 of: 26th
annual symposium on foundations of computer science. IEEE.
Bottu, Gert-Jan, & simonpj. (2018). Quantified constraints - proposals. https://github.com/
Gertjan423/ghc-proposals/blob/quantified-constraints/proposals/0000quantified-constraints.rst#overlap.
Bottu, Gert-Jan, Karachalias, Georgios, Schrijvers, Tom, Oliveira, Bruno, & Wadler, Philip. (2017).
Quantified class constraints. Acm sigplan haskell symposium.
Brady, Edwin. (2015). Type classes in Idris. https://groups.google.com/forum/#!topic/
idris-lang/OQQ3oc6zBaM.
Breazu-Tannen, Val, Coquand, Thierry, Gunter, Carl, & Scedrov, Andre. (1991). Inheritance as
implicit coercion. Information and computation, 93, 172–221. Also in .
Camarão, C., & Figueiredo, L. (1999). Type inference for overloading without restrictions,declarations or annotations. Pages 37–52 of: Flops. London, UK: Springer-Verlag.
Chakravarty, M., Keller, G., & Peyton Jones, S. L. (2005a). Associated type synonyms. Pages
241–253 of: Icfp. New York, NY, USA: ACM.
Chakravarty, M., Keller, G., Peyton Jones, S. L., & Marlow, S. (2005b). Associated types with class.
Pages 1–13 of: Popl. New York, NY, USA: ACM.
Chong, Stephen. (2017). Lecture 2: Logical relations part 2. https://www.seas.harvard.edu/
courses/cs252/2017fa/lectures/lec02-contextual-equiv.pdf.
Damas, Luı́s, & Milner, Robin. (1982). Principal type-schemes for functional programs. Pages
207–212 of: Popl. New York, NY, USA: ACM.
Devriese, D., & Piessens, F. (2011). On the bright side of type classes: Instance arguments in Agda.
Pages 143–155 of: Icfp. New York, NY, USA: ACM.
Dijkstra, A., & Swierstra, S. D. (2005). Making implicit parameters explicit. Tech. rept. Utrecht
University.
Dreyer, D., Harper, R., Chakravarty, M., & Keller, G. (2007). Modular type classes. Pages 63–70 of:Popl. New York, NY, USA: ACM.
Dunfield, Joshua, & Krishnaswami, Neelakantan R. (2013). Complete and easy bidirectional
typechecking for higher-rank polymorphism. Pages 429–442 of: Morrisett, Greg, & Uustalu,
Tarmo (eds), ACM SIGPLAN international conference on functional programming, icfp’13,
boston, ma, USA - september 25 - 27, 2013. ACM.
Eisenberg, Richard A., Vytiniotis, Dimitrios, Peyton Jones, Simon, & Weirich, Stephanie. (2014).
Closed type families with overlapping equations. Pages 671–683 of: Popl. New York, NY, USA:
ACM.
Garcia, Ronald, Jarvi, Jaakko, Lumsdaine, Andrew, Siek, Jeremy, & Willcock, Jeremiah. (2007). An
extended comparative study of language support for generic programming. J. funct. program.,17(2).
GHC. (2017). Ghc users guide: Overlapping instances. https://downloads.haskell.org/~ghc/latest/docs/html/users guide/glasgow exts.html#overlapping-instances.

ZU064-05-FPR

Main

52

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

GHC. (2017). Quantified Constraints – GHC. https://ghc.haskell.org/trac/ghc/wiki/
QuantifiedConstraints.
Gonthier, Georges, Ziliani, Beta, Nanevski, Aleksandar, & Dreyer, Derek. (2011). How to makead hoc proof automation less ad hoc. Pages 163–175 of: Proceedings of the 16th acm sigplan
international conference on functional programming. ICFP ’11. New York, NY, USA: ACM.
Gregor, D., Järvi, J., Siek, J. G., Stroustrup, B., Dos Reis, G., & Lumsdaine, A. (2006). Concepts:
linguistic support for generic programming in c++. Pages 291–310 of: Oopsla. New York, NY,
USA: ACM.
Hindley, J. Roger. (1969). The principal type-scheme of an object in combinatory logic. Transactionsof the american mathematical society, 146, 29–60.
Hulley, Brian. (2009).
A show-stopping problem for modular type classes?
http://
lists.seas.upenn.edu/pipermail/types-list/2009/001405.html.
Jones, M. P. (1992). A theory of qualified types. Esop.
Jones, M. P. (1995a). Qualified types: theory and practice. Cambridge University Press.
Jones, M. P. (1995b). Simplifying and improving qualified types. Fpca.
Jones, Simon Peyton, Vytiniotis, Dimitrios, Weirich, Stephanie, & Shields, Mark. (2007). Practical
type inference for arbitrary-rank types. Journal of functional programming, 17(1), 1–82.
Kahl, W., & Scheffczyk, J. (2001). Named instances for Haskell type classes. Haskell workshop.
Kiselyov, Oleg, & Shan, Chung-chieh. (2004). Functional pearl: Implicit configurations–or, typeclasses reflect the values of types. Proceedings of the 2004 acm sigplan workshop on haskell.
Haskell ’04.
Kmett, Edward. (2015). Type classes vs the world. https://www.youtube.com/watch?v=
hIZxTQP1ifo.
Le Botlan, Didier, & Rémy, Didier. (2003). MLF: Raising ML to the power of system F. Proceedingsof the eighth acm sigplan international conference on functional programming. ICFP ’03.
Leijen, Daan. (2008). HMF: Simple type inference for first-class polymorphism. Proceedings of the
13th acm sigplan international conference on functional programming. ICFP ’08.
Lewis, J., Launchbury, J., Meijer, E., & Shields, M. (2000). Implicit parameters: dynamic scopingwith static types. Pages 108–118 of: Popl. New York, NY, USA: ACM.
Liang, Chuck, & Miller, Dale. (2009). Focusing and polarization in linear, intuitionistic, and classicallogics. Theor. comput. sci., 410(46), 4747–4768.
Manna, Zohar, & Waldinger, Richard. (1980). A deductive approach to program synthesis. Acm
trans. program. lang. syst., 2(1), 90–121.
Marlow, Simon. (2012). Safe haskell and instance coherence. https://mail.haskell.org/
pipermail/haskell-cafe/2012-October/103887.html.
Martelli, Alberto, & Montanari, Ugo. (1982). An efficient unification algorithm. Acm trans. program.
lang. syst., 4(2), 258–282.
Miller, Dale. (1992). Unification under a mixed prefix. J. symb. comput., 14(4), 321–358.
Miller, Dale, Nadathur, Gopalan, Pfenning, Frank, , & Scedrov, Andre. (1991). Uniform proofs as afoundation for logic programming. Annals of pure and applied logic, 51(1–2), 125–157.
Milner, Robin. (1978). A theory of type polymorphism in programming. J. comput. syst. sci., 17(3),348–375.
Morris, J. G., & Jones, M. P. (2010). Instance chains: type class programming without overlapping
instances. Pages 375–386 of: Icfp. New York, NY, USA: ACM.
Morris, James Hiram, Jr. (1969). Lambda-calculus models of programming languages. Ph.D. thesis,
Sloan School of Management.
Mozilla Research, Team. (2017). The rust programming language. https://www.rust-lang.org/
en-US/.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits
Norell, Ulf. (2008). Dependently typed programming in agda.
functional programming.

53

Pages 230–266 of: Advanced

nponeccop. (2012).
Breaking data.set integrity without generalizednewtypederiving.
https://stackoverflow.com/questions/12735274/breaking-data-set-integritywithout-generalizednewtypederiving.
Odersky, M. (2010). The Scala language specification, version 2.8.
Odersky, Martin, & Läufer, Konstantin. (1996). Putting type annotations to work. Proceedings ofthe 23rd acm sigplan-sigact symposium on principles of programming languages. POPL ’96.
Odersky, Martin, Blanvillain, Olivier, Liu, Fengyun, Biboudis, Aggelos, Miller, Heather, & Stucki,
Sandro. (2017). Simplicitly: Foundations and applications of implicit function types. Proc. acm
program. lang., 2(POPL), 42:1–42:29.
oleg. (2006). Typeclass vs. prolog programming. https://mail.haskell.org/pipermail/haskell-cafe/2006-September/018500.html.
Oliveira, B. C. d. S., Moors, A., & Odersky, M. (2010). Type classes as objects and implicits. Oopsla.
New York, NY, USA: ACM.
Oliveira, B. C. d. S., Schrijvers, T., Choi, W., Lee, W., & Yi, K. (2012). The implicit calculus: A new
foundation for generic programming. Pldi ’12. New York, NY, USA: ACM.
Peyton Jones, S. L., Jones, M. P., & Meijer, E. (1997). Type classes: exploring the design space.
Haskell workshop.
Pfenning, Frank. (1993). On the undecidability of partial polymorphic type reconstruction. Fundam.
inform., 19(1/2), 185–199.
Pierce, Benjamin C. (2002). Types and programming languages. Cambridge, MA, USA: MIT Press.
Reynolds, John C. (1991). The coherence of languages with intersection types. Pages 675–700 of:Proceedings of the international conference on theoretical aspects of computer software. TACS
’91. London, UK, UK: Springer-Verlag.
rHaskell. (2006). The constraint trick for instances. https://www.reddit.com/r/haskell/
comments/3afi3t/the constraint trick for instances/cscb33j/?st=jjcz7zeh&sh=
1e5f3c8b.
Rouvoet, Arjen. (2016). Programs for Free: Towards the Formalization of Implicit Resolution in
Scala. M.Phil. thesis, TU Delft, the Netherlands.
Scharli, Nathanael, Ducasse, Stéphane, Nierstrasz, Oscar, & Black, Andrew P. (2003). Traits:
Composable units of behaviour. Pages 248–274 of: European conference on object-oriented
programming (ecoop 2003). Springer.
Schrijvers, T., Peyton Jones, S. L., Chakravarty, M., & Sulzmann, M. (2008). Type checking with
open type functions. Icfp. New York, NY, USA: ACM.
Siek, J. G. (2011).
The C++0x Concepts Effort.
concepts effort.pdf.

http://ecee.colorado.edu/~siek/

Siek, J. G., & Lumsdaine, A. (2005). Essential language support for generic programming. Pldi.
New York, NY, USA: ACM.
Sozeau, M., & Oury, N. (2008). First-class type classes. Tphols.
Sulzmann, M., Duck, G., Peyton Jones, S. L., & Stuckey, P. J. (2007). Understanding functional
dependencies via Constraint Handling Rules. Journal of functional programming, 17, 83–129.
Vytiniotis, Dimitrios, Weirich, Stephanie, & Peyton Jones, Simon. (2008). FPH: First-classpolymorphism for Haskell. Proceedings of the 13th acm sigplan international conference onfunctional programming. ICFP ’08.
Vytiniotis, Dimitrios, Peyton Jones, Simon, Schrijvers, Tom, & Suzmann, Martin. (2011).
OutsideIn(X): Modular Type Inference with Local Assumptions.
Journal of functional
programming, 21(4-5), 333–412.

ZU064-05-FPR

Main

54

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Wadler, P. L., & Blott, S. (1989). How to make ad-hoc polymorphism less ad hoc. Popl. New York,NY, USA: ACM.
Wadler, Philip. (2015). Propositions as types. Commun. ACM, 58(12), 75–84.
Wehr, S., Lämmel, R., & Thiemann, P. (2007). JavaGI: Generalized interfaces for java. Ecoop.
White, Leo, Bour, Frédéric, & Yallop, Jeremy. (2014). Modular implicits. Pages 22–63 of: Kiselyov,
Oleg, & Garrigue, Jacques (eds), Proceedings ML family/ocaml users and developers workshops,
ml/ocaml 2014, gothenburg, sweden, september 4-5, 2014. EPTCS, vol. 198.
Zhang, Edward. (2014).
Type classes: confluence, coherence and global uniqueness.
http://blog.ezyang.com/2014/07/type-classes-confluence-coherence-globaluniqueness/.
Zhang, Yizhou, Loring, Matthew C., Salvaneschi, Guido, Liskov, Barbara, & Myers, Andrew C.
(2015). Lightweight, flexible object-oriented generics. Proceedings of the 36th acm sigplan
conference on programming language design and implementation. PLDI ’15.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

55

Γ `F E : T(F-VAR )(F-A BS )(F-A PP )(x : T ) ∈ ΓΓ `F x : T

Γ, x : T1 `F E : T2
Γ `F λ x : T1 .E : T1 → T2

Γ `F E1 : T2 → T1

Γ `F E2 : T2

Γ `F E1 E2 : T1

(F-TA PP )

Γ `F E : ∀α.T2
Γ `F E T1 : T2 [T1 /α](F-TA BS )Γ, α `F E : TΓ `F Λα.E : ∀α.T

Fig. 11. System F Type System
A ProofsThis appendix summarizes the proofs for the theorems presented in the article as wellas those of the auxiliary lemmas that feature in those proofs. Several of the proofs havebeen mechanized in Coq; they are available from https://bitbucket.org/KlaraMar/cochiscoq and this appendix refers to them where appropriate.
Throughout the proofs we refer to the type system rules of System F listed in Figure 11,also formalized in file systemF.v (inductive definition Typing).

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.
Lemma A.1. IfthenΓ`e:ρ ;E|Γ| `F E : |ρ|Proof. See file Cochis.v, Lemma Typing TypePreservation.
Lemma A.2. IfthenΓ `ar ρ ; e|Γ| `F E : |ρ|Proof. See file Cochis.v, Lemma amb res TypePreservation.

ZU064-05-FPR

Main

56

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian
A.2 Auxiliary Lemmas About Non-Determistic Resolution

The non-deterministic resolution judgment enjoys a number of typical binder-related properties.
The first lemma is the weakening lemma: it states that an extended type environment
preserves all the derivations of the original environment.
Lemma A.3 (Weakening). IfthenΓ, Γ0 `ar ρ ; E
Γ, Γ00 , Γ0 `ar ρ ; E

Proof. See file Cochis.v, Lemma amb res weaken.

The second lemma is the substitution lemma which states that we can drop an axiom
from the type environment if it is already implied by the remainder of the type environment.
Lemma A.4 (Substitution). IfandΓ, ?ρ ; x, Γ0 `ar ρ 0 ; E 0thenΓ `ar ρ ; E
Γ, Γ0 `ar ρ 0 ; E 0 [E/x]

Proof. See file Cochis.v, Lemma sub eimpl amb res.
A.3 Soundness of Deterministic Resolution
The proofs of this section are split into subproofs for each sub-judgment (focusing, lookup
and matching) of the deterministic resolution judgment. They all proceed by induction
on the corresponding deterministic resolution judgment. Therefore, their dependencies,
depicted in the diagram below, follow those of the sub-judgments that constitute the main
deterministic resolution judgment. Because the proofs of this section are mechanized, an
auxiliary lemma is necessary to handle the multiple substitutions that rule (L-M ATCH)
uses.

Lemma A.5
Det. resolution
soundness

Lemma A.6
Det. focusing
soundness

Lemma A.7
Det. lookup
soundness

Lemma A.4
Substitution

Lemma A.8
Det. matchingsoundnessunder subst.

Lemma A.9
Det. matchingsoundness

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

57

Lemma A.5 states that deterministic resolution is sound with respect to non-deterministic
resolution.
Lemma A.5. IfthenΓ `r ρ ; EΓ `ar ρ ; E

Proof. See file CochisDet.v, Lemma DRes Soundness.
The lemma immediately follows from Lemma A.6.
Lemma A.6. Ifthenᾱ; Γ `r [ρ] ; EΓ `ar ρ ; E

Proof. See file CochisDet.v, Lemma DRes focus Soundness.
This lemma is proved together with Lemma A.7 by mutual induction on the derivationof the first hypothesis of both lemmas.
Lemma A.7. Ifthenᾱ; Γ; [Γ0 ] `r τ ; EΓ `ar τ ; E

Proof. See file CochisDet.v, Lemma DRes lookup Soundness.
The proof proceeds by induction on the derivation, mutually with the previous proof.
The above proof relies on the following lemma.
Lemma A.8. IfandΓ; [ρ] ; E `r ρ̄ ; x̄; τ ; E 0andΓ `ar ρ ; EthenΓ `ar ρ̄ ; ĒΓ `ar τ ; E 0 [Ē/x̄]

Proof. See file CochisDet.v, Lemma DRes match Soundness.
The proof proceeds by induction on the derivation of the first assumption and relies on
Lemmas A.4 (Substitution) and A.9.

ZU064-05-FPR

Main

7 December 2018

58

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian`unamb Γ(UE-E MPTY )(UE-TVAR )`unamb ε`unamb Γ(UE-VAR )(UE-I MPL )`unamb Γ, α`unamb Γ`unamb Γ, x : ρ`unamb Γ

Fig. A 1. Unambiguous Type Environment`unamb ρ`unamb Γ, ?ρ ; x

Lemma A.9. IfandΓ; [ρ] ; E `r ρ̄ ; x̄; τ ; E 0thenΓ `ar ρ ; E
Γ, ?ρ̄ ; x̄ `ar τ ; E 0

Proof. See file CochisDet.v, Lemma DRes match impl vars.

A.4 Deterministic Resolution is Deterministic
Similarly to Section A.3, the proofs of this section are split into subproofs for each subjudgment (focusing, lookup and matching) of the deterministic resolution judgment. Theirdependencies, depicted in the diagram below, follow those of the sub-judgments that constitute the main deterministic resolution judgment.

Lemma A.10
Deterministic
resolution
judgment isdeterministic

Lemma A.11
Focusing
judgment isdeterministic

Lemma A.12
Lookupjudgment isdeterministic

Lemma A.13
Matching
judgment isdeterministic

Figure A 1 defines the judgment `unamb Γ which states that a typing environment isunambiguous. Essentially, the definition requires that all types ρ in Γ are unambiguous.
This definition will be used throughout this section.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

59

Lemma A.10. If`unamb Γand`unamb ρandandΓ `r ρ ; E1then

Γ `r ρ ; E2
E1 = E2

Proof. From the lemma’s third and fourth hypotheses, the hypothesis of rule (R-M AIN)
and Lemma A.11 the desired result follows
E1 = E2

Lemma A.11. If`unamb Γand`unamb ρandandᾱ; Γ `r [ρ] ; E1thenᾱ; Γ `r [ρ] ; E2
E1 = E2

Proof. The proof proceeds by induction on the derivation of the third hypothesis.
(R-IA BS)ᾱ; Γ `r [ρ1 ⇒ ρ2 ] ; λ x : |ρ1 |.E1

It follows that the lemma’s fourth hypothesis is also derived by rule (R-IA BS). It follows
from the lemma’s second hypothesis that`unamb ρ1∧`unamb ρ2

From this and lemma’s first hypothesis, it follows that`unamb Γ, ?ρ1 ; x

From the rule’s hypothesis and the induction hypothesis, it follows that
E1 = E2

ZU064-05-FPR

Main

7 December 2018

60

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. MarntirosianHence, we may conclude
λ x : |ρ1 |.E1 = λ x : |ρ1 |.E2
(R-TA BS)ᾱ; Γ `r [∀α.ρ] ; Λα.E1

It follows that the lemma’s fourth hypothesis is also derived by rule (R-TA BS). It follows
from the lemma’s second hypothesis thatα `unamb ρ
The unambiguity judgment enjoys a weakening property which we use here to obtain`unamb ρ
From the lemma’s first hypothesis, it follows that`unamb Γ, αFrom the rule’s hypothesis and the induction hypothesis, it follows that
E1 = E2
Hence, we may conclude
Λα.E1 = Λα.E2(R-S IMP)ᾱ; Γ `r [τ] ; E1

It follows that the lemma’s fourth hypothesis is also derived by rule (R-S IMP). We obtain
the desired result from Lemma A.12
E1 = E2

Lemma A.12. If`unamb Γand`unamb Γ0andandᾱ; Γ; [Γ0 ] `r τ ; E1thenᾱ; Γ; [Γ0 ] `r τ ; E2
E1 = E2

Proof. The proof proceeds by induction on the derivation of the third hypothesis.
(L-M ATCH)

ᾱ; Γ; [Γ0 , ?ρ ; x] `r τ ; E1 [Ē10 /x̄]

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

61

The rule’s two hypotheses arewhere Σ1 = ρ10 ; x , andΓ; [ρ] ; x `r Σ1 ; τ ; E1ᾱ; Γ `r [ρ10 ] ; E10(∀ρ10 ∈ ρ 01 )Then the fourth hypothesis was either derived from rule (L-M ATCH), or from rule
(L-N O M ATCH). However, the hypothesis of the latter is not satisfied: ε; E1 ; Σ1 forms
a counter-example. Hence, using rule (L-M ATCH) the fourth hypothesis is also derived.
Then it follows from the first hypothesis of the rule (given above), from the first hypothesis of the lemma, which entails `unamb ρ, and from Lemma A.13 (with σ̄1 = σ̄2 = σ̄10 =σ̄20 = ε) that
E1 = E2∧

Σ1 = Σ2

From the second hypothesis of the rule and Lemma A.11 it also follows thatĒ10 = Ē20
Hence, we may conclude
0

E1 [Ē10 /x̄] = E2 [E¯2 /x̄]
(L-N O M ATCH)

ᾱ; Γ; [Γ0 , ?ρ ; x] `r τ ; E10

Then the fourth hypothesis was either derived from rule (L-M ATCH), or from rule
(L-N O M ATCH). However, the hypothesis of the former is not satisfied, as it would bea counter-example for the first hypothesis of the assumed rule of the third hypothesis.
Hence, the fourth hypothesis is also formed by rule (L-N O M ATCH).
From the second hypothesis of the lemma we derive `unamb Γ0 . Then from the second
hypothesis of the rule and the induction hypothesis we conclude the desired result
E10 = E20
(L-VAR)ᾱ; Γ; [Γ0 , x : ρ] `r τ ; E1

Clearly the fourth hypothesis is also derived by rule (L-VAR). Moreover, from thesecond hypothesis it follows that `unamb Γ0 . Hence, from the induction hypothesis weconclude that
E1 = E2(L-T Y VAR)ᾱ; Γ; [Γ0 , α] `r τ ; E1
Clearly the fourth hypothesis is also derived by rule (L-T Y VAR). Moreover, from thesecond hypothesis it follows that `unamb Γ0 . Hence, from the induction hypothesis weconclude that
E1 = E2

ZU064-05-FPR

Main

7 December 2018

62

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Before proceeding with the matching judgment, we present a version of it that is annotated with the sequence of substitution types σ̄ used to instantiate the universal quantifiers.
σ̄ ; Γ; [ρ] ; E `r Σ; τ ; E 0(M-S IMP ) ε; Γ; [τ] ; E `r ε; τ ; E(M-IA PP )σ̄ ; Γ, ?ρ1 ; x; [ρ2 ] ; E x `r Σ; τ ; E 0

x freshσ̄ ; Γ; [ρ[σ /α]] ; E |σ | `r Σ; τ ; E 0Γ`σσ̄ ; Γ; [ρ1 ⇒ ρ2 ] ; E `r ρ1 ; x, Σ; τ ; E 0(M-TA PP )σ̄ , σ ; Γ; [∀α.ρ] ; E `r Σ; τ ; E 0

It is not difficult to see that any derivation of the annotated judgment is in one to one
correspondence with a derivation of the unannotated judgment.
Now we are ready to show that the judgment is deterministic.
Lemma A.13. Ifᾱ `unamb ρandandσ̄1 ; Γ; [ρ[σ̄2 /ᾱ]] ; E[|σ̄2 |/ᾱ] `r Σ1 ; τ ; E1

thenσ̄10 ; Γ; [ρ[σ̄20 /ᾱ]] ; E[|σ̄20 |/ᾱ] `r Σ2 ; τ ; E2σ̄1 = σ̄10∧σ̄2 = σ̄20∧

E1 = E2∧

Σ1 = Σ2∧`unamb Σ1

Proof. The proof proceeds by induction on the derivation of the first hypothesis.
(UA-S IMP)ᾱ `unamb τ 0Then the second and third hypothesis of the lemma must have been formed by rule
(M-S IMP) and henceσ̄1 = ε = σ̄10
For the same reason we have that τ 0 [σ̄2 /ᾱ] = τ = τ 0 [σ̄20 /ᾱ]. Since we know that ᾱ ⊆ftv(τ), it must follow also thatσ̄2 = σ̄20
As a consequence, we also have that
E1 = E[|σ̄2 |/ᾱ] = E[|σ̄20 |/ᾱ] = E2
Finally, it also follows from rule (M-S IMP) that
Σ1 = ε = Σ2

ZU064-05-FPR

Main

7 December 2018

10:26

63

Cochis: Stable and Coherent Implicits
and trivially`unamb εᾱ `unamb ρ1 ⇒ ρ2

(UA-IA BS)

Then the second and third hypothesis of the lemma must have been formed by rule
(M-IA PP). From their two hypotheses and from the hypothesis of the rule and theinduction hypothesis, we obtain the desired resultsσ̄1 = σ̄10∧σ̄2 = σ̄20∧∧

E1 = E2

Σ1 , ρ1 [|σ̄2 |/ᾱ] ; x = Σ2 , ρ1 [|σ̄20 |/ᾱ] ; x

We also derive from the induction hypothesis that `unamb Σ1 . Since ᾱ `unamb ρ1 ⇒ ρ2 ,we also have `unamb ρ1 . Hence we also conclude`unamb Σ1 , ρ1 ; x(UA-TA BS)ᾱ `unamb ∀α.ρThen the second and third hypothesis of the lemma must have been formed by rule0 , σ 0 . From their two hypotheses and from
(M-TA PP), with σ̄1 = σ̄1,1 , σ1,2 and σ̄10 = σ̄1,1
1,2
the hypothesis of the rule and the induction hypothesis, we obtain0
σ̄2 , σ1,2 = σ̄20 , σ1,2∧0
σ̄1,1 = σ̄1,1∧E1 = E2∧∧

Σ1 = Σ2

Σ1 = Σ2∧`unamb Σ1

From this we conclude the desired resultσ̄1 = σ̄10∧σ̄2 = σ̄20∧

E1 = E2∧`unamb Σ1

A.5 Resolution and Typing Stability
The proofs of this section concern stability of the deterministic resolution judgment, as
well as stability of typing. The first part, similarly to Section A.4, is split into subproofs foreach auxiliary judgment (focusing, lookup and matching) of the deterministic resolution
judgment and follows their dependencies. The second part uses the main result of thefirst part to establish stability of typing under type application reduction. In addition, it
uses the preservation-under-type-substitution properties of typing and of the unambiguity
judgment. The dependencies of the proofs of this section are depicted in the diagram below,
where main results are indicated with double borders.

ZU064-05-FPR

Main

7 December 2018

64

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Lemma A.14
Deterministic
resolution
is stable

Lemma A.15
Focusing
judgment
is stable

Lemma A.16
Lookupjudgment
is stable

Lemma A.17
Matching
judgment
is stable

Lemma A.19
Typingpreservation
under type
substitution

Lemma A.18
Typing is stable
under typeapplication
reduction

Lemma A.20
Unambiguity
preservation
under type
substitution

Lemma A.21
Unambiguity
preservation
under type
substitution

Deterministic resolution is stable under substitution.
Lemma A.14. If
thenΓ, α, Γ0 `r ρ ; E
Γ, Γ0 [σ /α] `r ρ[σ /α] ; E[|σ |/α]

Proof. The proof proceeds by induction on the first derivation and uses Lemma A.15.
The hypothesis of rule (R-M AIN) then isftv(Γ), α, ftv(Γ0 ); Γ, α, Γ0 `r [ρ] ; E

From Lemma A.15 it follows thatftv(Γ), ftv(Γ0 ); Γ, Γ0 [σ /α] `r [ρ[σ /α]] ; E[|σ |/α]

As ftv(Γ0 ) = ftv(Γ0 [σ /α]), the desired result follows from rule (R-M AIN)Γ, Γ0 [σ /α] `r ρ[σ /α] ; E[|σ |/α]
The next two proofs make use of the auxiliary definition R, shown in Figure A 2. The
relation R(Γ; α; Γ0 ; Γ00 ; Γ000 ; σ ) states that when performing a type substitution Γ, α, Γ0 `[σ /α], then any Γ00 ⊆ Γ, α, Γ0 , results to Γ000 after the substitution has been performed. The
two cases of the relation are necessary to separate between α ∈ Γ00 and α ∈/ Γ00 .
Lemma A.15. Ifthenᾱ, α, ᾱ; Γ, α, Γ0 `r [ρ] ; Eᾱ, ᾱ 0 ; Γ, Γ0 [σ /α] `r [ρ[σ /α]] ; E[|σ |/α]

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

65

R(Γ; α; Γ0 ; Γ00 ; Γ000 ; σ )
(R-1)
(R-2)

R(Γ1 , Γ2 ; α; Γ0 ; Γ1 ; Γ1 ; σ )R(Γ; α; Γ01 , Γ02 ; Γ, α, Γ01 ; Γ, Γ01 [σ /α]; σ )Fig. A 2. Auxiliary Definition R
Proof. The proof proceeds by induction on the derivation of the first hypothesis, mutuallywith Lemma A.16.
(R-IA BS)ᾱ, α, ᾱ 0 ; Γ, α, Γ0 `r [ρ1 ⇒ ρ2 ] ; λ x : |ρ1 |.E

From the rule’s hypothesis and the induction hypothesis we haveᾱ, ᾱ 0 ; Γ, (Γ0 , ?ρ1 ; x)[σ /α] `r [ρ2 [σ /α]] ; E[|σ |/α]

From the definition of substitution and rule (R-IA BS) we then concludeᾱ, ᾱ 0 ; Γ, Γ0 [σ /α] `r [(ρ1 ⇒ ρ2 )[σ /α]] ; (λ x : |ρ1 |.E)[|σ |/α](R-TA BS)ᾱ, α, ᾱ 0 ; Γ, α, Γ0 `r [∀β .ρ] ; Λβ .E

From the rule’s hypothesis and the induction hypothesis we haveᾱ, ᾱ 0 ; Γ, (Γ0 , β )[σ /α] `r [ρ[σ /α]] ; E[|σ |/α]

From the definition of substitution and rule (R-TA BS) we then concludeᾱ, ᾱ 0 ; Γ, Γ0 [σ /α] `r [(∀β .ρ)[σ /α]] ; (Λβ .E)[|σ |/α](R-S IMP)ᾱ, α, ᾱ 0 ; Γ, α, Γ0 `r [τ] ; E

From the rule’s hypothesis and Lemma A.16 we conclude

andᾱ, ᾱ 0 ; Γ, Γ0 [σ /α]; [Γ000 ] `r τ[σ /α] ; E[|σ |/α]R(Γ; α; Γ0 ; Γ, α, Γ0 ; Γ000 ; σ )The latter could only have been obtained by rule (R-2). Hence, we know that Γ000 =Γ, Γ0 [σ /α] and the former is equivalent toᾱ, ᾱ 0 ; Γ, Γ0 [σ /α]; [Γ, Γ0 [σ /α]] `r τ[σ /α] ; E[|σ |/α]With this fact we can conclude by rule (R-S IMP)ᾱ, ᾱ 0 ; Γ, Γ0 [σ /α] `r [τ[σ /α]] ; E[|σ |/α]

ZU064-05-FPR

Main

7 December 2018

66

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Lemma A.16. Ifᾱ, α, ᾱ 0 ; Γ, α, Γ0 ; [Γ00 ] `r τ ; E

andΓ00 ⊆ Γ, α, Γ0thenᾱ, ᾱ 0 ; Γ, Γ0 [σ /α]; [Γ000 ] `r τ[σ /α] ; E[|σ |/α]andR(Γ; α; Γ0 ; Γ00 ; Γ000 ; σ )Proof. The proof proceeds by induction on the derivation of the first hypothesis, mutuallywith Lemma A.15.
ᾱ, α, ᾱ 0 ; Γ, α, Γ0 ; [Γ00 , ?ρ ; x] `r τ ; E(L-M ATCH)

Then it follows from the first hypothesis of the rule and of Lemma A.17 thatΓ, Γ0 [σ /α]; [ρ[σ /α]] ; E[|σ |/α] `r ρ̄[σ /α] ; x̄; τ[σ /α] ; E 0 [|σ |/α]Also it follows from the second hypothesis of the rule and of Lemma A.15 thatα, ᾱ 0 ; Γ, Γ0 [σ /α] `r [ρ̄[σ /α]] ; Ē[|σ |/α]

By combining these two observations with rule (L-M ATCH) we obtain the first desired
resultᾱ, ᾱ 0 ; Γ, Γ0 [σ /α]; [Γ000 , ?ρ[σ /α] ; x] `r τ[σ /α] ; E[|σ |/α]

We obtain the second desired result by case analysis on Γ00 ⊆ Γ, α, Γ0 :1. Γ = Γ1 , ?ρ ; x, Γ2 ∧ Γ00 = Γ1 :In this case we can use rule (R-1) to establish:

R((Γ1 , ?ρ ; x), Γ2 ; α; Γ0 ; Γ1 , ?ρ ; x; Γ1 , ?ρ ; x; σ )which is equivalent toR(Γ; α; Γ0 ; Γ00 , ?ρ ; x; Γ00 , ?ρ ; x; σ )2. Γ0 = Γ01 , ?ρ ; x, Γ02 ∧ Γ00 = Γ, α, Γ01 :In this case we can use rule (R-2) to establish:

R(Γ; α; (Γ01 , ?ρ ; x), Γ02 ; Γ, α, (Γ01 , ?ρ ; x); Γ, (Γ01 , ?ρ ; x)[σ /α]; σ )which is equivalent toR(Γ; α; Γ0 ; Γ00 , ?ρ ; x; Γ, (Γ01 , ?ρ ; x)[σ /α]; σ )(L-N O M ATCH)

ᾱ, α, ᾱ 0 ; Γ, α, Γ0 ; [Γ00 , ?ρ ; x] `r τ ; E 0

The rule’s first hypothesis states that
6 ∃θ , E, Σ, dom(θ ) ⊆ (ᾱ, α, ᾱ 0 ) : θ (Γ, α, Γ0 ); [θ (ρ)] ; x `r Σ; θ (τ) ; E

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

67

Hence, the above also holds when we restrict θ to be of the form θ 0 · [σ /α]. In this case,the above simplifies to
6 ∃θ 0 , E, Σ, dom(θ ) ⊆ (ᾱ, ᾱ 0 ) : θ 0 (Γ, Γ0 [σ /α]); [θ 0 (ρ[σ /α])] ; x `r Σ; θ 0 (τ[σ /α]) ; E

From the rule’s second hypothesis and the induction hypothesis we haveᾱ, ᾱ 0 ; Γ, Γ0 [σ /α]; [Γ000 ] `r τ[σ /α] ; E 0 [|σ |/α]With rule (L-N O M ATCH) we combine these two observations into the desired first resultᾱ, ᾱ 0 ; Γ, (Γ0 , ?ρ ; x)[σ /α]; [Γ000 ] `r τ[σ /α] ; E 0 [|σ |/α]

Similarly, following the rule’s second hypothesis and the induction hypothesis we have:R(Γ; α; Γ0 ; Γ00 ; Γ000 ; σ )We do a case analysis on the derivation of this judgment.
1. (R-1):
Then we have
Γ = Γ1 , x : ρ, Γ2∧

Γ00 = Γ1∧

Γ000 = Γ1

By rule (R-2) we then haveR((Γ1 , x : ρ), Γ2 ; α; Γ0 ; Γ1 , ?ρ ; x; Γ1 , ?ρ ; x; σ )which, given all the equations we have, is equivalent to

2. (R-2):
Then we haveR(Γ; α; Γ0 ; Γ00 , ?ρ ; x; Γ00 , ?ρ ; x; σ )Γ0 = Γ01 , Γ02∧Γ00 = Γ, α, Γ01∧

Γ000 = Γ, Γ01 [σ /α]Since Γ00 , ?ρ ; x ⊆ Γ, α, Γ0 , it follows that Γ02 =?ρ ; x, Γ02,2 . Hence, by rule (R-2)
we can establish
R(Γ; α; (Γ01 , ?ρ ; x), Γ02 ; Γ, α, (Γ01 , ?ρ ; x); Γ, (Γ01 , ?ρ ; x)[σ /α]; σ )which, given all the equations we have, is equivalent toR(Γ; α; Γ0 ; Γ00 , ?ρ ; x; Γ, (Γ01 , ?ρ ; x)[σ /α]; σ )(L-VAR)ᾱ, α, ᾱ 0 ; Γ, α, Γ0 ; [Γ00 , x : ρ] `r τ ; E

Then following the rule’s hypothesis and the induction hypothesis we have:ᾱ, ᾱ 0 ; Γ, Γ0 [σ /α]; [Γ000 ] `r τ[σ /α] ; E[|σ |/α]

By rule (L-VAR) and the definition of substitution we then haveᾱ, ᾱ 0 ; Γ, Γ0 [σ /α]; [Γ000 , x : ρ[σ /α]] `r τ[σ /α] ; E[|σ |/α]

Similarly, following the rule’s hypothesis and the induction hypothesis we have:R(Γ; α; Γ0 ; Γ00 ; Γ000 ; σ )ZU064-05-FPR

Main

7 December 2018

68

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

We do a case analysis on the derivation of this judgment.
1. (R-1):
Then we have∧

Γ = Γ1 , x : ρ, Γ2

Γ00 = Γ1

Γ000 = Γ1∧

By rule (R-2) we then haveR((Γ1 , x : ρ), Γ2 ; α; Γ0 ; Γ1 , x : ρ; Γ1 , x : ρ; σ )which, given all the equations we have, is equivalent toR(Γ; α; Γ0 ; Γ00 , x : ρ; Γ00 , x : ρ; σ )2. (R-2):
Then we have
Γ0 = Γ01 , Γ02Γ00 = Γ, α, Γ01∧∧

Γ000 = Γ, Γ01 [σ /α]Since Γ00 , x : ρ ⊆ Γ, α, Γ0 , it follows that Γ02 = x : ρ, Γ02,2 . Hence, by rule (R-2) we
can establish
R(Γ; α; (Γ01 , x : ρ), Γ02 ; Γ, α, (Γ01 , x : ρ); Γ, (Γ01 , x : ρ)[σ /α]; σ )which, given all the equations we have, is equivalent toR(Γ; α; Γ0 ; Γ00 , x : ρ; Γ, (Γ01 , x : ρ)[σ /α]; σ )(L-T Y VAR)ᾱ, α, ᾱ 0 ; Γ, α, Γ0 ; [Γ00 , β ] `r τ ; E

Then following the rule’s hypothesis and the induction hypothesis we have:ᾱ, ᾱ 0 ; Γ, Γ0 [σ /α]; [Γ000 ] `r τ[σ /α] ; E[|σ |/α]

By rule (L-T Y VAR) and the definition of substitution we then haveᾱ, ᾱ 0 ; Γ, Γ0 [σ /α]; [Γ000 , β ] `r τ[σ /α] ; E[|σ |/α]

Similarly, following the rule’s hypothesis and the induction hypothesis we have:R(Γ; α; Γ0 ; Γ00 ; Γ000 ; σ )We do a case analysis on the derivation of this judgment.
1. (R-1):
Then we have
Γ = Γ1 , Γ2∧

Γ00 = Γ1∧

Γ000 = Γ1

We further distinguish between two mutually exclusive cases:(a) Γ2 = ε
It follows that α = β and we can establish by means of (R-2) thatR(Γ1 , Γ2 ; α; ε, Γ0 ; Γ1 , Γ2 , α; Γ1 , Γ2 , ε[σ /α]; σ )which, given all the equations we have, is equivalent toR(Γ; α; Γ0 ; Γ00 , β ; Γ; σ )ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

69(b) Γ2 6= εThen it follows that Γ2 = β , Γ2,2 and by rule (R-2) we haveR((Γ1 , β ), Γ2,2 ; α; Γ0 ; Γ1 , β ; Γ1 , β ; σ )which, given all the equations we have, is equivalent toR(Γ; α; Γ0 ; Γ00 , β ; Γ1 , β ; σ )2. (R-2):
Then we have
Γ0 = Γ01 , Γ02∧Γ00 = Γ, α, Γ01∧

Γ000 = Γ, Γ01 [σ /α]Since Γ00 , β ⊆ Γ, α, Γ0 , it follows that Γ02 = β , Γ02,2 . Hence, by rule (R-2) we canestablish
R(Γ; α; (Γ01 , β ), Γ02 ; Γ, α, (Γ01 , β ); Γ, (Γ01 , β )[σ /α]; σ )which, given all the equations we have, is equivalent toR(Γ; α; Γ0 ; Γ00 , β ; Γ, (Γ01 , β )[σ /α]; σ )Lemma A.17. If
Γ, α, Γ0 ; [ρ] ; E `r ρ̄ ; x̄; τ ; E 0thenΓ, Γ0 [σ /α]; [ρ[σ /α]] ; E[|σ |/α] `r ρ̄[σ /α] ; x̄; τ[σ /α] ; E 0 [|σ |/α]

Proof. The proof proceeds by induction on the derivation of the hypothesis.
(M-S IMP)Γ, α, Γ0 ; [τ] ; E `r ε; τ ; E

The desired conclusion follows directly from rule (M-S IMP)Γ, Γ0 [σ /α]; [τ[σ /α]] ; E[|σ /α|] `r ε; τ[σ /α] ; E[|σ /α|](M-IA PP)Γ, α, Γ0 ; [ρ1 ⇒ ρ2 ] ; E `r Σ, ρ1 ; x; τ ; E 0

From the rule’s hypothesis and the induction hypothesis we haveΓ, (Γ0 , ?ρ1 ; x)[σ /α]; [ρ2 [σ /α]] ; (E x)[|σ |/α] `r (ρ1 ; x, Σ)[σ /α]; τ[σ /α] ; E 0 [|σ |/α]Then from the definition of substutition and rule (M-IA PP) we conclude

Γ, Γ0 [σ /α]; [(ρ1 ⇒ ρ2 )[σ /α]] ; E[|σ |/α] `r Σ[σ /α]; τ[σ /α] ; E 0 [|σ |/α]
(M-TA PP)Γ, α, Γ0 ; [∀β .ρ] ; E `r Σ; τ ; E 0

From the rule’s hypothesis and the induction hypothesis we haveΓ, Γ0 [σ /α]; [ρ[σ 0 /β ][σ /α]] ; (E|σ 0 |)[|σ |/α] `r Σ[σ /α]; τ[σ /α] ; E 0 [|σ |/α]

ZU064-05-FPR

Main

7 December 2018

70

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

We conclude by rule (M-TA PP), reasoning modulo the definition of substitution
Γ, Γ0 [σ /α]; [(∀β .ρ)[σ /α]] ; E[|σ |/α] `r Σ[σ /α]; τ[σ /α] ; E 0 [|σ |/α]
Lemma A.18. IfΓ ` (Λα.e) σ : ρ[σ /α] ; (Λα.E) |σ |then

Γ ` e[σ /α] : ρ[σ /α] ; E[|σ |/α]

Proof. By case analysis, the two last rules used in the derivation of the theorem’s hypothesis must be instances of (T Y-TA BS) and (T Y-TA PP), as shown below.

T Y-TA BST Y-TA PP

Γ, α ` e : ρ ; EΓ ` Λα.e : ∀α.ρ ; Λα.EΓ ` (Λα.e) σ : ρ[σ /α] ; (Λα.E) |σ |Therefore, it suffices to show that

If Γ, α ` e : ρ ; E
then Γ ` e[σ /α] : ρ[σ /α] ; E[|σ |/α]This can be proven as a special case (Γ0 = ε) of the following theorem.
Lemma A.19. If
Γ, α, Γ0 ` e : ρ ; E

thenΓ, Γ0 [σ /α] ` e[σ /α] : ρ[σ /α] ; E[|σ |/α]

Proof. The proof proceeds by induction on the first hypothesis.
(T Y-VAR)

Γ, α, Γ0 ` x : ρ ; x

From the rule’s premise, we know that (x : ρ) ∈ Γ, α, Γ0 . Hence, it also holds that
(x : ρ[σ /α]) ∈ Γ, Γ0 [σ /α]. Rule (T Y-VAR) can then be instantiated with the latter, toconclude Γ, Γ0 [σ /α] ` x : ρ[σ /α] ; x.
(T Y-A BS)

Γ, α, Γ0 ` λ x : ρ1 .e : ρ1 → ρ2 ; λ x : |ρ1 |.E

From the rule’s premise, we get Γ, α, Γ0 , x : ρ1 ` e : ρ2 ; E . By passing this to the
induction hypothesis, we obtainΓ, Γ0 [σ /α], x : ρ1 [σ /α] ` e : ρ2 [σ /α] ; E[|σ |/α]

From the definition of substitution and by supplying the latter to rule (T Y-A BS), we reachthe goal.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits(T Y-A PP)

71

Γ, α, Γ0 ` e1 e2 : ρ2 ; E1 E2

From the assumptions of rule (T Y-A PP), the induction hypothesis and the definition ofsubstitution, we obtainandΓ, Γ0 [σ /α] ` e2 : ρ1 [σ /α] → ρ2 [σ /α] ; E1 [|σ |/α]Γ, Γ0 [σ /α] ` e1 : ρ1 [σ /α] ; E2 [|σ |/α]

By instantiating rule (T Y-A PP) with the two judgments above, we obtain our goal.
(T Y-TA BS)

Γ, α, Γ0 ` Λα 0 .e : ∀α 0 .ρ ; Λα 0 .E

From the assumptions of rule (T Y-TA BS) and the induction hypothesis, we obtain
Γ, (Γ0 , α 0 )[σ /α] ` e[σ /α] : ρ ; E|σ |/α]where, from the definition of substitution, we have (Γ0 , α 0 )[σ /α] = Γ0 [σ /α], α 0 . Using thisequation in the judgment above, we reach the goal by applying rule (T Y-TA BS) on it.
(T Y-TA PP)

Γ, α, Γ0 ` e ρ1 : ρ2 [ρ1 /α 0 ] ; E |ρ1 |The first assumption of rule (T Y-TA PP) is
Γ, α, Γ0 ` e : ∀α 0 .ρ2 ; E

Then, from the induction hypothesis and the definition of substitution, we getΓ, Γ0 [σ /α] ` e[σ /α] : ∀α 0 .(ρ2 [σ /α]) ; E[|σ |/α]

Using this in rule (T Y-TA PP), we getΓ, Γ0 [σ /α] ` (e[σ /α]) (ρ1 [σ /α]) : (ρ2 [σ /α])[ρ1 [σ /α]/α 0 ] ; E[|σ |/α] |ρ1 [σ /α]|which is syntactically equal to our goal, since by the definition of substitution and typetranslation and from the commutativity-like property of substitution composition, we get
the following equations.
(e[σ /α]) (ρ1 [σ /α]) = (e ρ1 )[σ /α](ρ2 [σ /α])[ρ1 [σ /α]/α 0 ] = ρ2 [ρ1 /α 0 ][σ /α]E[|σ |/α] |ρ1 [σ /α]| = E[|σ |/α] |ρ1 |[|σ |/α] = (E ρ1 )[|σ |/α]
(T Y-IA BS)

Γ, α, Γ0 ` λ? ρ1 .e : ρ1 ⇒ ρ2 ; λ x : |ρ1 |.E

From the first assumption of rule (T Y-IA BS) and the induction hypothesis, we getΓ, Γ0 [σ /α], ?ρ1 [σ /α] ; x ` e[σ /α] : ρ2 [σ /α] ; E[|σ |/α]

Passing the second assumption of rule (T Y-IA BS) to Lemma A.20, we get`unamb ρ1 [σ /α]ZU064-05-FPR

Main

7 December 2018

72

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

By using the two obtained results and the freshness assumption of rule (T Y-IA BS) to
instantiate a new (T Y-IA BS) rule, we reach the goal.
(T Y-IA PP)

Γ, α, Γ0 ` e1 with e2 : ρ1 ; E1 E2

From the two assumptions of rule (T Y-IA PP), the induction hypothesis and the definitionof substitution, we obtainΓ, Γ0 [σ /α] ` e1 [σ /α] : ρ2 [σ /α] ⇒ ρ1 [σ /α] ; E1 [|σ |/α]andΓ, Γ0 [σ /α] ` e2 [σ /α] : ρ2 [σ /α] ; E2 [|σ |/α]

By passing the two judgments above to rule (T Y-IA BS), we obtain the desired result.
(T Y-Q UERY)

Γ, α, Γ0 `?ρ : ρ ; E

From the first assumption of rule (T Y-Q UERY), where we consider deterministic resolution, and Lemma A.14 we getΓ, Γ0 [σ /α] `r ρ[σ /α] ; E[|σ |/α]

Passing the second assumption of rule (T Y-Q UERY) to Lemma A.20 results in`unamb ρ[σ /α]Then, we can instantiate rule (T Y-Q UERY) with the two obtained results above, to reachthe goal of this case.
Lemma A.20. If`unamb ρ
then`unamb ρ[σ /α]Proof. The proof proceeds by induction on the theorem’s third hypothesis, mutually with
the next proof. The only induction case of this proof, (UA-M AIN), is proved as a special
case (ᾱ = ε) of Lemma A.21, since naturally α ∈/ ε.
Lemma A.21. Ifᾱ `unamb ρ
and
α∈
/ ᾱ
then
ᾱ `unamb ρ[σ /α]Proof. The proof proceeds by induction on the theorem’s first hypothesis, mutually withthe previous proof.

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits(UA-S IMP)73ᾱ `unamb τWe need to show that ᾱ `unamb τ[σ /α], which can be satisfied only by (an appropriate
instance of) rule (UA-S IMP). Therefore, it suffices to show that ᾱ ⊆ ftv(τ[σ /α]), whereftv(τ[σ /α]) = (ftv(τ) \ {α}) ∪ ftv(σ ).
From the assumption of rule (UA-M AIN) and the second hypothesis of the theorem, we
have that ᾱ ⊆ ftv(τ) \ {α}. Then trivially it also holds that ᾱ ⊆ (ftv(τ) \ {α}) ∪ ftv(σ ).
(UA-TA BS)ᾱ `unamb ∀β .ρ

From the second hypothesis of the theorem and the adopted Barendregt convention, it
follows that α ∈/ ᾱ, β .
From the assumption of the rule and the induction hypothesis, we getᾱ, β `unamb ρ[σ /α]
By using this in rule (UA-TA BS) and from the definition of substitution, we reach the goal:ᾱ `unamb (∀β .ρ)[σ /α](UA-IA BS)

ᾱ, α, ᾱ 0 `unamb ρ1 ⇒ ρ2

Passing the first assumption of rule (UA-IA BS) to Lemma A.20 results in`unamb ρ1 [σ /α]From the second assumption of rule (UA-IA BS) and the induction hypothesis, we getᾱ `unamb ρ2 [σ /α]
By the definition of substitution and the last two obtained results used with rule (UA-IA BS),
we reach the goal:ᾱ `unamb (ρ1 ⇒ ρ2 )[σ /α]

A.6 Auxiliary Lemmas About the Unification Algorithm
This section concerns properties of the unification algorithm that are required by the proofsof the next sections. For this purpose, a notion of a partial order over substitutions is also
used.
Definition A.1 (Partial Order over Substitutions). A substitution θ1 is more general than asubstitution θ2 , denoted with θ2 v θ1 , iff there is a θ 0 such that θ2 = θ 0 · θ1 .
Lemma A.22 states that the unification algorithm produces a substitution that indeed
unifies its two input types.

ZU064-05-FPR

Main

74

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Lemma A.22. If
θ = unifyΓ;ᾱ (τ, τ 0 )thenθ (τ) = θ (τ 0 )andᾱ; Γ ` θ
Proof. Straightforward induction on the derivation.
We assume the following two properties of unification as given.
Assumption A.1 states that unifyΓ;ᾱ (τ, τ 0 ) is the most general unifier for τ and τ 0 .
Assumption A.1. If
θ (τ) = θ (τ 0 )andᾱ; Γ ` θthen
θ v unifyΓ;ᾱ (τ, τ 0 )Assumption A.2. If
θ (τ) = τ 0andᾱ; Γ ` θandᾱ ⊆ ftv(τ)
and∀α ∈ ᾱ, ∀β ∈ ftv(τ 0 ),β >Γ αthenθ = unifyΓ;ᾱ (τ, τ 0 )
A.7 Soundness of the Algorithmic wrt Deterministic Resolution
This section proves soundness of the resolution algorithm with respect to its declarative
specification. As summarized in the diagram below, the main lemma depends on threeauxiliary soundness lemmas, one for each of the algorithmic focusing, lookup and matching judgments. The dependencies of these proofs follow those of the definitions of thecorresponding judgments.
Interestingly, the proof for algorithmic lookup soundness also uses completeness of thealgorithmic stability judgment. The latter requires a correctness property of the unification
algorithm. One more auxiliary correctness property is used by the algorithmic matchingsoundness proof.

ZU064-05-FPR

Main

7 December 2018

10:26

75

Cochis: Stable and Coherent Implicits

Lemma A.23
Algorithmic
resolution issound wrt
det. resolution

Lemma A.24
Algorithmic
focusing issound wrt
det. focusing

Lemma A.25
Algorithmic
lookup is soundwrt det. lookup

Lemma A.26
Algorithmic
matching issound wrt
det. matching

Assum. A.1
Unification
algorithm
produces mostgen. unifier

Lemma A.31
Algorithmic
stability iscomplete wrt
det. matching

Lemma A.22
Unification
algorithm
unifiesLemma A.23. IfthenΓ `alg ρ ; EΓ `r ρ ; E

Proof. From the hypothesis it follows thattyvars(Γ); Γ `alg ρ ; E

Hence, by Lemma A.24 and rule (R-M AIN) the desired conclusion follows.
Lemma A.24. Ifthenᾱ; Γ `alg ρ ; E
ᾱ; Γ `r [ρ] ; E

Proof. The proof proceeds by induction on the derivation of the hypothesis.
Cases (A LG -R-IA BS) and (A LG -R-TA BS) follow from the isomorphism between therule sets of the two judgments. Case (A LG -R-S IMP) follows from Lemma A.25.
Lemma A.25. Ifthenᾱ; Γ; [Γ0 ] `alg ρ ; E
ᾱ; Γ; [Γ0 ] `r ρ ; E

Proof. The proof proceeds by induction on the derivation of the hypothesis.
(A LG -L-M ATCH)

ᾱ; Γ; [Γ0 , ?ρ ; x] `alg τ ; E[Ē/x̄]

ZU064-05-FPR

Main

7 December 2018

76

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

From the rule’s first hypothesis and Lemma A.26 we have
Γ; [ρ] ; E `r ρ̄ ; x̄; τ ; E 0
where θ = ε, as the only possibility such that ε; Γ ` θ . Then, using Lemma A.24 andrule (L-M ATCH) we conclude
ᾱ; Γ; [Γ0 , ?ρ ; x] `r τ ; E[Ē/x̄](A LG -L-N O M ATCH)

ᾱ; Γ; [Γ0 , ?ρ ; x] `alg τ ; E 0

From the rule’s second premise and the induction hypothesis we haveᾱ; Γ; [Γ0 ] `r τ ; E 0
From the rule’s first premise and the negation of Lemma A.31, there are no substitution,
θ , expression, E, and set of goals, Σ, such that both judgments below hold.
ᾱ; Γ ` θ

θ (Γ); [θ (ρ)] ; x `r Σ; θ (τ) ; E

andHence, with rule (L-N O M ATCH) we conclude
ᾱ; Γ; [Γ0 , ?ρ ; x] `r τ ; E 0(A LG -L-VAR)

ᾱ; Γ; [Γ0 , x : ρ] `alg τ ; E

From the rule’s hypothesis and the induction hypothesis we obtainᾱ; Γ; [Γ0 ] `r τ ; E
By rule (L-VAR) we conclude
ᾱ; Γ; [Γ0 , x : ρ] `r τ ; E(A LG -L-T Y VAR)ᾱ; Γ; [Γ0 , α] `alg τ ; E

From the rule’s hypothesis and the induction hypothesis we obtainᾱ; Γ; [Γ0 ] `r τ ; E
By rule (L-T Y VAR) we conclude
ᾱ; Γ; [Γ0 , α] `r τ ; E

ZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

77

Lemma A.26. If
ᾱ; Γ; [ρ] ; E ; Σ `alg Σ0 ; τ ; E 0

then, there is a substitution θ such thatᾱ; Γ ` θandfor Σ00 such that

θ (Γ); [θ (ρ)] ; |θ |(E) `r Σ00 ; θ (τ) ; E 0
Σ0 = θ (Σ), Σ00

Proof. The proof proceeds by induction on the derivation of the first hypothesis.
(A LG -M-S IMP)ᾱ; Γ; [τ 0 ] ; E ; Σ `alg θ (Σ); τ ; |θ |(E) with θ = unifyΓ;ᾱ (τ, τ 0 )From the hypothesis of the rule and Lemma A.22, it follows that ᾱ; Γ ` θ and θ (τ 0 ) =θ (τ). The latter allows us to use rule (M-S IMP), with which we obtain the goal judgment.
θ (Γ); [θ (τ 0 )] ; |θ |E `r ε; θ (τ 0 ) ; |θ |E(A LG -M-IA PP)

ᾱ; Γ; [ρ1 ⇒ ρ2 ] ; E ; Σ `alg Σ0 ; τ ; E 0

From the premise of the rule, the induction hypothesis and the definition of substitution,
there is a substitution θ such thatᾱ; Γ, ?ρ ; x ` θandθ (Γ), ?θ (ρ1 ) ; x; [θ (ρ2 )] ; |θ |(E x) `r Σ00 ; θ (τ) ; E 0

where Σ0 = θ (Σ, ρ1 ; x), Σ00 . From the first result, because θ regards only type variable
substitutions, it is easy to deduce
ᾱ; Γ ` θ
By rule (M-IA PP), applied on the second result of the induction hypothesis, we may
concludeθ (Γ); [θ (ρ1 ⇒ ρ2 )] ; |θ |(E) `r θ (ρ1 ; x), Σ00 ; θ (τ) ; E 0

Trivially, the last condition of the theorem holds, since Σ0 = θ (Σ), ((θ (ρ1 ; x), Σ00 ).
(A LG -M-TA PP)

ᾱ; Γ; [∀α.ρ] ; E ; Σ `alg Σ0 ; τ ; E 0

From the premise of the rule and the induction hypothesis, there is a substitution, θ ,such thatᾱ, α; Γ, α ` θ

ZU064-05-FPR

Main

78

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosianandθ (Γ, α); [θ (ρ)] ; |θ |(E α) `r Σ00 ; θ (τ) ; E 0
where Σ0 = θ (Σ), Σ00 .
By case analysis on the first result, it follows that θ = [σ /α] · θ 0 , where Γ ` σ andᾱ; Γ ` θ 0 . Note that α ∈/ ftv(τ). Therefore, the deterministic matching judgment above
can be refined toθ 0 (Γ); [θ 0 (ρ[[σ /α]])] ; |θ |0 (E |σ |) `r Σ00 ; θ 0 (τ) ; E 0
Hence, it follows from rule (M-TA PP) and the type well-formedness judgment for σthatθ 0 (Γ); [θ 0 (∀α.ρ)] ; |θ |0 (E) `r Σ00 ; θ 0 (τ) ; E 0

A.8 Completeness of the Algorithm wrt Deterministic Resolution
This section proves completeness of the resolution algorithm with respect to its declarative
counterpart. Like in Section A.7, the main lemma depends on three auxiliary completenesslemmas, one for each of the focusing, lookup and matching judgments. The dependenciesof these proofs follow those of the definitions of the corresponding declarative judgments.
In symmetry with the proof of the auxiliary lookup lemma for algorithmic soundness,the proof for algorithmic lookup completeness also uses soundness of the algorithmic
matching judgment, resulting in interdependent soundness and completeness proofs. Additionally, an auxiliary correctness property of the unification algorithm is necessary forproving completeness of algorithmic matching.

ZU064-05-FPR

Main

7 December 2018

10:26

79

Cochis: Stable and Coherent Implicits
Lemma A.27
Algorithmic
resolution iscomplete wrt
det. resolution

Lemma A.32
Alg. stability
implies alg.
matching

Assum. A.2
Unification
algorithm
matchesLemma A.28
Algorithmic
focusing iscomplete wrt
det. focusing

Lemma A.29
Algorithmic
lookup iscomplete wrt
det. lookup

Lemma A.30
Algorithmic
matching iscomplete wrt
det. matching

Lemma A.26
Algorithmic
matching issound wrt
det. matching

Lemma A.22
Unification
algorithm
unifiesLemma A.27. If`unamb Γand`unamb ρandthenΓ `r ρ ; EΓ `alg ρ ; E

Proof. From the third hypothesis it follows thattyvars(Γ); Γ `r [ρ] ; E

Hence, by Lemma A.28 and rule (A LG -R-M AIN) the desired conclusion follows
Γ `alg ρ ; E

ZU064-05-FPR

Main

7 December 2018

80

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Lemma A.28. If`unamb Γand`unamb ρandᾱ; Γ `r [ρ] ; E

thenᾱ; Γ `alg ρ ; E

Proof. The proof proceeds by induction on the derivation of the third hypothesis.
Cases (R-IA BS) and (R-TA BS) follow from the isomorphism between the rule sets ofthe two judgments. Case (R-S IMP) follows from Lemma A.29.
Lemma A.29. If`unamb Γ0andthenᾱ; Γ; [Γ0 ] `r ρ ; E
ᾱ; Γ; [Γ0 ] `alg ρ ; E

Proof. The proof proceeds by induction on the derivation of the second hypothesis.
(L-M ATCH)

ᾱ; Γ; [Γ0 , ?ρ ; x] `r τ ; E[Ē/x̄]

From the first hypothesis of the theorem, we derive that `unamb ρ. From the rule’s second
hypothesis and Lemma A.30, with θ = ε and α = ε, we haveε; Γ; [ρ] ; x; ε `alg ρ̄ ; x̄; τ ; E 0

Then, using Lemma A.28 and rule (A LG -L-M ATCH) we conclude
ᾱ; Γ; [Γ0 , ?ρ ; x] `alg τ ; E[Ē/x̄](L-N O M ATCH)

ᾱ; Γ; [Γ0 , ?ρ ; x] `r τ ; E 0

From the rule’s second hypothesis and the induction hypothesis we haveᾱ; Γ; [Γ0 ] `alg τ ; E 0

From the rule’s first hypothesis, there are no θ , Σ1 and E1 such that ᾱ; Γ ` θ andθ (Γ); [θ (ρ)] ; x `r E1 ; Σ1 ; τFrom the negation of Lemma A.26 and then the negation of Lemma A.32, we have:ᾱ; Γ; ρ 6`sta τZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

81

Hence with rule (A LG -L-N O M ATCH) we conclude
ᾱ; Γ; [Γ0 , ?ρ ; x] `alg τ ; E 0(L-VAR)ᾱ; Γ; [Γ0 , x : ρ] `r τ ; E

From the rule’s hypothesis and the induction hypothesis we obtainᾱ; Γ; [Γ0 ] `alg τ ; E

By rule (A LG -L-VAR) we conclude

ᾱ; Γ; [Γ0 , x : ρ] `alg τ ; E

ᾱ; Γ; [Γ0 , α] `r τ ; E(L-T Y VAR)

From the rule’s hypothesis and the induction hypothesis we obtainᾱ; Γ; [Γ0 ] `alg τ ; E

By rule (A LG -L-T Y VAR) we conclude

ᾱ; Γ; [Γ0 , α] `alg τ ; E
Lemma A.30. Ifθ (Γ); [θ (ρ)] ; |θ |(E) `r Σ0 ; τ ; E 0andᾱ `unamb ρanddom(θ ) ⊆ ᾱand∀α ∈ ᾱ, ∀β ∈ ftv(τ),β >Γ αthen, for all Σ,
ᾱ; Γ; [ρ] ; E ; Σ `alg θ (Σ), Σ0 ; τ ; E 0

Proof. The proof proceeds by induction on the derivation of the first hypothesis.
(M-S IMP)θ (Γ); [θ (τ 0 )] ; |θ |(E) `r ε; τ ; E 0with τ = θ (τ 0 ) and E 0 = |θ |(E)

From the second hypothesis of the theorem, we have that ᾱ ⊆ ftv(τ 0 ). By using this,
together with the third and fourth hypotheses of the theorem and the side condition thatτ = θ (τ 0 ), in Assumption A.2, we getθ = unifyΓ;ᾱ (τ, τ 0 )Trivially, from rule (A LG -M-S IMP) we haveᾱ; Γ; [τ 0 ] ; E ; Σ `alg θ (Σ); τ ; |θ |(E)

ZU064-05-FPR

Main

7 December 2018

10:26

82

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian(M-IA PP)θ (Γ); [θ (ρ1 ⇒ ρ2 )] ; |θ |(E) `r θ (ρ1 ) ; x, Σ0 ; τ ; E 0

From the hypothesis of the rule and the induction hypothesis, we have that∀Σ,ᾱ; Γ, ?ρ1 ; x; [ρ2 ] ; E x; Σ `alg θ (Σ), Σ0 ; τ ; E 0

Then, by choosing Σ = Σ00 , ρ1 ; x with any Σ00 , the above can be refined to∀Σ00 ,

ᾱ; Γ, ?ρ1 ; x; [ρ2 ] ; E x; Σ00 , ρ1 ; x `alg θ (Σ00 , ρ1 ; x), Σ0 ; τ ; E 0

By rule (A LG -M-IA PP) we may then conclude∀Σ00 ,(M-TA PP)ᾱ; Γ; [ρ1 ⇒ ρ2 ] ; E ; Σ00 `alg θ (Σ00 ), θ (ρ1 ) ; x, Σ0 ; τ ; E 0

θ (Γ); [θ (∀α.ρ)] ; |θ |(E) `r Σ0 ; τ ; E 0

From the definition of substitution and the premise of the rule, we have
θ (Γ); [θ (ρ)[σ /α]] ; |θ |(E |σ |) `r Σ0 ; τ ; E 0

The Barendregt convention allows us to asses that α ∈/ θ (Γ). Thus, we can consider θ 0 =[σ /α] · θ , for which it follows that dom(θ 0 ) ⊆ ᾱ, α. From the definition of substitution,
θ 0 (ρ) = θ (ρ)[σ /α]θ 0 (Γ, α) = θ (Γ)|θ 0 |(E α) = |θ |(E |σ |)Also, since α does not appear free in |θ |(E), the substitution [σ /α] does not affect it.
The premise of the rule can, then, be rewritten asθ 0 (Γ, α); [θ 0 (ρ)] ; |θ 0 |(E α) `r Σ0 ; τ ; E 0

From the second hypothesis of the theorem, we have thatᾱ, α `unamb ρand since α is fresh, it holds that for any β ∈ ftv(τ), β >Γ α. We can now use theinduction hypothesis, to obtainᾱ, α; Γ; [ρ] ; E α ; Σ `alg θ 0 (Σ), Σ0 ; τ ; E 0 ,Hence, it follows from rule (A LG -M-TA PP) thatᾱ; Γ; [∀α.ρ] ; E ; Σ `alg θ 0 (Σ), Σ0 ; τ ; E 0
Lemma A.31. Ifandθ1 (Γ); [θ1 (ρ)] ; E `r Σ0 ; θ1 (τ) ; E 0ᾱ; Γ ` θ1thenᾱ; Γ; ρ `sta τZU064-05-FPR

Main

7 December 2018

10:26

Cochis: Stable and Coherent Implicits

83

Proof. The proof proceeds by induction on the derivation of the first hypothesis.
(M-S IMP)θ1 (Γ); [θ1 (τ 0 )] ; E `r ε; θ1 (τ) ; E

where θ1 (τ) = θ1 (τ 0 )By Assumption A.1 applied on the second hypothesis of the theorem and the side
condition that θ1 (τ) = θ1 (τ 0 ), we getθ1 v unifyΓ;ᾱ (τ, τ 0 )Trivially, from rule (S TA -S IMP) we haveᾱ; Γ; τ 0 `sta τ(M-IA PP)

θ1 (Γ); [θ1 (ρ1 ⇒ ρ2 )] ; E `r θ1 (ρ1 ) ; x, Σ0 ; θ1 (τ) ; E 0

From the hypothesis of the rule and the induction hypothesis, we have thatᾱ; Γ, ?ρ1 ; x; ρ2 `sta τ

We can strengthen this—which we use without proof—to obtain:ᾱ; Γ; ρ2 `sta τ
Then, by rule (S TA -IA PP) we conclude
ᾱ; Γ; ρ1 ⇒ ρ2 `sta τ(M-TA PP)

θ1 (Γ); [θ1 (∀α.ρ)] ; E `r Σ0 ; θ1 (τ) ; E 0

From the definition of substitution and the first premise of the rule, we have
θ1 (Γ); [θ1 (ρ)[σ /α]] ; E |σ | `r Σ0 ; θ1 (τ) ; E 0

The Barendregt convention allows us to assess that α ∈/ dom(θ1 ). Thus, we can consider
θ 0 = [σ /α] · θ1 . By instantiating rule (S-C ONS) with the theorem’s second hypothesis
and the second premise of rule (M-TA PP), we haveᾱ, α; Γ, α ` θ 0
where, from the definition of substitution,
θ 0 (ρ) = θ1 (ρ)[σ /α] and θ 0 (Γ, α) = θ1 (Γ)
In addition, since α does not appear free in the type θ1 (τ), it follows that the substitution[σ /α] does not affect it. The premise of the rule can, then, be rewritten asθ 0 (Γ, α); [θ 0 (ρ)] ; E σ `r Σ0 ; θ 0 (τ) ; E 0

From the induction hypothesis, we have thatᾱ, α; Γ, α; ρ `sta τ,
Hence, it follows from rule (S TA -TA PP) thatᾱ; Γ; ∀α.ρ `sta τZU064-05-FPR

Main

84

7 December 2018

10:26

T. Schrijvers, B. Oliveira, P. Wadler and K. Marntirosian

Lemma A.32. If
ᾱ; Γ; ρ `sta τthen for all E, Σ there exist E 0 , Σ0 such thatᾱ; Γ; [ρ] ; E ; Σ `alg Σ0 ; τ ; E 0

Proof. The proof is straightforward induction on the derivation. The conclusion’s judgement is an annotated version of the hypothesis’ judgement.