smunix · October 18, 2015 16:41 · Nov 8, 2014 · Nov 8, 2014 · Nov 8, 2014 · Nov 8, 2014
diff --git a/typing.md b/typing.md
@@ -1514,7 +1514,7 @@ the `Integral` class:
 
 ``` haskell
 tiPat (PNpk i k)  = do t <- newTVar Star
-                 return ([IsIn "Integral" t], [i:>:toScheme t], t)
+                       return ([IsIn "Integral" t], [i:>:toScheme t], t)
 ```
 
 The case for constructed patterns is slightly more complex:

diff --git a/typing.md b/typing.md
@@ -1103,7 +1103,7 @@ toHnf                 :: Monad m => ClassEnv -> Pred -> m [Pred]
 toHnf ce p | inHnf p   = return [p]
            | otherwise = case byInst ce p of
                            Nothing -> fail "context reduction"
-                                 Just ps -> toHnfs ce ps
+                           Just ps -> toHnfs ce ps
 ```
 
 Another way to simplify a list of predicates is to reduce the number of

diff --git a/typing.md b/typing.md
@@ -214,8 +214,9 @@ operations from the `List` and `Monad` libraries:
 
 ``` haskell
 module TypingHaskellInHaskell where
-import List(nub, (\\), intersect, union, partition)
-import Monad(msum)
+
+import Data.List (nub, (\\), intersect, union, partition)
+import ControlMonad (msum)
 ```
 
 For the most part, our choice of variable names follows the notational
@@ -1096,13 +1097,13 @@ process is captured in the following definition:
 ``` haskell
 toHnfs      :: Monad m => ClassEnv -> [Pred] -> m [Pred]
 toHnfs ce ps = do pss <- mapM (toHnf ce) ps
-            return (concat pss)
+                 return (concat pss)
 
 toHnf                 :: Monad m => ClassEnv -> Pred -> m [Pred]
 toHnf ce p | inHnf p   = return [p]
-     | otherwise = case byInst ce p of
-                     Nothing -> fail "context reduction"
-                           Just ps -> toHnfs ce ps
+           | otherwise = case byInst ce p of
+                           Nothing -> fail "context reduction"
+                                 Just ps -> toHnfs ce ps
 ```
 
 Another way to simplify a list of predicates is to reduce the number of

diff --git a/typing.md b/typing.md
@@ -610,8 +610,8 @@ match t1 t2                 = fail "types do not match"
 One of the most unusual features of the Haskell type system, at least in
 comparison to those of other polymorphically typed languages like ML, is
 the support that it provides for *type classes*. Described by Wadler and
-Blott [Wadler & Blott,
-1989](#blott-1991)
+Blott [[Wadler & Blott,
+1989](#blott-1991)]
 as a general mechanism that subsumes several ad-hoc forms of
 overloading, type classes have found many uses (and, sometimes, abuses!)
 in the ten years since they were introduced. A significant portion of

diff --git a/typing.md b/typing.md
@@ -99,7 +99,7 @@ This paper presents a formal description of the Haskell type system
 using the notation of Haskell itself as a specification language.
 Indeed, the source code for this paper is itself an executable Haskell
 program that is passed through a custom preprocessor and then through
-L^A^T~E~X to obtain the typeset version. The type checker is available
+LaTeX to obtain the typeset version. The type checker is available
 [on Hackage](https://hackage.haskell.org/package/thih). We hope that
 this will serve as a resource for the Haskell community, and that it
 will be a significant step in addressing the problems described

diff --git a/typing.md b/typing.md
@@ -99,11 +99,11 @@ This paper presents a formal description of the Haskell type system
 using the notation of Haskell itself as a specification language.
 Indeed, the source code for this paper is itself an executable Haskell
 program that is passed through a custom preprocessor and then through
-L^A^T~E~X to obtain the typeset version. The type checker was
-available in source form, but the link is now dead
-(http://www.cse.ogi.edu/~mpj/thih/). We hope that this will serve as a
-resource for the Haskell community, and that it will be a significant
-step in addressing the problems described previously.
+L^A^T~E~X to obtain the typeset version. The type checker is available
+[on Hackage](https://hackage.haskell.org/package/thih). We hope that
+this will serve as a resource for the Haskell community, and that it
+will be a significant step in addressing the problems described
+previously.
 
 One audience whose needs may not be particularly well met by this paper
 are researchers in programming language type systems who do not have

diff --git a/typing.md b/typing.md
@@ -99,10 +99,11 @@ This paper presents a formal description of the Haskell type system
 using the notation of Haskell itself as a specification language.
 Indeed, the source code for this paper is itself an executable Haskell
 program that is passed through a custom preprocessor and then through
-L^A^T~E~X to obtain the typeset version. The type checker is available
-in [source form](http://www.cse.ogi.edu/~mpj/thih/). We hope that this
-will serve as a resource for the Haskell community, and that it will
-be a significant step in addressing the problems described previously.
+L^A^T~E~X to obtain the typeset version. The type checker was
+available in source form, but the link is now dead
+(http://www.cse.ogi.edu/~mpj/thih/). We hope that this will serve as a
+resource for the Haskell community, and that it will be a significant
+step in addressing the problems described previously.
 
 One audience whose needs may not be particularly well met by this paper
 are researchers in programming language type systems who do not have

diff --git a/typing.md b/typing.md
@@ -1813,9 +1813,7 @@ satisfied by any choice of a default:
 
 ``` haskell
 type Ambiguity       = (Tyvar, [Pred])
