Exploring the Design Space forType-based Implicit Parameterization
Technical Report

Mark P. Jones
Oregon Graduate Institute of Science and Technology
20000 N.W. Walker Road, Beaverton, OR 97006, USA
July 1999
Abstract
A common task in programming is to arrange for data to be passed
from the point where it first becomes available to the places where itis needed, which may be much further down the call hierarchy. One
approach is to store the data in a global variable. Another alternative
is to add extra parameters at each level to thread it from the point of
supply to the point of use. Neither of these is particularly attractive:
The former is inflexible, while the latter requires modification of the
program text, adding auxiliary parameters to each function definitionand call.
This paper explores the design space for a third alternative, using
types to direct the introduction and use of implicit parameters and socarry data from supply to use. This gives the flexibility of parameterization without the burden of adding parameters by hand. The mostgeneral point in the design space uses relations on types to support sophisticated forms of overloading, and includes several known systems
as special cases, including Haskell type classes and a recent proposal
for dynamic scoping in statically-typed languages. Our work provides
new insights about the relationships between these systems, as well
as some new ideas that are useful in their own right. A particularnovelty of this paper is in the application of ideas from the theory of
relational databases to the design of type systems.

1

1

Introduction

A common task in everyday programming projects is to arrange for data
to be passed from the point where it first becomes available to the places
where it is needed. For example, any command line settings that are passed
in at the top level of a program must be available much further down thecall hierarchy in the parts where they are actually used. One way to deal
with this is to store the data in a global variable, or at least in a variable
whose scope extends over some relevant portion of the call graph. Anotheralternative is to add auxiliary parameters at each intermediate level in thecall graph, whose sole purpose is to thread data from the point of supply tothe point of use. These two approaches are illustrated side by side in thefollowing example:
main x = . . . a . . .
where
a = ... b ...
b = ... c ...
c = ... x ...

main x
a x
bx
cx

=
=
=
=

... a x ...
... b x ...
... c x ...
... x ...

In both cases, the goal is to pass the value x that is supplied to main throughthe functions a and b to the point where it is used in the computation ofc. The code on the left achieves this by placing the definition of c within
the scope of x . Unfortunately, this also restricts the scope of c and forces
us to do the same with the definitions of a and b. Moreover, because thevariable x is hard-wired into the definition of c, it is difficult for the main
program to invoke a more than once with a different value for x each time.
In practice, these problems are often avoided by storing the value for x ina global variable, and using side-effects to change it if different values are
required at different times during execution. While this is often an adequate
solution, it can also be limiting, and a source of subtle bugs.
The code on the right illustrates an alternative approach, avoiding the problems of the version on the left by adding x as a parameter to each of a, b,
and c. Because the dependency on x has been made explicit, this program
would still work perfectly well if these definitions were split across multiple
compilation units. However, this flexibility comes at a price, requiring mod2

ifications throughout the program text, which makes it harder to maintain,
and harder to read, as well as opening up another potential source of bugs.
This paper explores the design space for a third alternative, using implicit
parameters to carry data from supply to use, as in the following example:
main x =where abc. . . a with ?x = x . . .
= ... b ...
= ... c ...
= . . . ?x . . .

In this example, which uses language features first proposed by Lewis etal. [12], the with construct in the definition of main binds x to an implicit
parameter ?x , which is subsequently accessed at the point where it appears
in the definition of c. Any such use of implicit parameters can be implemented by translating the source code into an equivalent program where theparameters are explicit: this translation is performed automatically by thecompiler. Only the points at which data is supplied or used must be flaggedin the source text using one of the constructs mentioned above. Most importantly, the added parameters do not clutter the definitions of values like a
and b at intermediate levels in the call graph. Thus we obtain the flexibilityof parameterization, without the burden of adding parameters by hand.

1.1

Contributions of This Paper

In this paper, we study a range of different systems that support implicit
parameterization. In each case, types play a central role, both as the mechanism for guiding the translation from implicit to explicit parameterization,
and as a way to ensure type safety. In particular, we will show how themechanisms used in the above example, as well as other proposals, including
Haskell overloading [19], and parametric type classes [3], can be describedand compared as distinct points in the design space. In addition, we identify
two new designs at opposite ends of the range, and show that each is usefulin its own right. The most general of these systems is described in terms ofprogrammer-defined relations on types together with sets of functional dependencies that these relations are required to satisfy. This can be seen as
a form of multiple-parameter type classes [18], but avoiding the expressivity
3

problems and ambiguities that occur with previous proposals. A particularnovelty here is in the application of functional dependencies—from the theoryof relational databases [13, 1]—to the design of programming language typesystems. At the opposite end of the spectrum, the simplest system we consider allows types to be annotated with simple tags. Typechecking ensuresthat these tags are automatically propagated through the call graph, where
they can be used for simple forms of program analysis. The following diagram summarizes the relationships between some of the systems mentioned
here, and gives a simplified view of the design space.
Type Relations with
Functional
Dependencies@@
R@
Dynamic Scoping with
Static Types

Type Classes

@
@
R
@

Tags

For concreteness, the ideas in this paper are presented as extensions of thefunctional language Haskell [17], and have been prototyped as extensions to
the Hugs interpreter [11]. In principle, however, they could be applied to amuch wider range of typed languages.

1.2

Structure of This Paper

