�anti�ed Class Constraints

12

Gert-Jan Bo�u

3
4

KU Leuvengertjan.bo�u@student.kuleuven.be

5
6

8

10

13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

39

Abstract

which seemed to require instance declarations that were impossible
to express in the type-class system of Haskell at that time.
Unfortunately, Hinze and Peyton Jones never did elaborate on
quanti�ed class constraints. Later, Lämmel and Peyton Jones [21]found a workaround for the particular problem of the derivabletype classes work that did not involve quanti�ed class constraints.
Nevertheless the idea of quanti�ed class constraints has whet theappetite of many researchers and developers. GHC ticket #28931 ,requesting for quanti�ed lass constraints, was opened in 2008 andis still open today. Commenting on this ticket in 2009, Peyton
Jones states that “their lack is clearly a wart, and one that may
become more pressing”, yet clari�es in 2014 that “(t)he trouble is that
I don’t know how to do type inference in the presence of polymorphic
constraints.” In 2010, 10 years a�er the original idea, Hinze [10]rues that the feature has not been implemented yet. As recently as
2016, Chauhan et al. [5] regret that “Haskell does not allow the useof universally quanti�ed constraints” and now in 2017 Spivey [34]has to use pseudo-Haskell when modeling with quanti�ed classconstraints. While various workarounds have been proposed andare used in practice [20, 31, 36], none has stopped the clamor for
proper quanti�ed class constraints.
�is paper �nally elaborates the original idea of quanti�ed classconstraints into a fully �edged language design.
Speci�cally, the contributions of this paper are:

�anti�ed class constraints have been proposed many years ago
to raise the expressive power of type classes from Horn clauses
to �rst-order logic. Yet, while it has been much asked for over
the years, the feature was never implemented or studied in depth.
Instead, several workarounds have been proposed, all of which areultimately stopgap measures.
�is paper revisits the idea of quanti�ed class constraints andelaborates it into a practical language design. We show the meritof quanti�ed class constraints in terms of more expressive modelingand in terms of terminating type class resolution. In addition, we
provide a declarative speci�cation of the type system as well as a
type inference algorithm that elaborates into System F. Moreover,
we discuss termination conditions of our system and also provide a
prototype implementation.
CCS Concepts •�eory of computation →Type structures;•So�ware and its engineering →Functional languages;
Keywords Haskell, type classes, type inference
ACM Reference format:
Gert-Jan Bo�u, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira,and Philip Wadler. 2017. �anti�ed Class Constraints. In Proceedings of
ACM SIGPLAN Haskell Symposium 2017, Oxford, UK, September 7 – 8, 2017
(Haskell’17), 14 pages.
DOI: 10.475/123 4

40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

1

KU Leuventom.schrijvers@cs.kuleuven.be

University of Edinburgh
wadler@inf.ed.ac.uk• We provide an overview of the two main advantages of quanti�ed class constraints (Section 2):
1. they provide a natural way to express more of a type class’s
speci�cation, and2. they enable terminating type class resolution for a larger
class of applications.
• We elaborate the type system sketch of Hinze and Peyton Jones[12] for quanti�ed type class constraints into a full-�edged formalization (Section 3). Our formalization borrows the idea of
focusing from C����� [32], a calculus for Scala-style implicits [26, 27], and adapts it to the Haskell se�ing. We accountfor two notable di�erences: a global set of non-overlapping
instances and support for superclasses.
• We present a type inference algorithm that conservatively extends that of Haskell 98 (Section 4) and comes with a dictionarypassing elaboration into System F (Section 5).
• We discuss the termination conditions on a system with quanti�ed class constraints (Section 6).
• We provide a prototype implementation, which incorporates
higher-kinded datatypes and accepts all2 examples in this paper,at h�ps://github.com/gkaracha/quantcs-impl.

37
38

Tom Schrijvers

Philip Wadler

�e University of Hong Kong
bruno@cs.hku.hk

9

12

KU Leuvengeorgios.karachalias@cs.kuleuven.be

Bruno C. d. S. Oliveira

711Georgios Karachalias

Introduction

Since Wadler and Blo� [38] originally proposed type classes as ameans to make adhoc polymorphism less adhoc, the feature has
become one of Haskell’s cornerstone features. Over the years typeclasses have been the subject of many language extensions that
increase their expressive power and enable new applications. Examples of such extensions include: multi-parameter type classes [19];functional dependencies [18]; or associated types [4].
Several of these implemented extensions were inspired by theanalogy between type classes and predicates in Horn clauses. Yet,
Horn clauses have their limitations. As a small side-product of
their work on derivable type classes, Hinze and Peyton Jones [12]have proposed to raise the expressive power of type classes toessentially �rst-order logic with what they call quanti�ed classconstraints. �eir motivation was to deal with higher-kinded types
Permission to make digital or hard copies of part or all of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor pro�t or commercial advantage and that copies bear this notice and the full citationon the �rst page. Copyrights for third-party components of this work must be honored.
For all other uses, contact the owner/author(s).
Haskell’17, Oxford, UK© 2017 Copyright held by the owner/author(s). 123-4567-24-567/08/06. . . $15.00
DOI: 10.475/123 4

1 h�ps://ghc.haskell.org/trac/ghc/ticket/2893

2 except for the HFunctor example (Section 2.1), which needs higher-rank types [28].

1Haskell’17, September 7 – 8, 2017, Oxford, UK
1
2
3
4
5

2

Bo�u et al.

Motivation

nested datatypes [3]. For instance, Hinze [10] represents perfectbinary trees with the nested datatype�is section illustrates the expressive power a�orded by quanti�edclass constraints to capture several requirements of type class instances more succinctly, and to provide terminating resolution fora larger group of applications.

data Perfect a = Zero a | Succ (Perfect (a,a))

�is can be expressed with the generic representation as Mu HPerf ,the �xpoint of the second-order functor HPerf , de�ned as

6
7

2.1

8

Monad Transformers Consider the MTL type class for monadtransformers [15]:

9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

Precise and Succinct Speci�cations

data HPerf f a = HZero a | HSucc ( f (a,a))Johann and Ghani’s notion of second-order functor di�ers slightly
from Hinze’s.3 Ideally, their notion would be captured by the following class declaration:

class Trans t whereli� :: Monad m ⇒ m a → (t m) aclass (∀f .Functor f ⇒ Functor (h f )) ⇒ HFunctor h where
hfmap :: (Functor f , Functor д)⇒ (∀x .f x → д x ) → (∀x .h f x → h д x )What is not formally expressed in the above type class declaration,
but implicitly expected, is that for any type T that instantiates Trans
there should also be a Monad instance of the form:

Like in Hinze’s case, the quanti�ed class constraint expresses thata second-order functor takes �rst-order functors to �rst-order functors. Additionally, second-order functors provide a second-orderfmap, called hfmap, which replaces replaces f by д, to take valuesof type h f x to type h д x. Yet, in the absence of actual support forquanti�ed class constraints, Johann and Ghani provide the following declaration instead:instance Monad m ⇒ Monad (T m) where . . .

Because the type checker is not told about this requirement, it will
not accept the following de�nition of monad transformer composition.
newtype (t 1 ∗ t 2 ) m a = C { runC :: t 1 (t 2 m) a }class HFunctor h where�map :: Functor f ⇒ (a → b) → (h f a → h f b)
hfmap :: (Functor f , Functor д)⇒ (∀x .f x → д x ) → (∀x .h f x → h д x )instance (Trans t 1 , Trans t 2 ) ⇒ Trans (t 1 ∗ t 2 ) whereli� = C · li� · li��e idea of this code is to li� from monad m to (t 2 m) and then toli� from (t 2 m) to t 1 (t 2 m). However, the second li� is only valid if(t 2 m) is a monad and the type checker has no way of establishingthat this fact holds for all monad transformers t 2 . Workarounds
for this problem do exist in current Haskell [13, 31, 36], but theyclu�er the code with heavy encodings.
�anti�ed class constraints allow us to state this requirement
explicitly as part of the Trans class declaration:

In essence, they inline the fmap method provided by the quanti�edclass constraint in the HFunctor class. �is is unfortunate because
it duplicates the Functor class’s functionality.
2.2

Terminating Corecursive Resolution

�anti�ed class constraints were �rst proposed by Hinze and Peyton Jones [12] as a solution to a problem of diverging type classresolution. Consider their generalized rose tree datatypeclass (∀m.Monad m ⇒ Monad (t m)) ⇒ Trans t whereli� :: Monad m ⇒ m a → (t m) a

data GRose f a = GBranch a ( f (GRose f a))

�e instance for transformer composition t 1 ∗ t 2 now typechecks.

and its Show instanceinstance (Show a, Show ( f (GRose f a))) ⇒ Show (GRose f a)where show (GBranch x xs) = unwords [show x, �−�, show xs]

Second-Order Functors Another example can be found in thework of Hinze [11]. He represents parameterized datatypes, likepolymorphic lists and trees, as the �xpoint Mu of a second-orderfunctor:data Mu h a = In { out :: h (Mu h) a }Notice the two constraints in the instance context which are dueto the two show invocations in the method de�nition. Standard
recursive type class resolution would diverge when faced with theconstraint (Show (GRose [] Bool)). Indeed, it would recursively
resolve the instance context: Show Bool is easily dismissed, but
Show [GRose [] a] requires resolving Show (GRose [] Bool) again.
Clearly this process loops.
To solve this problem, Hinze and Peyton Jones proposed to write
the GRose instance with a quanti�ed type class constraint as:

data List2 f a = Nil | Cons a ( f a)
type List = Mu List2

A second-order functor h is a type constructor that sends functors
to functors. �is can be concisely expressed with the quanti�edclass constraint ∀f .Functor f ⇒ Functor (h f ), for example in the
Functor instance of Mu:

instance (Show a,∀x .Show x ⇒ Show ( f x )) ⇒ Show (GRose f a)where show (GBranch x xs) = unwords [show x, �−�, show xs]

