# Context reduction

TweetHello, Haskellers! Today I am going to explain what *context reduction* is and why it is necessary.

# Quiz

Let’s start with a quick quiz. What’s the type of `f`

?

`f xs y = xs == [y]`

The return type `f`

must be `Bool`

because the type of `==`

is `Eq a => a -> a -> Bool`

. If we assume the type of `y`

is `t`

, the type of `xs`

must be `[t]`

because two operands of `==`

must have the same type. The type constraint must be `Eq [t]`

because two lists are compared for equality. So we expect the type of `f`

should be `Eq [t] => [t] -> t -> Bool`

.

Let’s check the type in GHCi.

```
λ> f xs y = xs == [y]
f :: Eq t => [t] -> t -> Bool
```

Surprisingly, the context is `Eq t`

instead of `Eq [t]`

. Even though the equality is taken at the list type, the context must be simplified. This is called *context reduction* and is specified in Haskell 2010 Language Report (also in Haskell 98).

# Context reduction

Type Classes and Constraint Handling Rules mentions two reasons why context reduction in Haskell is important.

- Syntactically, context reduction allows the type checker to present type class constraints to the programmer in a more readable form.
- Operationally, context reduction allows the type checker to put type class constraints into a more efficient form. Type class constraints are translated into dictionaries. Hence, simplifying type class constraints may allow a more efficient translation.

Let’s visit each reason with concrete examples.

# Readability

What’s the type of `g`

?

`g a b = [show (a,a), show (a,b), show (b,a), show(b,b)]`

If the type checker infers the type without simplification, it will be

`g :: (Show (a,a), Show(b,b), Show (a,b), Show (b, a)) => a -> b -> [String]`

But Haskell simplifies the context to

`g :: (Show b, Show a) => a -> b -> [String]`

The inferred type looks simpler to programmers.

Surprisingly, GHCi reports the simplified type even though I explicitly annotate the type with the former.

```
λ> :type g
g :: (Show b, Show a) => a -> b -> [String]
```

# Efficient translation

GHC implements type classes as dictionary passing. Readers are referred to Section 4 of How to make ad-hoc polymorphism less ad hoc for the details.

Let’s see how type classes are actually translated by dumping the GHC simplifier output.

`ghc -ddump-simpl -ddump-to-file -c a.hs`

```
{-# NOINLINE f #-}
f :: (Eq a, Ord a) => a -> a -> Bool
f x y = x > y
main = print $ f 1 2
```

`g_rn6`

takes two dictionary arguments though the first one is never used (marked as `Dead`

).

```
f_rn6
:: forall a_aoY. (Eq a_aoY, Ord a_aoY) => a_aoY -> a_aoY -> Bool
[GblId, Arity=4, Caf=NoCafRefs, Str=DmdType]
f_rn6 =
\ (@ a_a1vN)
_ [Occ=Dead]
($dOrd_a1vP :: Ord a_a1vN)
(x_a1rc :: a_a1vN)
(y_a1rd :: a_a1vN) ->
> @ a_a1vN $dOrd_a1vP x_a1rc y_a1rd
```

Call sites of `g`

must create and pass these dictionary arguments when they call `g`

.

```
main :: IO ()
[GblId, Str=DmdType]
main =
print
@ Bool
GHC.Show.$fShowBool
(f_rn6
@ Integer
integer-gmp-1.0.0.1:GHC.Integer.Type.$fEqInteger
integer-gmp-1.0.0.1:GHC.Integer.Type.$fOrdInteger
1
2)
```

Simplifying type class constraints allow a more efficient translation because it removes redundant dictionary arguments.

```
{-# NOINLINE f #-}
f x y = x > y
main = print $ f 1 2
```

is translated to

```
f_rn6 :: forall a_a1vz. Ord a_a1vz => a_a1vz -> a_a1vz -> Bool
[GblId, Arity=3, Caf=NoCafRefs, Str=DmdType]
f_rn6 =
\ (@ a_a1vz)
($dOrd_a1zP :: Ord a_a1vz)
(x_aoY :: a_a1vz)
(y_aoZ :: a_a1vz) ->
> @ a_a1vz $dOrd_a1zP x_aoY y_aoZ
```

`g_rn6`

takes only one dictionary argument `$dOrd_a1zP`

because context reduction merged `(Eq a, Ord a)`

into `Ord a`

. This is a valid simplification because `Ord a`

implies `Eq a`

.

# Formal semantics

The Haskell report provides only informal hints about context reduction.

Fortunately, Section 7.4 of Mark P. Jones’ Typing Haskell in Haskell gives us the formal semantics of context reduction in Haskell. Section 3.2 of Type classes: exploring the design space also discusses context reduction. Interested readers are referred to both papers.