Notes on type inference and polymorphism

You might have heard that polymorphism is hard to combine with Hindley-Milner type inference, but what does this mean exactly?

First of all, remember two key properties of HM that we would like to preserve:

Second, Hindley-Milner works just fine with some types of polymorphism; parametric polymorphism comes with the definition, and there are other classes of polymorphism for which Hindley-Milner works just fine. However, if you try to add something like type classes, things get a bit more complicated. For example, let’s say our language lets us define a Monad type class like this:

class Monad m where
  (>>=)  :: m a -> (  a -> m b) -> m b
  return :: a -> m a

We could then say that a given type is a Monad instance:

data Maybe a = Nothing | Just a

instance Monad Maybe where
  (>>=) Nothing _  = Nothing
  (>>=) (Just x) f = f x
  return           = Just

These kinds of type classes are “open”; we can say that a type is an instance of a type class even outside the type’s definition. This means that user-defined types can be made instances of a type class defined in a package, and vice versa. However, this flexibility comes at a cost; inference for type classes is undecidable, which means that we sometimes have to add type annotations to functions that use them. I will demonstrate some examples of this below:

Overlapping instances

The first problem is overlapping instances. Let’s say you also want to define a functor instance for Maybe:

instance Functor Maybe where
  fmap Nothing _  = Nothing
  fmap (Just x) f = Just $ f x
  pure            = Just

However, if you also implement a functor instance like this elsewhere in the program:

instance Functor m => Monad m where
  fmap m = (>>=) . return
  pure   = return

… then these instances will overlap. For example, given the following program, Haskell will not know which instance to pick:

addOne x = fmap x (+ 1)

One way to solve this is to require type annotations to help disambiguate between instances, and have the type checker always pick the most specific instance. For example, given that we’ve explicitly said we want a Maybe, the type checker can resolve that to the Maybe instance of Functor:

addOne Maybe Int -> Maybe Int
addOne x = fmap x (+ 1)

However, this means we can no longer infer types for all expressions.

How to solve this?

To solve the problem with overlapping instances, we need to make sure there is only ever one implementation of a given type class. We can do this by only allowing defining type class instances when defining a type, similar to how Rust traits work. We might also need to disallow type variables in instance declarations (Haskell 98 had this limitation if I’m not mistaken?).

Ambiguous instances

The next problem is ambiguous instances. Let’s say we have two type classes that look like this:

class Monad m where
  (>>=)  :: m a -> (a -> m b) -> m b
  return :: a -> m a

class Pure m where
  return :: a -> m a

Given these definitions, which type class does the expression pure x refer to? We can’t tell, since both type classes define pure.

How to solve this?

One way to solve this is to get rid of “type classes” altogether and only allow overloading of individual functions:

instance (>>=)  :: m a -> (a -> m b) -> m b
instance return :: a -> m a

This is the approach taken in A Second Look At Overloading by Wadler and Odersky; this delimitation, together with some other restrictions, allows implementing polymorphism while maintaining inference of principal types.

While this approach gets rid of the ambiguous instance problem, we can no longer enforce that related functions are used together; for example, we might accidentally overload >>= with a different operation and get surprising behaviour in our program as a result.

MLSub by Dolan and Mycroft solves this by supporting union types; that is, if a value could potentially match both types A and B, it is inferred to have type A|B. This we can keep having type classes, and always be able to infer a principal type for each expression. If you’re interested in MLSub, you should refer to The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy.

Other notes

As we have seen, it is not trivial to combine type inference and type classes; while it’s still possible, the algorithms for type reconstruction are much less elegant than the original Hindley-Milner, and can also become computationally intensive.

In light of this we shouldn’t forget that there is a third option: Not inferring types at all! Fernando Boretti made a pretty compelling argument against type inference in Type Inference Was A Mistake; given that lack of annotations can make a program harder to read instead of easier, maybe we should skip inference altogether?

There is also another type inference technique that is less powerful, but both simpler in concept and implementation: Bidirectional Type-checking. The basic idea is that as long as we annotate all top-level functions, we can omit annotations for their arguments and return values. The whole concept is a bit too large to cover here, but David Christiansen has written a tutorial about it: Bidirectional Typing Rules: A Tutorial

« Go back