instance (∀f .Functor f ⇒ Functor (h f )) ⇒ Functor (Mu h)
where fmap f (In x ) = In (fmap f x )�is would avoid the diverging loop in the type system extension
they sketch, because the two recursive resolvents, Show Bool and∀x .Show x ⇒ Show [x] are readily discharged with the available
Bool and [a] instances.
When faced with the same looping issue in their Scrap Your
Boilerplate work, Lämmel and Peyton Jones [22] implemented a

Although this is Hinze’s preferred formulation he remarks that:
Unfortunately, the extension has not been implemented
yet. It can be simulated within Haskell 98 [36], but
the resulting code is somewhat clumsy.
Johann and Ghani use essentially the same data-generic representation, the �xpoint of second-order functors, to represent so-called

3 It is more in line with the category theoretical notion of endofunctors over the

category of endofunctors.
2�antified Class Constraints
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

di�erent solution: cycle-aware constraint resolution. �is approachdetects that a recursive resolvent is identical to one of its ancestors
and then ties the (co-)recursive knot at the level of the underlying
type class dictionaries.
Unfortunately, cycle-aware resolution is not a panacea. It only
deals with a particular class of diverging resolutions, those thatcycle. �e �xpoint of the second-order functor HPerf presented
above is beyond its capabilities.

x,y,z, f ::= �term variable name�a,b,c::= �type variable name�TC::= �class name�

instance (Show (h (Mu h) a)) ⇒ Show (Mu h a) whereshow (In x ) = show x

e ::= x | λx .e | e 1 e 2 | let x = e 1 in e 2

Resolving Show (Mu HPerf Int) diverges without cycling back to
the original constraint due to the nestedness of the perfect treetype:

A ::= • | A, C
C ::= Q | C1 ⇒ C2 | ∀a.C
Q ::= TC τ

axiom set
constraintclass constraint

�
�
�
�
�

21
22
23
24

28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

Show (Mu HPerf Int)
Show (HPerf (Mu HPerf ) Int)
Show Int, Show (Mu HPerf (Int, Int))
Show (HPerf (Mu HPerf ) (Int, Int))
Show (Int, Int), Show (Mu HPerf ((Int, Int), (Int, Int)))...

Γ ::= • | Γ,x : σ | Γ,aP ::= �AS , AI , AL �

Types also appear in Figure 1. Like all extensions of the DamasMilner system [6] with quali�ed types [14], we discriminate between monotypes τ , quali�ed types ρ and type schemes σ . Note
that, to avoid clu�er, our formalization does not feature higherkinded types, but our prototype implementation does.
Our calculus di�ers from Haskell’98 in that it conservatively generalizes the language of constraints. In Haskell’98 the constraints
that can appear in type signatures and in class and instance contexts
are basic class constraints Q of the form TC τ . As a consequence,the constraint schemes or axioms that are derived from instances(and for superclasses) are Horn clauses of the form:

In contrast, with quanti�ed type class constraints we can formulate
the instances in a way that resolution does terminate.
instance (Show a,∀f x .(Show x,∀y.Show y ⇒ Show ( f y)) ⇒ Show (h f x ))⇒ Show (Mu h a) where show (In x ) = show x

instance (Show a,∀x .Show x ⇒ Show ( f x )) ⇒ Show (HPerf f a)where show (HZero a) = �(Z � ++ show a ++ �)�
show (HSucc xs)= �(S � ++ show xs ++ �)�
2.3

Summary

In summary, quanti�ed type class constraints enable 1) expressing
more of a type class’s speci�cation in a natural and succinct manner, and 2) terminating type class resolution for a larger group of
applications.
In the remainder of this paper we provide a declarative typesystem for a Haskell-like calculus with quanti�ed class constraints(Section 3). Type inference is shown in Section 4 and Section 5 provides an elaboration into System F. Section 6 presents the conditions
we require to ensure termination in the presence of quanti�ed classconstraints. Finally, Section 7 discusses related work and Section 8
concludes.

3∀a.Q1 ∧ . . . ∧ Qn ⇒ Q0

�ese axioms are similar to rank-1 polymorphic types in the sensethat the quanti�ers (and the implication) only occur on the outside.
We allow a more general form of constraints C where, in analogy
with higher-rank types, quanti�ers and implications occur in nested
positions. �is more expressive form of constraints can occur insignatures and class/instance contexts. Consequently, the syntactic
sort C of constraints and axioms is one and the same.
Note that constraint schemes of the form ∀ā.(Q 1 ∧ . . . ∧ Q n ) ⇒Q 0 , used in earlier formalizations of type classes (e.g., [25]), arenot valid syntax for our constraints C because we do not provide anotation for conjunction. Yet, we can easily see the scheme notation
as syntactic sugar for a curried representation:

Declarative Type System

�is section provides the declarative type system speci�cation forour core Haskell calculus with quanti�ed class constraints.

53
54
55
56
57
58
59
60
61

3.1

typing environment
program theory

Figure 1. Source Syntax∀ā.(Q1 ∧ · · · ∧ Qn ) ⇒ Q0

51
52

term
monotype
quali�ed type
type scheme

20

27

programclass decl.
instance decl.

τ ::= a | τ1 → τ2
ρ ::= τ | C ⇒ ρσ ::= ρ | ∀a.σ

19

26

pgm ::= e | cls; pgm | inst; pgm
cls ::= class A ⇒ TC a where { f :: σ }inst ::= instance A ⇒ TC τ where { f = e }instance (Show a, Show ( f (a,a))) ⇒ Show (HPerf f a) whereshow (HZero a) = �(Z � ++ show a ++ �)�
show (HSucc xs) = �(S � ++ show xs ++ �)�

18

25

Haskell’17, September 7 – 8, 2017, Oxford, UK

Syntax≡∀ā.Q1 ⇒ (. . . (Qn ⇒ Q0 ) . . . )We denote a list of C-constraints as A, short for axiom set as we
use them to represent, among others, axioms given through typeclass instances.
Finally, Figure 1 presents typing environments Γ, which areentirely standard, and the program theory P. �e la�er is a tripleof three axiom sets: the superclass axioms AS , the instance axioms
AI and local axioms AL . We use the notation P,L C to denote that
we extend the local component of the triple, and similar notation

Figure 1 presents the, mostly standard, syntax of our source language. A program pgm consists of class declarations cls, instancedeclarations inst and a top-level expression e. For simplicity, eachclass has a single parameter and a single method.
Terms e comprise a λ-calculus extended with let-bindings. By
convention, we use f to denote a method name and x, y, z to denoteany kind of term variable name.
3Haskell’17, September 7 – 8, 2017, Oxford, UK
1
2

Term Typing

P; Γ �tm e : σ(x : σ ) ∈ Γ

3P; Γ �tm x : σ4Γ �ty τ1
P; Γ,x : τ1 �tm e : τ2

5
6
7

P; Γ �tm λx .e : τ1 → τ28910

Γ �cls cls : AS ; Γc

(→I)

12

14

P; Γ �inst inst : AIP; Γ,x : τ �tm e 1 : τT�V��P; Γ �tm e 1 : τ1 → τ2
P; Γ �tm e 2 : τ1
P; Γ �tm e 1 e 2 : τ2

P; Γ,x : τ �tm e 2 : σP; Γ �tm (let x = e 1 in e 2 ) : σ(→E)Γ �ct C
P,L C; Γ �tm e : ρ

P; Γ �tm e : C ⇒ ρ

(⇒I)

16
17

P; Γ �tm e : C ⇒ ρ
P; Γ |= C
P; Γ �tm e : ρΓ,a �ct Ci

Figure 2. Declarative Type System (Selected Rules)

20

24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

for the other components. In earlier type class formalizations theseseparate kinds of axioms are typically con�ated into a single axiom
set. However, in this paper it is convenient to distinguish themfor accurately stating the di�erent restrictions imposed on them.
Moreover, it is instructive for contrasting with regular Haskell. In
our se�ing, all three components support the same general form of
axioms. In contrast, in Haskell, the local constraints are basic typeclass constraints Q only, while the instance and superclass axioms
have the more expressive Horn clause form.
3.2

P; Γ �tm e : ∀a.σ
Γ �ty τP; Γ �tm e : [a �→ τ ]σ

(∀E)

C����

P,L A,L TC τ ; Γ,b �tm e : [τ /a]σ

19

23

(∀I)

Class Instance Typing

P; Γ �inst instance A ⇒ TC τ where { f = e } : [∀b.A ⇒ TC τ ]

22

(⇒E)

Γ,a �ty σ

1821P; Γ,a �tm e : σP; Γ �tm e : ∀a.σΓ �cls class (C1 , . . . , Cn ) ⇒ TC a where { f :: σ } : [∀a.TC a ⇒ Ci ]; [f : ∀a.TC a ⇒ σ ]b = fv(τ )Γ,b �ax A
P,L A; Γ,b |= [τ /a]Ci
class (C1 , . . . , Cn ) ⇒ TC a where { f :: σ }

15

T�L��

Class Declaration Typing

11

13

Bo�u et al.

I�������

In addition to checking the well-formedness of the method type,
we ensure that the class context (C1 , . . . , Cn ) is also well-formed,
extending the environment with the local variable a. In turn, this
implies that fv(Ci ) ⊆ {a}, in line with the Haskell standard.
As usual, typing a class declaration extends the typing environment with the method typing, and the program’s theory with thesuperclass axioms. For instance, the extended monad transformerclass yields the superclass axiom:

�e Type System∀t .Trans t ⇒ (∀m.Monad m ⇒ Monad (t m))

Figure 2 presents the main judgments of our declarative type system
for the language of Figure 1, namely term typing and typing ofclass and instance declarations.

Class Instance Typing Instance typing takes the form P; Γ �inst
inst : AI and is given by Rule I�������, also presented in Figure 2.
We check the well-formedness of the instance context A under the extended typing environment, and that each superclassconstraint Ci is entailed by the instance context.
Finally, we check that the method implementation e has the typeindicated by the class declaration, appropriately instantiated forthe instance in question.

