A static semantics for Haskell

Simon L Peyton Jones Philip Wadler

Department of Computing Science, University of Glasgow, G12 8QQ

(email: {simonpj, wadler}@cs.glasgow.ac.uk) February 19, 1992

Abstract

This paper gives a static semantics for a large subset of Haskell, including giving a translation into a language without overloading.

It is our intention to cover the complete language in due course. One innovative aspect is the use of ideas from the second-order lambda calculus to

record type information in the program.

Contents

1 Introduction 4 2 A sketch of how overloading is resolved 6 3 Notation 7 4 Abstract syntax 13 5 Programs 19 6 Type declarations 21 7 Class declarations 24 8 Instance declarations 26 9 Value declarations 28 10 Expressions 37 11 Pattern matching 40

12 Dictionary manipulation 45

13 Implementation notes 47

14 References 47

List of Figures

1 Syntax of semantic types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2 Environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3 Abstract syntax for Haskell: declarations and bindings . . . . . . . . . . . . . 14 4 Abstract syntax of Haskell: patterns and expressions . . . . . . . . . . . . . . 15 5 Abstract syntax of Haskell: types . . . . . . . . . . . . . . . . . . . . . . . . . 16 6 Extra syntax for translated programs . . . . . . . . . . . . . . . . . . . . . . . 16 7 Rule for programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 8 Rules for monotype . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 9 Rules for context and polytype . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 10 Rules for type declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 11 Rules for class declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 12 Instance declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 13 Rules for monobinds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 14 Rules for binds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 15 Rules for bind . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 16 Type signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 17 Basic rules for expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 18 Non-syntactic rules for expressions . . . . . . . . . . . . . . . . . . . . . . . . 38 19 Rules for compound expressions . . . . . . . . . . . . . . . . . . . . . . . . . . 39 20 Data structures in expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 21 Rules for enumerations expressions . . . . . . . . . . . . . . . . . . . . . . . . 41 22 Rules for quals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 23 More realistic expression-signature rule . . . . . . . . . . . . . . . . . . . . . . 42 24 Rules for patterns . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

25 Rules for match, mrule and grhs . . . . . . . . . . . . . . . . . . . . . . . . . 44

26 Dictionary manipulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46

1 Introduction

The purpose of this paper is to give a complete static semantics for Haskell (Hudak et al. [1990]).

One approach to giving a static semantics is to give a translation from the full language into a core, which is then given a static semantics. This is economical, but since the translations are sometimes elaborate, it can lead to incomprehensible error messages from the type checker. Instead we have chosen to give a static semantics for the whole language directly.

Wadler & Blott [1989] give a formal set of type rules to describe the form of overloading in Haskell. While compact and elegant, the rules are quite hard to understand, especially since they do not take explicit account of Haskell class declarations. In effect they make each class have a single overloaded operation and identify the class with this operation. This is adequate, because the operation could be a dictionary, but it does not mesh very well with Haskell, and performing the mental translation between the two is quite tricky.

In this paper we provide a set of type rules which avoids these difficulties, and covers the complete language rather than a small subset.

1.1 Overview

We have modelled this paper on “The definition of Standard ML” (Harper, Milner & Tofte [1989]), which provided a very useful source of ideas and a high standard to work to.

In addition to performing type inference, our type system gives a translation of the original source program into one in which two implied aspects are made explicit:

• Polymorphism is made explicit, using type abstraction and application exactly as in the second-order lambda calculus.

It is often necessary in later stages of the compiler to know the types of parts of the program. For example, a strictness analyser needs to know this when when looking for fixed points, and a code generator may be able to generate better code when it knows that only certain types can occur.

It would be possible to include type information by annotating the parse tree of the program, but it is very hard to maintain this information when the program is transformed by subsequent compiler passes. Using the machinery of the second-order lambda calculus is (so far as we know) an original way to ensure that type information is maintained consistently in the face of such transformations. It is rather nice to see a practical application of this very beautiful calculus.

• Overloading is made explicit, by passing extra dictionary parameters to overloaded functions; these dictionaries include the methods to implement the operations of the class.

Exactly how this is done is quite subtle, and is explained informally in Section 2.

Section 3 with a summary of the notation we use throughout the paper.

Section 4 then gives the abstract syntax of both the source language and the target translated language. This is followed by the type inference rules themselves, beginning with the rules for whole programs in Section 5 and working down to smaller constructs (Sections 6 through 12). A non-linear order of reading is more likely to be productive for these sections than a linear pass.

A careful correspondence is maintained between the source syntax and the inference rules:

• for every syntactic nonterminal there is a judgement form, and

• for every syntactic production of a nonterminal there is an inference rule for the judgement form corresponding to that nonterminal.

In addition, there are a few further inference rules which are not syntax driven. Examples are the rules SPEC and GEN for introducing and eliminating ∀ in polymorphic types.

1.2 Shortcomings

The paper is still incomplete. The aspects of Haskell that are not covered (and will be) are, in rough order of priority:

• Imports.

• Ambiguity.

• deriving clauses in data declarations.

• Default declarations in class declarations.

• Constant and n+k patterns. These require something substantially more sophisticated

than the ⊢^{pat} judgement given later. The reason for this is that constants involve some translation due to overloading, and n+k patterns require both this and some further translation to subtract the k.

In addition we hope to add some further sections giving advice about implementation.

Finally, here is list of unresolved issues:

• Prove substitution lemma.

• How do we prove a principal type theorem?

• Do all derivations give the same translation? Can we proved different ones equivalent?

• There is an interaction between monomorphic pattern-bindings and ambiguity. Consider the expression x where y=1. Making y monomorphic will result in a free dictionary, which will at some stage be resolved by the ambiguity mechanism. In other (nonnumeric) cases this might actually cause an error, because the ambiguity-resolution mechanism is restricted to numeric classes. All in all it seems better to exclude such unused definitions, and we assume this is done by the initial dependency analysis. But, we can’t simply remove unused defns in case they contain a type error! Also at top level, we must be careful to eliminate only thosre which are not exported.

2 A sketch of how overloading is resolved

The distinctive feature of the Haskell type system is the provision of systematic overloading. In this section we sketch informally how overloading is implemented; we assume familiarity with the programmers-eye-view of Haskell.

The overloading is resolved by translating the program into an equivalent non-overloaded one, in which overloaded functions take extra parameters. For example:

        f :: (Ord a, Num a) => a -> a -> a
        f x y = if (x>y) then x+y else x

x and y must belong to a type which is an instance of both Ord (for the > operation) and Num (for the + operation). The phrase (Ord a, Num a) is called a context, and consists of an ordered sequence of class assertions.

The translation of f looks like this:

        f dord dnum x y = if ((>) dord x y) then ((+) dnum x y) else x

f takes two extra dictionary arguments dord and dnum, one for each class assertion in the context in the type of f, and in the same order^{1}.

In the translated program, the functions (>) and (+) are selectors which extract the appropriate method from the dictionary to which they are applied; the method thus extracted is what does the actual comparison or addition.

Now consider a call of f:

        g :: Int -> Int
        g x = f x x

Here we have deliberately given g a less general type signature than it could have. Here is the translation of g:

                          g x = f ordInt numIntD x x

Two extra parameters are supplied to f, namely the Ord dictionary and the Num dictionary for the Int type.

The formal type rules deliberately abstract away from whether the dictionary arguments are passed in a curried fashion (as in this example), or in an uncurried fashion as a tuple of dictionaries. In our examples we will stick to the curried form.

1 Strictly speaking, translated programs have types attached to each variable in a pattern, but we omit them here for clarity.

2.1 Dictionaries

What does a dictionary contain? Its format is set by a class declaration; here, for example, is one taken from the Prelude:

        class (Real a, Fractional a) => RealFloat a where
                properFraction :: a -> (Integer, a)
                approxRational :: a -> a -> Rational

The dictionary for a class has two parts, either of which may be empty:

• The first part consists of the dictionaries for the superclasses, in this case Real and

     Fractional.

• The second part consists of the methods for the class itself, in this case methods for

     properFraction and approxRational.

The dictionary will usually be represented by a tuple of all these components, though the actual type rules abstract away from the details of the representation.

2.2 Instances

An instance declaration may have a context; for example

        instance (Eq a, Eq b) => Eq (a,b) where
                (==) (x1,y1) (x2,y2) = (x1 == x2) & (y1 == y2)

From this instance declaration we produce a dictionary function which, given dictionaries for equality on things of type a and b, returns a dictionary for equality on things of type (a,b). Suppose this function is called eqPairFun.

Now, given the function definition

        f :: (Eq a) => a -> a -> Bool
        f x y = (x,y) == (y,x)

we translate to the following

               f eqD x y = (==) (eqPairFun eqD eqD) (x,y) (y,x)

3 Notation

This section summarises our notational conventions.

3.1 Sequences

The notation

⟨x_{1}, …, x_{n}⟩

stands an ordered sequence of the identifiers x_{1}, …, x_{n}. Sequences can be concatenated with ++.

3.2 Judgements

There is one judgement form for each nonterminal in the abstract syntax, and one rule for that judgement form for each production of that nonterminal.

In total therefore, there is a large number of judgements, but they all take one of two forms. The first is quite conventional:

inherited ⊢^{nonterminal} construct : synthesised

which can be read: “given the information inherited we can derive the information synthesised from the construct construct”, where construct is the right-hand side of one of the productions of nonterminal. The most typical form of this general scheme is to deduce types, thus:

environment ⊢^{nonterminal} construct : type

but in general synthesised may not be a type; it might be a set of value-type bindings, or an overloaded context, for example.

The rules are designed to make the derivation of a type-inference algorithm as easy as possible. In particular, the inherited parts will generally be arguments to the type-inference function, and the synthesised parts will generally be its result.

The annotation nonterminal on the turnstile serves to identify the judgement form. At the beginning of the rules for each judgement form we always give the general form of the judgement, which makes explicit the form of the judgement.

Many of the rules also express the translation of a language construct, in which case the second form of judgement is used:

inherited ⊢^{nonterminal} construct ⇝ construct : synthesised

which can be read: “given the information inherited we can derive the information synthesised from the construct construct, which translates to construct”.

In general, we use italic for source language nonterminals (nonterminal), and bold font for target language nonterminals (nonterminal).

3.3 Types

We distinguish throughout between syntactic types written by a Haskell programmer, which have the abstract syntax given in Section 4, and semantic types manipulated by the type inference rules. The former are denoted by words, such as monotype, while the latter are denoted by symbols, such as τ. The correspondence between the two is given by this table:

Monotypes τ → α  Typevariables
| χ τ_{1} … τ (k ≥ 0 ) Structuredtype
| τ_{1} → τ_{2}  Functiontype
| [τ]  Listtype
| (τ_{1}, …, τ_{k})  (k = 0 or k ≥ 2 Tupletype
| Bool  Booleantype
Polytypes σ → τ
| ∀α_{1} … α_{k}. σ  Universalquantification
| θ ⇒ σ  Predication
Contexts θ → ⟨κ_{1} τ_{1}, …, κ_{n} τ_{n}⟩

Figure 1: Syntax of semantic types

Syntactic form Semantic form
Type variable  tyvar  α
Monotype  monotype  τ
Overloaded type (none)  ρ
Polytype polytype σ
Type constructor tycon  χ
Class  class  κ
Context  context  θ

This distinction leads to a number of rather trivial-looking rules which translate syntactic types into semantic types. They are not as trivial as they seem, since they perform three useful functions:

• Checking that only in-scope type variables, constructors and class names are used.

• Checking that type constructors are only used with the correct arity, and expanding type synonyms.

• Since the syntactic names of constructors and classes each appear as the domain of an environments (see Section 3.4), the environment combiners will check that a type constructor or class is not declared more than once.

Almost all of these goals could also be achieved by merging the syntactic and semantic forms, and giving rather simpler validation rules instead. The exception is the expansion of type synonyms, which is only conveniently done by translation.

Figure 1 gives the syntax of semantic types. The unit type, () is treated as a case of the tuple type with zero components. There is no 1-tuple type, however.

The syntax of monotypes, τ, includes cases for functions, lists, tuples and so on. All of these can be regarded as special cases of the second production, with particular type constructors χ.

Environment  Notation Type
Total environment  E  (TCE, TVE, VE, CE, IE)
Value environment  VE  (CVE, GVE, LVE)
Constructor value environment CVE  con ↦ σ
Global value environment  GVE  var ↦ σ
Local value environment  LVE  var ↦ τ
Type-constructor environment TCE  tycon ↦ Λα_{1} … α_{n}. τ
Type-variable environment  TVE  tyvar ↦ α
Class environment  CE  class ↦ (κ, ∀α(θ, methods : GVE))
Instance environment  IE  (GIE, LIE)
Global instance environment  GIE  dfun ↦ ∀α_{1} … α_{n}. θ ⇒ κ τ
Local instance environment  LIE  dvar ↦ κ τ

Figure 2: Environments

The first two productions for polytypes, σ are unsurprising. The third, θ ⇒ σ, is a predicated type, where the context, θ, is an ordered list of predicates of form κ τ enclosed in angle brackets ⟨⟩.

Notice that the syntax permits some rather peculiar types, such as:

∀α. κ_{1} α ⇒ ∀β. κ_{2} β ⇒ α → β → α

These types only arise (only) from class declarations. For example, the declaration

        class Foo x where
                op :: Bar y => x -> y -> x

attributes just such a type to op. The operational reading is that op is a function taking a dictionary for Foo, from which it extracts the method for op. This method is a function which takes a dictionary for Bar in order to do its work.

The function fv() applies to polytypes (and hence overloaded types and monotypes) and returns the free type variables of the type. It extends in the natural way to sets of types.

3.4 Environments

An environment is a finite function whose domain is some name space. Sometimes we package environments up into tuples, and still call the resulting tuple an environment.

There are a number of different sorts of environments, which are given in Figure 2.

There are a number of generic operations which can be performed on environments, which are described next. After this we discuss each individual environment separately.

3.4.1 Generic operations on environments

Environments may be written explicitly using curly brackets thus: GVE_{1} = {var_{1} : σ_{1}, var_{2} : σ_{2}}. An empty environment is denoted {}.

The domain and range of an environment may be extracted using the functions dom() and ran() respectively. Thus dom(GVE_{1}) = {var_{1}, var_{2}}, and ran(GVE_{1}) = {σ_{1}, σ_{2}}.

An environment is applied to a member of its domain to return the corresponding element of the range. For example, GVE_{1} var_{2} = σ_{2}.

The notation TE of E extracts the type environment TE from the total environment E, and similarly for all components of a tupled environment.

Every local value environment is also a global value environment, since every monotype is also a polytype. The environments ∀α. GVE and θ ⇒ GVE are defined thus:

(∀α. GVE) var = ∀α. (GVE var)
(θ ⇒ GVE) var = θ ⇒ (GVE var)

The operations ⊕ and ⊕^{→} combine environments. The former checks that the domains of its arguments are distinct, while the latter “shadows” its left argument with its right. For example:

(GVE_{1} ⊕ GVE_{2}) var = \{ \begin{matrix}GVE_{1} var & if var ∈ dom(GVE_{1}) and var ∉ dom(GVE_{2}) \\ GVE_{2} var & if var ∈ dom(GVE_{2}) and var ∉ dom(GVE_{1}) \end{matrix}
(GVE_{1} ⊕^{→} GVE_{2}) var = \{ \begin{matrix}GVE_{1} var & if var ∈ dom(GVE_{1}) and var ∉ dom(GVE_{2}) \\ GVE_{2} var & if var ∈ dom(GVE_{2}) \end{matrix}

and similarly for all other environments. For brevity, we write E_{1} ⊕ E_{2} instead of a tuple of the sums of the components of E_{1} and E_{2}; and we write E ⊕ CE to combine CE into the appropriate component of E (and similarly for other components of tupled environments).

Implicit side conditions There are two implicit side conditions associated with environments, as follows:

• If E_{1} ⊕E_{2} appears in a rule, then the side condition dom(E_{1})∩dom(E_{2}) = ∅ is implied.

• Similarly, if E var appears in a rule, then the side condition var ∈ dom(E) is implied.

3.4.2 Value environments

Value environments are quite conventional, mapping variable and constructor names to types.

We distinguish the local value envionment, whose range is monotypes, from the global value environment whose range is polytypes.

3.4.3 Type constructor environment

The type constructor environment, TCE, binds all type constructors, both those introduced by type and those introduced by data. It maps the name of a type constructor onto a function which maps types onto types. The arguments supplied to this function will be the arguments to the type constructor.

In the case of type synonyms, introduced with type, the application implements the expansion of the synonym.

In the case of a type constructor tycon introduced with data, the function will always be of the form

Λα_{1} … α_{n}.χ τ_{1} … τ_{k}

where χ is the semantic type constructor corresponding to tycon. The application has achieved no more than to check that the constructor is used with the correct arity.

3.4.4 Type-variable environment

A type variable environment just maps type variable syntactic names to their semantic counterparts. Its main use is local, in inference rules which validate type signatures written explicitly in Haskell, and checks that only in-scope type variables are mentioned.

However, it is part of the total environment, because it also binds the type variables mentioned in the headers of class and instance declarations.

3.4.5 Class environment

The class environment gives information about the semantic name and signature of a class. Members of its domain take the form

(κ, ∀α(θ, methods : GVE)

Here κ is the semantic name of the class and α is the type variable with respect to which overloading takes place. θ specifies its superclasses, in the order they must appear in a dictionary for the class. Finally, GVE gives the type signature of the class, while methods, a sequence of the variable names in dom(GVE), establishes the order in which the methods must appear in a dictionary for the class.

3.4.6 Global instance environment

The global instance environment associates a dictionary function name dfun with a type of form

∀α_{1} … α_{n}. θ ⇒ κ (χ β_{1} … β_{m})

This says that dfun is a (polymorphic) function which will take dictionaries corresponding to θ, and map them into a dictionary giving methods for the (χ β_{1} … β_{m}) instance of class κ. Notice that because instance declarations are syntactically restricted to declaring an instance of a class over a type of form (χ β_{1} … β_{m}), the types in the global instance environment also have this form.

It is important that each type constructor χ is an instance of a given class κ at most one way. This is ensured by adding the following extra implicit side condition to the operation GIE_{1} ⊕ GIE_{2}: no two types, from the range of GIE_{1} and GIE_{2} respectively, should have both the same class κ and same type constructor χ. In addition ⊕ should ensure that the dictionary function names are disjoint as usual, but since they are introduced by the type checker itself, this is just a way of saying that it should introduce a distinct name each time.

In a practical implementation the global instance environment is indexed by (κ, χ) pairs rather than the dictionary function names.

An important invariant is that these global instance types have no free variables; the ∀. α_{1} … α_{n} binds all the type variables β_{1} … β_{m} and those free in θ.

3.4.7 Local instance environment

The local instance environment maps a dictionary variable dvar to an expression of form κ τ. This asserts that dvar is a dictionary corresponding to the τ instance of class κ. In contrast to the global instance environment, the type τ may have free type variables.

The function zip constructs a local instance environment from a sequence of dictionary names dicts and a context θ, thus

{d_{1} : κ_{1} τ_{1}, …, d_{n} : κ_{n} τ_{n}} = zip ⟨dvar_{1}, …, dvar_{n}⟩ ⟨κ_{1} τ_{1}, …, κ_{n} τ_{n}⟩

4 Abstract syntax

In this section we give the abstract syntax of the source and translated language.

4.1 Source syntax

The abstract syntax of the source language is given in Figures 3, 4 and 5.

The abstract syntax expresses the parse tree of the program. The punctuation symbols of the concrete syntax, such as keywords and parentheses, which guide the parse, are therefore redundant and can be omitted. In particular, we omit from the abstract syntax all parentheses used for grouping, and all mention of operator fixity and precedence. To preserve legibility of the abstract syntax, however, we retain most of the remaining punctuation. An implementation would not do so.

The abstract syntax also differs from the concrete syntax of Haskell in a number of other important respects:

Grouping of declarations. The various sorts of declarations (type, class, instance and value) are assumed to be sorted into groups, as is shown by the program production.

Dependency analysis on value declarations. It is well known that in order to obtain the more general possible types from a group of local bindings in the Hindley-Milner system, it is necessary to perform dependency analysis on them so as to make explicit where recursion actually occurs and where it does not.

program → typedecl;classdecl;instdecl;binds
typedecl → typedecl_{1} ; typedecl_{2}  Type declarations
| data context => tycon tyvar_{1} … tyvar_{k}

= condecl (k ≥ 0 )

| type tycon tyvar_{1} … tyvar_{k}

= monotype (k ≥ 0 )

condecl → condecl_{1} | condecl_{2}  Constructor bindings
| con monotype_{1} … monotype_{k}  (k ≥ 0 )
classdecl → classdecl_{1} then classdecl_{2}  Class declarations
| class context => class tyvar

       where sigs

instdecl → instdecl_{1} ; instdecl_{2}  Instance declarations
| instance context => class monotype

       where binds

binds → bind
| bind with sigs
| binds_{1} then binds_{2}  Nested declarations
sigs → {}  Type signatures
| sigs_{1} and sigs_{2}
| var::polytype
bind → monobinds  Set of bindings
| rec monobinds  Recursive set of bindings
monobinds → monobinds_{1};monobinds_{2}  A set of bindings
| pat grhs  A pattern binding
| var match  A function binding
| {}  Empty set of bindings

Figure 3: Abstract syntax for Haskell: declarations and bindings

match → match_{1} match_{2}  Case alternatives
| mrule
mrule → grhs
| pat mrule
grhs → grhs_{1} grhs_{2}  Guarded right-hand side
| | guard = exp
| = exp
guard → exp
pat → var  Variable
| _Wildcard
| con pat_{1} … pat_{n}  Compound pattern
| ~pat  Lazy pattern
| var@pat  As-pattern
| [pat_{1}, …, pat_{n}]  (n ≥ 0 )  List pattern
| (pat_{1}, …, pat_{n})  (n ≥ 2 )  Tuple pattern
| ()  Unit pattern
exp → var  Variable
| con  Constructor
| integer
| float
| char
| string
| \ mrule  Lambda abstraction
| exp exp′  Application
| case exp of match  Case expression
| if exp_{1} then exp_{2} else exp_{3}  Conditional
| [exp|quals]  List comprehension
| [exp..]  Enumerations
| [exp_{1},exp_{2}..]
| [exp_{1}..exp_{2}]
| [exp_{1},exp_{2}..exp_{3}]
| let binds in exp  Local definitions
| [exp_{1}, …,exp_{n}] (n ≥ 0 ) Lists
| (exp_{1}, …,exp_{n})  (n = 0 or n ≥ 2 ) Tuples
quals → quals,quals  Qualifiers
| pat<-exp  Generator
| guard  Filter

Figure 4: Abstract syntax of Haskell: patterns and expressions

polytype → context => monotype
| monotype
monotype → tyvar  Type variable
| monotype_{1} -> monotype_{2}  Function type
| [monotype]  List type
| (monotype_{1}, …,monotype_{n})  (n = 0 or n ≥ 2 ) Tuple type (incl unit)
| tycon monotype_{1} … monotype_{n}  (n ≥ 0 )  Constructed type
context → (class_{1} tyvar_{1}, …,class_{n} tyvar_{n})

Figure 5: Abstract syntax of Haskell: types

pat → var : τ  Translated patterns
| var : κ τ  Dictionary variables
| … other productions as before
exp → Λα_{1} … α_{n} -> exp  Type abstraction
| exp τ_{1} … τ_{n}  Type application
| … other productions as before

Figure 6: Extra syntax for translated programs

We assume that this dependency analysis has already taken place before the program is presented to the type checker, so the abstract syntax allows the result of such dependency analysis to be expressed. In particular, groups of value bindings binds are (topologically) sorted into nested groups, combined with then. Each group is then either a non-recursive group monobinds or a recursive group rec monobinds. Declarations within a monobinds are combined together with ;.

The then production is used solely to allow the generation of most general types; it does not introduce a nested scope, so that no “shadowing” of names occurs as a result of its use.

We use the keyword let instead of where in the production for expressions as a reminder that bindings have this structure.

Type signatures. These are assumed to be split up so that each signature gives a type to only one variable.

Polytypes. The syntax for polymorphic types polytype does not contain any explicit quantification; instead, every such type is implicitly quantified over its free variables.

Generality. The abstract syntax for several constructs is more permissive than the concrete syntax.

For example, the abstract syntax for lambda abstractions allows multiple guarded bodies. The restriction to a single guarded body in the concrete syntax is done only on stylistic grounds. The syntax is more modular in the more general form we give here, and this gives rise directly to greater modularity in the type inference rules.

Similarly, the alternatives in a case expression can only have one pattern in the concrete syntax, rather than several as the above abstract syntax allows.

Similarly, there is an empty production for monobinds which is required only for instance declarations with no where clause.

The unit expression, written () in Haskell, is treated as a zero-tuple.

List comprehensions. The syntax does not permit a list comprehension with an empty qualifier list, whereas the Report does. This is an issue of style only; there is no deep issue here.

Class signatures. Default declarations are not (yet) incorporated, so csigs has no productions for them.

Notice also that the punctuation generated by the abstract syntax does not conform precisely to the concrete syntax, because the same nonterminal grhs is used for lambda abstractions as for function bindings. Since this is an abstract syntax, this does not matter in the slightest.

4.2 Translated syntax

The abstract syntax of the translated program is very similar to that of the source program. We write the nonterminals of translated programs in bold font: thus exp is a translated form of exp. Figure 6 gives the extra productions present in the translated program; all the existing productions are retained.

A program is translated to a binds, with only value bindings remaining. The other forms of declaration (import, class, instance, type, data, and type signatures) have been eliminated.

There are some extra productions to handle the second-order lambda caclulus constructs. In particular, every variable in a pattern has a type attached to it, and there are extra forms of expression for type abstraction and type application.

In the translation, dictionaries are introduced explicitly. We use dvar for variables bound to dictionaries. Dictionary variables are a distinct name-space from ordinary variables, so that there can be no name-clashes between dictionary variables and ordinary ones. The type of a dictionary, needed to annotate a dictionary variable in a pattern, is written κ τ.

4.3 Notation for translated programs

In constructing translations there are a number of design choices to be made, especially where overloading is concerned. For example, are dictionaries represented as tuples, or trees, or what? To avoid making a premature committments it is convenient to use some extra notation when writing down translations.

We interpret this extra notation as shorthand for a particular representation, rather than as extra productions for the abstract syntax of translations. In this section we summarise the extra notation, together with the design choices they imply.

4.3.1 Applying and constructing overloaded values

When an overloaded value is used, it must be applied to appropriate dictionaries. Dually, to construct an overloaded value, some form of lambda abstraction must be used.

• The notation exp dicts

where dicts is a sequence of dictionary names, stands for the application of a (overloaded) expression exp to the dictionaries in dicts. This notation abstracts away from whether the application is curried or not.

• The notation \dicts : θ -> exp

stands for a lambda abstraction of the dictionaries in dicts, each of which has the type given by the corresponding element of θ.

4.3.2 Building dictionaries and taking them apart

Recall that a dictionary for a particular instance of a class κ is a value which contains

• the methods for each operation of κ at that instance;

• and dictionaries for the superclasses of κ.

We need two constructs, one to build a dictionary, and one to take it apart.

• The notation ⟨dicts, methods⟩

where dicts is a sequence of dictionary names and methods is a sequence of method names, stands for a dictionary containing these methods and superclass dictionaries.

It will typically be represented as a flat tuple, with a component for each method or superclass dictionary. If there is only one method and no superclasses (or vice versa), then it will typically be represented by the method itself. The notation allows us to abstract away from these details.

E ⊢^{program} program ⇝ binds : E′

(1 ) (TCE of E) ⊕ (TCE of TE_{T}); CE_{C} ⊢^{typedecl} typedecl : (TCE_{T}, CVE_{T})
(2 ) E ⊕ TE_{T} ⊕ CVE_{T} ⊢^{classdecl} classdecl ⇝ binds_{C} : (GVE_{C} , CE_{C} , GIE_{C} )
(3 ) E′ = (TCE_{T}, (CVE_{T}, GVE_{C} , {}), CE_{C} , (GIE_{C} , {}))
(4 ) E ⊕ E′ ⊕ GIE_{I} ⊕ GVE_{V} ⊢^{inst} instdecl ⇝ monobinds_{I} : GIE_{I}
(5 ) E ⊕ E′ ⊕ GIE_{I} ⊢^{bind} binds ⇝ binds_{V} : ({}, GVE_{V} )

PROGRAM E ⊢^{program} typedecl;classdecl;instdecl;binds ⇝ binds_{C} then (rec monobinds_{I} ) then binds_{V} : E′ ⊕ GIE_{I} ⊕ GVE_{V}

Figure 7: Rule for programs

• The notation \⟨dicts : θ, methods : GVE⟩ -> exp

stands for a dictionary abstraction. The θ and GVE give the types for each variable bound by the abstraction.

This construct is actually used only for the selector functions which take a dictionary apart, in which case exp is just a single variable or dictionary variable.

4.3.3 Abstraction over bindings

The syntax in Figure 6, and the shorthand notation of Section 4.3.1, give notation for type and dictionary abstractions over expressions. In fact, it turns out that we need to abstract over sets of bindings rather than over a single expression, so the expression form is never used directly. Instead the notation

Λα_{1} … α_{n} -> \dicts : θ -> binds in monobinds

stands for the abstraction of the type variables α_{1} … α_{n} and the dictionaries dicts over the bindings in binds and monobinds. The resulting set of bindings bind only those variables bound in monobinds; the bindings in binds only scope over monobinds. This is rather a complicated construct, and it is discussed in some detail in Section 9.2.

5 Programs

WARNING: I HAVN’T LOOKED AT THIS SECTION FOR A WHILE, PENDING COM-PLETION OF THE IMPORTS STUFF.

** Should add stuff to check for cycles in type synonyms and class declarataions.

The inference rule for programs is given in Figure 7. It has six premises:

Premise(1) validates the program’s type declarations, and derives a type environment TE_{T}.

The T subscript identifies this environment as arising from type checking the type declarations. We use subscripts C for class declarations, I for instance declarations and V for value declarations.

Premise (2) deals with the class declarations, producing a some translated bindings, and three environments.

Premise (3) just combines together the environments derived so far into a total environment E′.

Premise (4) deals with instance declarations. Notice that they are all mutually recursive with each other and with the value declarations; this is specified by making GIE_{I} and GVE_{V} part of the environment for the judgement. To see that instance declarations can be mutually recursive among themselves, consider the program fragment:

        class C1 a where
                f1,g1 :: a -> Int
        class C2 a where
                f2,g2 :: a -> Int
        instance C1 Int where
                f1 x = f2 x
                g1 x = 4
        instance C2 Int where
                f2 x = g1 x
                g2 x = f1 x

Similarly, the GIE_{I} environment (obtained from typechecking the instance declarations) must clearly be in scope when typechecking the value declarations; and the GVE_{V} environment (obtained from typeckecking the value declarations) must be in scope when typechecking the instance declarations, because methods in an instance declarations may refer to values declared by a value declaration.

Premise(5) deals with the value declarations. Mutual recursion within value declarations is handled within the rules for binds. An empty LIE should be returned.

6 Type declarations

The rules for types and type declarations are given in Figures 8, 9 and 10.

The rules for monotype, context, and polytype look a bit trivial, but they formally specify the following:

• Checking that all uses of type constructors refer to type constructors which are in scope, which are specified by TE.

TCE; TVE ⊢^{monotype} monotype : τ

TVE tyvar = α

TYPE-TAUT

TCE; TVE ⊢^{monotype} tyvar : α
TCE; TVE ⊢^{monotype} monotype_{1} : τ_{1}
TCE; TVE ⊢^{monotype} monotype_{2} : τ_{2}

TYPE-FUN

TCE; TVE ⊢^{monotype} monotype_{1} -> monotype_{2} : τ_{1} → τ_{2}
TCE; TVE ⊢^{monotype} monotype : τ

TYPE-LIST

TCE; TVE ⊢^{monotype} [monotype] : [τ]
TCE; TVE ⊢^{monotype} monotype_{i} : τ_{i} (1 ≤ i ≤ n)

TYPE-TUPLE

TCE; TVE ⊢^{monotype} (monotype_{1}, …, monotype_{n}) : (τ_{1}, …, τ_{n})
TCE tycon = Λα_{1} … α_{n}.τ
TCE; TVE ⊢^{monotype} monotype_{i} : τ_{i} (1 ≤ i ≤ n)

TYPE-CON

TCE; TVE ⊢^{monotype} tycon monotype_{1} … monotype_{n} : τ[τ_{1}/α_{1}, …, τ_{n}/α_{n}]

Figure 8: Rules for monotype

• Ditto type variables, which are specified by TVE. In type signatures this is not significant, since all the type variables are implicitly universally quantified, but it is significant in data and type declarations, where the quantification is explicit.

• Ditto class names.

• Expanding type synonyms. (The expansion could contain info about the original syn-

onym too; that is decided by the ⊢^{typedecl} rule for type.)

• Checking that the type variables mentioned in the context part of a polytype are a subset of those mentioned in the monotype part (see rule POLYTYPE1).

• Checking that the context in a polytype predicates only type variables which are not bound in the enclosing scope, as defined by the TVE to the left of the turnstile. This enclosing TVE only contains bindings for type variables bound by a class or instance declaration.

Notice, for example, the use of an explicit environment TVE in the polytype judgement (Figure 9). It ensures that the quantification covers all the free variables of both the context and the monotype. Of course, it could contain some extra unused variables, but that does not matter.

TVE; CE ⊢^{context} context : θ

CE class_{i} = (κ_{i}, _) (1 ≤ i ≤ n)
TVE tyvar_{i} = α_{i} (1 ≤ i ≤ n)

CONTEXT

TCE; TVE; CE ⊢^{context} (class_{1} tyvar_{1}, …,class_{n} tyvar_{n}) : ⟨κ_{1} α_{1}, …, κ_{n} α_{n}⟩

TCE; TVE; CE ⊢^{polytype} polytype : σ

{tyvar_{1}, …, tyvar_{n}} = fv(monotype) \ dom(TVE)
TVE′ = {tyvar_{1} : α_{1}, …, tyvar_{n} : α_{n}}
TVE′; CE ⊢^{context} context : θ
TCE; TVE′ ⊕ TVE ⊢^{monotype} monotype : τ

POLYTYPE1 TCE; TVE; CE ⊢^{polytype} context => monotype : ∀α_{1} … α_{n}. θ ⇒ τ

{tyvar_{1}, …, tyvar_{n}} = fv(monotype) \ dom(TVE)
TVE′ = {tyvar_{1} : α_{1}, …, tyvar_{n} : α_{n}}
TCE; TVE′ ⊕ TVE ⊢^{monotype} monotype : τ

POLYTYPE2

TCE; TVE; CE ⊢^{polytype} monotype : ∀α_{1} … α_{n}. ⟨⟩ ⇒ τ

Figure 9: Rules for context and polytype

6.1 Contexts in data declarations

A context may appear just after the keyword data in a data declaration. Its effect is to make each constructor into an overloaded function, as you can see in the CONSTR rule. For example, consider

        data Eq a => Set a = EmptySet | Singleton a | Two (Set a) (Set a)

The types of the constructors are as follows:

                EmptySet :: ∀α. Set α
                Singleton :: ∀α. Eq α ⇒ α → Set α
                Two  :: ∀α. Eq α ⇒ Set α → Set α → Set α

Notice that EmptySet is not overloaded: only type variables free in the arguments of the constructor are predicated. The notation θ|_{{α_{1} ...α_{m} }} denotes the subset of θ which predicates type variables in {α_{1} … α_{m}}. (The reason Haskell is designed like this is to avoid needless ambiguity errors.)

TCE; CE ⊢^{typedecl} typedecl : (TE, CVE)

TVE = {tyvar_{1} : α_{1}, …, tyvar_{n} : α_{n}} TCE; TVE; θ; χ α_{1} … α_{n} ⊢^{condecl} condecl : CVE TVE; CE ⊢^{context} context : θ

DATA-DECL

TCE; CE ⊢^{typedecl} data context => tycon tyvar_{1} … tyvar_{n} = condecl : ({tycon : Λα_{1} … α_{n} -> χ α_{1} … α_{n}}, GVE)

TCE; {tyvar_{1} : α_{1}, …, tyvar_{n} : α_{n}} ⊢^{monotype} monotype : τ

SYN-DECL

TCE; CE ⊢^{typedecl} type tycon tyvar_{1} … tyvar_{n} = monotype : ({tycon : Λα_{1} … α_{n}. τ}, {})

TCE; CE ⊢^{typedecl} typedecl_{1} : (TCE_{1}, CVE_{1}) TCE; CE ⊢^{typedecl} typedecl_{2} : (TCE_{2}, CVE_{2})

TYPE-DECLS

TCE; CE ⊢^{typedecl} typedecl_{1};typedecl_{2} : (TCE_{1} ⊕ TCE_{2}, CVE_{1} ⊕ CVE_{2})

TCE; TVE; θ; τ ⊢^{condecl} condecl : CVE

TCE; TVE ⊢^{monotype} monotype_{i} : τ_{i} (1 ≤ i ≤ n) α_{1} … α_{m} = ⋃_{i} fv(τ_{i})

θ′ = θ|_{{α_{1} ...α_{m} }} CONSTR

TCE; TVE; θ; τ ⊢^{condecl} con monotype_{1} … monotype_{n} : {con : ∀α_{1} … α_{m}. θ′ ⇒ τ_{1} → … → τ_{n} → τ} TCE; TVE; θ; τ ⊢^{condecl} condecl_{1} : CVE_{1} TCE; TVE; θ; τ ⊢^{condecl} condecl_{2} : CVE_{2}

CONBIND

TCE; TVE; θ; τ ⊢^{condecl} condecl_{1} | condecl_{2} : CVE_{1} ⊕ CVE_{2} Figure 10: Rules for type declarations

6.2 A note on notation

A note on notation: in the TYPE-TUPLE rule, the premise above the bar is short for n premises, with i ranging from 1 to n. The constraints on n are given earlier, in the abstract syntax; in this case n must be at least 2. Similarly in the TYPE-CON rule, i varies between 1 and n, but here the abstract syntax tells that n ≥ 0 . The constraint 1 ≤ i ≤ n does not imply that n ≥ 1 .

7 Class declarations

The rules for class declarations are shown in Figure 11.

Rule CLASSES is straightforward; observe that the bindings inferred from classdecl_{1} are in scope for classdecl_{2} but not vice versa. This ensures that the superclass hierachy cannot contain cycles. Class operation names cannot clash with each other or other in-scope names because of the use of ⊕ to combine environments.

Rule CLASS is the interesting one.

Premise (1) validates the context, returning its semantic form, θ, and checking that only the type variable tyvar is mentioned.

Premise (2) validates the class signature. This produces GVE, a value environment containing bindings for the class operations.

Notice that the type signatures in a class declaration can be polytypes. This allows declarations such as

             class C a where
                     f :: D b => a -> b -> a

The type variable b will be polymorphic and overloaded.

Premise (3) defines methods, a sequence of the names of all and only the class operations, obtained by taking the domain of GVE. The significance of methods is that it records the order in which the methods must appear in the dictionary. This order is arbitrary, but the dictionaries created by instance declarations must agree with the selectors defined by the class declaration.

A pragmatic note: in a system supporting separate compilation, there will need to be some canonical ordering of the methods.cd

Premise (4) is a backwards use of zip . The “input” is the context θ, and this premise invents new dictionary names dicts, and then zips them together with the context to produce a local instance environment LIE.

Conclusion. The translation of a class declaration is a set of bindings which bind the class operations to selector functions which extract the corresponding method from a dictionary for the class. Selectors are also generated to extract the dictionaries for superclasses.

E ⊢^{classdecl} classdecl ⇝ binds : (GVE, CE, GIE)

E ⊢^{classdecl} classdecl_{1} ⇝ binds_{1} : (GVE_{1}, CE_{1}, GIE_{1}) E ⊕ (GVE_{1}, CE_{1}, GIE_{1}) ⊢^{classdecl} classdecl_{2} ⇝ binds_{2} : (GVE_{2}, CE_{2}, GIE_{2})

CLASSES E ⊢^{classdecl} classdecl_{1} then classdecl_{2} ⇝ binds_{1} then binds_{2} : (GVE_{1} ⊕ GVE_{2}, CE_{1} ⊕ CE_{2}, GIE_{1} ⊕ GIE_{2})

(1 ) {tyvar : α}; CE of E ⊢^{context} context : θ
(2 ) CE of E; TCE of E; {tyvar : α} ⊢^{sigs} sigs : GVE
(3 ) methods = dom(GVE)
(4 ) LIE = zip dicts θ

CLASS E ⊢^{classdecl} class context => class tyvar where sigs ⇝ \{ \begin{matrix}var = Λα -> \⟨dicts : θ, methods : GVE⟩ -> var \\ | var ∈ dom(LIE) ∪ dom(GVE) \end{matrix} \} : (∀α. ⟨κ α⟩ ⇒ GVE, \{class : (κ, ∀α(θ, methods : GVE))\}, ∀α. ⟨κ α⟩ ⇒ LIE)

CE; TCE; TVE ⊢^{sigs} sigs : GVE

CE; TCE; TVE ⊢^{sigs} sigs_{1} : GVE_{1} CE; TCE; TVE ⊢^{sigs} sigs_{2} : GVE_{2}

SIGS CE; TCE; TVE ⊢^{sigs} sigs_{1} and sigs_{2} : GVE_{1} ⊕ GVE_{2}

TCE; TVE; CE ⊢^{polytype} polytype : σ

SIG

TCE; TVE; CE ⊢^{sigs} var::polytype : {var : σ}) SIG EMPTY

CE; TCE; TVE ⊢^{sigs} {} : {}

Figure 11: Rules for class declarations

E ⊢^{instdecl} instdecl ⇝ monobinds : GIE

E ⊢^{instdecl} instdecl_{1} ⇝ monobinds_{1} : GIE_{1}
E ⊢^{instdecl} instdecl_{2} ⇝ monobinds_{2} : GIE_{2}

INSTS E ⊢^{instdecl} instdecl_{1} ; instdecl_{2} ⇝ monobinds_{1} ; monobinds_{2} : GIE_{1} ⊕ GIE_{2}

(1 ) (CE of E) class = (κ, ∀α(superdicts : θ_{C} , methods : GVE_{C} )
(2 ) TVE = {tyvar_{1} : α_{1}, …, tyvar_{n} : α_{n}}
(3 ) TCE of E; TVE ⊢^{monotype} monotype : τ
(4 ) τ = χ α_{1} … α_{n}  (α_{1}, …, α_{n} distinct)
(5 ) TVE; CE of E ⊢^{context} context : θ_{I}
(6 ) LIE_{I} = zip dicts θ_{I}
(7 ) GIE of E; LIE_{I} ⊢^{dicts} zip superdicts (θ_{C} [τ/α]) ⇝ binds_{super}
(8 ) E ⊕ TVE ⊢^{binds} binds ⇝ binds_{methods} : (LIE_{I} , GVE_{C} [τ/α])

INST E ⊢^{instdecl} instance context => class monotype where monobinds ⇝ \{dfun = \begin{matrix}Λα_{1} … α_{n} -> \\ \dicts : θ_{I} -> \\ let & binds & super & in \\ let & binds & methods & in \\ ⟨superdicts, methods⟩ \end{matrix} \} : \{dfun : ∀α_{1} … α_{n}. θ_{I} ⇒ κ τ\}

Figure 12: Instance declarations

The existence of these selectors is recorded in the environments returned: the class operation selectors appear in the value environment GVE, while the superclass selectors appear in the instance environment GIE.

8 Instance declarations

Figure 12 gives the rules for instance declarations.

The INSTS rule is straightforward. By contrast with CLASSES, the bindings inferred from instdecl_{1} are not made in scope in instdecl_{2}. Instead, the top-level rule PROGRAM makes the entire collection of instance declarations mutually recursive.

The INST rule is the most complex single rule in the entire system. It has seven premises, which are listed here:

Premise (1) looks up the class class in the class environment, to get its semantic name κ

and its type ∀α(superdicts : θ_{C} , methods : GVE_{C} ).

Premise(2) defines a type-variable environment, with bindings for (exactly) the names of the free type variables of monotype in the instance declaration.

Premises (3) and (4) validate monotype. Premise (4) checks that the form of monotype is correct: it must be a type constructor applied to simple type variables.

Premise (5) validates context, checking that it mentions no type variables which are not free in monotype (which would not make sense).

Premise (6) builds a local instance environment LIE_{I} from the context θ, generating suitable new dictionary variables dicts.

Premise (7) confirms that the superclass dictionaries described by the τ instance of LIE_{C} can indeed be constructed from dictionaries provided by the instance declaration LIE_{I} . It witnesses this fact by producing a set of bindings which give the former in terms of

the latter. The ⊢^{dicts} judgement is discussed in Section 12.

Premise (8) type checks the value bindings in the body of the instance declaration, and verifies that they match the τ instance of GVE_{C} obtained from the class environment in Premise (1).

The conclusion gives as translation the function which takes dictionaries corresponding to the context θ, and delivers a dictionary for the class, complete with its superclass dictionaries and methods.

Note the type abstraction in the binding for the dictionary function dfun: it is polymorphic!

In the INST rule as given, notice that κ τ is not in the local instance environment LIE_{I} . This means that instance declarations such as

   instance Eq a => Eq (Foo a) where
           (==) p q = ...
           (/=) p q = not (p == q)

where one method calls another, will generate a rather inefficient translation. The call to (==) in the definition of (/=) will result in a second call to the dictionary function for Eq (Foo a). Instead it would have been possible to add dvar : κ τ to LIE_{I} , and produce the following translation for the instance declaration:

{dfun = Λα_{1} … α_{n} -> \dicts : θ_{I} ->

       let rec

dvar = let binds_{super} in
let binds_{methods} in

⟨superdicts, methods⟩

       in

dvar }

Sets of bindings: E ⊢^{monobinds} monobinds ⇝ monobinds : (LIE, LVE)

E ⊢^{monobinds} monobinds_{1} ⇝ monobinds_{1} : (LIE_{1}, LVE_{1})
E ⊢^{monobinds} monobinds_{2} ⇝ monobinds_{2} : (LIE_{2}, LVE_{2})

UNION

E ⊢^{monobinds} monobinds_{1};monobinds_{2} ⇝ monobinds_{1};monobinds_{2} : (LIE_{1} ⊕ LIE_{2}, LVE_{1} ⊕ LVE_{2})

CVE of E ⊢^{pat} pat ⇝ pat : (τ, LVE)
E ⊢^{grhs} grhs ⇝ grhs : (LIE, τ)

PATBIND E ⊢^{monobinds} pat grhs ⇝ pat grhs : (LIE, LVE)

E ⊢^{match} match ⇝ match : (LIE, τ)

FUNBIND

E ⊢^{monobinds} var match ⇝ var match : (LIE, {var : τ})

EMPTYBIND

E ⊢^{monobinds} {} ⇝ {} : ({}, {})

Figure 13: Rules for monobinds

The declaration of the dictionary is made recursive, thus witnessing the addition of the extra assertion to the class declaration. This modification somewhat complicates the rule in exchange for a probable increase in efficiency.

9 Value declarations

The syntax and type rules for value declarations are structured in three layers:

• A monobinds is a group of declarations, typechecked with ⊢^{monobinds} to give a monomorphic environment (Figure 13). The fact that the envrionment is monomorphic ensures that in the right-hand sides of mutually-recursive definitions the variables being defined have only a monomorphic and non-overloaded type. The judgement

E ⊢^{monobinds} monobinds ⇝ monobinds : (LIE, LVE)

should be read “in environment E, the declarations monobinds translate to the declarations monobinds, and the types of variables bound in those declarations are given by the type environment LVE, under the class constraints given by the local instance environment LIE”. Since pattern bindings may bind zero, one or several variables, there may be more or fewer typings in LVE than declarations in monobinds. (Pattern bindings which bind no varibles are not very useful, but it is inconvenient to exclude them and they do no harm.) It is always the case that fv(LIE) ⊆ fv(LVE).

Binds: E ⊢^{binds} binds ⇝ binds : (LIE, GVE)

E ⊢^{bind} bind ⇝ bind : (LIE, GVE)

BINDS-TRIV E ⊢^{binds} bind ⇝ bind : (LIE, GVE)

E ⊢^{binds} binds_{1} ⇝ binds_{1} : (LIE_{1}, GVE_{1})
E ⊕^{→} GVE_{1} ⊢^{binds} binds_{2} ⇝ binds_{2} : (LIE_{2}, GVE_{2})

BINDS-THEN E ⊢^{binds} binds_{1} then binds_{2} ⇝ binds_{1} then binds_{2} : (LIE_{1} ⊕ LIE_{2}, GVE_{1} ⊕ GVE_{2})

E ⊢^{bind} bind ⇝ bind : (LIE, GVE)

CE of E; TCE of E; TVE of E ⊢^{sigs} sigs ⇝ GVE :

BINDS-SIG E ⊢^{bind} bind with sigs ⇝ bind : (LIE, GVE)

Figure 14: Rules for binds

Bind: E ⊢^{bind} bind ⇝ bind : (LIE, GVE)

E ⊢^{bind-1} bind ⇝ bind : (LIE, GVE)
α_{1} … α_{n} ∉ VE of E
α_{1} … α_{n} ∉ TVE of E
α_{1} … α_{n} ∉ LIE

BIND-GEN E ⊢^{bind} bind ⇝ Λα_{1} … α_{n} -> bind : (LIE, ∀α_{1} … α_{n}. GVE)

E ⊢^{bind-2} bind ⇝ bind : LIE, LVE)

GIE of E; (LIE_{encl} ⊕ LIE_{bind}) ⊢^{dicts} LIE ⇝ monobinds LIE_{bind} = zip dicts θ bind contains only function bindings

BIND-PRED E ⊢^{bind-1} bind ⇝ \dicts : θ -> monobinds in bind : (LIE_{encl}, θ ⇒ LVE)

E ⊕^{→} LVE ⊢^{monobinds} monobinds ⇝ monobinds : (LIE, LVE)

BIND-REC E ⊢^{bind-2} rec monobinds ⇝ rec monobinds : (LIE, LVE)

E ⊢^{monobinds} monobinds ⇝ monobinds : (LIE, LVE)

BIND-TRIV E ⊢^{bind-2} monobinds ⇝ monobinds : (LIE, LVE)

Figure 15: Rules for bind

Type signatures: E; GVE ⊢^{sigs} sigs ⇝ binds : GVE

SIGS-EMPTY

E; GVE ⊢^{sigs} {} ⇝ {} : {}

E; GVE ⊢^{sigs} sigs_{1} ⇝ binds_{1} : GVE_{1}E; GVE ⊢^{sigs} sigs_{2} ⇝ binds_{2} : GVE_{2}

SIGS E; GVE ⊢^{sigs} sigs_{1} and sigs_{2} ⇝ binds_{1} then binds_{2} : GVE_{1} ⊕ GVE_{2}

TCE of E; TVE of E; CE of E ⊢^{polytype} polytype : σ GVE var = σ

SIG

E; GVE ⊢^{sigs} var::polytype ⇝ {} : {var : σ}
(1 ) TCE of E; TVE of E; CE of E ⊢^{polytype} polytype : ∀β_{1} … β_{m}. θ_{sig} ⇒ τ_{sig}
(2 ) GVE var = ∀α_{1} … α_{n}. θ ⇒ τ
(3 ) γ_{1}, …, γ_{m} ∉ E ⊕ GVE
(4 ) τ_{sig}[γ_{1}/β_{1}, …, γ_{m}/β_{m}] = τ[τ_{1}/α_{1}, …, τ_{n}/α_{n}]
(5 ) LIE = zip dicts θ[τ_{1}/α_{1}, …, τ_{n}/α_{n}]
(6 ) LIE_{sig} = zip dicts_{sig} θ_{sig}[γ_{1}/β_{1}, …, γ_{m}/β_{m}]
(7 ) GIE of E; LIE_{sig} ⊢^{dicts} LIE ⇝ binds

SIG1

E; GVE ⊢^{sigs} var::polytype ⇝ \{var = \begin{matrix}Λβ_{1} … β_{m} -> \\ \dicts_{sig} : LIE_{sig} -> \\ let & binds & in \\ var τ_{1} … τ_{n} dicts \end{matrix} \} : \{var : ∀β_{1} … β_{m}. θ_{sig} ⇒ τ_{sig}\}

Figure 16: Type signatures • A bind deals with recursion, by optionally adding a rec to the monobinds. The typing

rules are given in Figure 15.

Once recursion is thus dealt with, the monotyped environment can be overloaded (BIND-PRED) and generalised (BIND-GEN) to give a polymorphic environment GVE.

BIND-PRED only applies to sets of declarations all of which are function bindings, or in which a simple variable is bound directly to a lambda abstraction. This constraint is the one required to implement Haskell’s (rather unsatisfactory) “monomorphic pattern binding” rule. BIND-GEN will still be able to generalise over any type variables not constrained in the instance environment.

There are several important operational issues here, which are discussed further below in Sections 9.1, 9.2 and 9.3.

• Finally, a binds is a nested set of bind groups, each of which can optionally have a group of type signatures attached to it, connected with then. The typing rules are in Figures 14 and 16.

The then construct is used only to get the most general type, and not for scoping purposes. Hence ⊕ is used in conclusion of the BINDS-THEN rule, rather than ⊕^{→}. We still use ⊕ in the second premise, because the declarations in bind_{1} might shadow outer bindings in E.

The BINDS-SIG rule is rather a cop-out. It simply says that the type environment for the bind should be the same as that specified by the sigs. This is perfectly correct, but the implementation is much more complicated than the rule implies. A type inference algorithm cannot clairvoyantly infer the (perhaps less than most-general) types for the bind specified by sigs. Rather, it will infer the most general types, and a separate process must then specialise the inferred types to the specified ones, modifying the translation appropriately.

9.1 Rule order

The three rules BIND-TRIV/BIND-REC, BIND-PRED and BIND-GEN must be applied in an appropriate order:

• First apply BIND-TRIV or BIND-REC, depending on whether the declarations are recursive or not.

• Next use BIND-PRED to discharge all the possible assumptions in the local instance environment.

• Finally use BIND-GEN to bind all free type variables.

The reason for this ordering is to maintain the form of types given in Figure 1. This rule

order is indicated by giving numbers to the turnstiles, thus ⊢^{bind-1}, ⊢^{bind-2}.

9.2 Translating type and dictionary abstractions

The translations given in BIND-GEN and BIND-PRED involve new constructs in the translated syntax for type and multidictionary abstraction. These constructs can readily be translated into existing ones, but there is more than one way to do, as we will see in this section. By using a new construct for each, we avoid making a premature committment as to the appropriate translation.

We now explore the possible translations of the new constructs. We discuss only the multidictionary abstraction; the type abstraction is analogous but a little simpler. Our discussion here is by example only, but the generalisation is straightforward, if tedious.

Consider the mutually recursive definitions^{2}:

        rec {   f x = g (x==x) x;
                g b x = abs (f x)
        }

Recall that abs is an operation of class Num; that == is an operation of class Eq. Recall also that Eq is a superclass for Num; that is, the class declaration for Num looks like this:

        class (Eq a) => Num a where ...

The fact that Eq is a superclass of Num means that every Num dictionary contains an Eq dictionary. This is recorded in the global instance environment with the entry

                          eqFromNum : ∀α. Num α ⇒ Eq α

which says that eqFromNum (the name is arbitrary) maps a Num dictionary to an Eq dictionary.

Returning the the example, after the recursive binding for f and g has been typechecked by

⊢^{monobinds}, the translated binding will be:

        rec { f x = g ((==) de x x) x; g b x = abs dn (f x) }

The inferred local type environment will be {f : α → α, g : Bool → α → α} and the local instance environment will have the assumption {dn : Num α, de : Eq α}, where dn is the name of the (Num) dictionary passed to abs, and de is the name of the (Eq) dictionary passed to == (again, the dictionary names are arbitrary). Now, applying BIND-PRED and then BIND-GEN produces the binding:

        \\a -> \dn -> {de = eqFromNum a dn} in
        rec { f a x:a = g a ((==) a de x x) x;
              g a b:Bool x:a = abs a dn (f a x) }

and the type environment now has overloaded types for f and g, namely {f : ∀α. Num α ⇒ α → α, g : ∀α. Num α ⇒ Bool → α → α}. (Because typewriter font does not include greek letters, we use \\ for Λ and a for α.) Notice the type signatures on bound variables. Notice also that the Eq dictionary, de, is obtained by applying the global function eqFromNum to the Num dictionary dn.

2 To keep the example short it is degenerate: f and g both fail to terminate.

What does this binding abstraction mean? It is a binds which gives values for both f and g, each of which is a function taking a type a and a dictionary dn as its arguments. If the bindings were not mutually recursive, and if there were no dictionary bindings (in this case the binding for de) to take into account this would be easy: just add a and dn as extra parameters to each definition.

In the case of mutual recursion, this is not possible, because the recursive calls do not pass this extra parameter. Furthermore, there is the question of what is to be done with the dictionary bindings. One alternative is to add the extra parameters to all the recursive calls, and to replicate the dictionary bindings in each right-hand side, thus (we omit the type signatures on arguments from now on, for brevity):

rec { f a dn x   = let {de = eqFromNum a dn} in  g a dn ((==) a de x x) x;
          g a dn b x = let {de = eqFromNum a dn} in  abs a dn (f a dn x)
        }

There are a number of problems with this translation. Firstly, there may be several dictionaries which need to be repeatedly passed rather than just one. Depending on the implementation this may impose a significant overhead. Secondly, the dictionary bindings are duplicated, perhaps increasing code size. In this case the binding for de can be dropped from the right-hand side of g, since it is not used, but this may not always be so. Thirdly, and perhaps most importantly, the expression (eqFromNum a dn) is recomputed at every recursion. This loses a property known as full laziness, and unfortunately the standard full laziness transformation will not recover it. Finally, it is an untidy transformation to express in the type rules because it involves a “second pass” over the translated expression to replace uses of f with (f a dn), and similarly for g.

A second possible translation is this:

    { f a dn = let {de = eqFromNum a dn} in
               let rec {f x = g ((==) a de x x) x; g b x = abs a dn (f x)} in
               f;
      g a dn = let {de = eqFromNum a dn} in
               let rec {f x = g ((==) a de x x) x; g b x = abs a dn (f x)} in
               g
        }

This translation recovers full laziness, because (eqFromNum a dn) is only computed once, but at the cost of duplicating the bindings for f and g as well as those for the dictionaries! However, it is usually the case that of a mutually-recursive group of definitions, only one is used in the subsequent code. In the case of our example, perhaps only f is called subsequently. This would mean that the (top-most) definition of g could be dropped entirely, which eliminates the duplication. But this single-use property cannot be guaranteed.

A third possible translation, which does not duplicate code, is as follows:

    { tup a dn = let {de = eqFromNum a dn} in
                 let rec {f x = g ((==) a de x x) x; g b x = abs a dn (f x)} in
                 (f,g)

      f a dn = case (tup a dn) of (f,g) -> f;
      g a dn = case (tup a dn) of (f,g) -> g;
        }

It appears that this translation is somewhat less efficient than the previous one, because of the tupling and untupling. However, in the common case where only f, say, is used subsequently, the definition of g can be dropped; in this case, the definition of tuple can safely be substituted for its occurrence in the body of f, and after little simplification the second translation (given above) emerges. For this reason, this third alternative seems to be the best.

9.3 Choosing which type variables to generalise over

The rules as given are correct (I hope) regardless of which parts of the LIE are selected as LIE_{bind} by BIND-PRED, and which type variables are chosen for generalisation by BIND-GEN. Nevertheless, in a type-inferencer, a suitable set must be chosen, and this section discusses the issues.

9.3.1 Generalisation

Firstly, BIND-GEN will not choose any type variables which are free in VE; this is part of the BIND-GEN rule. We call these type variables the constrained type variables. Nor is there any point in BIND-GEN choosing any type variables which are not free in the LVE being generalised. So we conclude that BIND-GEN should select exactly the type variables which are free in any of the types in LVE, and which are not constrained by the enclosing VE. We call these the target type variables.

This seems innocuous enough, but consider the bindings

        { tup = (\x -> x,  \y -> y) }
        then
        { (f,g) = tup }

Type inference for the first binding will derive the environment

{tup : ∀α, β. (α → α, β → β}

Type inference for the second binding, prior to BIND-GEN will infer the environment

{f : α → α, g : β → β}

Now BIND-GEN will generalise over both α and β, giving the environment

{f : ∀α, β. α → α, g : ∀α, β. β → β}

Curious! Both f and g take two type arguments, though their types only use one of them. There is no real problem here (especially since type abstractions and applications vanish in most real implementations) but it is worth noting.

9.3.2 Predication

The situation with BIND-PRED is more interesting still. Firstly, there is not much point in BIND-PRED selecting any predicates in LIE which predicate constrained type variables. (Remember, a predicate in LIE can predicate more than one type variable; for example Eq (α, β).) Any predicates in LIE which predicate only constrained type variables can therefore be eliminated from consideration. Predicates affecting some constrained and some unconstrained type

variables can be simplified using ⊢^{dicts} until none remain with this property. The remaining predicates affect only unconstrained type variables.

Here’s an example of this separation process:

        f x y = ... where
                    g z1 z2 = if (x>y) then z1 else z2

When the declaration of g is typechecked in an environment which gives x and y the type α, the (LIE, LVE) pair returned is

({d : Ord α}, {g : β → β → β})

The translation of g’s body will mention the dictionary d when it makes the comparion of x and y. Since α is not free in the type of g, BIND-PRED should leave the dictionary constraint on d in the LIE it returns, for later resolution by the BIND-PRED which deals with the declaration of f.

9.3.3 Ambiguity

Finally, the situation may arise of predicates which affect type variables which are neither constrained nor target variables. These predicates are ambiguous.

Should really say more here.

9.4 Type signatures

Type signatures are attached to possibly-recursive groups of declarations, rather than to individual declarations, because the types given cannot be checked until overloading and generalisation has taken place, which must be done for a group as a whole.

Type signatures are validated by the ⊢^{sigs} judgement, which uses the GVE for the declaration group to check that the type signatures attached to a declaration group mention only variables declared in the group, and with exactly the correct type (Figure 16).

If this were all it did, the judgement would need to return no result. While this is perfectly legitimate, it is no help at all to a type inference engine. It requires that the inference engine “clairvoyantly” derives a perhaps-less-than-fully-general type for the original binding, so that this inferred type precisely matches that given in the type signature.

This is implausible. What will happen in practice is that the most general type will be inferred, and the signature will specialise it. Notice that some translation may be required in this case. For example, suppose we infer that f has type ∀α. Num α ⇒ α → α. Then given the type signature f::Int -> Int, we need to make a new binding for f of the form

        f = f intD

where intD is the Num dictionary for Ints. (Note: this is a non-recursive binding! The f being defined is distinct from, and a specialised form of, the f on the right-hand side.) This re-binds f to be a version specialised to Int.

For this reason, the ⊢^{sigs} judgement form takes as returns a set of extra bindings, together with the modified GVE. The rule SIG1 deals with coercing a general type to a more specific one. It is considerably more compliated than the original, because in effect it incorporates DGEN, SPEC, DPRED and REL! It works like this:

Premise (1) validates the polytype given in the type signature.

Premise (2) checks that the variable being typed does indeed have a binding in the current group, and finds its inferred type.

Premise (3) grabs a fresh set of type variables.

Premise (4) checks that the most general instance of the given type is an instance of the inferred type. τ_{1}, …, τ_{n} are the types which instantiate the inferred type to the given type.

Premise (5) generates an LIE from the inferred context θ, inventing new dictionary names.

Premise (6) does the same for the given context θ_{sig}.

Premise (7) finally generates the new bindings which produce the dictionaries needed by (the instance of) θ from those made available by θ_{sig}.

10 Expressions

The rules for typechecking expressions are given in Figures 17, 18, 19, 20, 21 and 22. The expression judgement form is

E ⊢^{exp} exp ⇝ exp : (LIE, σ)

which should be read “in environment E, the expression exp is translated to exp and has type σ, under the class constraints given by the local instance environment LIE”. It is always the case that

fv(LIE) ⊆ fv(σ)

Some points to notice:

TAUT-LVAR and TAUT-GVAR apply only if there is a binding for the variable in the local or global value environments, so typing fails if the variable is not in scope.

Expressions: E ⊢^{exp} exp ⇝ exp : (LIE, σ)

(GVE of E) var = σ

TAUT-GVAR  var ∈ dom(GVE of E)

E ⊢^{exp} var ⇝ var : ({}, σ)

(LVE of E) var = τ

TAUT-LVAR  var ∈ dom(LVE of E)

E ⊢^{exp} var ⇝ var : ({}, τ)

(CVE of E) con = σ

TAUT-CON

E ⊢^{exp} con ⇝ con : ({}, σ)

TAUT-INTEGER E ⊢^{exp} integer ⇝ fromInteger ⟨dvar⟩ integer : ({dvar : Num τ}, τ)

TAUT-FLOAT

E ⊢^{exp} float ⇝ fromRational ⟨dvar⟩ float : ({dvar : Fractional τ}, τ)

TAUT-CHAR

E ⊢^{exp} char ⇝ char : ({}, Char)

TAUT-STRING E ⊢^{exp} string ⇝ string : ({}, [Char])

Figure 17: Basic rules for expressions

E ⊢^{exp} var ⇝ exp : (LIE, ∀α_{1} … α_{k}. ρ)

SPEC

E ⊢^{exp} var ⇝ exp τ_{1} … τ_{k} : (LIE, ρ[τ_{1}/α_{1}, …, τ_{k}/α_{k}])

E ⊢^{exp} exp ⇝ exp : (LIE, θ ⇒ τ)

LIE′ = zip dicts θ

REL

E ⊢^{exp} exp ⇝ (exp dicts) : (LIE ⊕ LIE′, τ)

Figure 18: Non-syntactic rules for expressions

TAUT-INTEGER and TAUT-FLOAT introduce overloaded numeric and fractional constants respectively. It is for this reason that they interact with the instance environment.

TAUT-STRING deals with literal strings. Notice that even the empty string "" is given the type [Char]. This means that, though the empty string is implemented as the empty list, the expression [1] ++ "" will fail the type checker (in constrast to the LML compiler, for example, which passes it).

GEN and SPEC manipulate a group of type variables at once, rather than working one type variable at a time as is more conventional. There is no deep reason for this, except the analogy with PRED and REL.

REL. (REL is short for “Release”.) Mutter mutter. Need to give some explanation here.

E ⊢^{exp} exp ⇝ exp : ({}, σ)

TCE of E; TVE of E; CE of E ⊢^{polytype} polytype : σ

EXPSIG

E ⊢^{exp} (exp::polytype) ⇝ exp : ({}, σ)

E; {} ⊢^{mrule} mrule ⇝ mrule : (LIE, τ)

LAMBDA

E ⊢^{exp} \mrule ⇝ \mrule : (LIE, τ)
E ⊢^{exp} exp ⇝ exp : (LIE, τ′ → τ)
E ⊢^{exp} exp′ ⇝ exp′ : (LIE′, τ′)

COMB

E ⊢^{exp} (exp exp′) ⇝ (exp exp′) : (LIE ⊕ LIE′, τ)

E ⊢^{binds} binds ⇝ binds : (LIE, GVE) E ⊕^{→} GVE ⊢^{exp} exp ⇝ exp : (LIE′, τ)

LET E ⊢^{exp} (let binds in exp) ⇝ (let binds in exp) : (LIE ⊕ LIE′, τ)

E ⊢^{exp} exp ⇝ exp : (LIE, τ)
E ⊢^{match} match ⇝ match : (LIE′, τ → τ′)

CASE E ⊢^{exp} (case exp of match) ⇝ (case exp of match) : (LIE ⊕ LIE′, τ′)

E ⊢^{exp} exp_{1} ⇝ exp_{1} : (LIE_{1}, Bool)
E ⊢^{exp} exp_{2} ⇝ exp_{2} : (LIE_{2}, τ)
E ⊢^{exp} exp_{3} ⇝ exp_{3} : (LIE_{3}, τ)

IF E ⊢^{exp} if exp_{1} then exp_{2} else exp_{3} ⇝ if exp_{1} then exp_{2} else exp_{3} : (LIE_{1} ⊕ LIE_{2} ⊕ LIE_{3}, τ)

E ⊢^{qual} quals ⇝ quals : (LIE, LVE) E ⊕^{→} LVE ⊢^{exp} exp ⇝ exp : (LIE′, τ)

LISTCOMP E ⊢^{exp} [exp|quals] ⇝ [exp|quals] : (LIE ⊕ LIE′, [τ])

Figure 19: Rules for compound expressions

E ⊢^{exp} exp_{i} ⇝ exp_{i} : (LIE_{i}, τ) (0 ≤ i ≤ n)

LIST E ⊢^{exp} [exp_{1}, …,exp_{n}] ⇝ [exp_{1}, …,exp_{n}] : (LIE_{1} ⊕ … ⊕ LIE_{n}, [τ])

E ⊢^{exp} exp_{i} ⇝ exp_{i} : (LIE_{i}, τ_{i}) (1 ≤ i ≤ n)

TUPLE E ⊢^{exp} (exp_{1}, …,exp_{n}) ⇝ (exp_{1}, …,exp_{n}) : (LIE_{1} ⊕ … ⊕ LIE_{n}, (τ_{1}, …, τ_{n}))

Figure 20: Data structures in expressions

E ⊢^{exp} exp ⇝ exp : (LIE, τ)

ENUM-FROM E ⊢^{exp} [exp..] ⇝ (enumFrom ⟨dvar⟩ exp) : (LIE ⊕ {dvar : Enum τ}, [τ])

E ⊢^{exp} exp_{1} ⇝ exp_{1} : (LIE_{1}, τ)
E ⊢^{exp} exp_{2} ⇝ exp_{2} : (LIE_{2}, τ)

ENUM-FROM-THEN

E ⊢^{exp} [exp_{1},exp_{2}..] ⇝ (enumFromThen ⟨dvar⟩ exp_{1} exp_{2}) : (LIE_{1} ⊕ LIE_{2} ⊕ {dvar : Enum τ}, [τ])

E ⊢^{exp} exp_{1} ⇝ exp_{1} : (LIE_{1}, τ)
E ⊢^{exp} exp_{2} ⇝ exp_{2} : (LIE_{2}, τ)

ENUM-FROM-TO

E ⊢^{exp} [exp_{1}..exp_{2}] ⇝ (enumFromTo ⟨dvar⟩ exp_{1} exp_{2}) : (LIE_{1} ⊕ LIE_{2} ⊕ {dvar : Enum τ}, [τ])

E ⊢^{exp} exp_{1} ⇝ exp_{1} : (LIE_{1}, τ)
E ⊢^{exp} exp_{2} ⇝ exp_{2} : (LIE_{2}, τ)
E ⊢^{exp} exp_{3} ⇝ exp_{3} : (LIE_{3}, τ)

ENUM-FROM-THEN-TO

E ⊢^{exp} [exp_{1},exp_{2}..exp_{3}] ⇝ (enumFromThenTo ⟨dvar⟩ exp_{1} exp_{2} exp_{3}) : (LIE_{1} ⊕ LIE_{2} ⊕ LIE_{3} ⊕ {dvar : Enum τ}, [τ])

Figure 21: Rules for enumerations expressions

EXPSIG handles type signatures on expressions. Like the SIG rule for bindings, this rule is rather unrealistic, because it requires that the inference engine derive a less-than-most-general type for the expression, so that it exactly matches the signature given.

A more useful rule is given in Figure 23.

List comprehensions and case expressions. Notice that bindings in both list comprehensions and case expressions are monomorphic. It is easy to see how to make those in

list comprehensions polymorphic, by adding a GEN rule to ⊢^{qual}, but less easy to see how to do the same for case expressions.

QUALS. Note the use of ⊕^{→} in the conclusion of this rule, expressing the fact that that bindings within a list comprehension can shadow each other. For example

{xs | xs <- ys; xs <- xs} is allowed.

E ⊢^{qual} quals ⇝ quals : (LIE, LVE)

E ⊢^{qual} quals_{1} ⇝ quals_{1} : (LIE, LVE_{1})
E ⊕^{→} LVE_{1} ⊢^{qual} quals_{2} ⇝ quals_{2} : (LIE_{2}, LVE_{2})

QUALS E ⊢^{qual} quals_{1},quals_{2} ⇝ quals_{1},quals_{2} : (LIE_{1} ⊕ LIE_{2}, LVE_{1} ⊕ LVE_{2})

E ⊢^{exp} exp ⇝ exp : (LIE, Bool)

FILTER E ⊢^{qual} exp ⇝ exp : (LIE, {})

CVE of E ⊢^{pat} pat ⇝ pat : (τ, LVE)
E ⊢^{exp} exp ⇝ exp : (LIE, [τ])

GENERATOR E ⊢^{qual} pat<-exp ⇝ pat<-exp : (LIE, LVE)

Figure 22: Rules for quals

(1 ) E ⊢^{exp} exp ⇝ exp : (LIE, τ)
(2 ) α_{1} … α_{n} ∉ E
(3 ) TCE of E; TVE of E; CE of E ⊢^{polytype} polytype : ∀β_{1} … β_{m} θ_{sig} ⇒ τ_{sig}
(4 ) γ_{1} … γ_{m} ∉ E ∪ LIE ∪ τ
(5 ) τ_{sig}[γ_{1}/β_{1}, …, γ_{m}/β_{m}] = τ[τ_{1}/α_{1}, …, τ_{n}/α_{n}]
(6 ) LIE_{sig} = zip dicts_{sig} θ_{sig}[γ_{1}/β_{1}, …, γ_{m}/β_{m}]
(7 ) GIE of E; LIE_{sig} ⊢^{dicts} LIE ⇝ binds

EXPSIG1

E ⊢^{exp} exp::polytype ⇝ let binds in exp : (LIE_{sig}, τ_{sig}[γ_{1}/β_{1}, …, γ_{m}/β_{m}])

Figure 23: More realistic expression-signature rule

11 Pattern matching

Patterns are type-checked using the judgement form ⊢^{pat}, whose typing rules are given in Figure 24. The judgement form is written thus

CVE ⊢^{pat} pat ⇝ pat : (τ, LVE)

and should should be read: “in the constructor value environment CVE, the pattern pat is translated to pat with type τ, and the bindings of variables within it is given by LVE.” The judgement guarantees that LVE contains bindings for all and only the variables of pat, and that the pattern is linear (ie contains no repeated variables). The translated pattern pat gives an explicit type to each variable, which is necessary in the second-order lambda calculus.

The ⊢^{mrule} judgement type-checks mrules, which are sequences of patterns followed by a sequence of guarded expressions. mrules are used by both function bindings and lambda ab-

Patterns: CVE ⊢^{pat} pat ⇝ pat : (τ, LVE)

TAUT-PAT

CVE ⊢^{pat} var ⇝ (var : τ) : (τ, {var : τ})
CVE con = σ
σ ≤ τ_{1} → … → τ_{n} → τ
CVE ⊢^{pat} pat_{i} ⇝ pat_{i} : (τ_{i}, LVE_{i}) (1 ≤ i ≤ n)

CONSTR-PAT

CVE ⊢^{pat} con pat_{1} … pat_{n} ⇝ con pat_{1} … pat_{n} : (τ, LVE_{1} ⊕ … ⊕ LVE_{n})

CVE ⊢^{pat} pat ⇝ pat : (τ, LVE)

AS-PAT

CVE ⊢^{pat} var@pat ⇝ var@pat : (τ, LVE ⊕ {var : τ})
CVE ⊢^{pat} pat ⇝ pat : (τ, LVE)

LAZY-PAT

CVE ⊢^{pat} ~pat ⇝ ~pat : (τ, LVE)

WILD-PAT

CVE ⊢^{pat} _⇝ _: (τ, {})

CVE ⊢^{pat} pat_{i} ⇝ pat_{i} : (τ, LVE_{i}) (0 ≤ i ≤ n)

LIST-PAT CVE ⊢^{pat} [pat_{1}, …,pat_{n}] ⇝ [pat_{1}, …,pat_{n}] : ([τ], LVE_{1} ⊕ … ⊕ LVE_{n})

CVE ⊢^{pat} pat_{i} ⇝ pat_{i} : (τ_{i}, LVE_{i}) (1 ≤ i ≤ n)

TUPLE-PAT

CVE ⊢^{pat} (pat_{1}, …,pat_{n}) ⇝ (pat_{1}, …,pat_{n}) : ((τ_{1}, …, τ_{n}), LVE_{1} ⊕ … ⊕ LVE_{n})

Figure 24: Rules for patterns

stractions.

Finally, the ⊢^{grhs} judgement type-checks a sequence of guarded expressions. The typing rules for this and the mrule judgement form are given in Figure 25.

The following points are worth noting:

Linearity is ensured by the use of ⊕ in AS-PAT, LIST-PAT, TUPLE-PAT and CONSTR-PAT.

MRULE-ABS and MRULE-GRHS. The ⊢^{mrule} judgement carries down a monomorphic value environment LVE, which contains bindings for all the variables bound by the patterns in the current sequence of patterns. This environment is initialised empty by the MATCH rule, and augmented by the MRULE-ABS rule using a the non-shadowing ⊕ operation, thus checking for linearity among the patterns.

Matches: E ⊢^{match} match ⇝ match : (LIE, τ)

E ⊢^{match} match_{1} ⇝ match_{1} : (LIE_{1}, τ)

E ⊢^{match} match_{2} ⇝ match_{2} : (LIE_{2}, τ)

MATCHES

E ⊢^{match} match_{1} match_{2} ⇝ match_{1} match_{2} : (LIE_{1} ⊕ LIE_{2}, τ)
E; {} ⊢^{mrule} mrule ⇝ mrule : (LIE, τ)

MATCH

E ⊢^{match} mrule ⇝ mrule : (LIE, τ)

Mrules: E; LVE ⊢^{mrule} mrule ⇝ mrule : (LIE, τ)

E ⊕^{→} LVE ⊢^{grhs} grhs ⇝ grhs : (LIE, τ)

MRULE-GRHS

E; LVE ⊢^{mrule} grhs ⇝ grhs : (LIE, τ)
CVE of E ⊢^{pat} pat ⇝ pat : (τ, LVE′)
E; LVE ⊕ LVE′ ⊢^{mrule} mrule ⇝ mrule : (LIE, τ′)

MRULE-ABS

E; LVE ⊢^{mrule} pat mrule ⇝ pat mrule : (LIE, τ → τ′)

Guarded right-hand sides: E ⊢^{grhs} grhs ⇝ grhs : (LIE, τ)

E ⊢^{grhs} grhs_{1} ⇝ grhs_{1} : (LIE_{1}, τ)

E ⊢^{grhs} grhs_{2} ⇝ grhs_{2} : (LIE_{2}, τ)

GUARD-OR

E ⊢^{grhs} grhs_{1} grhs_{2} ⇝ grhs_{1} grhs_{2} : (LIE_{1} ⊕ LIE_{2}, τ)
E ⊢^{exp} guard ⇝ guard : (LIE_{1}, Bool)
E ⊢^{exp} exp ⇝ exp : (LIE_{2}, τ)

GUARD

E ⊢^{grhs} |guard=exp ⇝ |guard=exp : (LIE_{1} ⊕ LIE_{2}, τ)

E ⊢^{exp} exp ⇝ exp : (LIE, τ)

GUARD-DEFAULT

E ⊢^{grhs} =exp ⇝ exp : (LIE, τ)

Figure 25: Rules for match, mrule and grhs

Dictionary equivalence: GIE; LIE ⊢^{dicts} LIE′ ⇝ binds

DICT-TRIV

GIE; LIE ⊢^{dicts} {} ⇝ {}
GIE; LIE ⊢^{dicts} LIE_{1} ⇝ binds_{1}
GIE; LIE ⊢^{dicts} LIE_{2} ⇝ binds_{2}

DICTS

GIE; LIE ⊢^{dicts} LIE_{1} ⊕ LIE_{2} ⇝ binds_{1} then binds_{2}
GIE dfun = ∀α_{1} … α_{n}. θ ⇒ κ τ
LIE′ = zip dicts θ[τ_{1}/α_{1}, …, τ_{n}/α_{n}]
GIE; LIE ⊢^{dicts} LIE′ ⇝ binds

DICT-GLOBAL

GIE; LIE ⊢^{dicts} {dvar : κ τ[τ_{1}/α_{1}, …, τ_{n}/α_{n}]} ⇝ binds then {dvar = dfun τ_{1} … τ_{n} dicts}

LIE dvar′ = κ τ

DICT-DUP

GIE; LIE ⊢^{dicts} {dvar : κ τ} ⇝ {dvar = dvar′}

Figure 26: Dictionary manipulation

Finally, MRULE-GRHS typechecks the guarded right-hand side in a type environment LVE formed by combining the environment derived from the patterns to the main one E.

12 Dictionary manipulation

The ⊢^{dicts} judgement form tells how to express some dictionaries in terms of others. It takes the form

GIE; LIE ⊢^{dicts} LIE′ ⇝ binds

Here, LIE′ is a local instance environment containing assumptions of form dvar : κ τ, and this judgement shows how to translate LIE′ to a collection of bindings monobinds which give values to the dictionaries mentioned in LIE′ in terms of those mentioned in GIE and LIE.

There are four main places ⊢^{dicts} is used:

• In the INST rule, it shows how to construct dictionaries for the superclasses in terms of those provided by the context in the instance declaration.

• Many judgements return a local instance environment LIE as part of their result, which tracks the names of all the dictionaries used in the translation of the construct, together with their types. These LIEs are merged together up the expression tree, thereby producing a merged LIE. The latter may be highly redundant, in the sense that some

dictionaries can be produced from others, and the ⊢^{dicts} judgement allows this redundancy to be eliminated.

• Type signatures on declarations.

• Type signatures on expressions.

There are three ways in which ⊢^{dicts} can give a binding for a dictionary dvar with type κ τ:

• If LIE contains a dictionary with identical type, a trivial binding will suffice (DICTS-DUP).

• If τ is of form χ τ_{1} … τ_{n} then there should have been an instance declaration for the χ instance of κ. In this case, GIE will contain a matching assumption, which is used in the DICTS-GLOBAL rule to translate dvar : κ τ to a binding and a simpler collection of LIE assumptions.

• Finally, if τ is just a type variable α, it may nevertheless be that there is another assumption in LIE of form dvar′ :: κ′ α where κ is a superclass of κ′. In this case it is possible to express dvar in terms of dvar′. The DICTS-GLOBAL rule copes with this too, but it in implementation terms this case is the trickiest to handle, because it involves conditionally using the superclass hierachy.

13 Implementation notes

When generalising (DGEN) it is sufficient (I think) to look at LVE, and not GVE, because while GVE may contain free type variables, they are only free because they are also free in LVE (otherwise they would have been ∀-bound).

14 References

R Harper, R Milner & M Tofte [May 1989], “The definition of Standard ML (Version 3),” ECS-LFCS-89-81, LFCS, Dept of Computer Science, University of Edinburgh.

P Hudak, PL Wadler, Arvind, B Boutel, J Fairbairn, J Fasel, K Hammond, J Hughes, T Johnsson, R Kieburtz, RS Nikhil, SL Peyton Jones, M Reeve, D Wise & J Young [April 1990], “Report on the functional programming language Haskell,” Department of Computing Science, Glasgow University.

P Wadler & S Blott [Jan 1989], “How to make ad-hoc polymorphism less ad hoc,” in Proc 16th ACM Symposium on Principles of Programming Languages, Austin, Texas, ACM.

Index

AS-PAT, 43

bind, judgement form, 20, 30, 31, \underline{31} bind-1, judgement form, 31 bind-2, judgement form, 31 BIND-GEN, 31 BIND-PRED, 31 BIND-REC, 31 BIND-TRIV, 31 binds, judgement form, 27, 30, \underline{30}, 30, 39 BINDS-SIG, 30 BINDS-THEN, 30 BINDS-TRIV, 30

CASE, 39 CLASS, 25 classdecl, judgement form, 20, 25, \underline{25}, 25 CLASSES, 25 COMB, 39 CONBIND, 23 condecl, judgement form, 23, \underline{23} CONSTR, 23 CONSTR-PAT, 43 CONTEXT, 22 context, judgement form, 22, \underline{22}, 23, 25, 27

DATA-DECL, 23 DICT-DUP, 46 DICT-GLOBAL, 46 DICT-TRIV, 46 DICTS, 46 dicts, judgement form, 27, 31, 32, 36, 42,

45, 46, \underline{46}

EMPTYBIND, 29 ENUM-FROM, 41 ENUM-FROM-THEN, 41 ENUM-FROM-THEN-TO, 41 ENUM-FROM-TO, 41 exp, judgement form, 37, 38, \underline{38}, 39–42, 44 EXPSIG, 39 EXPSIG1, 42

FILTER, 42 FUNBIND, 29 GENERATOR, 42 grhs, judgement form, 29, 44, \underline{44}, 44, 45 GUARD, 44 GUARD-DEFAULT, 44 GUARD-OR, 44

IF, 39 INST, 27 inst, judgement form, 20 instdecl, judgement form, 27, \underline{27} INSTS, 27

judgement form bind, 20, 30, 31, \underline{31} bind-1, 31 bind-2, 31 binds, 27, \underline{30}, 30, 39 classdecl, 20, 25, \underline{25} condecl, 23, \underline{23}, 23 context, 22, \underline{22}, 23, 25, 27 dicts, 27, 31, 32, 36, 42, 45, 46, \underline{46}, 46 exp, 37, 38, \underline{38}, 39–42, 44 grhs, 29, 44, \underline{44}, 44, 45 inst, 20 instdecl, 27, \underline{27} match, 29, 39, 44, \underline{44} monobinds, 28, 29, \underline{29}, 31, 33 monotype, 21, \underline{21}, 22, 23, 27 mrule, 39, 44, \underline{44}, 45 nonterminal, 8 pat, 5, 29, 42, 43, \underline{43}, 43–45 polytype, 22, \underline{22}, 25, 32, 39, 42 program, 20, \underline{20} qual, 39, 40, \underline{42}, 42 sigs, 25, \underline{25}, 25, 30, 32, \underline{32}, 32, 36, 37 typedecl, 20, 22, 23, \underline{23}, 23

LAMBDA, 39 LAZY-PAT, 43 LET, 39 LIST, 40 LIST-PAT, 43 LISTCOMP, 39

MATCH, 44 match, judgement form, 29, 39, 44, \underline{44} MATCHES, 44 monobinds, judgement form, 28, 29, \underline{29}, 31,

33 monotype, judgement form, 21, \underline{21}, 22, 23,

27 mrule, judgement form, 39, 44, \underline{44}, 45 MRULE-ABS, 44 MRULE-GRHS, 44

nonterminal, judgement form, 8

pat, judgement form, 5, 29, 42, 43, \underline{43}, 44,

45 PATBIND, 29 polytype, judgement form, \underline{22}, 22, 25, 32,

39, 42 POLYTYPE1, 22 POLYTYPE2, 22 PROGRAM, 20 program, judgement form, 20, \underline{20}

qual, judgement form, 39, 40, 42, \underline{42}, 42 QUALS, 42

REL, 38

SIG, 25, 32 SIG1, 32 x EMPTY, 25 SIGS, 25, 32 sigs, judgement form, 25, \underline{25}, 25, 30, \underline{32}, 32,

36, 37 SIGS-EMPTY, 32 SPEC, 38 SYN-DECL, 23

TAUT-CHAR, 38 TAUT-CON, 38 TAUT-FLOAT, 38 TAUT-GVAR, 38 TAUT-INTEGER, 38 TAUT-LVAR, 38 TAUT-PAT, 43 TAUT-STRING, 38 TUPLE, 40 TUPLE-PAT, 43 TYPE-CON, 21 TYPE-DECLS, 23 TYPE-FUN, 21 TYPE-LIST, 21 TYPE-TAUT, 21 TYPE-TUPLE, 21 typedecl, judgement form, 20, 22, 23, \underline{23},

23

UNION, 29

WILD-PAT, 43