The remainder of this paper is as follows. In Section 2, we describe the key
elements of type-based implicit parameterization. Two features distinguishthe approach used here from more conventional type systems. First, we
combine typing with translation by including both source terms and theirtranslations in each typing judgment. Second, we work with assumption setsthat associate each implicit parameter with the variable that will be used as
its translation, and with its expected type.
In Section 3, we use our framework to complete the presentation of Lewis etal.’s proposal for dynamic scoping with static types. We add rules for the4constructs that bind and access implicit parameters, and place a restriction
on the form of assumption sets.
In Section 4, we show that overloading can be supported by allowing assumption sets to contain multiple translations for each implicit parameter. The
key requirement is that each translation has a different type, which meansthat we can use typing information to choose between them in any given
context.
In Section 5, we discuss coherence. This refers to the problems that occur
when the semantics of a language is defined in terms of a (potentially nondeterministic) translation: If different translations of a source term havedifferent meanings, then a semantic ambiguity results. We explain how suchcases can be detected using a syntactic notion of ambiguity on inferred types.
In Section 6, we show that there is a range of language designs for overloading,varying in the level of detail that must be provided to declare and use an
overloaded symbol. Haskell type classes and the system that we describe in
Section 4 are at opposite ends of this spectrum, but use the same underlying
machinery. Moreover, for each different approach to overloading, there is acorresponding version of the dynamic scoping proposal from Section 3.
In Section 7, we shift to a more general and less operational view of the systems in previous sections by thinking in terms of tuples from a programmerdefined relation on types. In the terminology of Haskell, these relations
correspond to multiple parameter type classes [18], except that, critically, we
also allow the programmer to specify functional dependencies between theparameters. For example, a dependency of the form X ; Y indicates that
the Y components of each tuple are uniquely determined by the X components. This enables us to give a more accurate specification for each typerelation, and to use more powerful rules for resolving overloading at the sametime as a less restrictive characterization of ambiguity. In addition, we showthat the treatment of dynamic scoping and of overloading in Sections 3 and 4
are just the special cases that occur when the only dependencies are of theform ∅ ; Y and X ; ∅, respectively. Firm theoretical foundations for theseideas are provided by earlier work on improvement for qualified types [9].
In Section 8, we highlight the further special case that occurs with nullary
relations, corresponding to a form of implicit parameter whose type is fixed,
once and for all, at the point where it is defined. The overall effect is to allow

5the types of certain operations to be tagged, and to propagate these tags
throughout the call hierarchy, where they can be used for program analysis.
In Section 9, we draw our final conclusions.

2Type-based Implicit Parameterization

The example in the introduction shows how implicit parameters might beused in a practical setting, but leaves several important questions unanswered. For instance, how can we determine where implicit parameters are
required, and which values to pass or abstract over in each case? And how
can we ensure that the type of any value bound to an implicit parameter isconsistent with the type that is expected at the point of use?
An obvious answer to these questions is to reflect uses of implicit parametersin the types assigned to each expression or variable. More precisely, we will
give each function a qualified type [7] of the form P ⇒ τ . Here, τ gives
the explicit portion the function’s type, which includes the return type andthe type of any explicit parameters. The predicate part, P , contains zeroor more predicates, π, each of which acts as the specification for an implicit
parameter. For example, a predicate of the form (?x τ ) indicates that an
implicit parameter ?x is required with a value of type τ . In our earlier
example, the use of ?x in the definition of c would result in a predicate of
the form (?x τ ) in the type of c, and hence in the types of both b and a.
This will eventually be discharged by the with construct in the definitionof main, at which point we can also check that x has the type τ that itneeds to be bound to ?x . As a notational convenience, we will allow multiple
predicates to be written together in a tuple. For example, (π1 , π2 ) ⇒ τ andπ1 ⇒ π2 ⇒ τ represent exactly the same qualified type, as do () ⇒ τ and τ .
To make this work, typechecking and translation must be combined into asingle process. This can be captured using judgments of the form: I |A `E ; E 0 : σ. Here, E is a source term of type σ, and E 0 is its translation.
On the left of the ` symbol, A holds pairs of the form (x : σ), each of which
records an assumption about the type σ of an explicit parameter or named
constant x . The set I plays a similar role for implicit parameters, using
assumptions of the form (i : π). In this case, i is the variable that represents
the implicit parameter specified by π in the translation E 0 . We will assume6

that no x (resp. i ) appears more than once in any A (resp. I ). If a term has
an inferred type of the form π ⇒ ρ, then its translation will include an extra
parameter, as shown in the following rule:I ∪ {i : π}|A ` E ; E 0 : ρ
I |A ` E ; (λi .E 0 ) : π ⇒ ρ(⇒I )In a similar way, to use a value of type π ⇒ ρ, we must first supply an
implicit parameter meeting the specification π to obtain a result of type ρ:
I |A ` E ; F : π ⇒ ρ I `` e : π
I |A ` E ; Fe : ρ(⇒E )For the time being, the entailment I `` e : π used here means simply that(e : π) is one of the assumptions in I .
The (⇒I ) and (⇒E ) rules that we have just described are a fundamental,
appearing in one form or another in all of the systems that we describe inthis paper. A more complete list of such typing rules appears in Figure 1,
most of which are fairly standard [4, 14, 6, 7]. Note the use of different symbols τ (monotypes), ρ (qualified types), and σ (polymorphic type schemes)
to restrict the application of certain rules to specific sets of type expressions.
In passing, we note that the (∀I ) and (∀E ) rules for dealing with polymorphism can be thought of as a form of implicit parameterization over types[8]. The judgment I `` S : I 0 in rule (weak ) is a shorthand for a collection ofentailments I `` e : π, with one for each (i : π) ∈ I 0 . The results are collected
in S , a substitution on terms, mapping each i to the corresponding e. In
the case described above, where entailment just means membership, this isequivalent to writing I ⊇ I 0 , and using the null substitution for S . Note alsothat we write TV (A) in the statement of (∀I ), and elsewhere in this paper,
to denote the set of type variables that appear free in A.