Type & Constraint Well-Scopedness �e judgments for wellscopeness of types, constraints and axiom sets are denoted Γ �ty σ ,Γ �ct C and Γ �ax A respectively. �eir de�nitions are straightforward
and can be found in Appendix A.
Term Typing Term typing takes the form P; Γ �tm e : σ and can beread as “under program theory P and typing environment Γ, expression e has type σ ”. �e rules are almost literally those of Chakravarty
et al. [4]. �ere are only two di�erences, which are simpli�cations
for the sake of convenience. Firstly we adopt the Barendregt convention [2], that variables in binders are distinct, throughout thispaper. �is allows us to omit explicit freshness conditions. Secondly, following Vytiniotis et al. [37] we have opted for recursive
let-bindings that are not generalized.
Apart from that, there are no noticeable di�erences with conventional Haskell in the typing rules. All the interesting di�erences
are concentrated in the de�nition of the constraint entailment judgment P; Γ |= C, which is used in the constraint elimination Rule(⇒E). �e de�nition of this auxiliary judgment is discussed in detailin Section 3.3.

Program Typing �e judgment for program typing ties everything together and takes the form P; Γ �pgm pgm : σ . Its de�nition isstraightforward and can be found in Appendix A.
3.3

Constraint Entailment

Following the approach of Schrijvers et al. [32] for their C�����
calculus, we present constraint entailment in two steps. First, we
provide an easy-to-understand and expressive, yet also highly ambiguous, speci�cation. �en we present a syntax-directed, semialgorithmic variant that takes the ambiguity away, but has a more
complicated formulation inspired by the focusing technique usedin proof search [1, 23, 24].

Class Declaration Typing Typing for class declarations takes
the form Γ �cls cls : AS ; Γc and is given by Rule C����, presented in
Figure 2.
4

Declarative Speci�cation Constraint entailment takes the form
P; Γ |= C, and its high-level declarative speci�cation is given by the�antified Class Constraints
1

Haskell’17, September 7 – 8, 2017, Oxford, UK

following rules:

2
3
4
5
6

C∈P

P; Γ |= C

8P; Γ |= C1 ⇒ C2

9

11
12
13
14
15
16
17
18
19
20
21
22

27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

P; Γ |= [τ /a]CP; Γ |= C1 ⇒ C2
P; Γ |= C1

Eq a ∈ P

P; Γ |= Eq a

24

26

(⇒IC)

(∀IC)

P; Γ |= C2

versusEq a ∈ P �P � ; Γ |= Eq a

(S���C)

P; Γ |= Eq a ⇒ Eq a(⇒IC)

P; Γ |= Eq a

P; Γ |= Eq a

P; Γ |= [C](∀EC)
P; Γ |= [C]P; Γ |= C

Constraint Resolution
P,L C1 ; Γ |= [C2 ]P; Γ |= [C1 ⇒ C2 ](⇒EC)

P; Γ,b |= [C](⇒R)

C ∈ P : Γ; [C] |= Q � A

P; Γ |= [∀b.C](∀R)∀Ci ∈ A : P; Γ |= [Ci ]P; Γ |= [Q](QR)

Constraint Matching

Γ; [C] |= Q � A

Γ; [C2 ] |= Q � A

Γ; [C1 ⇒ C2 ] |= Q � A, C1

Γ; [[τ /b]C] |= Q � AΓ; [∀b.C] |= Q � AΓ �ty τ

(∀L)

(⇒L)

Γ; [Q] |= Q � •(QL)

Figure 3. Tractable Constraint Entailment(S���C)Eq a ∈ P

Constraint Entailment

P; Γ |= C

If we interpret constraints C as logical formulas, the above rules
are nothing more than the rules of �rst-order predicate logic. Rule
(S���C) is the standard axiom rule. Rules (⇒IC) and (⇒EC) correspond to implication introduction and elimination, respectively.
Similarly, Rules (∀IC) and (∀EC) correspond to introduction andelimination of universal quanti�cation, respectively. �ese are alsoessentially the rules Hinze and Peyton Jones [12] propose.
While compact and elegant, there is a serious downside to theserules: �ey are highly ambiguous and give rise to many triviallydi�erent proofs for the same constraint. For instance, assumingΓ = •,a and P = �•, •, Eq a�, here are only two of the in�nitely
many proofs of P; Γ |= Eq a:

23

25

P; Γ |= ∀a.C

P,L C1 ; Γ |= C2

7

10(S���C)P; Γ,a |= C

P; Γ |= ∀a.C
Γ �ty τgoal and there are no new goals. Rule (⇒L) handles an implication
axiom C1 ⇒ C2 by recursively checking whether C2 matches thegoal. At the same time it yields a new goal C1 which needs to beentailed in order for the axiom to apply. Finally, Rule (∀L) handles
universal quanti�cation by instantiating the quanti�ed variable ina way that recursively yields a match.
It is not di�cult to see that this type-directed formulation ofentailment greatly reduces the number of proofs for given goal.4
For instance, for the example above there is only one proof:(S���C)(⇒EC)

where P � = P,L Eq a. Observe that the la�er proof makes an unnecessary appeal to implication introduction.

Eq a ∈ P

Type-Directed Speci�cation To avoid the trivial forms of ambiguity like in the example, we adopt a solution from proof search
known as focusing [1]. �is solution was already adopted by theC����� calculus, for the same reason. �e key idea of focusing is toprovide a syntax-directed de�nition of constraint entailment where
only one inference rule applies at any given time.
Figure 3 presents our de�nition of constraint entailment withfocusing. �e main judgment P; Γ |= C is de�ned in terms of two
auxiliary judgments, P; Γ |= [C] and Γ; [C] |= Q � A, each ofwhich is de�ned by structural induction on the constraint enclosed
in square brackets.
�e main entailment judgment is equivalent to the �rst auxiliary
judgment P; Γ |= [C]. �is auxiliary judgment focuses on theconstraint C whose entailment is checked – we call this constraint
the “goal”. �ere are three rules, for the three possible syntactic
forms of C. Rules (⇒R) and (∀R) decompose the goal by applying
implication and quanti�er introductions respectively. Once thegoal is stripped down to a simple class constraint Q, Rule (QR)
selects an axiom C from the theory P to discharge it. �e selectedaxiom must match the goal, a notion that is captured by the second
auxiliary judgment. Matching gives rise to a sequence A of new (andhopefully simpler) goals whose entailment is checked recursively.
�e second auxiliary judgment Γ; [C] |= Q � A focuses on theaxiom C and checks whether it matches the simple goal Q. Again,
there are three rules for the three possible forms the axiom can take.
Rule (QL) expresses the base case where the axiom is identical to theΓ; [Eq a] |= Eq a � • (QL)

P; Γ |= [Eq a](QR)

P; Γ |= Eq a

3.4

Remaining Nondeterminism

While focusing makes the de�nition of constraint entailment typedirected, there are still two sources of nondeterminism. As a consequence, the speci�cation is still ambiguous and not an algorithm.
Overlapping Axioms �e �rst source of non-determinism is thatin Rule (QR) there may be multiple matching axioms that make theentailment go through. For applications of logic where proofs areirrelevant this is not a problem, but in Haskell where the proofs havecomputational content (namely the method implementations) thisis a cause for concern. Haskell’98 also faces this problem. Consider
two instances for the same type:class Default a where { default :: a }instance Default Bool where { default = True }instance Default Bool where { default = False }�e two instances give rise to two di�erent proofs for Default Bool,with distinct computational content (True vs. False). We steer awayfrom this problem in the same was as Haskell’98, by requiring that
instance declarations do not overlap. �is does not rule out thepossibility of distinct proofs for the same goal, but at least distinct
4 Without loss of expressive power. See for example [30].

5Haskell’17, September 7 – 8, 2017, Oxford, UK
1
2

proofs have the same computational content. Consider a classhierarchy where C is the superclass of both D and E.

3

5
6

8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

a �unamb Ca �unamb Q(QU)a,a �unamb Ca �unamb ∀a.C(∀U)

unamb(C1 )a �unamb C2

a �unamb C1 ⇒ C2(⇒U)

Figure 4. Unambiguity
type inference. �e parts of the rules highlighted in gray concern
elaboration and are discussed in Section 5.
To make the connection to the relations of the declarative speci�cation (Section 3.2) more clear, corresponding rules share thesame name.
4.1

Preliminaries

Before diving into the details of the algorithm, we �rst introduce
some additional notation and constructs.
Variable-Annotated Constraints & Type Equalities Since ourgoal is to perform type inference and elaboration to System F simultaneously, we annotate all constraints with their corresponding
System F evidence term (dictionary variable d). We keep the notational burden minimal by reusing the same le�ers as in Figure 1,
yet with a calligraphic font:�e third instance gives rise to the axiom ∀a.C a ⇒ D Int. When
resolving D Int with this axiom we can choose a to be either Charor Bool and thus select a di�erent C instance.
Haskell’98 avoids this problem by requiring that all quanti�ed
type variables, like a in the example, appear in the head of theaxiom. Because our axioms have a more general, recursively nested
form, we generalize this requirement in a recursively nested fashion.
�e predicate unamb(C) in Figure 4 formalizes the requirementin terms of the auxiliary judgment a �unamb C, where a are typevariables that need to be determined by the head of C. Rule (QU)
constitutes the base case where Q is the head and contains thedeterminable type variables a. Rule (∀U) processes a quanti�er
by adding the new type variable to the list of determinable typevariables a. Finally, Rule (⇒U) checks whether the head C2 of theimplication determines the type variables a. It also recursively
checks whether C1 is unambiguous on its own. �e la�er check isnecessary because le�-hand sides of implications are themselves
added as axioms to the theory in Rule (⇒R); hence they must be
well-behaved on their own.
�e predicate unamb(C) must be imposed on all constraints thatare added to the theory. �is happens in four places: the instanceaxioms added in Rule I�������, the superclass axioms added inRule C����, the local axioms added when checking against a given
signature in Rule (⇒I) and the local axioms added during constraint
entailment checking in Rule (⇒R). �ese four places can be traced
back to three places in the syntax: class and instance heads, and(method) signatures.

4

U����

Unambiguitya ⊆ fv(Q)instance C Char where { . . . }instance C Bool where { . . . }instance C a ⇒ D Int where { . . . }27

