Reasoning about type inhabitants in Haskell

type-inhabitants.markdown

This is material to go along with a 2014 Boston Haskell talk.

We are going to look at a series of type signatures in Haskell and explore how parametricity (or lack thereof) lets us constrain what a function is allowed to do.

Let's start with a decidedly non-generic function signature. What are the possible implementations of this function which typecheck?

wrangle :: Int -> Int

I've deliberately picked a meaningless name so it doesn't influence our thinking.

Haskell gives us some guarantees about what wrangle can't do. It can't launch the missiles, write to the file system, etc. If it were allowed to do any of those things it would have to return an IO Int. (I'm ignoring unsafePerformIO. Yes technically there are some functions that let you subvert the type system, but we're going to ignore those for purposes of this discussion. There's also something called Safe Haskell if you really want to enforce these things with more than a "gentleman's agreement" to not use evil functions like unsafePerformIO.)

But other than that, this function can do pretty much anything with the Int it's given. It could add 42 then multiply by 19, always return 0, etc. The type of wrangle doesn't tell us very much about what its implementation might do.

Note: A bit of jargon--an 'inhabitant' of a type is just a value with that type. So \x -> x+1 (also written (1+)) is one inhabitant of the type Int -> Int. You might hear people talk about 'type inhabitants' as another way of saying 'values of that type'.

Now compare that to this signature:

pwrangle :: forall a . a -> a
pwrangle :: a -> a -- the forall is implicit in this version, any lowercase type variables are universally quantified

When you write a function that deals with concrete types, like Int, the implementation of that function has access to the entire universe of functions defined on those concrete types. In contrast, when you write a polymorphic function that deals with quantified type variables, the implementation only gets access to functions and values that are passed in. We are carving out a tiny little universe of possibilities for ourselves, and the typechecker will enforce we don't make assumptions beyond this universe. When I write pwrangle a = ..., I have not been given the ability to do anything with that a value. All I can do is return it! Hence pwrangle must be the identity function, pwrangle a = a.

More examples:

oog :: a -> (a,a)
oog a = (a,a)

This also has only one implementation. Since we can't conjure up an a, our only option is to pass the input to both sides of the pair.

What about this?

ding :: a -> a -> a -- how many implementations?

This has exactly two implementations - we can choose the first argument or the second. We might say that a -> a -> a contains as much information as Bool.

Another example: both these types have exactly one implementation:

zonks :: a -> b -> a
zonks' :: a -> b -> b

One often hears the claim that it's better to wait on abstracting code until it really 'proves necessary'. A counterpoint to this sort of rule of thumb is that generalizing code gives you more help from the typechecker in ensuring that code is implemented correctly. Here's a simple example:

data Pt = Pt Double Double

x :: Pt -> Double
x (Pt a _) = a

But note that if we made Pt polymorphic, we could give x the more precise type:

x :: Pt x y -> x

which has only one implementation. Moreover, functions that don't care whether x and y have the same type could be appropriately parametric, and the typechecker will tell us if we ever accidentally confuse the two, something we don't get if we specialize to Double, or if we give Pt just one type parameter shared by both dimensions!

It's often more idiomatic in FP to write more polymorphic functions, which are explicitly passed any arguments (possibly higher order) needed to do their job, rather than specializing functions to particular concrete types. More generic functions are (locally) more limited in what they can do, and we get more help from the typechecker when writing them. As an added bonus, they are often easier to test, because we can instantiate type variables to simple types that are easier to 'mock' for purposes of a test.

Question, what's wrong with this function:

ohno :: [a] -> a

Since we are parametric in a, we have no way to produce an a other than obtaining one from the input list. Thus, ohno [] = ??? has nothing it can do other that throw an error! A better signature is [a] -> Maybe a.

Another example - based on the same reasoning, this type has exactly one inhabitant:

blah :: [a] -> [b]
blah _ = []

Since blah has no source of b values, it has no choice but to return the empty list!

Free theorems

Since a function polymorphic in some type a is not allowed to inspect or conjure up a values other than by using the function arguments, this gives us a powerful source of 'free theorems'. To motivate, let's look at some examples.

Question: is the following equation true?

reverse (fmap f xs) == fmap f (reverse xs)
-- equivalently reverse . fmap f = fmap f . reverse

That is, can we reverse a list before or after mapping a function f and obtain the same result? Yes, we can.

Now, what if instead of reverse we have an arbitrary function of type phi :: [a] -> [a]? Is it still the case that:

phi . fmap f = fmap f . phi

Yes! Whatever decisions are made by phi, it is not allowed to care about the actual elements of the list, so we can make those same decisions before or after transforming the list via fmap f. Note that we were able to read this theorem purely from the type of phi, we don't care about its implementation. We say that it is a free theorem of the type forall a . [a] -> [a].

Before generalizing this, let's look at one more concrete example. Given:

safeHead : [a] -> Maybe a
safeHead [] = Nothing
safeHead (h:t) = Just h

Is it the case that:

safeHead . fmap f == fmap f . safeHead

On the left side, we first map a function f over a list, then take the head of the list, safely. On the right side, we do it in the reverse order, take the safeHead and the map f over the Maybe value returned from safeHead. A little thought shows these give the same results. Why? Because safeHead does not care about the type of the elements, we can apply a transformation to the element(s) before or after taking safeHead, and obtain the same result.

Generalizing a bit more, we notice that we don't care about the implementation of safeHead. For any phi :: [a] -> Maybe a, it is true that:

phi . fmap f == fmap f . phi

This is the free theorem for the type [a] -> Maybe a.

Generalizing this a bit more, for any polymorphic function in one variable, phi :: t a -> u a, it is a free theorem that:

phi . fmap f == fmap f . phi

In the case of reverse, t and u were both []. In the case of safeHead, t was [] and u was Maybe.

This same rule also applies to functions like length : [a] -> Int. This does not seem to fit the pattern for phi, since it returns an Int, rather than a u a, but if we let u be the Const functor:

data Const k a = Const { getConst :: k }

instance Functor (Const k) where
  fmap _ (Const k) = Const k -- ignores the function!

Then we still get the free theorem:

length . fmap f == getConst . fmap f . Const . length

The right side fmap is mapping over a Const Int.

These free theorems have a connection to category theory. Parametricity ensures 'naturality', and polymorphic functions can be considered natural transformations between functors.

Other notes

• The more general scheme for free theorems, for polymorphic functions of multiple variables, with type variables appearing in positive and negative position, is given in Theorems for free, which is the original Wadler paper introducing free theorems. I don't totally follow Wadler's explanation for the general scheme for arbitrary polymorphic functions of multiple type variables. Perhaps someone reading this could offer a better explanation in the comments and we can incorporate it.
• Here is a 'free theorem' generator. You enter a Haskell type, and it tells you the free theorem(s) for that type!
• This post has some good discussion about free theorems and their relationship to category theory, and I've stolen a number of examples from there.
• The strength of parametricity is often surprising. On several occasions, a 'law' required of some typeclass or function has been later shown to be a free theorem given by parametricity. For instance, the second functor law, fmap f . fmap g == fmap (f . g) turns out be derivable from the first fmap id == id Proof. I believe a few (?) of the laws required of Traversable as given in the original paper Applicative programming with effects are actually free theorems.
• Fast and loose reasoning is morally correct discusses this sort of reasoning in light of the existence of nontermination and other forms of partiality.

Closing remarks

The old rule of thumb about abstraction, that one should hold off on abstracting code until it really 'proves necessary', is in my opinion a little too simplistic, and something of a relic from older, OO / procedural languages and their bad/nonexistent types systems. In a language like Haskell with great support for writing higher order functions and generic functions and types, their's often no real penalty to abstracting code early on, and one can obtain greater safety and more help from the typechecker while writing more abstract code.

Appendix: safer alternatives to keyword-based arguments

If you really do have a monomorphic function, and multiple arguments of the same type, a safe way of letting the compiler catch misuse is to newtype one or more of the arguments.

wrange2 :: Double -> Double -> Double
wrangle numerator denominator = numerator / denominator

This becomes:

newtype Numerator a = Numerator a

wrangle2 :: Numerator Double -> Double -> Double

And callers must write wrangle2 (Numerator x) y, explicitly indicating that x is to be the numerator. I don't necessarily endorse doing this in all cases, but it's just an example of how we can use Haskell's type system to force us to be more explicit and catch certain types of errors.

I don't see how "the implementation only gets access to functions and values that are passed in" would be the case for prwrangle any more than for wrangle; wouldn't it have "access to the entire universe of functions defined" on that type? Just that that universe is limited to id and pwrangle.