# Type inference for Haskell, part 22

Posted on January 23, 2019

This is part 22 of the series on type inference for Haskell.

(THIH Section 11.6.2, Implicitly Typed Bindings)

At the very beginning of this series of posts, I said that you could think of a function defined like:

``foo x y z = ...``

as being equivalent to:

``foo = (\x -> (\y -> (\z -> ...)))``

The point was that `foo` is actually a single argument function which only takes a value of `x`. It just happens to return another function which takes a value `y`, and so on.

But, I also said that they are not completely equivalent.

For a concrete example of where there is a difference, consider these two implementations of a function for adding two numbers:

``````plus1 x y = x + y
plus2 = (\x y -> x + y)``````

It looks like `plus1` and `plus2` should both be able to handle any kind of number, right? `plus1` has the type you’d expect:

``plus1 :: Num a => a -> a -> a``

But oddly, `plus2` has a less general type:

``plus2 :: Integer -> Integer -> Integer``

Why on earth is that the case?

This is due to a odd feature of Haskell called the “Monomorphism Restriction.”

## What it is?

In short, it’s where Haskell sometimes uses a more restricted type for bindings that look like they might not be functions. It considers a binding to look like a function when there are argument patterns to the left of the `=` in the declaration.

In what way does it restrict the types? It makes them monomorphic (hence the name, monomorphism restriction). What does monomorphic mean? It means that there are no type variables in the type that can be used to change the type. It’s the opposite of polymorphic - it means that the type can only take on one “shape.” The type `a -> a` is polymorphic, but the type `Int -> Int` is monomorphic. The monomorphism restriction only makes certain parts of the type monomorphic. There can still be type variables left in the type after the restriction has been applied.

How does it make a type monomorphic? It applies a defaulting substitution. In the previous post, I said that this function would be used later:

``````defaultSubst :: Monad m => ClassEnv -> [Tyvar] -> [Pred] -> m Subst
defaultSubst = withDefaults (\vps ts -> zip (map fst vps) ts)``````

This chooses default types in the same way as `defaultedPreds` did. The only difference is that now instead of returning predicates that can be removed, it returns a substitution to apply to the types. That substitution replaces polymorphic type variables with monomorphic types.

In the `plus2` example above, the type might have originally been the same as `plus1`’s type: `(Num a) => a -> a -> a`. When the monomorphism restriction gets applied to this type, the substitution changed it to `Integer -> Integer -> Integer`.

## When does it apply?

First of all, it doesn’t apply to explicitly typed bindings. For example, it does not apply to this function (even though it is otherwise the same as `plus2`):

``````plus3 :: Num a => a -> a -> a
plus3 = (\x y -> x + y)``````

It also doesn’t apply when the type doesn’t involve any type classes. For example, it does not apply to the following function:

``identity = (\x -> x)``

The type for that is still inferred to be `a -> a`.

The most interesting of the rules is that it only applies to bindings with no patterns. That is to say, it only applies when a binding looks like a variable, not a function. This is the reason why it applied to `plus2` but not `plus1` in the example above. `plus1` has the patterns `x` and `y` (both `PVar` patterns if you recall the post on pattern matching).

Lastly, it only picks default types when there are predicates for certain classes. It’s only able to pick a default type for a type variable if the predicates for that type variable are all standard type classes and at least one of them is a number class. That worked for `plus2` since the only class was `Num`. If you create an ambiguous declaration with some other type class or one without a number class, inference will fail:

``someFn = (\x -> show x)``

Type inference fails for definitions like these because it attempts to find a default type that matches, but the predicates don’t meet the requirements for defaulting.

## Why does it exist?

This may seem like a very strange feature to have. Why make the types more narrow for seemingly no good reason? It turns out that there actually is a good reason for this.

Let’s say you bind `x` to the result of some expensive computation (maybe it computes the Ackermann function for a large value):

``x = someReallyExpensiveNumericComputation 12345``

And let’s say that the function this calls has the type `(Num a) => a -> a`. That function could be called with an integer and return an integer, or called with a float and return a float. It could be used with any type that is an instance of `Num`. When the value of `x` is computed, what type will it be?

Without the monomorphism restriction, code like this puts us in an awkward position. It looks like a variable not a function, so we wouldn’t expect it to be re-computed every time it is used. Yet, it can be used by code wanting it to be a float and by code wanting it to be an int. We cannot have both at once: either you can use it as different types and accept recomputing it, or you use it as a single type and only compute it once. Haskell’s designers chose to go with the later option.

I think this was a good design decision since it follows the principle of least astonishment. If you assumed that it would only be computed once but it was actually recomputed at every usage, that could lead to performance bugs that are really difficult to track down. On the other hand, if you assume that it is usable as different types, the compiler will catch the error and tell you what went wrong.

## The code

The function to ask if a binding is restricted is fairly simple (no pun intended):

``````restricted :: [Impl] -> Bool
restricted bs = any simple bs
where simple (i,alts) = any (null . fst) alts``````

Remember that an `Impl` is an implicitly typed binding. (An `Impl` is a `(Id, [Alt])`, and an `Alt` is a `([Pat], Expr)`.) This function is given an entire binding group (a set of mutually recursive functions). It asks if any of the bindings in that group are “simple.” A binding is simple if it has no patterns/arguments. For example, `f` is simple but `g` and `h` are not:

``````f = (\x -> 123)
g x = 123
h Nothing = 123``````

The `restricted` function is called from one place, the end of the `tiImpls` function. The `tiImpls` function is returning a tuple containing a list of predicates and a list of assumptions. In the code below, `bs` is the list of implicitly typed bindings in a single binding group.

When the group is restricted, two things change.

First, the retained predicates `rs` are returned in addition to the deferred predicates `ds`.

Second, the schemes in the assumptions change. They no longer have any predicates of their own (`[] :=>` instead of `rs :=>`) and the set of type variables they are quantified over changes. `gs` is the set of type variables that appear only in the types of the bindings in this group, and not in the types of other bindings. Instead of quantifying over `gs`, it quantifies over the variables in `gs` that don’t also appear in the retained predicates `rs`. Quantifying over fewer type variables results in a less general type.

Specifically, the type is no longer generalized over a type variable that is mentioned in one of the predicates that defaulting will remove. In the `plus2` example above, this would be the type variable `a` in the type `(Num a) => a -> a -> a`. It isn’t generalizing over `a` because `a` is going to be replaced with `Integer` later on.

``````  if restricted bs then
let gs'  = gs \\ tv rs
scs' = map (quantify gs' . ([] :=>)) ts'
in return (ds++rs, zipWith (:>:) is scs')
else
let scs' = map (quantify gs . (rs :=>)) ts'
in return (ds, zipWith (:>:) is scs')``````

So far we’ve moved the predicates around and made the scheme less general, but haven’t actually replaced type variables with monomorphic types. That happens as a last step at the end of type inference for the whole program.

``````tiProgram :: ClassEnv -> [Assump] -> Program -> [Assump]
tiProgram ce as bgs = runTI \$ do
(ps, as') <- tiSeq tiBindGroup ce as bgs
s         <- getSubst
rs        <- reduce ce (apply s ps)
s'        <- defaultSubst ce [] rs
return (apply (s'@@s) as')``````

The call to `defaultSubst` finds the remaining ambiguities and resolves them through defaulting. If it can’t resolve them with defaulting, type inference fails. The example above that defined `someFn` demonstrated this.

At this point I’d encourage you to open a new Haskell file and play around with the monomorphic restriction.

This wraps up the discussion of how type class predicates are handled. All that remains is to show how this connects to the rest of the type inference code.