29

unamb(C)Guessing Polymorphic Instantiation A second source of ambiguity is that Rule (∀L) requires guessing an appropriate type τ forsubstituting the type variable b. Guessing is problematic because
there are an in�nite number of types to choose from and more than
one of those choices can make the entailment work out. Choosing
an appropriate type is a problem for the type inference algorithm
in the next section. Di�erent choices leading to di�erent proofs is amore fundamental problem that also manifests itself in Haskell’98.
Consider the following instances.

26

28• �unamb C

�is gives rise to the superclass axioms ∀a.D a ⇒ C a and ∀a.E a ⇒C a. Given additionally two local constraints D τ and E τ , we have
two ways to establish C τ . �e proofs are distinct, yet ultimately
the computational content is the same. �is is easy to see as only
instances supply the computational content and there can be at
most one instance for any given type τ .
In summary, non-overlap of instances is su�cient to ensure
coherence.

25

Unambiguity

unamb(C)class C a where { . . . }class C a ⇒ D a where { . . . }class C a ⇒ E a where { . . . }4

7Bo�u et al.

P ::= �AS , A I , A L �
A ::= • | A, C
C ::= d : C
Q ::= d : Qvariable-annotated theory
variable-annotated axiom set
variable-annotated constraint
variable-annotated class constraint

Additionally, like every HM(X)-based system, our type-inference
algorithm proceeds by �rst generating type constraints from theprogram text (constraint generation) and then solving these constraints independently of the program text (constraint solving).
During constraint generation, our algorithm gives rise to both(variable-annotated) constraints A, as well as type equalities E:
E ::= • | E,τ1 ∼ τ2

type equalitiesθ ::= • | θ · [τ /a]η ::= • | η · [t/d]type substitution
evidence substitution

Type & Evidence Substitutions Furthermore, we introduce twokinds of substitutions: type substitutions θ and dictionary substitutions η:

A type substitution θ maps type variables to monotypes, while anevidence substitution η maps dictionary variables d to System F
terms t (see Section 5.1 for the formal syntax of System F terms).
4.2

Constraint Generation For Terms

Figure 5 presents constraint generation for terms. �e relation takes
the form Γ �tm e : τ � t | A; E. Given a typing environment Γ anda term e we infer (1) a monotype τ , (2) a set of wanted constraints
A, and (3) a set of wanted equalities E. Its de�nition is standard.
Rule T�V�� handles variables. We instantiate the polymorphic
type ∀a.C ⇒ τ of a term variable x with fresh uni�cation variables b, introducing C as wanted constraints, instantiated likewise.
Rule T�A�� assigns a fresh uni�cation variable to the abstracted

Type Inference

We provide a type inference algorithm with elaboration into System
F [8]. To simplify the presentation, this section focuses solely on
6�antified Class Constraints
12

Γ �tm e : τ � t | A; E

Term Typingb, d fresh(x : ∀a.C ⇒ τ ) ∈ Γ

3
4
5
6

Haskell’17, September 7 – 8, 2017, Oxford, UKΓ �tm x : [b/a]τ � x b d | ( d : [b/a]C); •a fresh7T�V��Γ,x : a �tm e : τ � t | A; EΓ �tm λx .e : a → τ � λ(x : a).t | A; E

8
9

T�A��

a freshΓ,x : a �tm e 1 : τ1 � t 1 | A1 ; E1
Γ,x : τ1 �tm e 2 : τ2 � t 2 | A2 ; E2
�ty τ1 � υ 1

Γ �tm let x = e 1 in e 2 : τ2 � let x : υ 1 = t 1 in t 2 | (A1 , A2 ); (E1 , E2 ,a ∼ τ1 )a freshΓ �tm e 1 : τ1 � t 1 | A1 ; E1

Γ �tm e 2 : τ2 � t 2 | A2 ; E2

Γ �tm e 1 e 2 : a � t 1 t 2 | (A1 , A2 ); (E1 , E2 ,τ1 ∼ τ2 → a)

T�L��

T�A��

Figure 5. Constraint Generation for Terms with Elaboration

10
11
12
13
14
15
16
17

term variable x, and adds it to the context for checking the bodyof the abstraction. Rule T�A�� handles applications (e 1 e 2 ). We
collect wanted class and equality constraints from each subterm,
we generate a fresh type variable a for the result and record thatthe type of e 1 is a function type (τ1 ∼ τ2 → a). Rule T�L�� handles(possibly recursive) let bindings.

a; P |= A1 � A2 ; η�C ∈ A1 : a; P |= [C] � A2 ; ηa; P |= A1 � A1 ; •a; P |= [C] � A2 ; η 1

4.3

20

�e type class and equality constraints derived from terms are
solved with the following two algorithms.

21
22
23
24
25
26
27
28
29
30
31
32
33

Constraint Solving

44
45

f x = [x] == [x]

34
35
36
37
38
39
40
41
42
43

46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

�ct C1 � υ 1
�d ,d 1 ,d 2 freshS���a; P,L ( d 1 : C1 ) |= [ d 2 : C2 ] � ( d : C) ; ηη � = [λ(d 1 : υ 1 ).[d � d 1 /d](η(d 2 ))/d 0 ]a; P |= [ d 0 : C1 ⇒ C2 ] � ( d � : C1 ⇒ C) ; η ��d ,d C freshη = [Λb.[d � b/d](η(d C ))/d 0 ](∀R)

a; P |= [ d 0 : ∀b.C0 ] � ( d � : ∀b.C) ; η �C ∈ P : a; [C] |= Q � A; θ ; ηa; P |= [Q] � A ; η

a; [C] |= Q � A; θ ; η

d 1 ,d 2 fresh(QR)

Constraint Matchinga; [ d 2 : C2 ] |= Q � A; θ ; ηa; [ d : C1 ⇒ C2 ] |= Q � A, d 1 : θ (C1 ); θ ; [d d 1 /d 2 ] · ηd � fresha; [ d � : C] |= Q � A; θ ; ηa; [ d : ∀b.C] |= Q � A; θ ; [d (θ (b))/d � ] · ηθ = unify(a; τ1 ∼ τ2 )a; [ d : TC τ1 ] |= d : TC τ2 � •; θ ; [d �/d]�(⇒R)

a,b; P |= [ d C : C0 ] � ( d : C) ; η

�

(⇒L)

(∀L)

(QL)

Figure 6. Constraint Entailment with Dictionary Construction

Haskell simpli�es the derived constraint Eq [a] to Eq a, yielding
the signature ∀a.Eq a ⇒ a → Bool.

Simpli�cation Auxiliary judgment a; P |= [C] � A ; η uses
the theory P to simplify a single constraint C to a set of simpler
constraints without instantiating any of the untouchable type variables a. Following the focusing approach, the judgment is de�nedby three rules, one for each of the syntactic forms of the goal C.
Rules (⇒R) and (∀R) recursively simplify the head of the goal.
Observe that we add the bound variable b to the untouchables awhen going under a binder in Rule (∀R). Once the goal is stripped
down to a simple class constraint Q, Rule (QR) selects an axiom
C whose head matches the goal, and uses it to replace the goalwith a set of simpler constraints A (a process known as context

a; P |= A1 , A2 � A3 ; η 2Constraint Simpli�cationa; P |= [C] � A ; η

Solving Equality Constraints We solve a set of equality constraints E by means of uni�cation. �e function unify(a; E) = θ ⊥takes the set of equalities and a set of “untouchable” type variables,and returns either the most general uni�er θ of the equalities or fails
if none exists. �e untouchable type variables a originate from typesignatures; all other type variables are uni�cation variables. �euni�er is of course only allowed to substitute uni�cation variables.
�e de�nition of this uni�cation function is folklore, following
Damas and Milner [6] and accounting for signatures; it can befound in Appendix A.
Solving Type Class Constraints Figure 6 de�nes the judgment
for solving type class constraints; it takes the form a; P |= A1 �
A2 ; η . Given a set of untouchable type variables a and a theory
P, it (exhaustively) replaces a set of constraints A1 with a setof simpler, residual constraints A2 , via the auxiliary judgment
a; P |= [C] � A ; η , explained below.
�is form di�ers from the speci�cation in Figure 3: we allow constraints to be partially entailed, which in turn allows us to perform
simpli�cation [17] of top-level signatures. �is is standard practicein Haskell when inferring types. For instance, when inferring thesignature forS���

a; P |= A1 , C � A3 ; (η 2 · η 1 )18
19

Constraint Solving Algorithm

reduction [16]). Goal matching is performed by judgment a; [C] |=Q � A; θ ; η , discussed below.

Matching Auxiliary judgment a; [C] |= Q � A; θ ; η focuseson the axiom C and checks whether it matches the simple goal
Q. �e main di�erence between this algorithmic relation and its
declarative speci�cation in Figure 3 lies in the type substitution θ .
Instead of guessing a type for instantiating a polymorphic axiom
in Rule (∀L) (top-down), we defer the choice until the head of theaxiom is met, in Rule (QL) (bo�om-up). Observe that Rule (∀L) does
not record b as untouchable, e�ectively turning it into a uni�cation
variable. �us, by unifying the head of the axiom with the goal we
7

Haskell’17, September 7 – 8, 2017, Oxford, UK
1
2
3
4
5
6
7
8
9
10
11
12
13
14

Bo�u et al.

Γ �cls cls : AS ; Γc � fdata; fval

Class Declaration Typing

Γ,a �ty σ

Γ,a �ct Ci

�ty σ � υ

�ct Ci � υi

n+1
fval 1 = let f : (∀a.TTC a → υ) = Λa.λ(d : TTC a).projTC(d )nfdata = data TTC a = KTC υ n υ

d,d freshifval i2 = let di : (∀a.TTC a → υi ) = Λa.λ(d : TTC a).projTC(d )nΓ �cls (class (C1 , . . . , Cn ) ⇒ TC a where { f :: σ }) : [ di : ∀a.TC a ⇒ Ci ]; [f : ∀a.TC a ⇒ σ ] � fdata; fval 1 , fval 2
P; Γ �inst inst : A I � fval