-```
 
-``` haskell
 ambiguities         :: ClassEnv -> [Tyvar] -> [Pred] -> [Ambiguity]
 ambiguities ce vs ps = [ (v, filter (elem v . tv) ps) | v <- tv ps \\ vs ]
 ```

diff --git a/typing.md b/typing.md
@@ -30,7 +30,6 @@ which to explore new proposals.
 
 ## Table of Contents
 
-* [Abstract](#abstract)
 * [Introduction](#introduction)
 * [Preliminaries](#preliminaries)
 * [Kinds](#kinds)

diff --git a/typing.md b/typing.md
@@ -30,36 +30,36 @@ which to explore new proposals.
 
 ## Table of Contents
 
-* [Abstract](*abstract)
-* [Introduction](*introduction)
-* [Preliminaries](*preliminaries)
-* [Kinds](*kinds)
-* [Types](*types)
-* [Substitutions](*substitutions)
-* [Unification and Matching](*unification-and-matching)
-* [Type Classes, Predicates and Qualified Types](*type-classes-predicates-and-qualified-types)
-  * [Basic Definitions](*basic-definitions)
-  * [Class Environments](*class-environments)
-  * [Entailment](*entailment)
-  * [Context Reduction](*context-reduction)
-* [Type Schemes](*type-schemes)
-* [Assumptions](*assumptions)
-* [A Type Inference Monad](*a-type-inference-monad)
-* [Type Inference](*type-inference)
-  * [Literals](*literals)
-  * [Patterns](*patterns)
-  * [Expressions](*expressions)
-  * [Alternatives](*alternatives)
-  * [From Types to Type Schemes](*from-types-to-type-schemes)
-    * [Ambiguity and Defaults](*ambiguity-and-defaults)
-  * [Binding Groups](*binding-groups)
-    * [Explicitly Typed Bindings](*explicitly-typed-bindings)
-    * [Implicitly Typed Bindings](*implicitly-typed-bindings)
-    * [Combined Binding Groups](*combined-binding-groups)
-    * [Top-level Binding Groups](*top-level-binding-groups)
-* [Conclusions](*conclusions)
-* [Acknowledgments](*acknowledgments)
-* [References](*references)
+* [Abstract](#abstract)
+* [Introduction](#introduction)
+* [Preliminaries](#preliminaries)
+* [Kinds](#kinds)
+* [Types](#types)
+* [Substitutions](#substitutions)
+* [Unification and Matching](#unification-and-matching)
+* [Type Classes, Predicates and Qualified Types](#type-classes-predicates-and-qualified-types)
+  * [Basic Definitions](#basic-definitions)
+  * [Class Environments](#class-environments)
+  * [Entailment](#entailment)
+  * [Context Reduction](#context-reduction)
+* [Type Schemes](#type-schemes)
+* [Assumptions](#assumptions)
+* [A Type Inference Monad](#a-type-inference-monad)
+* [Type Inference](#type-inference)
+  * [Literals](#literals)
+  * [Patterns](#patterns)
+  * [Expressions](#expressions)
+  * [Alternatives](#alternatives)
+  * [From Types to Type Schemes](#from-types-to-type-schemes)
+    * [Ambiguity and Defaults](#ambiguity-and-defaults)
+  * [Binding Groups](#binding-groups)
+    * [Explicitly Typed Bindings](#explicitly-typed-bindings)
+    * [Implicitly Typed Bindings](#implicitly-typed-bindings)
+    * [Combined Binding Groups](#combined-binding-groups)
+    * [Top-level Binding Groups](#top-level-binding-groups)
+* [Conclusions](#conclusions)
+* [Acknowledgments](#acknowledgments)
+* [References](#references)
 
 ## Introduction
 

diff --git a/typing.md b/typing.md
@@ -28,6 +28,39 @@ descriptions of Haskell, both as a starting point for discussions
 about existing features of the type system, and as a platform from
 which to explore new proposals.
 
+## Table of Contents
+
+* [Abstract](*abstract)
+* [Introduction](*introduction)
+* [Preliminaries](*preliminaries)
+* [Kinds](*kinds)
+* [Types](*types)
+* [Substitutions](*substitutions)
+* [Unification and Matching](*unification-and-matching)
+* [Type Classes, Predicates and Qualified Types](*type-classes-predicates-and-qualified-types)
+  * [Basic Definitions](*basic-definitions)
+  * [Class Environments](*class-environments)
+  * [Entailment](*entailment)
+  * [Context Reduction](*context-reduction)
+* [Type Schemes](*type-schemes)
+* [Assumptions](*assumptions)
+* [A Type Inference Monad](*a-type-inference-monad)
+* [Type Inference](*type-inference)
+  * [Literals](*literals)
+  * [Patterns](*patterns)
+  * [Expressions](*expressions)
+  * [Alternatives](*alternatives)
+  * [From Types to Type Schemes](*from-types-to-type-schemes)
+    * [Ambiguity and Defaults](*ambiguity-and-defaults)
+  * [Binding Groups](*binding-groups)
+    * [Explicitly Typed Bindings](*explicitly-typed-bindings)
+    * [Implicitly Typed Bindings](*implicitly-typed-bindings)
+    * [Combined Binding Groups](*combined-binding-groups)
+    * [Top-level Binding Groups](*top-level-binding-groups)
+* [Conclusions](*conclusions)
+* [Acknowledgments](*acknowledgments)
+* [References](*references)
+
 ## Introduction
 
 Haskell benefits from one of the most sophisticated type systems of

diff --git a/typing.md b/typing.md
@@ -237,7 +237,7 @@ enumId n = "v" ++ show n
 ```
 
 The `enumId` function will be used in the definition of the `newTVar`