3

Dynamic Scoping with Static Types

In this section, we return to our description of Lewis et al.’s [12] proposal for
dynamic scoping with static types, hereafter referred to simply as DS. We
7

Variables:(var )

Weakening:(weak )

Explicit
Parameters:

(→I )

(→E )

Implicit
Parameters:

(⇒I )

(⇒E )

Polymorphism: (∀I )(x : σ) ∈ A
I |A ` x ; x : σ
I 0 |A ` E ; E 0 : σ

I `` S : I 0

I |A ` E ; SE 0 : σ
I |Ax , x : τ 0 ` E ; E 0 : τ
I |A ` (λx .E ) ; (λx .E 0 ) : τ 0 → τ
I |A ` E ; E 0 : τ 0 → τ

I |A ` F ; F 0 : τ 0

I |A ` EF ; E 0 F 0 : τI ∪ {i : π}|A ` E ; E 0 : ρ
I |A ` E ; (λi .E 0 ) : π ⇒ ρ
I |A ` E ; E 0 : π ⇒ ρ I `` e : π
I |A ` E ; E 0 e : ρ
I |A ` E ; E 0 : σ

t 6∈ TV (A) t 6∈ TV (I )I |A ` E ; E 0 : ∀t.σ
I |A ` E ; E 0 : ∀t.σ(∀E )I |A ` E ; E 0 : [τ /t]σFigure 1: Core type system for Implicit Parameterization

8

start by giving rules for the constructs that are used to bind and access implicit parameters. The first shows how application is used in the translationof with:
I |A ` E ; E 0 : (?x τ ) ⇒ ρ I |A ` F ; F 0 : τ
I |A ` (E with ?x = F ) ; E 0 F 0 : ρIn practice, uses of this rule would normally be preceded by (⇒I ) to obtainan appropriate type for E . This suggests a more direct rule for with:I ∪ {i : (?x τ )}|A ` E ; E 0 : ρ I |A ` F ; F 0 : τ
I |A ` (E with ?x = F ) ; (let i = F 0 in E 0 ) : ρ
The remaining rule is an axiom, which shows that an implicit parameter ?xis treated as an (implicitly parameterized) identity function:
I |A `?x ; (λi .i ) : ∀a.(?x a) ⇒ a
A more direct rule can be obtained by combining this with (⇒E )—and witha single β-reduction—to obtain:
I `` e : (?x τ )I |A `?x ; e : τ
These two derived rules show very clearly how accesses and bindings of implicit parameters translate into the standard constructs for accessing andbinding variables.
To complete our definition of DS, we need to add the restriction that no?x can appear more than once in any given I . For example, this prevents
us from using an I that contains two distinct assumptions i : (?x τ ) andj : (?x τ ), with two different interpretations for ?x in the same context. Thevery fact that such parameters are implicit means that there would be noway for a programmer to specify which alternative should be used. As aresult, the expression (?x , ?x )—a pair that uses the same implicit parameterin each component—will have a most general type of ∀a.(?x a) ⇒ (a, a),9with the same type for each component and with translation (λi .(i , i )). On
the other hand, the expression (1+?x , not ?x ), which uses ?x as a number
and as a boolean in the same scope, is not well-typed.
The typing rules in Figure 1 do not include a rule for local definitions. A
suitable definition for DS is as follows:∅|A ` E ; E 0 : σ

I |Ax , x : σ ` F ; F 0 : τ