Class Instance Typing�class (C1� , . . . , Cm
) ⇒ TC a where { f :: σ }ΓI �ct Ci

C����

n

�

d,d ,d I freshb = fv(τ )nb; PI ,L ( d I : ∀b.C ⇒ TC τ ); ΓI �tm e : [τ /a]σ � t

PI = P,L d : C

ΓI = Γ,bb; PI |= d : [τ /a]C � � •; η�

�ct Ci � υiI�������

P; Γ �inst (instance (C1 , . . . , Cn ) ⇒ TC τ where { f = e }) : [ d I : ∀b.C ⇒ TC τ ] � let d I : (∀b.υ → TTC τ ) = Λb.λ(d : υ).KTC τ η(d � ) t
Figure 7. Declaration Elaboration

15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

can determine without guessing an instantiation for all top-level
quanti�ers, captured by the type substitution θ .
As an example, consider the derivation of one-step simpli�cationof ∀b.Eq b ⇒ Eq [b], when (∀a.Eq a ⇒ Eq [a]) ∈ P:5
unify(b; a ∼ b) = θ = [b/a]b; [Eq [a]] |= Eq [b] � •; θa; P; Γ �tm e : σ � tb; [∀a.Eq a ⇒ Eq [a]] |= Eq [b] � Eq b; θ
b; P, Eq b |= [Eq [b]] � Eq bb; P |= [Eq b ⇒ Eq [b]] � (Eq b ⇒ Eq b)Γ �tm e : τ1 � t | Ae ; Eed fresh�ct Ci � υi

(QL)b; [Eq a ⇒ Eq [a]] |= Eq [b] � Eq b; θExplicitly Annotated Term Typingθ = unify(a,b; Ee ,τ1 ∼ τ2 )a,b; P,L d : C |= θ (Ae ) � •; ηa; P; Γ �tm e : (∀b.C ⇒ τ2 ) � Λb.λ(d : υ).η(θ (t ))

(⇒L)

(�)

Figure 8. Subsumption Rule

(∀L)
(QR)

•; P |= [∀b.Eq b ⇒ Eq [b]] � (∀b.Eq b ⇒ Eq b)(⇒R)

one, we get stuck when recursively resolving E a. However, if webacktrack and consider the second one instead, we can recursively
resolve G a against the given local constraint.
In summary, because we do not see a general way to avoid search,
our prototype implementation uses backtracking for choosing between the di�erent axioms.

(∀R)

Search As Section 3.4 has remarked, there may be multiple matching axioms, e.g., due to overlapping superclass axioms. �e straightforward algorithmic approach to the involved nondeterminism issearch, possibly implemented by backtracking. �e GHC Haskell
implementation can employ a heuristic to keep this search shallow. It does so by using the superclass constraints very selectively:
whenever a new local constraint is added to the theory, it proactively derives all its superclasses and adds them as additional
local axioms. When looking for a match, it does not consider thesuperclass axioms and prefers the local axioms over the instanceaxioms. If a matching local axiom exists, it immediately discharges
the entire goal without further recursive resolution. �is is the casebecause in regular Haskell local axioms are always simple classconstraints Q.
In our se�ing, we can also implement a (modi�ed version) of
GHC’s heuristic, but this does not obviate the need for deep search.
�e reason is that our local axioms are not necessarily simple axioms, and matching against them may leave residual goals that
require further recursive resolution. When that recursive resolution gets stuck, we have to backtrack over the choice of axiom.
Consider the following example.

Implementation Our prototype implementation is available ath�ps://github.com/gkaracha/quantcs-impl. It incorporates higherkinded datatypes and performs type inference, elaboration into
System F (as explained in the next section), and type checking of
the generated code.
�e examples we have tested with the prototype provide con�dence that our system is sound and that the elaboration is typepreserving. �e formal proof of the metatheory is future work.
4.4

Checking Declarations

Figure 7 de�nes type checking of class and instance declarations.
Class Declaration Typing Typing for class declarations is given
by Rule C����. For the purposes of type inference, Rule C����
is identical to the corresponding rule of Figure 2, so we defer its
analysis to Section 5.5 which discusses elaboration.
Instance Declaration Typing Typing for instance declarations
takes the form P; Γ �inst inst : A I � fval and is given by Rule I��������. For the most part it is identical to the corresponding ruleof Figure 2.
�e most notable di�erence is the handling of the method implementation e: method implementations have their type imposedby the method signature in the class declaration. Hence, we needto check rather than infer their type.

class (E a ⇒ C a) ⇒ D aclass (G a ⇒ C a) ⇒ F a

Given local axioms D a, F a and G a, consider what happens when
we resolve the goal C a. �e superclasses E a ⇒ C a and G a ⇒ C aof respectively D a and F a both match this goal. If we pick the �rst
5 We omit the evidence substitutions for brevity.

8�antified Class Constraints
1
2
3
4
5
6
7
8
9

Haskell’17, September 7 – 8, 2017, Oxford, UK

fpgm ::= t | fval; fpgm | fdata; fpgm
fval ::= let x : υ = t
fdata ::= data T a = K υ

Rules T�V��, T�A�� and T�A�� are straightforward. Rule T����
elaborates a quali�ed type into a System F arrow type: the constraint C is translated into the dictionary type υ 1 , via relation
�ct C � υ which performs elaboration of constraints:

programvalue binding
datatypet ::= x | K | λ(x : υ).t | t 1 t 2 | Λa.t | t υ| let x : υ = t 1 in t 2 | case t 1 of K x → t 2term

υ ::= a | υ 1 → υ 2 | ∀a.υ | T υ

type�ty τ � υ

�ct TC τ � TTC υ�ct C1 � υ 1

11

13

15
16
17
18
19
20
21
22
23
24
25

�is operation is expressed succinctly by relation a; P; Γ �tm e :σ � t , presented in Figure 8. Essentially, it ensures that the inferred type for e subsumes the expected type σ . A type σ1 is said
to subsume type σ2 if any expression that can be assigned type σ1
can also be assigned type σ2 .
Rule (�) performs type inference and type subsumption checking
simultaneously: First, it infers a monotype τ1 for expression e,
as well as wanted constraints Ae and type equalities Ee . Typeequalities Ee should have a uni�er and the inferred type τ1 should
also be uni�able with the expected type τ2 . Finally, the given
constraints C should completely entail the wanted constraints Ae .

26

4.5

27

Type inference and elaboration for programs is straightforward
and can be found in Appendix A.

28
29
30
31
32
33

5

36

is elaborated into the type∀f a.TShow a → (∀x .TShow x → TShow ( f x )) → TShow (HPerf f a)
5.3

37
38
39
40
41
42

Program Typing

Translation to System F

Target Language: System F

5.4

Syntax �e syntax of System F [8] – extended with data types
and recursive let-bindings – is presented in Figure 9 and is entirely
standard. Like in the source language, we elide all mention of kinds.
Without loss of generality, we simplify ma�ers by allowing only
data types with a single type parameter and a single data constructor and case expressions with a single branch; this is su�cient forour dictionary-passing translation of type classes.

45
46
47

Simpli�cation �e evidence substitution η in the simpli�cation
relation shows how to construct a witness for the wanted constraint
C from the simpler constraints A � and program theory P.
�e goal of Rule (⇒R) is to build an evidence substitution η � ,�which constructs a proof for (d 0 : C1 ⇒ C2 ) from the proofs d forthe simpler constraints C1 ⇒ C. It is instructive to consider thegenerated evidence substitution in parts, also taking the types into
account:
1. η illustrates how to generate a proof for (d 2 : C2 ), from the local
assumption (d 1 : C1 ) and local residual constraints (d : C).
2. [d � d 1 /d] generates proofs for the (local) residual constraints(d : C), by applying the residual constraints (d � : C1 ⇒ C) tothe local assumption (d 1 : C1 ).
3. ([d � d 1 /d] · η)(d 2 ) is a proof for C2 , under assumptions (d 1 : C1 )and (d � : C1 ⇒ C).
4. Finally, we construct the proof for (d 0 : C1 ⇒ C2 ) by explicitly
abstracting over d 1 : λ(d 1 : υ 1 ).[d � d 1 /d](η(d 2 ))Rule (∀R) proceeds similarly. Finally, Rule (QR) generates the evidence substitution via constraint matching, which we discuss next.

Semantics & Typing Since the operational semantics and typing
for System F with data types are entirely standard and do notcontribute to the novelty of this paper, we omit them from ourmain presentation. �ey can be found in Appendix B.

48
49
50
51
52
53
54

5.2

Elaboration of Types & Constraints

Our system follows the traditional approach of translating source
type class constraints into explicitly-passed System F terms, theso-called dictionaries [9, 38]. �is transition is re�ected in thetranslation of types, performed by judgment �ty σ � υ:

55
56
57
58
59
60
61

�ty a � a
�ct C � υ 1T�V���ty τ1 � υ 1

�ty ρ � υ 2

�ty C ⇒ ρ � υ 1 → υ 2

�ty τ2 � υ 2

�ty τ1 → τ2 � υ 1 → υ 2T�����ty σ � υT�A���ty ∀a.σ � ∀a.υ

Dictionary Construction

�e entailment algorithm of Figure 6 constructs explicit witness
proofs (in the form of dictionary substitutions) while entailing a
constraint.

43
44

Elaboration of Terms

Term elaboration is straightforward. Rule T�V�� handles term
variables. �e instantiation of the type scheme ∀a.C ⇒ τ to [b/a]τ
becomes explicit in the System F representation, by the applicationof x to type variables b, as well as the fresh dictionary variables d,corresponding one-to-one to the implicit constraints C. Rule T�A��
elaborates λ-abstractions. Since in System F all bindings are explicitly typed, in the elaborated term we annotate the binding ofx with its type a. Similarly, Rule T�L�� elaborates let bindings,
again explicitly annotating x with its type υ 1 in the elaborated term.
Rule T�A�� is straightforward.

�is section discusses the elaboration aspect of the algorithm presented in Section 4.
5.1

(C⇒)