-operator in [A Type Inference Monad](a-type-inference-monad)
+operator in [A Type Inference Monad](#a-type-inference-monad)
 to describe the allocation of fresh type variables during type
 inference. With the simple implementation shown here, we assume that
 variable names beginning with “v” do not appear in input programs.
@@ -1217,7 +1217,7 @@ instance Types Assump where
 ```
 
 Thanks to the instance definition for `Types` on lists
-([Substitutions](substitutions)),
+([Substitutions](#substitutions)),
 we can also use the `apply` and `tv` operators on the lists of
 assumptions that are used to record the type of each program variable
 during type inference. We will also use the following function to find
@@ -1240,7 +1240,7 @@ aspects of “plumbing” and to draw attention instead to more important
 aspects of a program's design [[Wadler, 1992](#wadler-1992].  The
 purpose of this section is to define the monad that will be used in
 the description of the main type inference algorithm in
-[Type Inference](type-inference).  Our choice of monad is motivated by
+[Type Inference](#type-inference).  Our choice of monad is motivated by
 the needs of maintaining a “current substitution” and of generating
 fresh type variables during typechecking. In a more realistic
 implementation, we might also want to add error reporting facilities,

diff --git a/typing.md b/typing.md
@@ -16,8 +16,7 @@
 
 *Converted to Markdown on November 8, 2014.*
 
-Abstract
---------
+## Abstract
 
 Haskell benefits from a sophisticated type system, but implementors,
 programmers, and researchers suffer because it has no formal
@@ -29,8 +28,7 @@ descriptions of Haskell, both as a starting point for discussions
 about existing features of the type system, and as a platform from
 which to explore new proposals.
 
-Introduction
----------------
+## Introduction
 
 Haskell benefits from one of the most sophisticated type systems of
 any widely used programming language. Unfortunately, it also suffers
@@ -166,16 +164,15 @@ we have made some use of Haskell overloading and do-notation, we have
 generally avoided using the more esoteric features of Haskell. In
 addition, some experience with the basics of Hindley-Milner style type
 inference
-[[Hindley, 1969](#hindley-1969),[Milner, 1978](#milner-1978),[Damas & Milner, 1982](#damas-milner-1982)]will
-be needed to understand the algorithms presented here. Although we
-have aimed to keep our presentation as simple as possible, some
+[[Hindley, 1969](#hindley-1969),[Milner, 1978](#milner-1978),[Damas & Milner, 1982](#damas-milner-1982)]
+will be needed to understand the algorithms presented here. Although
+we have aimed to keep our presentation as simple as possible, some
 aspects of the problems that we are trying to address have inherent
 complexity or technical depth that cannot be side-stepped. In short,
 this paper will probably not be useful as a tutorial introduction to
 Hindley-Milner style type inference!
 
-2  Preliminaries
-----------------
+## Preliminaries
 
 For simplicity, we present the code for our typechecker as a single
 Haskell module. The program uses only a handful of standard prelude
@@ -190,7 +187,7 @@ import Monad(msum)
 
 For the most part, our choice of variable names follows the notational
 conventions set out in
-Figure [1](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#fig-notation).
+Figure 1.
 
 | Description | Symbol | Type  |
 |:------------|:-------|:------|
@@ -218,7 +215,7 @@ Figure [1](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#fig-not
 | alternative       | `alt, ...` | `Alt` |
 | binding group     | `bg, ...` | `BindGroup` |
 
-Figure 1: Notational Conventions
+**Figure 1: Notational Conventions**
 
 A trailing `s` on a variable name usually indicates a list. Numeric
 suffices or primes are used as further decoration where necessary. For
@@ -240,14 +237,12 @@ enumId n = "v" ++ show n
 ```
 
 The `enumId` function will be used in the definition of the `newTVar`
-operator in
-Section [10](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-atimonad)
+operator in [A Type Inference Monad](a-type-inference-monad)
 to describe the allocation of fresh type variables during type
 inference. With the simple implementation shown here, we assume that
 variable names beginning with “v” do not appear in input programs.
 
-3  Kinds
---------
+## Kinds
 
 To ensure that they are valid, Haskell type constructors are classified
 into different *kinds*: the kind `*` (pronounced “star”) represents the
@@ -267,15 +262,12 @@ Kinds play essentially the same role for type constructors as types do
 for values, but the kind system is clearly very primitive. There are a
 number of extensions that would make interesting topics for future
 research, including polymorphic kinds, subkinding, and record/product
-kinds. A simple extension of the kind system-adding a new `row` kind-has
-already proved to be useful for the Trex implementation of extensible
-records in Hugs [[Gaster & Jones,
-1996](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#GasterJones),[Jones
-& Peterson,
-1999](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#HugsManual)].
+kinds. A simple extension of the kind system-adding a new `row`
+kind-has already proved to be useful for the Trex implementation of
+extensible records in Hugs
+[[Gaster & Jones, 1996](#gaster--jones-1996),[Jones & Peterson, 1999](#jones--peterson-1999)].
 
-4  Types
---------
+## Types
 
 The next step is to define a representation for types. Stripping away
 syntactic sugar, Haskell type expressions are either type variables or
@@ -297,8 +289,7 @@ data Tycon = Tycon Id Kind
 This definition also includes types of the form `TGen n`, which
 represent “generic” or quantified type variables. The only place where
 `TGen` values are used is in the representation of type schemes, which
-will be described in
-Section [8](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-schemes).
+will be described in [Type Schemes](#type-schemes).
 
 The following examples show how standard primitive datatypes are
 represented as type constants:
@@ -387,8 +378,7 @@ have a kind `k'->k`, where `k'` is the kind of `t'` and `k` is the kind
 of the whole application. This shows that we need only traverse the
 leftmost spine of a type expression to calculate its kind.
 
-5  Substitutions
-----------------
+## Substitutions
 
 Substitutions-finite functions, mapping type variables to types-play a
 major role in type inference. In this paper, we represent substitutions
@@ -495,8 +485,7 @@ how the first of these composition operators is used to describe
 unification, while the second is used in the formulation of a matching
 operation.
 
-6  Unification and Matching
----------------------------
+## Unification and Matching
 
 The goal of unification is to find a substitution that makes two types
 equal-for example, to ensure that the domain type of a function matches
@@ -508,19 +497,18 @@ will lead to most general types. More formally, a substitution `s` is a
 with the property that any other unifier `s` can be written as `s'@@u`,
 for some substitution `s'`.
 
-The syntax of Haskell types has been chosen to ensure that, if two types
-have any unifying substitutions, then they have a most general unifier,
-which can be calculated by a simple variant of Robinson's algorithm
-[[Robinson,
-1965](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Robinson)].
-One of the reasons for this is that there are no non-trivial equalities
-on types. Extending the type system with higher-order features (such as
-lambda expressions on types), or with other mechanisms that allow
-reductions or rewriting in the type language, could make unification
-undecidable, non-unitary (meaning that there may not be most general
-unifiers), or both. This, for example, is why Haskell does not allow
-type synonyms to be partially applied (and interpreted as some
-restricted kind of lambda expression).
+The syntax of Haskell types has been chosen to ensure that, if two
+types have any unifying substitutions, then they have a most general
+unifier, which can be calculated by a simple variant of Robinson's
+algorithm [[Robinson, 1965](#robinson-1965)].  One of the reasons for
+this is that there are no non-trivial equalities on types. Extending
+the type system with higher-order features (such as lambda expressions
+on types), or with other mechanisms that allow reductions or rewriting
+in the type language, could make unification undecidable, non-unitary
+(meaning that there may not be most general unifiers), or both. This,
+for example, is why Haskell does not allow type synonyms to be
+partially applied (and interpreted as some restricted kind of lambda
+expression).
 
 The calculation of most general unifiers is implemented by a pair of
 functions:
@@ -584,8 +572,7 @@ match (TCon tc1) (TCon tc2)
 match t1 t2                 = fail "types do not match"
 ```
 
-7  Type Classes, Predicates and Qualified Types
------------------------------------------------
+## Type Classes, Predicates and Qualified Types
 
 One of the most unusual features of the Haskell type system, at least in
 comparison to those of other polymorphically typed languages like ML, is
@@ -603,7 +590,7 @@ pattern matching-which are often elided in more theoretical
 presentations-are also significant contributors, as is the extra level
 of detail and precision that is needed in executable code.)
 
-### 7.1  Basic Definitions
+### Basic Definitions
 
 A Haskell type class can be thought of as a set of types (of some
 particular kind), each of which supports a certain collection of *member
@@ -637,11 +624,11 @@ For example, using the `Qual` and `Pred` datatypes, the type
 ```
 
 It would be easy to extend the `Pred` datatype to allow other forms of
-predicate, as is done with Trex records in Hugs [[Jones & Peterson,
-1999](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#HugsManual)].
-Another frequently requested extension is to allow classes to accept
-multiple parameters, which would require a list of `Type`s rather than
-the single `Type` in the definition above.
+predicate, as is done with Trex records in Hugs
+[[Jones & Peterson, 1999](#jones--peterson-1999)].  Another frequently
+requested extension is to allow classes to accept multiple parameters,
+which would require a list of `Type`s rather than the single `Type` in
+the definition above.
 
 The extension of `Types` to the `Qual` and `Pred` datatypes is
 straightforward:
@@ -702,7 +689,7 @@ additional information for each declaration, such as the list of member
 functions for each class and details of their implementations in each
 particular instance.
 
-### 7.2  Class Environments
+### Class Environments
 
 The information provided by the class and instance declarations in a
 given program can be captured by a class environment of type:
@@ -751,17 +738,17 @@ modify ce i c = ce{classes = \j -> if i==j then Just c
                                            else classes ce j}
 ```
 
-The `defaults` component of a `ClassEnv` value is used to provide a list
-of types for defaulting, as described in
-Section [11.5.1](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-default).
-Haskell allows programmers to specify a value for this list using a
-`default` declaration; if no explicit declaration is given, then a
-`default (Integer,Double)` declaration is assumed. It is easy to
-describe this using the `ClassEnv` type. For example,
-`cedefaults=[tInt]` is the result of modifying a class environment `ce`
-to reflect the presence of a `default (Int)` declaration. Further
-discussion of defaulting is deferred to
-Section [11.5.1](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-default).
+The `defaults` component of a `ClassEnv` value is used to provide a
+list of types for defaulting, as described in
+[Ambiguity and Defaults](#ambiguity-and-defaults).  Haskell allows
+programmers to specify a value for this list using a `default`
+declaration; if no explicit declaration is given, then a `default
+(Integer,Double)` declaration is assumed. It is easy to describe this
+using the `ClassEnv` type. For example, `cedefaults=[tInt]` is the
+result of modifying a class environment `ce` to reflect the presence
+of a `default (Int)` declaration. Further discussion of defaulting is
+deferred to Section
+[Ambiguity and Defaults](#ambiguity-and-defaults).
 
 In the remainder of this section, we will show how to build an
 appropriate class environment for a given program, starting from an
@@ -893,13 +880,13 @@ overlaps as an error. Extensions to Haskell to support overlapping
 instances in certain special cases have been considered elsewhere; they
 appear to have interesting applications, but also have some potentially
 troublesome impact on program semantics [[Peyton Jones *et al.* ,
-1997](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#multi)].
+1997](#peyton-jones-et-al--1997)].
 We will not consider such issues further in this paper.
 
 To illustrate how the `addInst` function might be used, the following
 definition shows how the standard prelude class environment can be
 extended to include the four instances for `Ord` from the example in
-Section [7.1](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-basic-pred):
+[Basic Definitions](#basic-definitions).
 
 ``` haskell
 exampleInsts ::  EnvTransformer
@@ -926,20 +913,19 @@ straightforward but tedious to verify, we have chosen not to include
 tests for them here, and instead assume that they have been checked
 during static analysis prior to type checking.
 
-### 7.3  Entailment
+### Entailment
 
 In this section, we describe how class environments can be used to
-answer questions about which types are instances of particular classes.
-More generally, we consider the treatment of *entailment*: given a
-predicate `p` and a list of predicates `ps`, our goal is to determine
-whether `p` will hold whenever all of the predicates in `ps` are
-satisfied. In the special case where `p = IsIn i t` and `ps = []`, this
-amounts to determining whether `t` is an instance of the class `i`. In
-the theory of qualified types [[Jones,
-1992](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Quality)],
-assertions like this are captured using judgements of the form
-`ps ||- p`; we use a different notation here-the `entail` function that
-is defined at the end of this section-to make the dependence on a class
+answer questions about which types are instances of particular
+classes.  More generally, we consider the treatment of *entailment*:
+given a predicate `p` and a list of predicates `ps`, our goal is to
+determine whether `p` will hold whenever all of the predicates in `ps`
+are satisfied. In the special case where `p = IsIn i t` and `ps = []`,
+this amounts to determining whether `t` is an instance of the class
+`i`. In the theory of qualified types [[Jones, 1992](#jones-1992)],
+assertions like this are captured using judgements of the form `ps ||-
+p`; we use a different notation here-the `entail` function that is
+defined at the end of this section-to make the dependence on a class
 environment explicit.
 
 As a first step, we can ask how information about superclasses and
@@ -1019,48 +1005,46 @@ would be very difficult because there is no obvious way to choose a
 particular `q`, and, in general, there will be infinitely many potential
 candidates to consider. Fortunately, a technical condition in the
 Haskell report [[Peyton Jones & Hughes,
-1999](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Haskell98),Condition
+1999](#peyton-jones--hughes-1999),Condition
 1 on Page 47] reassures us that this is not necessary: if `p` can be
 obtained as an immediate superclass of some predicate `q` that was built
 using an instance declaration in an entailment `entail ce ps q`, then
 `ps` must already be strong enough to deduce `p`. Thus, although we have
 not formally proved these properties, we believe that our algorithm is
 sound, complete, and guaranteed to terminate.
 
-### 7.4  Context Reduction
+### Context Reduction
 
 Class environments also play an important role in an aspect of the
-Haskell type system that is known as *context reduction*. The basic goal
-of context reduction is to reduce a list of predicates to an equivalent
-but, in some sense, simpler list. The Haskell report [[Peyton Jones &
-Hughes,
-1999](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Haskell98)]provides
-only informal hints about this aspect of the Haskell typing, where both
-pragmatics and theory have important parts to play. We believe therefore
-that this is one of the areas where a more formal specification will be
-particularly valuable.
+Haskell type system that is known as *context reduction*. The basic
+goal of context reduction is to reduce a list of predicates to an
+equivalent but, in some sense, simpler list. The Haskell report
+[[Peyton Jones & Hughes, 1999](#peyton-jones--hughes-1999)]
+provides only informal hints about this aspect of the Haskell typing,
+where both pragmatics and theory have important parts to play. We
+believe therefore that this is one of the areas where a more formal
+specification will be particularly valuable.
 
 One way to simplify a list of predicates is to simplify the type
-components of individual predicates in the list. For example, given the
-instance declarations in the Haskell standard prelude, we could replace
-any occurrences of predicates like `Eq [a]`, `Eq (a,a)`, or
+components of individual predicates in the list. For example, given
+the instance declarations in the Haskell standard prelude, we could
+replace any occurrences of predicates like `Eq [a]`, `Eq (a,a)`, or
 `Eq ([a],Int)` with `Eq a`. This is valid because, for any choice of
 `a`, each one of these predicates holds if, and only if, `Eq a` holds.
 Notice that, in some cases, an attempt to simplify type components-for
 example, by replacing `Eq (a, b)` with `(Eq a, Eq b)`-may increase the
 number of predicates in the list. The extent to which simplifications
 like this are used in a system of qualified types has an impact on the
 implementation and performance of overloading in practical systems
-[[Jones,
-1992](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Quality),Chapter
-7]. In Haskell, however, the decisions are made for us by a syntactic
-restriction that forces us to simplify predicates until we obtain types
-in a kind of “head-normal form”. This terminology is motivated by
-similarities with the concept of *head-normal forms* in l-calculus. More
-precisely, the syntax of Haskell requires class arguments to be of the
-form `v t1 ... tn`, where `v` is a type variable, and `t1`,...,`tn` are
-types (and n ³ 0). The following function allows us to determine whether
-a given predicate meets these restrictions:
+[[Jones, 1992](#jones-1992),Chapter 7]. In Haskell, however, the
+decisions are made for us by a syntactic restriction that forces us to
+simplify predicates until we obtain types in a kind of “head-normal
+form”. This terminology is motivated by similarities with the concept
+of *head-normal forms* in l-calculus. More precisely, the syntax of
+Haskell requires class arguments to be of the form `v t1 ... tn`,
+where `v` is a type variable, and `t1`,...,`tn` are types (and n ³
+0). The following function allows us to determine whether a given
+predicate meets these restrictions:
 
 ``` haskell
 inHnf       :: Pred -> Bool
@@ -1140,8 +1124,7 @@ scEntail        :: ClassEnv -> [Pred] -> Pred -> Bool
 scEntail ce ps p = any (p `elem`) (map (bySuper ce) ps)
 ```
 
-8  Type Schemes
----------------
+## Type Schemes
 
 Type schemes are used to describe polymorphic types, and are represented
 using a list of kinds and a qualified type:
@@ -1209,13 +1192,12 @@ toScheme t     = Forall [] ([] :=> t)
 To complete our description of type schemes, we need to be able to
 instantiate the quantified variables in `Scheme` values. In fact, for
 the purposes of type inference, we only need the special case that
-instantiates a type scheme with fresh type variables. We therefore defer
-further description of instantiation to
-Section [10](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-atimonad)
-where the mechanisms for generating fresh type variables are introduced.
+instantiates a type scheme with fresh type variables. We therefore
+defer further description of instantiation to
+[A Type Inference Monad](#a-type-inference-monad) where the mechanisms
+for generating fresh type variables are introduced.
 
-9  Assumptions
---------------
+## Assumptions
 
 Assumptions about the type of a variable are represented by values of
 the `Assump` datatype, each of which pairs a variable name with a type
@@ -1235,7 +1217,7 @@ instance Types Assump where
 ```
 
 Thanks to the instance definition for `Types` on lists
-(Section [5](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-substs)),
+([Substitutions](substitutions)),
 we can also use the `apply` and `tv` operators on the lists of
 assumptions that are used to record the type of each program variable
 during type inference. We will also use the following function to find
@@ -1251,23 +1233,21 @@ This definition allows for the possibility that the variable `i` might
 not appear in `as`. In practice, occurrences of unbound variables will
 probably have been detected in earlier compiler passes.
 
-10  A Type Inference Monad
---------------------------
+## A Type Inference Monad
 
-It is now quite standard to use monads as a way to hide certain aspects
-of “plumbing” and to draw attention instead to more important aspects
-of a program's design [[Wadler,
-1992](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Wadler:Essence)].
-The purpose of this section is to define the monad that will be used in
+It is now quite standard to use monads as a way to hide certain
+aspects of “plumbing” and to draw attention instead to more important
+aspects of a program's design [[Wadler, 1992](#wadler-1992].  The
+purpose of this section is to define the monad that will be used in
 the description of the main type inference algorithm in
-Section [11](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-typeinf).
-Our choice of monad is motivated by the needs of maintaining a “current
-substitution” and of generating fresh type variables during
-typechecking. In a more realistic implementation, we might also want to
-add error reporting facilities, but in this paper the crude but simple
-`fail` function from the Haskell prelude is all that we require. It
-follows that we need a simple state monad with only a substitution and
-an integer (from which we can generate new type variables) as its state:
+[Type Inference](type-inference).  Our choice of monad is motivated by
+the needs of maintaining a “current substitution” and of generating
+fresh type variables during typechecking. In a more realistic
+implementation, we might also want to add error reporting facilities,
+but in this paper the crude but simple `fail` function from the
+Haskell prelude is all that we require. It follows that we need a
+simple state monad with only a substitution and an integer (from which
+we can generate new type variables) as its state:
 
 ``` haskell
 newtype TI a = TI (Subst -> Int -> (Subst, Int, a))
@@ -1353,8 +1333,7 @@ instance Instantiate Pred where
   inst ts (IsIn c t) = IsIn c (inst ts t)
 ```
 
-11  Type Inference
-------------------
+## Type Inference
 
 With this section we have reached the heart of the paper, detailing our
 algorithm for type inference. It is here that we finally see how the
@@ -1371,16 +1350,15 @@ type Infer e t = ClassEnv -> [Assump] -> e -> TI ([Pred], t)
 
 In more theoretical treatments, it would not be surprising to see the
 rules expressed in terms of judgments G;P | A\\vdash e:t, where G is a
-class environment, P is a set of predicates, A is a set of assumptions,
-`e` is an expression, and `t` is a corresponding type [[Jones,
-1992](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Quality)].
-Judgments like this can be thought of as 5-tuples, and the typing rules
-themselves just correspond to a 5-place relation. Exactly the same
-structure shows up in types of the form `Infer e t`, except that, by
-using functions, we distinguish very clearly between input and output
-parameters.
+class environment, P is a set of predicates, A is a set of
+assumptions, `e` is an expression, and `t` is a corresponding type
+[[Jones, 1992](#jones-1992)].  Judgments like this can be thought of
+as 5-tuples, and the typing rules themselves just correspond to a
+5-place relation. Exactly the same structure shows up in types of the
+form `Infer e t`, except that, by using functions, we distinguish very
+clearly between input and output parameters.
 
-### 11.1  Literals
+### Literals
 
 Like other languages, Haskell provides special syntax for constant
 values of certain primitive datatypes, including numerics, characters,
@@ -1410,7 +1388,7 @@ tiLit (LitRat _)  = do v <- newTVar Star
                        return ([IsIn "Fractional" v], v)
 ```
 
-### 11.2  Patterns
+### Patterns
 
 Patterns are used to inspect and deconstruct data values in lambda
 abstractions, function and pattern bindings, list comprehensions, do
@@ -1542,7 +1520,7 @@ patterns above. It is also useful in other situations where lists of
 patterns are used, such as on the left hand side of an equation in a
 function definition.
 
-### 11.3  Expressions
+### Expressions
 
 Next we describe type inference for expressions, represented by the
 `Expr` datatype:
@@ -1560,18 +1538,18 @@ literals, respectively. The `Const` constructor is used to deal with
 named constants, such as the constructor or selector functions
 associated with a particular datatype or the member functions that are
 associated with a particular class. We use values of type `Assump` to
-supply a name and type scheme, which is all the information that we need
-for the purposes of type inference. Function application is represented
-using the `Ap` constructor, while `Let` is used to represent let
-expressions. (Note that the definition of the `BindGroup` type, used
-here to represent binding groups, will be delayed to
-Section [11.6.3](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-bindgroup).)
-Of course, Haskell has a much richer syntax of expressions-which
-includes l-abstractions, case expressions, conditionals, list
-comprehensions, and do-notation-but they all have simple translations
-into `Expr` values. For example, a l-expression like `\x->e` can be
-rewritten using a local definition as `let f x = e in f`, where `f` is a
-new variable.
+supply a name and type scheme, which is all the information that we
+need for the purposes of type inference. Function application is
+represented using the `Ap` constructor, while `Let` is used to
+represent let expressions. (Note that the definition of the
+`BindGroup` type, used here to represent binding groups, will be
+delayed to [Binding Groups](#binding-groups).)  Of course, Haskell has
+a much richer syntax of expressions-which includes l-abstractions,
+case expressions, conditionals, list comprehensions, and
+do-notation-but they all have simple translations into `Expr`
+values. For example, a l-expression like `\x->e` can be rewritten
+using a local definition as `let f x = e in f`, where `f` is a new
+variable.
 
 Type inference for expressions is quite straightforward:
 
@@ -1595,13 +1573,13 @@ tiExpr ce as (Let bg e)       = do (ps, as') <- tiBindGroup ce as bg
 ```
 
 The final case here, for `Let` expressions, uses the function
-`tiBindGroup` presented in
-Section [11.6.3](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-bindgroup),
-to generate a list of assumptions `as'` for the variables defined in
+`tiBindGroup` presented in [Binding Groups](#binding-groups), to
+generate a list of assumptions `as'` for the variables defined in
 `bg`. All of these variables are in scope when we calculate a type `t`
-for the body `e`, which also serves as the type of the whole expression.
+for the body `e`, which also serves as the type of the whole
+expression.
 
-### 11.4  Alternatives
+### Alternatives
 
 The representation of function bindings in following sections uses
 *alternatives*, represented by values of type `Alt`:
@@ -1614,13 +1592,12 @@ An `Alt` specifies the left and right hand sides of a function
 definition. With a more complete syntax for `Expr`, values of type `Alt`
 might also be used in the representation of lambda and case expressions.
 
-For type inference, we begin by using `tiPats` to infer a type for each
-of the patterns, and to build a new list `as'` of assumptions for any
-bound variables, as described in
-Section [11.2](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-pat).
-Next, we calculate the type of the body in the scope of the bound
-variables, and combine this with the types of each pattern to obtain a
-single (function) type for the whole `Alt`:
+For type inference, we begin by using `tiPats` to infer a type for
+each of the patterns, and to build a new list `as'` of assumptions for
+any bound variables, as described in [Patterns](#patterns).  Next, we
+calculate the type of the body in the scope of the bound variables,
+and combine this with the types of each pattern to obtain a single
+(function) type for the whole `Alt`:
 
 ``` haskell
 tiAlt                :: Infer Alt Type
@@ -1653,7 +1630,7 @@ that we generate and pass in a fresh type variable `v` in the parameter
 `t` to `tiAlts`, and then inspect the value of `v` under the current
 substitution when it returns.
 
-### 11.5  From Types to Type Schemes
+### From Types to Type Schemes
 
 We have seen how lists of predicates are accumulated during type
 inference; now we will describe how those predicates are used to
@@ -1676,21 +1653,20 @@ For example:
 
 -   The list `ps` can often be simplified using the context reduction
     process described in
-    Section [7.4](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-ctxtred).
+    [Context Reduction](#context-reduction).
     This will also ensure that the syntactic restrictions of Haskell are
     met, requiring all predicates to be in head-normal form.
 
--   Some of the predicates in `ps` may contain only “fixed” variables
+- Some of the predicates in `ps` may contain only “fixed” variables
     (i.e., variables appearing in the assumptions), so including those
-    constraints in the inferred type will not be of any use [[Jones,
-    1992](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Quality),Section
-    6.1.4]. These predicates should be “deferred” to the enclosing
-    bindings.
+    constraints in the inferred type will not be of any use
+    [[Jones, 1992](#jones-1992)],Section 6.1.4]. These predicates
+    should be “deferred” to the enclosing bindings.
 
 -   Some of the predicates in `ps` could result in *ambiguity*, and
     require defaulting to avoid a type error. This aspect of Haskell's
     type system will be described shortly in
-    Section [11.5.1](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-default).
+    [Ambiguity and Defaults](#ambiguity-and-defaults).
 
 In this paper we use a function called `split` to address these issues.
 For the situation described previously where we have inferred a type `t`
@@ -1718,7 +1694,7 @@ variables over which we would like to quantify; for the example above,
 it would just be the variables in `(tv t \\ fs)`. It is possible for
 `ps` to contain variables that are not in either `fs` or `gs` (and hence
 not in the parameter `(fs++gs)` that is passed to `defaultedPreds`). In
-Section [11.5.1](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-default)
+[Ambiguity and Defaults](#ambiguity-and-defaults)
 we will see that this is an indication of ambiguity.
 
 There are three stages in the `split` function, corresponding directly
@@ -1732,16 +1708,15 @@ of all such predicates in `rs'`. Hence the final set of retained
 predicates is produced by the expression `rs \\ rs'` in the last line of
 the definition.
 
-#### 11.5.1  Ambiguity and Defaults
+#### Ambiguity and Defaults
 
-In the terminology of Haskell [[Peyton Jones & Hughes,
-1999](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Haskell98),Section
-4.3.4], a type scheme `ps => t` is *ambiguous* if `ps` contains generic
-variables that do not also appear in `t`. This condition is important
-because theoretical studies [[Blott,
-1991](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Blott),[Jones,
-1992](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Quality)]have
-shown that, in the general case, we can only guarantee a well-defined
+In the terminology of Haskell
+[[Peyton Jones & Hughes, 1999](#peyton-jones--hughes-1999),Section
+4.3.4], a type scheme `ps => t` is *ambiguous* if `ps` contains
+generic variables that do not also appear in `t`. This condition is
+important because theoretical studies
+[[Blott, 1991](#blott-1991),[Jones, 1992](#jones-1992)]have shown
+that, in the general case, we can only guarantee a well-defined
 semantics for a term if its most general type is not ambiguous. As a
 result, expressions with ambiguous types are considered ill-typed in
 Haskell and will result in a static error. The following definition
@@ -1814,8 +1789,8 @@ ambiguities ce vs ps = [ (v, filter (elem v . tv) ps) | v <- tv ps \\ vs ]
 ```
 
 Given one of these pairs `(v,qs)`, and as specified by the Haskell
-report [[Peyton Jones & Hughes,
-1999](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Haskell98),Section
+report
+[[Peyton Jones & Hughes, 1999](#peyton-jones--hughes-1999),Section
 4.3.4], defaulting is permitted if, and only if, all of the following
 conditions are satisfied:
 
@@ -1846,7 +1821,7 @@ conditions are satisfied:
     in `qs`. The first such type will be selected as the default. The
     list of default types can be obtained from a class environment by
     using the `defaults` function that was described in
-    Section [7.2](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-classenv).
+    [Class Environments](#class-environments).
 
 These conditions are captured rather more succinctly in the following
 definition, which we use to calculate the candidates for resolving a
@@ -1906,18 +1881,18 @@ if the ambiguous variables don't appear anywhere in the assumptions or
 in the inferred types, then applying this substitution to those
 components would have no effect. In fact, we will only need
 `defaultSubst` at the top-level, when type inference for an entire
-module is complete [[Peyton Jones & Hughes,
-1999](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Haskell98),Section
+module is complete
+[[Peyton Jones & Hughes, 1999](#peyton-jones--hughes-1999),Section
 4.5.5, Rule 2]. In this case, it is possible that Haskell's infamous
 “monomorphism restriction” (see
-Section [11.6.2](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-impbind))
-may prevent generalization over some type variables. But Haskell does
-not allow the types of top-level functions to contain unbound type
+[Implicitly Typed Bindings](#implicitly-typed-bindings)) may prevent
+generalization over some type variables. But Haskell does not allow
+the types of top-level functions to contain unbound type
 variables. Instead, any remaining variables are considered ambiguous,
 even if they appear in inferred types; the substitution is needed to
 ensure that they are bound correctly.
 
-### 11.6  Binding Groups
+### Binding Groups
 
 Our last remaining technical challenge is to describe typechecking for
 binding groups. This area is neglected in most theoretical treatments of
@@ -1930,7 +1905,7 @@ by describing the treatment of explicitly typed bindings and implicitly
 typed bindings as separate cases, and then show how these can be
 combined.
 
-#### 11.6.1  Explicitly Typed Bindings
+#### Explicitly Typed Bindings
 
 The simplest case is for explicitly typed bindings, each of which is
 described by the name of the function that is being defined, the
@@ -1946,11 +1921,9 @@ enforce that here.
 
 Type inference for an explicitly typed binding is fairly easy; we need
 only check that the declared type is valid, and do not need to infer a
-type from first principles. To support the use of polymorphic recursion
-[[Henglein,
-1993](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Henglein:polyrec),[Kfoury
-*et al.* ,
-1993](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Kfoury:polyrec)],
+type from first principles. To support the use of polymorphic
+recursion
+[[Henglein, 1993](#henglein-1993),[Kfoury *et al.* , 1993](#kfoury-et-al--1993)],
 we will assume that the declared typing for `i` is already included in
 the assumptions when we call the following function:
 
@@ -1992,7 +1965,7 @@ along with the appropriate sets of fixed and generic variables. If there
 are any retained predicates after context reduction, then an error is
 reported, indicating that the declared context is too weak.
 
-#### 11.6.2  Implicitly Typed Bindings
+#### Implicitly Typed Bindings
 
 Two complications occur when we deal with implicitly typed bindings. The
 first is that we must deal with groups of mutually recursive bindings as
@@ -2046,32 +2019,31 @@ tiImpls ce as bs = do ts <- mapM (\_ -> newTVar Star) bs
 ```
 
 In the first part of this process, we extend `as` with assumptions
-binding each identifier defined in `bs` to a new type variable, and use
-these to type check each alternative in each binding. This is necessary
-to ensure that each variable is used with the same type at every
-occurrence within the defining list of bindings. (Lifting this
-restriction makes type inference undecidable [[Henglein,
-1993](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Henglein:polyrec),[Kfoury
-*et al.* ,
-1993](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Kfoury:polyrec)].)
+binding each identifier defined in `bs` to a new type variable, and
+use these to type check each alternative in each binding. This is
+necessary to ensure that each variable is used with the same type at
+every occurrence within the defining list of bindings. (Lifting this
+restriction makes type inference undecidable
+[[Henglein, 1993](#henglein-1993),[Kfoury *et al.* , 1993](#kfoury-et-al--1993)].)
 Next we use `split` to break the inferred predicates in `ps'` into a
-list of deferred predicates `ds` and retained predicates `rs`. The list
-`gs` collects all the generic variables that appear in one or more of
-the inferred types `ts'`, but not in the list `fs` of fixed variables.
-Note that a different list is passed to `split`, including only
-variables that appear in *all* of the inferred types. This is important
-because all of those types will eventually be qualified by the same set
-of predicates, and we do not want any of the resulting type schemes to
-be ambiguous. The final step begins with a test to see if the
-monomorphism restriction should be applied, and then continues to
-calculate an assumption containing the principal types for each of the
-defined values. For an unrestricted binding, this is simply a matter of
-qualifying over the retained predicates in `rs` and quantifying over the
-generic variables in `gs`. If the binding group is restricted, then we
-must defer the predicates in `rs` as well as those in `ds`, and hence we
-can only quantify over variables in `gs` that do not appear in `rs`.
-
-#### 11.6.3  Combined Binding Groups
+list of deferred predicates `ds` and retained predicates `rs`. The
+list `gs` collects all the generic variables that appear in one or
+more of the inferred types `ts'`, but not in the list `fs` of fixed
+variables.  Note that a different list is passed to `split`, including
+only variables that appear in *all* of the inferred types. This is
+important because all of those types will eventually be qualified by
+the same set of predicates, and we do not want any of the resulting
+type schemes to be ambiguous. The final step begins with a test to see
+if the monomorphism restriction should be applied, and then continues
+to calculate an assumption containing the principal types for each of
+the defined values. For an unrestricted binding, this is simply a
+matter of qualifying over the retained predicates in `rs` and
+quantifying over the generic variables in `gs`. If the binding group
+is restricted, then we must defer the predicates in `rs` as well as
+those in `ds`, and hence we can only quantify over variables in `gs`
+that do not appear in `rs`.
+
+#### Combined Binding Groups
 
 Haskell requires a process of *dependency analysis* to break down
 complete sets of bindings-either at the top-level of a program, or
@@ -2164,10 +2136,9 @@ report does indicate that a modification of the example to include an
 explicit type for `g` would be illegal. This is a consequence of a
 throw-away comment specifying that all explicit type signatures in a
 binding group must have the same context up to renaming of variables
-[[Peyton Jones & Hughes,
-1999](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#Haskell98),Section
-4.5.2]. This is a syntactic restriction that can easily be checked prior
-to type checking. Our comments here, however, suggest that it is
+[[Peyton Jones & Hughes, 1999](#peyton-jones--hughes-1999),Section
+4.5.2]. This is a syntactic restriction that can easily be checked
+prior to type checking. Our comments here, however, suggest that it is
 unnecessarily restrictive.
 
 In addition to the function bindings that we have seen already, Haskell
@@ -2228,7 +2199,7 @@ tiSeq ti ce as (bs:bss) = do (ps,as')  <- ti ce as bs
                              return (ps++qs, as''++as')
 ```
 
-#### 11.6.4  Top-level Binding Groups
+#### Top-level Binding Groups
 
 At the top-level, a Haskell program can be thought of as a list of
 binding groups:
@@ -2255,124 +2226,119 @@ tiProgram ce as bgs = runTI $
 
 This completes our presentation of the Haskell type system.
 
-12  Conclusions
----------------
+## Conclusions
 
 We have presented a complete Haskell program that implements a type
 checker for the Haskell language. In the process, we have clarified
 certain aspects of the current design, as well as identifying some
 ambiguities in the existing, informal specification.
 
-The type checker has been developed, type-checked, and tested using the
-“Haskell 98 mode” of Hugs 98 [[Jones & Peterson,
-1999](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#HugsManual)].
-The full program includes many additional functions, not shown in this
-paper, to ease the task of testing, debugging, and displaying results.
-We have also translated several large Haskell programs-including the
-Standard Prelude, the Maybe and List libraries, and the source code for
-the type checker itself-into the representations described in
-Section [11](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#sec-typeinf),
-and successfully passed these through the type checker. As a result of
-these and other experiments we have good evidence that the type checker
-is working as intended, and in accordance with the expectations of
-Haskell programmers.
+The type checker has been developed, type-checked, and tested using
+the “Haskell 98 mode” of Hugs 98
+[[Jones & Peterson, 1999](#jones--peterson-1999)].  The full program
+includes many additional functions, not shown in this paper, to ease
+the task of testing, debugging, and displaying results.  We have also
+translated several large Haskell programs-including the Standard
+Prelude, the Maybe and List libraries, and the source code for the
+type checker itself-into the representations described in
+[Type Inference](#type-inference), and successfully passed these
+through the type checker. As a result of these and other experiments
+we have good evidence that the type checker is working as intended,
+and in accordance with the expectations of Haskell programmers.
 
 We believe that this typechecker can play a useful role, both as a
 formal specification for the Haskell type system, and as a testbed for
 experimenting with future extensions.
 
-Acknowledgments
----------------
+## Acknowledgments
 
-This paper has benefited from feedback from Johan Nordlander, Tom
 Pledger, Lennart Augustsson, Stephen Eldridge, Tim Sheard, Andy Gordon,
 and from an anonymous referee. The research reported in this paper was
 supported, in part, by the USAF Air Materiel Command, contract \#
 F19628-96-C-0161, and by the National Science Foundation grants
 CCR-9703218 and CCR-9974980.
 
-References
-----------
+## References
 
-## Blott, 1991
+### Blott, 1991
 
 Blott, Stephen M. (1991). *An approach to overloading with
     polymorphism*. Ph.D. thesis, Department of Computing Science,
     University of Glasgow.
 
-## Damas & Milner, 1982
+### Damas & Milner, 1982
 
 Damas, L., & Milner, R. (1982). Principal type schemes for functional
     programs. *Pages 207-212 of:* *9th Annual ACM Symposium on
     Principles of Programming Languages*.
 
-## Gaster & Jones, 1996
+### Gaster & Jones, 1996
 
 Gaster, Benedict R., & Jones, Mark P. (1996). *A polymorphic type
     system for extensible records and variants*. Technical Report
     NOTTCS-TR-96-3. Computer Science, University of Nottingham.
 
-## Henglein, 1993
+### Henglein, 1993
 
 Henglein, Fritz. (1993). Type inference with polymorphic recursion.
 *ACM Transactions on Programming Languages and Systems*, **15**(2),
 253-289.
 
-## Hindley, 1969
+### Hindley, 1969
 
 Hindley, R. (1969). The principal type-scheme of an object in
     combinatory logic. *Transactions of the American Mathematical
     Society*, **146**, 29-60.
 
-## Jones, 1992
+### Jones, 1992
 
 Jones, Mark P. (1992). *Qualified types: Theory and practice*. Ph.D.
     thesis, Programming Research Group, Oxford University Computing
     Laboratory. Published by Cambridge University Press, November
     1994.
 
-## Jones & Peterson, 1999
+### Jones & Peterson, 1999
 
 Jones, Mark P., & Peterson, John C. (1999). *Hugs 98 User Manual*.
-    Available from `http://www.haskell.org/hugs/`.
+    Available from [the Hugs homepage](http://www.haskell.org/hugs/).
 
-## Kfoury *et al.* , 1993
+### Kfoury *et al.* , 1993
 
 Kfoury, A.J., Tiuryn, J., & Urzyczyn, P. (1993). Type reconstruction
     in the presence of polymorphic recursion. *ACM Transactions on
     Programming Languages and Systems*, **15**(2), 290-311.
 
-## Milner, 1978
+### Milner, 1978
 
 Milner, R. (1978). A theory of type polymorphism in programming.
 *Journal of Computer and System Sciences*, **17**(3).
 
-## Peyton Jones & Hughes, 1999
+### Peyton Jones & Hughes, 1999
 
 Peyton Jones, Simon, & Hughes, John (eds). (1999). *Report on the
     Programming Language Haskell 98, A Non-strict Purely Functional
     Language*. Available from `http://www.haskell.org/definition/`.
 
-## Peyton Jones *et al.* , 1997
+### Peyton Jones *et al.* , 1997
 
 Peyton Jones, Simon, Jones, Mark, & Meijer, Erik. (1997). Type
     classes: Exploring the design space. *Proceedings of the second
     haskell workshop*.
 
-## Robinson, 1965
+### Robinson, 1965
 
 Robinson, J.A. (1965). A machine-oriented logic based on the
     resolution principle. *Journal of the Association for Computing
     Machinery*, **12**.
 
-## Wadler, 1992
+### Wadler, 1992
 
 Wadler, P. (1992). The essence of functional programming (invited
     talk). *Pages 1-14 of:* *Conference record of the Nineteenth
     annual ACM SIGPLAN-SIGACT symposium on Principles of Programming
     Languages*.
 
-## Wadler & Blott, 1989
+### Wadler & Blott, 1989
 
 Wadler, P., & Blott, S. (1989). How to make *ad hoc* polymorphism less
     *ad hoc*. *Pages 60-76 of:* *Proceedings of 16th ACM Symposium on

diff --git a/typing.md b/typing.md
@@ -32,11 +32,10 @@ which to explore new proposals.
 Introduction
 ---------------
 
-Haskell[^2]
-benefits from one of the most sophisticated type systems of any widely
-used programming language. Unfortunately, it also suffers because there
-is no formal specification of what the type system should be. As a
-result:
+Haskell benefits from one of the most sophisticated type systems of
+any widely used programming language. Unfortunately, it also suffers
+because there is no formal specification of what the type system
+should be. As a result:
 
 - It is hard for Haskell implementors to be sure that their systems
   accept the same programs as other implementations. The informal
@@ -411,7 +410,7 @@ nullSubst   = []
 ```
 
 Almost as simple are the substitutions
-`(u +-> t)`[^3^](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tthFtNtAAD)
+`(u +-> t)`
 that map a single variable `u` to a type `t` of the same kind:
 
 ``` haskell
@@ -613,7 +612,7 @@ types in each class (known as `instances`) are specified by a collection
 of instance declarations. Haskell types can be *qualified* by adding a
 (possibly empty) list of *predicates*, or class constraints, to restrict
 the ways in which type variables are
-instantiated[^4^](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tthFtNtAAE):
+instantiated:
 
 ``` haskell
 data Qual t = [Pred] :=> t
@@ -734,7 +733,7 @@ this condition might be guaranteed by static analysis prior to type
 checking. Alternatively, we can resort to a dynamic check by testing
 `defined (classes ce i)` before applying either function. The function
 `defined` used here is defined as
-follows[^5^](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tthFtNtAAF):
+follows:
 
 ``` haskell
 defined :: Maybe a -> Bool
@@ -2378,35 +2377,3 @@ Wadler, P. (1992). The essence of functional programming (invited
 Wadler, P., & Blott, S. (1989). How to make *ad hoc* polymorphism less
     *ad hoc*. *Pages 60-76 of:* *Proceedings of 16th ACM Symposium on
     Principles of Programming Languages*.
-
-* * * * *
-
-### Footnotes:
-
-[^1^](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tthFrefAAB)An
-earlier version of this paper was presented at the Haskell workshop in
-Paris, France, on October 1, 2000. Both papers describe the same type
-system, but some significant parts of this version have been rewritten,
-restructured, or expanded to clarify the presentation.
-
-[^2]: Throughout, we use “Haskell” as an abbreviation for “Haskell 98”.
-
-[^3^](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tthFrefAAD)The
-“maps to” symbol `+->` is written as `+->` in the concrete syntax of
-Haskell.
-
-[^4^](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tthFrefAAE)The
-symbol `:=>` (pronounced “then”) is written as `:=>` in the concrete
-syntax of Haskell, and corresponds directly to the ` =>` symbol that is
-used in instance declarations and in types.
-
-[^5^](http://web.cecs.pdx.edu/~mpj/thih/TypingHaskellInHaskell.html#tthFrefAAF)The
-same function appears in the standard `Maybe` library, but with a less
-intuitive name: `isJust`.\
-\
-
-* * * * *
-
-File translated from T~E~X by
-[T~T~H](http://hutchinson.belmont.ma.us/tth/), version 2.73.\
-On 23 Nov 2000, 08:00.
diff --git a/typing.md b/typing.md
@@ -14,6 +14,8 @@
 
 *Version of November 23, 2000.*
 
+*Converted to Markdown on November 8, 2014.*
+
 Abstract
 --------
 

diff --git a/typing.md b/typing.md
@@ -1,3 +1,5 @@
+# Typing Haskell in Haskell
+
 **MARK P. JONES**
 
 **Pacific Software Research Center**

diff --git a/typing.md b/typing.md