I |A ` (let x = E in F ) ; (let x = E 0 in F 0 ) : τ(let)

Requiring an empty set, ∅, of implicit parameter assumptions here in the typing of E here is critical, both to ensure a coherent semantics (see Section 5)
and to obtain the desired form of dynamic, rather than static scoping. Consider, for example, the following term:(let y =?x in (y with ?x = 0)) with ?x = 1.
With static scoping, we would evaluate y using the definition ?x = 1 that is
in scope at the point where y is defined, and so the whole expression would
evaluate to 1:
let i = 1 in (let y = i in (let i = 0 in y))=⇒ 1.
However, our (let) rule can only be applied if we have first moved any predicates that are required by E into the inferred type σ, typically using (⇒I ).
The overall effect is to defer the binding of implicit parameters to the pointof use. Returning to the current example, this leads to a translation thatsimulates dynamic scoping, using the definition ?x = 0 that is in scope at
the point where y is used, so that the whole expression evaluates to 0:
let i = 1 in (let y = (λi .i ) in (let i = 0 in y i ))=⇒ 0.
Notice that we do not allow dynamic scoping of λ-bound variables: The (→I )and (→E ) rules in Figure 1 allow only simple monotypes τ as function arguments, and not qualified types. This can be viewed as a distinct advantageof the approach described here because it helps to avoid some of the context
bugs that occur with more traditional forms of dynamic scoping [5].
104Overloading

In this section, we will show very briefly that a simple form of overloading—in which a single symbol can have multiple interpretations within the same
scope—can be understood as a form of implicit parameterization. Several
aspects of our presentation are new, but the observations on which it is based
can be traced back at least as far as Wadler and Blott’s original proposal for
type classes [19], which was subsequently refined and adopted as part of thestandard for Haskell [17].
Consider again the restriction that we made to complete our definition of DS
in the previous section. By insisting that no ?x appear more than once in any
given I , we rule out examples like I1 = {i : (?x τ ), j : (?x τ )}—which is entirely
reasonable because there is no way to choose between the two translations.
However, we also prohibit examples like I2 = {i : (?x τ ), j : (?x τ 0 )}, where
different types τ 6= τ 0 could be used to guide such a choice.
To pursue this idea in a little more depth, we introduce a second class of
implicit parameters, with names of the form !x , and with exactly the same
typing rules as the ?x form that we saw in the previous section. The only
difference will be to require that no !x appears more than once with the same
type1 in any given I . With this more relaxed condition, the most general
type of the expression (!x , !x ) will be: ∀a, b.(!x a, !x b) ⇒ (a, b), with atranslation (λi .λj .(i , j )), allowing each component of the resulting pair tohave a different type. The following example illustrates more clearly how
these constructs can be used to support a simple form of overloading, leaving
the type system to match up each use of an implicit parameter with anappropriate binding:((1+!x , not !x ) with !x = 41) with !x = True=⇒ (42, False).
1

A stronger version of this restriction is required for languages, where the type ofan expression may not be uniquely determined. In a language with a Hindley/Milner
type system, for example, we would need to prohibit any I that associates two or more
unifiable types with the same implicit parameter: if two types are unifiable, then there aresubstitution instances at which they would be equal and an ambiguity would occur.

11

5

Coherence and Ambiguity

Unfortunately, in some cases, it is not possible for the type system to determine which binding of an implicit parameter should be used. The following
example uses a polymorphic function, length, to calculate the length of a list
!xs, in the presence of two bindings for !xs, one of which is a list of integersof length 3, the other a list of booleans of length 2:
length !xs with !xs = [1, 2, 3]
with !xs = [True, False]
There is nothing in the way that !xs is used here to indicate which of thesetwo possibilities is intended. We can even see this in the principal typeof length !xs, which is ∀ a . (!xs [a]) ⇒ Int; notice that there is nothing in
the portion of the type to the right of the ⇒ symbol, reflecting the explicit
context in which the term might be used, that would help to determine anappropriate type for a. Indeed, we can construct two translations for thisterm, one of which uses the first binding and evaluates to 3, while the otheruses the second, and evaluates to 2. In other words, this is a semanticallyambiguous expression because it does not have a well-defined meaning.
Practical experience suggests that semantic ambiguities do not occur too
frequently in more realistic (and hence larger) applications; the context inwhich an overloaded symbol appears will usually give enough information todetermine which interpretation is required. But we cannot expect to avoid
ambiguity problems altogether. The best we can hope for is some simple test
that a typechecker can use to detect such problems, and report them to theprogrammer.
Motivated by examples like the one above, we say that a type of the formP ⇒ τ is ambiguous if there is a variable in TV (P ) that does not appear inTV (τ ). Now we can apply the results of previous work [2, 7] which guaranteethat a term has a well-defined, or coherent semantics if its principal type is not
ambiguous. This important result relates semantic ambiguity to a syntactic
property of principal types, which is easy for a compiler to check.
In some cases, this characterization of ambiguity is too restrictive. Thereis no need to regard a type of the form ∀a.(?x a) ⇒ Int as ambiguous, forexample, because we can never have more than one binding for ?x in scope at12any given time. In effect, the choice of a will be determined, unambiguously,by the caller, rather than by the context in which ?x is used. For similarreasons, we do not need to treat ∀a.(?x a, !x a) ⇒ Int as an ambiguous
type, even though the type variable a appears to the left of the ⇒ in a !x
predicate; this use of a is ‘covered’ by the simultaneous occurrence of a in
the ?x predicate, which means that it will be uniquely determined.
Later, in Section 7.3.3, we will give a more useful definition of syntactic
ambiguity that reflects the intuitions presented here. For the time being, let
us just summarize the key differences that we have observed between the ?x
and !x forms of implicit parameterization:• If (?x τ ) and (?x τ 0 ) both hold in the same context, then τ must be
equal to τ 0 . No such restriction is needed for the !x form of predicates.
• If a type variable a appears in a predicate (!x τ 0 ) ∈ P of an inferred
type P ⇒ τ , but not in the body τ , then the type is ambiguous. No
such test is needed for the ?x form of predicates.
In the remaining sections we show that these differences arise naturally byviewing the two forms of implicit parameterization as special cases of a moregeneral system.

6

Declaring Implicit Parameters

In this section, we show that the system of overloading that we described in
Section 4 is just one point in a spectrum of closely related designs, varying in
the degree to which programmers are expected to declare overloaded operators before they are used. The !x form of overloading is the most lightweight,
requiring no explicit declaration. At the other extreme, where declarations
are used to specify the name, type and predicate of each overloaded operator,
we obtain a system more like Haskell type classes [19, 17]. More interestingly, for each variation on the theme of overloading, there is a corresponding
language design for the dynamic scoping mechanisms that were presented in
Section 3.
We start with the !x form of overloading that was described in Section 4
in which there is no need—and indeed, no possibility—for programmers to13

declare a variable as an overloaded symbol; in effect, we have reserved a lexically distinct family of identifiers, specifically for that purpose. In addition,for each overloaded identifier, we have also provided a corresponding formof predicate, which is related to the identifier by the fact that it uses thesame symbol. If, for example, we wanted to define an overloaded equality
function that could be used to compare values of several different types, thenwe might naturally choose to use the symbol !eq for that purpose, with type∀a.(!eq a) ⇒ a.
An alternative to this is to have only one lexical form of identifier, and allow
programmers to specify which will be used as overloaded operators:
overload eq.
Given this declaration, free occurrences of eq, would be treated as constantsof type ∀a.(eq a) ⇒ a; without it, they would be flagged as errors. All thatdeclarations like this really do is give programmers more freedom in choosing
names for overloaded operators.
It is a small step to allow declarations of overloaded symbols to specify atype, constraining, but also documenting the way in which those symbols
are expected to be used. The following illustrates one possible syntax:
overload eq a :: a → a → Bool .
The effect of this would be to treat eq as a function of type ∀a.(eq a) ⇒ a →a → Bool . The declared type is treated as a template, with the expectationthat any attempt to bind or use eq at a type that does not match it will
be flagged as an error. Note that we use a predicate of the form eq a; we
do not need to include the full type of eq here, just the part that can varyfrom one binding to another. With the particular choice of syntax here, theprogrammer writes the general form of the predicate to the left of the ::symbol; note that there may be more than one type argument if the typeon the right has more than one free variable. The ability to declare types
explicitly can result in a strictly more expressive system. For example, thefollowing declaration associates a polymorphic type with the identifier unit:
overload unit m :: ∀ a . a → m a.
14

This takes us beyond the limits of Hindley-Milner typing because it meansthat a translation will need to pass around a polymorphic function as animplicit parameter.
The final variation that we consider provides a syntax that allows multiple
overloaded symbols to be associated with a single form of predicate. The
only difference here with the syntax for Haskell type classes is in the use ofoverload instead of class:overload Eq a whereeq:: a → a → Bool
notEq :: a → a → Bool
Here, both eq and notEq would be treated as functions of type ∀a.(Eq a) ⇒a → a → Bool . The implicit parameter in this case would be a tuple orrecord containing the implementations of these two functions for a particular
choice of a, while eq and notEq would be implemented by the corresponding
projections. This extension does not make the language any more expressive,
but it can often be useful as a means of grouping related entities into a single
package. In practice, it can also help to reduce the number of predicatesin inferred types because multiple overloaded symbols can share the same
predicate.
The four points in the design space for overloading that we have describedhere have corresponding points in the design space for DS-like system. Apart,
perhaps, from using a different keyword to distinguish dynamic scoping mechanisms from overloading, the notation, and motivation in each case would be
the same as in each of the examples above. The only difference would be in
the rules for detecting ambiguity, and for preventing multiple interpretationsof a symbol, with the same differences that we described for the ?x and !x
styles of implicit parameter at the end of Section 5.

7

Type Classes and Type Relations

In previous sections, we have assumed a fairly operational interpretation for
qualified types, thinking in terms of the additional parameters that they willlead to in the translation of a given program. Another way to understand15

the predicates in a qualified type is as constraints on the way that a typecan be instantiated—in fact that was the original motivation for the term
‘predicate’. For example, given the following typing:eq :: ∀a.(Eq a) ⇒ a → a → Bool ,we can think of the (Eq a) predicate as restricting the choices for the (otherwise universally quantified) type variable a to types for which an equality
has been defined. In fact, we can identify Eq with that particular set oftypes, and think of the predicate (Eq a) as meaning a ∈ Eq, and of thetype for eq as representing all the types in the set {t → t → Bool | t ∈ Eq}.
It is this set theoretic view of predicates representing membership within aset (or ‘class’) that motivates our use of the term ‘type class’. In Haskell, atype class is populated by a collection of instance declarations that can beextended as necessary to include additional datatypes. These declarations,which correspond to a kind of top-level with construct, provide general rule
schemes that can be used to construct bindings for overloaded symbols atmany different types. This can be reflected in the definition of entailment[7], but we will not discuss these issues any further in this paper.
We can also think of the (?x τ ) and (!x τ ) forms of predicates as representing
sets of types in a similar way. We can tell a little more about the kind ofsets that can be represented by recalling the restrictions that we placed on
the use of such predicates in an assumption set I . For example, the setscorresponding to predicates using ?x will have at most one element. Of
course, different one element sets might be needed to interpret ?x at different
points in a program, depending on the way that with bindings have beenused.
We have already mentioned the possibility that a predicate may have multiple
type arguments. In this case, we can think of the predicate as representing a
relation on types. In the context of Haskell, these relations are referred to as
multiple parameter type classes. In the ten years since type classes were first
introduced, many interesting applications have been proposed for multiple
parameter type classes [18], and several of the current Haskell implementations provide support for them. However, in our experience, the results canoften be disappointing, leading to many ambiguities, and resulting in weakor inaccurate inferred types that delay the compiler’s ability to detect typeerrors. This is probably why even the most recent revision of the Haskell
16

standard [17] does not provide support for multiple parameter type classes.

7.1

Example: Collection Types

To illustrate the kinds of problem that can occur, consider the task of providing uniform interfaces to a wide range of different collection types. The
following declaration, greatly simplified for the purposes of this presentation,
introduces a two parameter class that could be used as the starting point forsuch a project:class Collects e c where
empty
:: c
insert:: e → c → cmember :: e → c → Bool
The intention here is that Collects e c holds if c represents a collection ofvalues of type e, which would be demonstrated by providing appropriate
definitions for the operations listed in the body of the class. To define theentries in this relation, we might use a collection of instance declarations,something like the following2 :instance Eq e ⇒ Collects e [e] where . . .
instance Collects Char BitSet where . . .
instance Eq e ⇒ Collects e (e → Bool ) where . . .
instance (Hashable a, Collects a c)
⇒ Collects a (Array Int c) where . . .
The first line declares lists of type [e] as collections of elements of type e,
provided that e is an equality type. The second line indicates that bit sets canbe used to represent sets of characters. The third line uses the representationof a collections as a characteristic functions. The last declaration is forhashtables, represented by arrays, with integer hash codes as indices, andusing a second collection type to gather the elements in each bucket (i.e.,elements with the same hash code).
2

For brevity, we omit the definitions for empty, insert, and member in each case.

17

At first glance, this approach seems very attractive, but in practice, wequickly run into serious problems. For example, if we look more closely
at the definition of empty, then we see that it has an ambiguous type:empty :: Collects e c ⇒ c.
As a result, any program that uses empty will have an ambiguous type, andwill be rejected by the typechecker. Different kinds of problem occurs withdefinitions like:
findEither x y c = member x c || member y c.
For this example, we can infer a principal type:
findEither :: (Collects e1 c, Collects e2 c)⇒ e1 → e2 → c → Bool .
However, this is actually more general than we would hoped for because
it allows the arguments x and y to have different types. For the familyof collection types that we are trying to model here, we expect any given
collection to contain only one type of value, but the type system is notstrong enough to capture this.
7.1.1

Using Constructor Classes

One way to avoid the problems with Collects is to use constructor classes [10],and replace the definition of Collects given previously with the following:class Collects e t whereempty:: t einsert:: e → t e → t emember :: e → t e → Bool
This is the approach taken by Okasaki [15], and by Peyton Jones [16], inmore realistic attempts to build this kind of library. Note that the type cin the original definition has been replaced with a unary type constructor18

t; a function of kind ∗ → ∗. This solves the immediate problems with thetypes for empty and findEither mentioned previously by separating out thecontainer from the element type. However, it is considerably less flexible:
Only the first of the four instance declarations given previously can be
modified to work in this setting; the remaining instances define collections
using types that do not unify with the form t e that is required here.
7.1.2

Using Parametric Type Classes

Another alternative is to use parametric type classes [3], which allows predicates of the form c ∈ Collects e, meaning that c is a member of the classCollects e. Intuitively, we think of having one type class Collects e for eachpossible choice of the e parameter. The definition of a parametric Collects
class looks much like the original:
class c ∈ Collects e where
empty
:: c
insert:: e → c → cmember :: e → c → Bool
What makes it different is the implied assumption that the element type e
is uniquely determined by the collection type c. A compiler that supports
parametric type classes must ensure that the declared instances of Collects
do not violate this property. In return, it can often use the same information
to avoid ambiguity and to infer more accurate types. For example, the typeof empty is now ∀e, c.(c ∈ Collects e) ⇒ c, and we do not need to treat
this as being ambiguous, because the unknown element type e is uniquelydetermined by c.
7.1.3

Using Functional Dependencies

In this paper, we introduce a generalization of parametric type classes thatallows programmer to declare explicit dependencies between the parametersof a predicate. For example, this allows us to annotate the original classdefinition with a dependency c ; e, indicating that the element type e is19uniquely determined by the choice of c:class Collects e c | c ; e where
empty
:: c
insert:: e → c → cmember :: e → c → Bool
We defer more detailed discussion about the interpretation of these dependency annotations to Section 7.3. We note, however, that this approach isstrictly more general than parametric type classes because it allows us toexpress a larger class of dependencies, including mutual dependencies suchas {a ; b, b ; a}. It is also easier to integrate with the existing syntax ofHaskell because it does not require any changes to the syntax of predicates.

7.2

Relations and Functional Dependencies

Before we given any further examples, we pause for a brief primer on relations
and functional dependencies, and for a summary of our notation. These ideas
were originally developed as a foundation for the study of relational databases[1]. They are well-established, and detailed presentations of the theory, andof useful algorithms for working with them in practical settings, can be foundin standard textbooks on the theory of databases [13]. The novelty of thecurrent paper is in applying them to the design of a type system.
7.2.1

Relations

Following standard terminology, a relation R over an indexed family of sets
{Di }i∈I is just a set of tuples, each of which is an indexed family of values{ti }i∈I such that ti ∈ Di for each i ∈ I . More formally, R is just a subsetof Πi ∈ I .Di , where a tuple t ∈ (Πi ∈ I .Di ) is a function that maps eachindex value i ∈ I to a value ti ∈ Di called the i th component of t. In thespecial case where I = {1, . . . , n}, this reduces to the familiar special casewhere tuples are values (t1 , . . . , tn ) ∈ D1 × . . . × Dn . If X ⊆ I , then we writetX , pronounced “t at X ”, for the restriction of a tuple t to X . Intuitively,tX just picks out the values of t for the indices appearing in X , and discards
any remaining components.
20

7.2.2Functional Dependencies

In the context of an index set I , a functional dependency is a term of theform X ; Y , read as “X determines Y ,” where X and Y are both subsetsof I . If X and Y are known sets of elements, say X = {x1 , . . . , xn } andY = {y1 , . . . , ym }, then we will often write the dependency X ; Y in theform x1 . . . xn ; y1 . . . ym . If a relation satisfies a functional dependency
X ; Y , then the values of any tuple at Y are uniquely determined by thevalues of that tuple at X . More formally, we write:
R |= X ; Y ⇐⇒ ∀t, s ∈ R.tX = sX ⇒ tY = sY .
This also extends to sets of dependencies:
R |= F ⇐⇒ ∀(X ; Y ) ∈ F .R |= X ; Y .
For example, if we take I = {1, 2}, then the relations satisfying {{1} ; {2}}are just the partial functions from D1 to D2 , and the relations satisfying{{1} ; {2}, {2} ; {1}} are the partial injective functions from D1 to D2 .
If F is a set of functional dependencies, and J ⊆ I is a set of indices, thenthe closure of J with respect to F , written JF+ is the smallest set such that:• J ⊆ JF+ ; and• If (X ; Y ) ∈ F , and X ⊆ JF+ , then Y ⊆ JF+ .
For example, if I = {1, 2}, and F = {{1} ; {2}}, then {1}+F = I , and++{2}F = {2}. Intuitively, the closure JF is just the set of indices that are
uniquely determined, either directly or indirectly, by the indices in J andthe dependencies in F . Closures like this are easy to compute; for practical
purposes, a simple fixed point iteration will suffice.

7.3

Typing with Functional Dependencies

This section describes the steps that are needed to make use of information about functional dependencies during type checking. We will assume
that dependencies are specified as part of whatever mechanism the language
provides for introducing new forms of predicate, whether it be class declarations as in Section 7.1, overload declarations as in Section 6, or some21

other construct altogether. More specifically, we will assume that there issome collection of predicate symbols p, each of which has an associated setof indices Ip , and an associated set of functional dependencies Fp . We will
also assume that all predicates are written in the form p t, where t is a tupleof types indexed by Ip .
The techniques described in the following subsections have been used toextend the Hugs interpreter [11] to allow the declarations of classes to beannotated with sets of functional dependencies, as suggested in Section 7.1.3.
The implementation works well in practice, and we expect that it will be
included in the next public distribution. Pleasingly, some early users havealready found new applications for this extension in their own work.
Formal justification for these techniques comes from the theory of improvement for qualified types [9]. The main idea is that we can apply certain
forms of satisfiability-preserving substitutions during type checking, resulting in more accurate inferred types, without compromising on a useful notionof principal types.
7.3.1

Ensuring that Dependencies are ValidOur first task is to ensure that all declared instances for a predicate symbol p
are consistent with the functional dependencies in Fp . For example, supposethat we have an instance for p of the form:
instance . . . ⇒ p t where . . .
Now, for each (X ; Y ) ∈ Fp , we must ensure that TV (tY ) ⊆ TV (tX ) orotherwise the elements of tY might not be uniquely determined by the elements of tX . A further restriction is needed to ensure pairwise compatibility
between instances for p. For example, if we have a second instance:
instance . . . ⇒ p s where . . . ,and a dependency (X ; Y ) ∈ Fp , then we must ensure that tY = sY whenever tX = sX . In fact, on the assumption that the two instances will normallycontain type variables—which could later be instantiated to more specifictypes—we will actually need to check that: if tX and sX have a most general22

unifier U , then UtY = UsY . This is enough to guarantee that the declareddependencies are satisfied. For example, the instance declarations in Section 7.1 are consistent with the dependency c ; a that we are assuming forthe predicate symbol Collects.
7.3.2

Improving Inferred Types

There are two ways that a dependency (X ; Y ) ∈ Fp for a predicate symbol
p can be used to help infer more accurate types:• Suppose that we have two predicates p t and p s. If tX = sX , then tY
and sY must be equal.
• Suppose that we have an inferred predicate p t, and an instance:
instance . . . ⇒ p t 0 where . . .
If tX = StX0 , for some substitution S (which could be calculated by
one-way matching), then tY and StY0 must be equal.
In both cases, we can use unification to ensure that the equalities are satisfied:If unification fails, then we have detected a type error.
7.3.3

Detecting Ambiguity

As we described in Section 5, we must reject any program with an ambiguous
principal type because of the potential for semantic ambiguity. With ourprevious definition, a type of the form P ⇒ τ is considered ambiguous if
there is a type variable a ∈ TV (P ) that is not also in TV (τ ); our intuitionis that, if there is no reference to a in the body of the type, then there will be
no way to determine how it should be resolved. However, we have also seenthat more relaxed notions of ambiguity can be used in situations where thepotentially ambiguous variable a might be resolved by some other means.
So, in fact, we need not insist that every a ∈ TV (P ) is mentioned explicitlyin τ , so long as it is uniquely determined by the variables in TV (τ ).

23The first step to formalizing this idea is to note that every set of predicates P
induces a set of functional dependencies FP on the type variables in TV (P ):{ TV (tX ) ; TV (tY ) | (p t) ∈ P , (X ; Y ) ∈ Fp }.
This has a fairly straightforward reading: if all of the variables in tX are
known, and if X ; Y , then the components of t at X are also known, andhence so are the components, and thus the type variables, in t at Y .
To determine if a particular type P ⇒ τ is ambiguous, we should first calculate the set of dependencies FP , and then take the closure of TV (τ ) withrespect to FP to obtain the set of variables that are determined by τ . The
type is ambiguous only if there are variables in P that are not included inthis closure. More concisely, the type P ⇒ τ is ambiguous if, and only if:
TV (P ) 6⊆ (TV (τ ))+
FP .

7.4

A Unified View of Implicit Parameters

We are now in a position to show that the mechanisms for dynamic scoping
and for overloading in earlier sections are really just special cases of our moregeneral system using type relations and functional dependencies:• For dynamic scoping, we add a dependency of the form ∅ ; a for eachpredicate argument a.
• For overloading, we add a dependency of the form a ; ∅ for each predicate argument a.
The different treatments of multiple interpretations and of ambiguity forthese two forms of implicit parameter that we observed in Section 5 follow
directly from the more general definitions in Sections 7.3.2 and 7.3.3, respectively; it is as if we had declared a pair of classes for each identifier x :class (?x a) | ; a where ?x :: aclass (!x a) | a ; where !x :: a.
In a similar way, each of the different designs described in Section 6, including
Haskell type classes, can be understood as special cases of the more generalsystem presented here.
24

8

Tags

In this penultimate section, we hint briefly at the potential of a further
special case that occurs when we use predicates that have no parameters,
and so corresponding to nullary relations. This provides a mechanism for
attaching a ‘tag’ to the type of a function f , that will then be propagatedthrough the call hierarchy to all functions that depend on f , either directly
or indirectly. Thus we can use types to effect a dependency analysis on a
program, and because it is type-based, this analysis can be made to work in a
way that is compatible with separate compilation. We can be more selective
in our analysis by tagging only some of the functions that might be used. One
area where facilities like this would be particularly useful is in security. For
example, if a language provides unsafe primitives, then they could be tagged
as such using a definition like the following to ensure that the potential for
unsafe behavior is clearly signaled in the type of any program that uses thisprimitive:class Unsafe where
unsafePerformIO :: IO a → a
Another possibility might be to define a security hierarchy, as in the following
simple example:
class Public where . . .
class Public ⇒ LowSecurity where . . .
class LowSecurity ⇒ HighSecurity where . . .
class HighSecurity ⇒ TopSecret where . . .
The intention here would be to assign appropriate levels of security for potentially restricted operations, and then use type inference to determine whichlevel of security any given program requires. The corresponding implicit parameters could be used to thread the required key or access code through theprogram to the point where it is required, without exposing it as an explicit
parameter that could be inspected, modified, or misused.

25

9Conclusions and Future WorkIn this paper we have explored the design space for type-based implicit parameterization, investigating the similarities between different systems, andexposing some of the choices for language design. Our most general system
makes essential use of relations on types, together with functional dependencies, and is useful in its own right, as well as providing a unified view of othersystems.
In constructing this system, we have used ideas from the theory of relational
databases. One interesting area for future work would be to see if otherideas developed there could also be exploited in the design of programming
language type systems.

Acknowledgments
I would like to thank my friends and colleagues in PacSoft at the Oregon
Graduate Institute for a stimulating environment, and for their interest in
this work. Particular thanks to Jeff Lewis for helping me to understand his
implementation of implicit parameters in Hugs, and to Lois Delcambre of the
Database and Object Technology Laboratory at OGI for explaining the rolethat functional dependencies play in database theory.
The research reported in this paper was supported by the USAF Air MaterielCommand, contract # F19628-96-C-0161.

References[1] W. W. Armstrong. Dependency structures of data base relationships.
In IFIP Cong., Geneva, Switzerland, 1974.
[2] S. M. Blott. An approach to overloading with polymorphism. PhD thesis,
Department of Computing Science, University of Glasgow, July 1991.
(draft version).

26

[3] K. Chen, P. Hudak, and M. Odersky. Parametric type classes (extended
abstract). In ACM conference on LISP and Functional Programming,
San Francisco, CA, June 1992.
[4] L. Damas and R. Milner. Principal type schemes for functional programs. In 9th Annual ACM Symposium on Principles of Programming
languages, pages 207–212, Albuquerque, NM, January 1982.
[5] M. J. Gordon. Programming Language Theory and its Implementation.
Prentice Hall International, 1988.
[6] R. Hindley. The principal type-scheme of an object in combinatory
logic. Transactions of the American Mathematical Society, 146:29–60,
December 1969.
[7] M. P. Jones. Qualified Types: Theory and Practice. PhD thesis, Programming Research Group, Oxford University Computing Laboratory,
July 1992. Published by Cambridge University Press, November 1994.
[8] M. P. Jones. ML typing, explicit polymorphism and qualified types.
In TACS ’94: Conference on theoretical aspects of computer software,
Sendai, Japan, New York, April 1994. Springer-Verlag. Lecture Notes
in Computer Science, 789.
[9] M. P. Jones. Simplifying and improving qualified types. In International
Conference on Functional Programming Languages and Computer Architecture, pages 160–169, June 1995.
[10] M. P. Jones. A system of constructor classes: overloading and implicit
higher-order polymorphism. Journal of Functional Programming, 5(1),January 1995.
[11] M. P. Jones and J. C. Peterson. Hugs 98 User Manual, May 1999.
Available on the web from http://www.haskell.org/hugs/.
[12] J. Lewis, M. Shields, J. Launchbury, and E. Meijer. Implicit parameters: Dynamic scoping with static types. manuscript, submitted for
publication, July 1999.
[13] D. Maier. The Theory of Relational Databases. Computer Science Press,
1983.
27

[14] R. Milner. A theory of type polymorphism in programming. Journal ofComputer and System Sciences, 17(3), 1978.
[15] C. Okasaki. Edison User’s Guide, May 1999.
[16] S. Peyton Jones. Bulk types with class. In Proceedings of the Second
Haskell Workshop, Amsterdam, June 1997.
[17] S. Peyton Jones and J. Hughes, editors.
Report on the
Programming Language Haskell 98, A Non-strict Purely Functional Language, February 1999.
Available on the web fromhttp://www.haskell.org/definition/.
[18] S. Peyton Jones, M. Jones, and E. Meijer. Type classes: Exploring the design space.
In Proceedings of the Second Haskell
Workshop, Amsterdam, June 1997. Available on the web fromhttp://www.cse.ogi.edu/~mpj/pubs/multi.html.
[19] P. Wadler and S. Blott. How to make ad hoc polymorphism less ad hoc.
In Proceedings of 16th ACM Symposium on Principles of Programming
Languages, pages 60–76, Jan 1989.

28