∀f a.Show a ⇒ (∀x .Show x ⇒ Show ( f x )) ⇒ Show (HPerf f a)3435

�ct C2 � υ 2(C∀)

Rule (CQ) elaborates a class constraint (TC τ ) into a type constructor application (TTC υ), which corresponds to the type of dictionaries that witness (TC τ ). Rule (C∀) is straightforward. Rule (C⇒)
elaborates implication constraints of the form (C1 ⇒ C2 ) into
System F arrow types (υ 1 → υ 2 ), that is, types of dictionary transformers. As a concrete example, the constraint corresponding to
the Show instance for type HPerf (Section 2.2):1214�ct ∀a.C � ∀a.υ

�ct C1 ⇒ C2 � υ 1 → υ 2

Figure 9. System F Syntax

10�ct C � υ

(CQ)

T�A��
9

Haskell’17, September 7 – 8, 2017, Oxford, UK
1
2
3
4
5
6
7
8
9
10
11

Bo�u et al.

Matching Similarly, the evidence substitution η in the matching
relation shows how to construct a witness for the wanted constraint
Q from the simpler constraints A and program theory P.
Rule (⇒L) generates two fresh dictionary variables, d 1 for the
residual constraint θ (C1 ), and d 2 for the local assumption C2 . Finally, dictionary d 2 is replaced by the application of the dictionarytransformer d to the residual dictionary d 1 . Rule (∀L) behaves similarly. �e instantiation of the axiom d becomes explicit, by applying
it to the chosen type θ (b). Finally, Rule (QL) is straightforward:
since the wanted and the given constraints are identical (given thatthey unify), the wanted dictionary d is replaced by the given d � .

Overall Strategy We show termination by characterising the resolution process as a (resolution) tree with goals in the nodes andaxioms on the (multi-)edges. �e initial goal sits at the root of thetree. A multi-edge from a parent node to its children presents anaxiom that matches the parent node’s goal and its children are theresidual goals. Resolution terminates i� the tree is �nite. Hence, if
it does not terminate, there is an in�nite path from the root in thetree, that denotes an in�nite sequence of axiom applications.
To show that there cannot be such an in�nite path, we use anorm �·� that maps the head 6 of every goal C to a natural number,its size. �e size of a class constraint TC τ is the size of its typeparameter τ , which is given by the following equations:

12
13
14
15
16
17
18
19
20
21
22

5.5

27
28
29

i
(d ) ≡ case d of KTC x k → x i
projTC

31

33

36

39

41
42
43
44
45
46
47
48
49

52
53
54
55
56
57
58
59
60
61

term(∀a.C)

(∀T)

(⇒T)

Rule (⇒T) for C1 ⇒ C2 enforces the main condition, that the sizeof the residual constraint’s head Q1 is strictly smaller than thehead Q2 of C2 . In addition, the rule ensures that this property isstable under type substitution. Consider for instance the axiom∀a.C (a → a) ⇒ C (a → Int → Int). �e head’s size 5 is strictly
greater than the context constraint’s size 3. Yet, if we instantiate
a to (Int → Int → Int), then the head’s size becomes 10 while
the context constraint’s size becomes 11. Declaratively, we canformulate stability as:

Given dictionaries d – corresponding to the given context constraints – we need to provide all arguments of the data constructor
KTC : (a) the instantiation of the class type parameter, (b) the superclass dictionaries, and (c) the method implementation. �e �rst
argument is trivial. We obtain the superclass dictionaries by ap�
plying the evidence substitution η on the dictionary variables dthat abstract over the required superclass constraints. �e method
implementation t is elaborated via premise∀θ .dom(θ ) ⊆ fv(C1 ) ∪ fv(C2 ) ⇒ �θ (Q1 )� < �θ (Q2 )�

�e rule uses instead an equivalent algorithmic formulation whichstates that the number of occurrences of any free type variable a
may not be larger in Q1 than in Q2 . Here the number of occurrences of a type variable a in a class constraint TC τ (denoted asocca (TC τ )) is the same as the number of free occurrences of a in
the parameter τ , where function occa (τ ) is de�ned as:�
1 , if a = bocca (b)=0 , if a � bocca (τ1 → τ2 ) = occa (τ1 ) + occa (τ2 )b; PI ; ΓI �tm e : [τ /a]σ � twhich elaborates type subsumption in a similar manner.

6term(C)term(C1 ⇒ C2 )let d I : (∀b.υ → TTC τ ) = Λb.λ(d : υ).KTC τ η(d � ) t

50
51,x k freshElaboration of Class Instances A class instance is elaborated
into a System F dictionary transformer d I :

40

(QT)

term(C1 )term(C2 )Q2 = head (C2 )�Q1 � < �Q2 �
Q1 = head (C1 )∀a ∈ fv(C1 ) ∪ fv(C2 ) : occa (Q1 ) ≤ occa (Q2 )d sc : ∀t .TTrans t → (∀m.TMonad m → TMonad (t m))
d sc = Λt .λ(d : TTrans t ). case d of { KTrans d � → d � }3538term(Q)

where k denotes the arity of data constructor KTC . E.g., the superclass projection function for class Trans takes the form:

34

37

Termination Condition It is trivial to show that the size strictly
decreases, if we require that every axiom makes it so. �is requirement is formalised as the termination condition of axioms
term(C):

Accordingly, we generate n + 1 projection functions that extract
each of the arguments (di extracts the i-th superclass dictionaryi (d ) to denoteand f the method implementation). We use projTCpa�ern matching against d and extracting the i-th argument:

30

32

If we can show that this size strictly decreases from any parent
goal to its children, then we know that, because the order on thenatural numbers is well-founded, on any path from the root thereis evantually a goal that has no children.

data TTrans t = KTrans (∀m.TMonad m → TMonad (t m))(∀m a.TMonad m → m a → (t m) a)

24

26

�a�
= 1
�τ1 → τ2 � = 1 + �τ1 � + �τ2 �

Elaboration of Class Declarations A declaration for a class TC
is encoded in System F as a dictionary type TTC , with a single
data constructor KTC and n + 1 arguments: n arguments for thesuperclass dictionaries (of type υ n ) and one more for the method
implementation (of type υ). For example, the Trans declaration ofSection 2.1 gives rise to the following dictionary type:23

25

Declaration Elaboration

Figure 7 presents the elaboration of both class and instance declarations into System F.

Termination of Resolution

Finally, as the constraints have a recursive structure whereby theircomponents are themselves used as axioms, the rules also enforce
the termination condition recursively on the components.

Termination of resolution is the cornerstone of the overall termination of type inference. �is section discusses how to enforce
termination by means of syntactic conditions on the axioms. �ese
conditions are adapted from those of C����� [32] and generalize
the earlier conditions for Haskell by Sulzmann et al. [35].

6 �e head of a constraint is de�ned as: head (Q) = Q ; head (∀a .C) = head (C) ; and10head (C1 ⇒ C2 ) = head (C2 ) .

�antified Class Constraints
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

Superclass Condition If we could impose the termination condition above on all axioms in the theory P, we would be set. Unfortunately, this condition is too strong for the superclass axioms.
Consider the superclass axiom ∀a.Ord a ⇒ Eq a of the standard
Haskell’98 Ord type class. Here both Ord a and Eq a have size 1; inother words, the size does not strictly decrease and so the axiom
does not satisfy the termination condition.
To accommodate this and other examples, we impose an alternative condition for superclass axioms. �is superclass condition
relaxes the strict size decrease to a non-strict size decrease andmakes up for it by requiring that the superclass relation forms a
directed acyclic graph (DAG). �e superclass relation is de�ned asfollows on type classes.

20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57

class Monad t t where
treturn :: Monad m ⇒ a → t m atbind :: Monad m ⇒ t m a → (a → t m b) → t m bclass Monad t t ⇒ Trans t whereli� :: Monad m ⇒ m a → t m a

While this approach captures the intention of the quanti�ed constraint, it does not enable the type checker to see that Monad (t m)holds for any transformer t and monad m. While the monad methods are available for t m, they do not have the usual name.
For this reason, Trifonov presents a further (non-Haskell’98) re�nement of the encoding, which was adopted by the Monatron [13]library8 among others. A non-essential di�erence is that Monatronmerges the above Monad t and Trans into a single class:class (C1 , . . . , Cn ) ⇒ TC a where { f :: σ }17

19name. �is expresses the Trans problem as follows:De�nition 6.1 (Superclass Relation). Given a class declaration

16

18

Haskell’17, September 7 – 8, 2017, Oxford, UK

class MonadT t whereli�:: Monad m ⇒ m a → t m atreturn :: Monad m ⇒ a → t m atbind :: Monad m ⇒ t m a → (a → t m b) → t m beach type class TC i is a superclass of TC, where head (Ci ) = TC i τi .
Observe that the DAG induces a well-founded partial order ontype classes. Hence, on any path in the resolution tree, any uninterrupted sequence of superclass axiom applications has to be �nite.
For the length of such a sequence, the size of the goal does notincrease (but might not decrease either). Yet, a�er a �nite numberof steps the sequence has to come to an end. If the path still goeson at that point, it must be due to the application of an instance or
local axiom, which strictly decreases the goal size. Hence, overall
we have preserved the variant that the goal size decreases a�er abounded number7 of steps.

7

�e key novelty is that it also makes the methods treturn and tbind
available under their usual name with a single Monad instance forall monad transformers.
instance (Monad m, MonadT t ) ⇒ Monad (t m) wherereturn = treturn(>>=) = tbind
With these de�nitions the monad transformer composition does
type check. Unfortunately, the head of the Monad (t m) instance ishighly generic and easily overlaps with other instances.

Related Work

The MonadZipper Because they found Monatron’s overlapping
instances untenable, Schrijvers and Oliveira [31] presented a different workaround for this problem in the context of their monadzipper datatype, which is an extended form of transformer composition. �eir solution adds a method mw to the Trans type class:�is section discusses related work, focusing mostly on comparing
our approach with existing encodings/workarounds in Haskell. �ehistory of quanti�ed class constraints and their demand in previous
research was already discussed in Section 1.

class Trans t whereli� :: Monad m ⇒ m a → t m a
mw :: Monad m ⇒ MonadWitness t m

The Coq Proof Assistant Coq provides very �exible support for
type classes [33] and allows for arbitrary formulas in class andinstance contexts – actually the contexts are just parameters. For
instance, we can model the Trans class as:

For any monad m this method returns a GADT [29] witness for thefact that t m is a monad. �is is possible because with GADTs, typeclass instances can be stored in the data constructors.

Class Trans (T : (Type -> Type) -> Type -> Type)�{forall M, �{Monad M} -> Monad (T M)} :={ lift : forall A M, �{Monad M} -> M A -> (T M) A }.

data MonadWitness (t :: (∗ → ∗) → (∗ → ∗)) m where
MW :: Monad (t m) ⇒ MonadWitness t m

�e downside of Coq’s �exibility is that resolution can be ambiguous and non-terminating. �e accepted workaround is for the
programmer to perform resolution manually when necessary. �isis acceptable in the context of Coq’s interactive approach to proving,
but would mean a great departure from Haskell’s non-interactive
type inference.

By pa�ern matching on the witness of the appropriate type theprogrammer can bring the required Monad (t 2 m) constraint into
scope to satisfy the type checker.
instance (Trans t 1 , Trans t 2 ) ⇒ Trans (t 1 ∗ t 2 ) whereli� :: ∀m a.Monad m ⇒ m a → (t 1 ∗ t 2 ) m ali� = case (mw :: MonadWitness t 2 m) of
MW → C · li� · li�

Trifonov’s Workaround and Monatron Trifonov [36] gives anencoding of quanti�ed class constraints in terms of regular classconstraints. �e encoding introduces a new type class that encapsulates the quanti�ed constraint, e.g. Monad t t for ∀m.Monad m ⇒Monad (t m), and that provides the implied methods under a new

mw = . . .
�e downside of this approach is that it o�oads part of the typechecker’s work on the programmer. As a consequence the code
becomes clu�ered with witness manipulation.

58
59
60
61

7 bounded by the height of the superclass DAG

8 For the implementation see h�ps://hackage.haskell.org/package/Monatron

11

Haskell’17, September 7 – 8, 2017, Oxford, UK
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

Bo�u et al.

The constraint Library Kme�’s constraint library [20] provides
generic infrastructure for reifying quanti�ed constraints in termsof GADTs, not unlike in the MonadZipper solution above. While
not impossible, encoding the Trans problem with this library is adaunting task indeed.

13th International Symposium, Proceedings (FLOPS 2016), Oleg Kiselyov and Andy
King (Eds.). Springer International Publishing, 126–143.
[8] Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and Types. Cambridge
University Press, New York, NY, USA.
[9] Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler.
1996. Type Classes in Haskell. ACM Trans. Program. Lang. Syst. 18, 2 (March
1996), 109–138.
[10] Ralf Hinze. 2000. Perfect trees and bit-reversal permutations. J. Funct. Program.
10, 3 (2000), 305–317.
[11] Ralf Hinze. 2010. Adjoint Folds and Unfolds: Or: Scything �rough the �icketof Morphisms. In Proceedings of the 10th International Conference on Mathematics
of Program Construction (MPC’10). Springer-Verlag, Berlin, Heidelberg, 195–228.
[12] Ralf Hinze and Simon Peyton Jones. 2000. Derivable Type Classes. In Proceedingsof the Fourth Haskell Workshop. Elsevier Science, 227–236.
[13] Mauro Jaskelio�. 2011. Monatron: an extensible monad transformer library. In
Proceedings of the 20th international conference on Implementation and applicationof functional languages (IFL’08). Springer-Verlag, Berlin, Heidelberg, 233–248.
[14] Mark P. Jones. 1992. A theory of quali�ed types. In ESOP ’92, Bernd KriegBrückner (Ed.). LNCS, Vol. 582. Springer Berlin Heidelberg, 287–306.
[15] Mark P. Jones. 1995. Functional Programming with Overloading and HigherOrder Polymorphism. In Advanced Functional Programming, First International
Spring School on Advanced Functional Programming Techniques-Tutorial Text.
Springer-Verlag, London, UK, UK, 97–136.
[16] Mark P. Jones. 1995. �ali�ed Types: �eory and Practice. Cambridge University
Press, New York, NY, USA.
[17] Mark P. Jones. 1995. Simplifying and Improving �ali�ed Types. In Proceedingsof the Seventh International Conference on Functional Programming Languages
and Computer Architecture (FPCA ’95). ACM, New York, NY, USA, 160–169.
[18] Mark P. Jones. 2000. Type Classes with Functional Dependencies. In Programming
Languages and Systems, Gert Smolka (Ed.). LNCS, Vol. 1782. Springer Berlin
Heidelberg, 230–244.
[19] Simon Peyton Jones, Mark Jones, and Erik Meijer. 1997. Type classes: an exploration of the design space. In Proceedings of the 1997 Haskell Workshop. ACM.
[20] Edward A. Kme�. 2017. �e constraint package. (2017). h�ps://hackage.haskell.
org/package/constraints-0.9.1.
[21] Ralf Lämmel and Simon Peyton Jones. 2003. Scrap Your Boilerplate: A Practical
Design Pa�ern for Generic Programming. SIGPLAN Not. 38, 3 (Jan. 2003), 26–37.
[22] Ralf Lämmel and Simon Peyton Jones. 2005. Scrap Your Boilerplate with Class:
Extensible Generic Functions. SIGPLAN Not. 40, 9 (Sept. 2005), 204–215.
[23] Chuck Liang and Dale Miller. 2009. Focusing and Polarization in Linear, Intuitionistic, and Classical Logics. �eor. Comput. Sci. 410, 46 (Nov. 2009), 4747–4768.
[24] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. 1989. Uniform Proofs As a Foundation for Logic Programming. Technical Report. Durham,
NC, USA.
[25] J. Garre� Morris. 2014. A Simple Semantics for Haskell Overloading. SIGPLAN
Not. 49, 12 (Sept. 2014), 107–118.
[26] Bruno C.d.S. Oliveira, Adriaan Moors, and Martin Odersky. 2010. Type Classes
As Objects and Implicits. SIGPLAN Not. 45, 10 (Oct. 2010), 341–360.
[27] Bruno C.d.S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, andKwangkeun Yi. 2012. �e Implicit Calculus: A New Foundation for Generic
Programming. SIGPLAN Not. 47, 6 (June 2012), 35–44.
[28] Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields.
2007. Practical Type Inference for Arbitrary-rank Types. J. Funct. Program. 17, 1(Jan. 2007).
[29] Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geo�rey
Washburn. 2006. Simple Uni�cation-based Type Inference for GADTs. SIGPLAN
Not. 41, 9 (Sept. 2006), 50–61.
[30] Frank Pfenning. 2010. Lecture Notes on Focusing. (2010). h�ps://www.cs.cmu.
edu/∼fp/courses/oregon-m10/04-focusing.pdf.
[31] Tom Schrijvers and Bruno C.d.S. Oliveira. 2011. Monads, Zippers and Views:
Virtualizing the Monad Stack. SIGPLAN Not. 46, 9 (Sept. 2011), 32–44.
[32] Tom Schrijvers, Bruno C. d. S. Oliveira, and Philip Wadler. 2017. Cochis: Deterministic and Coherent Implicits. Report CW 705. KU Leuven, Department ofComputer Science.
[33] Ma�hieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In �eorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008.
Proceedings (LNCS), Vol. 5170. Springer, 278–293.
[34] Mike Spivey. 2017. Faster Coroutine Pipelines. In International Conference on
Functional Programming (ICFP). accepted.
[35] Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones, and Peter J. Stuckey.
2007. Understanding Functional Dependencies via Constraint Handling Rules. J.
Funct. Program. 17, 1 (Jan. 2007), 83–129.
[36] Valery Trifonov. 2003. Simulating �anti�ed Class Constraints. In Proceedingsof the 2003 ACM SIGPLAN Workshop on Haskell (Haskell ’03). ACM, New York,NY, USA, 98–102.
[37] Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers. 2010. Let Should
Not Be Generalized. In Proceedings of the 5th ACM SIGPLAN Workshop on Types
in Language Design and Implementation (TLDI ’10). ACM, NY, USA, 39–50.
[38] P. Wadler and S. Blo�. 1989. How to Make Ad-hoc Polymorphism Less Ad Hoc.
In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages (POPL ’89). ACM, New York, NY, USA, 60–76.

Corecursive Resolution Fu et al. [7] address the divergence problem that arises for generic nested datatypes. �ey turn the diverging
resolution with user-supplied instances into a terminating resolution in terms of automatically derived instances. �ese auxiliary
instances are derived speci�cally to deal with the query at hand;
they shi� the pa�ern of divergence to the term-level in the formof co-recursively de�ned dictionaries. �e authors do point out
that the class of divergent cases they support is limited and thatderiving quanti�ed instances would be bene�cial.
C����� �e calculus of coherent implicits, C����� [32], and its
focusing-based resolution in particular, have been a major inspiration of this work. Just like this work, C����� supports recursive
resolution of quanti�ed constraints. Yet, there are a number ofsigni�cant di�erences. Firstly, C����� does not feature a separate
syntactic sort for type classes, but implicitly resolves regular terms
in the Scala tradition. As a consequence, it does not distinguishbetween instance and superclass axioms, e.g., for the sake of enforcing termination and coherence. Perhaps more signi�cantly,C����� features local “instances” as opposed to our globally scoped
instances. Local instances may overlap with one another and coherence is obtained by prioritizing those instances that are introducedin the innermost scope. �is way C�����’s resolution is entirely
deterministic, while ours is non- deterministic (yet coherent) due
to overlapping local and superclass axioms.

8

Conclusion

�is paper has presented a fully �edged design of quanti�ed classconstraints. We have shown that this feature signi�cantly increases
the modelling power of type classes, while at the same enables aterminating type class resolution for a larger class of applications.
Interesting future work we aim to pursue includes (a) establishing
the metatheory, (b) extending the system with quanti�cation overpredicates9 , raising the power of type classes to (a fragment of)second-order logic, and (c) studying the interaction of quanti�edclass constraints with commonly used type-level features like functional dependencies [18] or associated type families [4], allowing us
to integrate the new feature in Haskell’s ecosystem.

44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

References[1] Jean-marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear
Logic. Journal of Logic and Computation 2 (1992), 297–347.
[2] H. Barendregt. 1981. �e Lambda Calculus: its Syntax and Semantics, volume 103
of Studies in Logic and the Foundations of Mathematics. North-Holland.
[3] Richard S. Bird and Lambert G. L. T. Meertens. 1998. Nested Datatypes. In
Proceedings of the Mathematics of Program Construction (MPC ’98). SpringerVerlag, London, UK, 52–67.
[4] Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. 2005. Associated Type Synonyms. SIGPLAN Not. 40, 9 (Sept. 2005), 241–253.
[5] Satvik Chauhan, Piyush P. Kurur, and Brent A. Yorgey. 2016. How to Twist Pointers Without Breaking �em. In Proceedings of the 9th International Symposium
on Haskell (Haskell 2016). ACM, New York, NY, USA, 51–61.
[6] Luis Damas and Robin Milner. 1982. Principal Type-schemes for Functional Programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages (POPL ’82). ACM, New York, NY, USA, 207–212.
[7] Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, and Andrew Pond. 2016.
Proof Relevant Corecursive Resolution. In Functional and Logic Programming:

9 See GHC feature request #5927.

12

�antified Class Constraints

Haskell’17, September 7 – 8, 2017, Oxford, UK

1

A

Additional Judgments

2

A.1

Well-formedness of Types & Constraints

3
4
5

Well-formedness of types takes the form Γ �ty σ and is given by thefollowing rules:
a∈Γ

6
7

Γ �ty a8

Γ �ct C

9

12
13
14
15

18
19
20

Γ �ty τ2T����Γ,a �ty σΓ �ty τΓ �ct TC τ

(CQ)

T�A��

P; Γ �pgm (cls; pgm) : σ � fdata; fval; fpgm
P; Γ �inst inst : A I � fval
P,I A I ; Γ �pgm pgm : σ � fpgm

T�A��

Γ �ty ∀a.σ

22

Γ �ax •

23

Γ �ct C1Γ �ct C2Γ �ct C1 ⇒ C2(C⇒)Γ,a �ct CΓ �ct ∀a.CA�N��Γ �ax AΓ �ct CΓ �ax A, C

A.2

�e judgment for program typing takes the form P; Γ �pgm pgm : σ
and is given by the following rules:28

Γ �cls cls : AS ; Γc

P,S AS ; Γ, Γc �pgm pgm : σ

30
31

P; Γ �inst inst : AIP,I AI ; Γ �pgm pgm : σP; Γ �pgm (inst; pgm) : σ

32
33

P; Γ �tm e : σ34P; Γ �pgm e : σ

35P��E���

A.3

42
43
44
45
46
47
48
49
50
51
52
53
54
55

System F Semantics

Both the typing rules and call-by-name operational semantics for
System F are entirely standard and can be found elsewhere, we
include them here to keep the presentation self-contained. In thefollowing, we denote System F typing environments by Δ:

P��I���

39

41

Δ ::= • | Δ, T | Δ, K : υ | Δ,a | Δ,x : υ
B.1

Uni�cation Algorithm

�e uni�cation algorithm takes the form unify(a; E) = θ ⊥ and isgiven by the following equations:58

Δ �tmF x : υ(K : υ) ∈ Δ
Δ � K :υ
F
tm

59
60
61

T�V��

T�C��

Δ,a �tmF t : υΔ �tmF Λa.t : ∀a.υFunction unify is a straightforward extension of the standard �rstorder uni�cation algorithm [6]. �e only di�erence between the
two lies in the additional argument: the untouchable variables a.
�ese variables are treated by the algorithm as skolem constants
and therefore can not be substituted (they can be uni�ed withthemselves though).
A.4

Term Typing(x : υ) ∈ Δ

unify(a; •)= •= unify(a; E)
unify(a; E,b ∼ b)
= unify(a; θ (E)) · θ
unify(a; E,b ∼ τ )where b � a ∧ b � fv(τ ) ∧ θ = [τ /b]= unify(a; θ (E)) · θ
unify(a; E,τ ∼ b)
where b � a ∧ b � fv(τ ) ∧ θ = [τ /b]unify(a; E, (τ1 → τ2 ) ∼ (τ3 → τ4 )) = unify(a; E,τ1 ∼ τ3 ,τ2 ∼ τ4 )typing environment

Term Typing

F
Δ �tm
t :υ

Δ,x : υ 1 �tmF t 1 : υ 1

Δ,x : υ 1 �tmF t : υ 2

Δ �tyF υ 1

Δ �tmF t 1 : υ 1 → υ 2

Δ �tmF t 2 : υ 1

Δ �tmF λ(x : υ 1 ).t : υ 1 → υ 2
Δ � t1 t2 : υ2
F
tm

(∀I)

Δ �tmF t : ∀a.υΔ �tyF υ 1

Δ �tyF υ 1

Δ �tmF t υ 1 : [υ 1 /a]υΔ,x : υ 1 �tmF t 2 : υ 2

Δ � (let x : υ 1 = t 1 in t 2 ) : υ 2Ftm

Δ �tmF t 1 : T υ(K : ∀a.υ → T a) ∈ Δ
Δ,x : [υ/a]υ �tmF t 2 : υ 2
Δ �tmF (case t 1 of K x → t 2 ) : υ 2

56
57

PE��

Rules PC�� and PI�� handle class and instance declarations, respectively, and they are entirely standard. Rule PE�� performs standard
type-inference, simpli�cation [17] and generalization for a top-level
expression e. For simplicity, we do not utilize interaction rules (e.g.
we do not simplify the constraints {Eq a, Ord a} to {Ord a}), but
it is straightforward to do so. Finally, observe that superclass axioms AS are not used for the simpli�cation of wanted constraints.
�is is standard practice for Haskell but our distinction between
the axioms within the program theory allows us to express thisexplicitly.

B

38

40

�ct Ci � υi

P��C��

For brevity, if P = • and Γ = • we denote program typing as
�pgm pgm : σ .

37

PI��

�AS , A I , A L �; Γ �pgm e : ∀a.C ⇒ θ (τ ) � Λa.λ(d : υ).η(θ (t ))Program Typing

P; Γ �pgm (cls; pgm) : σ

2936a; �•, A I , A L � |= θ (A) � d : C; ηA�C���

25PC��Γ �tm e : τ � t | A; E
a = fv(θ (A)) ∪ fv(θ (τ ))θ = unify(•; E)

(C∀)

24

27

P; Γ �pgm (inst; pgm) : σ � fval; fpgm

Finally, an axiom set A is well-formed if all constraints it contains
are well-formed:

2126

Γ �cls cls : AS ; Γc � fdata; fval
P,S AS ; Γ, Γc �pgm pgm : σ � fpgm

It is entirely straightforward and ensures that type terms are wellscoped. Rule T���� requires checking the well-formedness of
our new form of constraints C, via relation Γ �ct C, given by thefollowing rules:

16
17

Γ �ty τ1Γ �ty τ1 → τ2Γ �ty ρΓ �ty C ⇒ ρ

10
11

T�V��

Program Elaboration

P; Γ �pgm pgm : σ � fpgm

Elaboration of Programs

B.2

Elaboration of programs is given by judgment P; Γ �pgm pgm :σ � fpgm :13

Well-formedness of Types

F
Δ �ty
υ

Type Well-formedness

(→I)

(→E)

(∀E)

T�L��

T�C���

Haskell’17, September 7 – 8, 2017, Oxford, UK
a∈Δ

1

F
ty

Δ� a

2
3
4

7
8
9

Δ,a �tyF υ

14
15

20
21

Δ � (data T a = K υ) : [T , K : ∀a.υ → T a]
B.5

Program Typing
Δ �tmF t : υFΔ �pgm
t :υ

27

33
34
35
36
37
38
39
40
41
42
43
44
45
46

P��E���

FΔ �valfval : Δv

F
Δ, Δv �pgm
fpgm : υP��V��

F
Δ �data
fdata : Δd

F
Δ, Δd �pgm
fpgm : υP��D���F
Δ �pgm(fval; fpgm) : υ

26

32

D���

Program TypingFΔ �pgmfpgm : υ

25

31

V��

Δ,a �tyF υ

F
val

24

30

Δ �tyF υ

Datatype Declaration Typing

23

29

T�A��

Datatype Declaration Typing

22

28

Δ �tyF υ 2

Δ � υ1 υ2Δ,x : υ �tmF t : υFΔ �data
fdata : Δfdata

17

19

F
ty

T�A��

Value Binding Typing

1618

Δ � υ1 → υ2

Δ � (let x : υ = t ) : [x : υ]B.4

Δ �tyF υ 2Fty

Δ �tyF υ 1

F
val

11

13

T�A��

Δ �tyF υ 1

Value Binding TypingFΔ �valfval : Δfval

10

12

Δ� T

Δ � ∀a.υ
B.3

T�C��

F
ty

F
ty

5
6

T ∈Δ

T�V��

Bo�u et al.

Δ � (fdata; fpgm) : υFFor brevity, if Δ = • we denote System F program typing as �pgm
fpgm : υ.
F
pgm

B.6

Call-by-name Operational Semantics

�e small-step, call-by-name operational semantics of System F arepresented below:t −→ t �

Operational Semantics (Small-step)(Λa.t ) υ −→ [υ/a]tT�B���

(λ(x : υ).t ) t � −→ [t �/x]t

t 1 −→ t 1�(case t 1 of K x → t 2 ) −→ (case t 1� of K x → t 2 )(case K t of K x → t ) −→ [t/x]tT�B���C���S���

C���B���

(let x : υ = t 1 in t 2 ) −→ [let x : υ = t 1 in t 1 /x]t 2

L��B���

47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

14