Partial application is one of the most useful tools in a Haskell programmer’s toolbelt. Since functions are just data, they can be passed around without being supplied any arguments, just as one would with any other value. Due to the ubiquity of higher-order functions in Haskell, the ability to partially apply things is extremely useful.
Alas, not everything can be partially applied. In particular, GHC offers a type families extension that lets you define functions for use at the type level, as in the following example:
If having to repeatedly type out
Const Int proves bothersome, then functional
programming wisdom would dictate that we factor it out into its own definition:
Surprisingly, however, GHC will bluntly reject the definition of
Oh dear. GHC just threw our usual intuition for partial application out the window,
since the typechecker is quite adamant that
Const be supplied with no fewer
than two arguments. This means that we must define
ConstInt like this
In general, a type family must be supplied with a minimum number of argument types in order to be considered valid, and that number is referred to as its arity. If a type family has been supplied with enough arguments to match its arity, then it is a fully saturated type family.
The saturation restriction is certainly nothing new—in fact, it’s documented quite clearly in the GHC users’ guide:
We call the number of parameters in a type family declaration, the family’s arity, and all applications of a type family must be fully saturated with respect to that arity.
However, when I recently attempted to explain to someone what exactly “arity” means, I realized that defining the notion of arity is trickier than I expected. The phrase “number of parameters” is a good approximation of arity, but it misses some subtleties that really only become apparent when one looks at different examples of interesting type families. My goal in this blog post is to tease out a more precise definition of arity. I won’t get it right on my first attempt, but we’ll get there in the end, I promise!
Aside 1: Why saturation?
At first blush, you might find the saturation requirement for type families somewhat baffling. Why can’t we just partially apply type families as we can any other function? The answer ultimately stems from the way GHC’s type inference engine works, and since type families can be used at the type level, they must be able to co-exist with type inference.
This is better explained with an example, which I’ve adapted from the wonderful paper Higher-order Type-level Programming in Haskell. Consider the following definition:
f a ~ f b is an equality constraint, which informs GHC’s constraint
f a is the same type as
f b. In order for the body of
be well typed, GHC’s typechecker must be able to conclude that
a is the same
b. Fortunately, this is quite possible. GHC can take the
f a ~ f b
constraint and decompose it to obtain the simpler constraint
a ~ b, which
suffices to show that
b are the same.
f is just an ordinary type variable, so
d should still typecheck
regardless of whether we instantiate
f to be
Either Bool, or any
other type constructor of kind
Type -> Type. Question: what happens if we
try to instantiate
f to be a type family? In particular, consider the
following instantiation of
Should this work? After all,
ConstInt is of kind
Type -> Type,
ConstInt Char does in fact equal
ConstInt Bool (since both things
Int) so it seems like this is a valid instantiation. Yet
something has gone horribly wrong here. If we decompose
ConstInt Char ~ ConstInt Bool, we obtain
Char ~ Bool, which is completely
Fortunately, GHC ensures that such blatant unsafety can never occur by
f only ever be instantiated with well formed types. An
Maybe is well formed without any extra stipulations. Type
families, on the other hand, are only well formed if they are fully saturated.
As a consequence, one cannot instantiate
f to be
is only well formed when it is supplied with an argument. This restriction,
heavy-handed as it may be, makes decomposing equalities like
f a ~ f b always
Observant readers might wonder if they can subvert this saturation
check by instantiating
f to be something like
/\b. ConstInt b, where
is a hypothetical syntax for a type-level lambda. The answer is no: neither
the surface syntax nor GHC’s internals support such a construct.
The ins and outs of arity
Since saturation is such an important property to be aware of when using type families, let’s try to nail down what exactly the arity of a type family is. Here is a crude first attempt:
Definition 1: the arity of a type family is the number of arguments it accepts.
Can you see anything wrong with this definition? For starters, it’s not exactly clear what “arguments” means in this context. To illustrate this point, consider the following examples:
M1 define the same thing… well, almost. They both have kind
Type -> Type, which means that they can each be applied to a single
argument. They differ, however, in their respective arities.
M0 was defined without any parameters, which gives it arity 0, whereas
was defined with one parameter, which gives it arity 1. In other words,
can be partially applied, but
This leads us to an important realization: the kind of a type family doesn’t
tell you everything. In particular, there is a distinction between the
arguments that must be supplied in order to be fully saturate a type family,
and the arguments that can optionally be supplied after a type family is saturated.
For example, it is not strictly required to supply
an argument in order to be well formed, but for
M1, it is mandatory.
This information cannot be gleaned
from the kind of a type family alone, as arity is a syntactic property.
It may be informative to see
M1 written with explicit return kinds:
I’m somewhat fond of this syntax since it suggests a fairly decent intuition
for how to compute arity: simply count the number of parameters to the left of
the double-colon (
M1, one parameter appears to the left of the
::, whereas in
M0, no parameters appear to the left of the
Now that we’ve seen this, we can make a better attempt at defining arity:
Definition 2: the arity of a type family is the number of parameters that appear before the return kind in its definition.
Note that return kinds can either be explicit
type family Blah ... :: Type -> Type where ...)
or implicit (e.g.,
type family Blah ... where ...) depending on which style
you prefer. I’ll use both forms in various places later in the post.
Are returns kinds a cheat code?
We have just seen an example of how
type family M0 :: Type -> Type was
strictly more powerful with respect to partial application than
type family M1 (a :: Type) :: Type. It is tantalizing to think that the
trick of putting everything in the return kind can make every type family
partially applicable. For instance, one might try defining this:
If this worked, we could finally have a version
ConstInt that we could
partially apply. But GHC is privy to such hijinks and will complain if one
tries to define
ConstInt this way:
Blast. Because we didn’t define any parameters to the left of the return kind,
we are only permitted to define equations that use, well, zero parameters. In
other words, we can only write
ConstInt = ..., not
ConstInt b = ...,
ConstInt b1 b2 = ..., or something of a similar ilk.
Therefore, while stuffing more arguments into the return kind grants more power in terms of partial applicability, it also removes the power to define certain things in the equations of the type famiily. Be aware of this tradeoff when deciding what shape your type family should have.
Now that we’ve sampled a taste of what arity is about, it’s time to add some spice to our examples. In particular, all of the examples we’ve seen up to this point involve very simple kinds. Things really become interesting, however, when polymorphic kinds enter the picture.
Unsurprisingly, we’re going to be making heavy use of GHC’s
language extension from here on out. We’re also going to be using some other
language extensions we haven’t formally introduced yet, but I’ll bring them up
when the situation is appropriate.
A brief introduction to
Just as types can be polymorphic, so too can kinds be polymorphic. Here is
the “hello world” of kind polymorphism, the
a ranges over types,
k ranges over kinds. For example, here are
some particular instantiations of
Each of those examples instantiates
k in a different way. Note that unlike
the type argument for
a, which must be explicitly written by the programmer,
the kind argument
k is omitted, as it is inferred by the typechecker
automatically. While this saves the
programmer some effort, it can occasionally hide interesting details from view.
If you want to specify what
k gets instantiated to explicitly, then
TypeApplications extension lets you just that:
Note that the code above will only work on GHC 8.8 or later, as that is the
first version to support
TypeApplications syntax at the kind level.
PolyKinds and type families
One can also have poly-kinded arguments in type families, as this example demonstrates:
Similarly, one can also use
TypeApplications syntax to spell out what the
k is in each equation (again, this assumes GHC 8.8 or later):
The arity of poly-kinded type families
Question: what is the arity of
PK? This is a surprisingly tricky question to
answer, and it is one the main reasons why I set out to write this blog post.
As we’ve seen in previous examples, one can write type family equations for
PK with either one or two arguments, depending on whether
is used or not. As a result, it’s not exactly clear whether the arity of
is 1 or 2.
One thing we can say with certainty is that the arity is at least 1. That much is evident by the fact that GHC is content with this definition:
But it is not happy with this one:
We have seen this error message before when attempting to apply a type family
to a number of arguments less than its arity. In those situations, the
should have X argument(s)” has always happened to be the arity of the type
family in question. For now, let’s trust this assumption and operate under
the premise that
PK has arity 1.
Having seen that, what happens if we push the kind variable
k into the
return kind? You end up with something like this:
Since the argument of kind
k is now part of the return kind, we can no
longer match against it in any type family equations, so something like
PKRetKind Int = Char is now out of the realm of possibility. (As a
consequence, I’ve simply defined
PKRetKind without any equations.)
On the flip side,
we can partially apply
PKRetKind, so it would be quite permissible to
PK0 = PKRetKind. It seems like
PKRetKind has arity 0, so
again, let’s operate under this premise (at least, for the time being).
Just because you can’t see it doesn’t mean it’s not there
Hopefully you saw through my hand-waving in the previous section and realized
that something is amiss here. Recall that we were able to define
PK @Type Int = Char. When we spell out
@Type like this,
it suggests that
PK is actually accepting another argument besides
Indeed, from this perspective, it is not inaccurate to say that
PK accepts two arguments: one invisible (
k) argument and
one visible (
We don’t normally account for the invisible argument, since GHC usually figures
it out for us, but it is still there lurking behind the scenes. You
can draw it out of its hiding place with the
@ syntax, which is sometimes
referred to as a “visibility override”.
For example, consider what happens the following code:
If you follow the type synonyms, the type
Ex eventually reduces down to
PKRetKind (PKRetKind True), or
PKRetKind @Type (PKRetKind @Bool True)
with kind arguments spelled out. Even though
PKRetKind appeared to be used
without any arguments in
Ex, in actuality, GHC knew about the invisible
@Bool arguments well in advance. You could just have well written
And have achieved the same end result.
Breaking the ranks
Most of the time, the details of invisible arguments can be completely ignored, since they’re usually a bookkeeping detail that GHC’s type inference engine accounts for. But in the case of type family arities, I argue that invisible arguments are actually essential to keep in mind, as invisible arguments can be the difference between whether or not a type family is well formed or not.
To see what I mean, let’s consider this intriguing definition:
What is interesting about
HRK is that its argument has a
forall k. k -> Type. The explicit
forall at the
front (made possible with the
RankNTypes language extension) indicates that
f can only be instantiated with types that are sufficiently polymorphic in
k. For instance, one cannot instantiate
f to be
Maybe since the kind of
Type -> Type, is not polymorphic enough. It is a good thing that
this is the case, lest we end up with the nonsensical types
One example of something that we can instantiate
f with is
forall k. k -> Type. As we have seen earlier,
Proxy Maybe, and
Proxy True are all perfectly valid types, so this is a
fine thing to do.
On the other hand, something that we cannot instantiate
f with is
Proxy @Type. This is because the kind of
Proxy @Type is no longer
forall k. k -> Type, but rather
Type -> Type, which is not polymorphic
enough to be used in a higher-rank situation.
OK, time for a quiz. Can we instantiate
PKRetKind? It seems like
we ought to be able to do this, since the kind of
PKRetKind, which is also
forall k. k -> Type, appears to be polymorphic
enough to be
used in a higher-rank context. What happens if we try to use the type
HRK PKRetKind? We get this:
I was deeply surprised to discover that GHC rejected this when I tried it
for the first time. Moreover, the rather inscrutable error message didn’t
exactly make clear where I had gone wrong. What I didn’t realize at the time
was that the arity of
PKRetKind was actually the root cause.
Return kinds, revisited
Let’s take another look at the definition of
PKRetKind, this time with a
Earlier, I claimed that its kind was
forall k. k -> Type. But where did this
forall k quantifier come from? It’s certainly not written out in the return
kind, so that seems to indicate that the
k is being implicitly quantified somewhere.
My gut instinct was to think that I wasn’t being explicit enough. I tried
this seemingly-equivalent definition of
When I did this,
HRK PKRetKind' now worked without issue! This was great, but
something felt off about the whole thing. If the two formulations of
PKRetKind were equivalent, then why did only one of them work when
used as the argument to
Well, it turns out my original assumption was wrong: the two definitions actually
aren’t equivalent. That’s because the first version of
PKRetKind has a
secret power: one can match on
k in type family equations! That is to say,
it can support things like this:
Type, then the first equation is matched, which reduces to
Type -> Type); otherwise, it falls through to the second equation,
which reduces to
Proxy (of kind
k -> Type). However, this seems to fly in the face
of the earlier intuition we developed about type family arities, which states
that only things that appear to the left of the
:: contribute toward the
arity (and, as a result, are permitted to appear on the left-hand sides of
equations). How can these two facts be reconciled?
It’s kind of important
As it turns out,
k actually does appear to the left of the
can’t see it under most circumstances. To be more precise,
k is implicitly
quantified, not as a part of
the return kind, but as a parameter to
PKRetKind itself. You can see this
for yourself by using the
:info command in GHCi with the
-fprint-explicit-kinds flag enabled :
Now we’ve uncovered the truth behind
PKRetKind. There actually is an
invisible parameter to the left of
::, which is why the equations of
PKRetKind are able to match on it. More importantly, this led me to realize
HRK PKRetKind doesn’t work—
PKRetKind really has an arity of 1!
That is, while
PKRetKind may not have any visible parameters to the left
::, it does have one invisible parameter, and this actually
makes a difference when it comes to its arity. Our earlier guess that
PKRetKind has arity 0 was wrong, and in reality, it has arity 1.
In the earlier
Comp PKRetKind PKRetKind True example, it seemed as though we had
PKRetKind with zero arguments. But this isn’t strictly
true, since GHC was actually supplying invisible
arguments under the hood. In actuality, the types we had written were
Comp (PKRetKind @Type) (PKRetKind @Bool) True, which make those uses
PKRetKind fully saturated.
On the other hand, there is no way to interpret
HRK PKRetKind as a well
formed type. If GHC doesn’t supply
PKRetKind with any invisible arguments,
then it would fall afoul of the type family saturation check. On the other hand,
if GHC tries to insert an invisible argument to make it
HRK (PKRetKind @k0) (for some type
k0), then the kind of
HRK’s argument would be
k0 -> Type, which isn’t polymorphic enough to
be used in a higher-rank setting (note the absence of a
It turns out that in practice, GHC actually attempts the latter approach when
which is why the error message complains about
k0 -> Type instead of the
number of arguments.
If you want a poly-kinded, arity-0 type family, then the
position of the
forall ends up being extremely important. This formulation
PKRetKind truly has arity zero:
PKRetKind' has no parameters, implicit or explicit, to the left of the
This means that in terms of partial applicability,
PKRetKind' receives top
marks. But remember that while arity giveth, arity also taketh away. In
exchange for the ability to be partially applied in more contexts,
PKRetKind' loses the ability to match on
in its type family equations. As a consequence, a definition like this one
This is because
Maybe is of kind
Type -> Type, which is not polymorphic
enough for the expected return kind of
forall k. k -> Type. This might work
k could be matched against
Type, but since
k is not bound to the left
::, this cannot happen. The only valid equations that
could possibly have must have truly polymorphic right-hand sides, such
as in this example:
Putting it all together
We have seen first-hand how invisible kind arguments can have a major influence on the design considerations of a type family. In light of this, I think it is worth giving these invisible arguments a special mention in the definition of arity, as their presence (or absence) can affect whether GHC accepts or rejects a partial application of a type family:
Definition 3: the arity of a type family is the number of parameters that are bound before the return kind in its definition, either visibly (through a user-written type variable binder) or invisibly (through implicit quantification).
This definition of arity is certainly the wordiest, but I think it best
captures all of the subtleties at play here. With this definition in mind,
let’s recap once more all of the poly-kinded type families we have discussed
in this post, this time using
While the kind of each of these type families is
forall k. k -> Type, each
one has completely different behavior vis-à-vis arity. They represent
different points on a spectrum, with one end (arity 2) having the most freedom
to match on its arguments in equations and the other end (arity 0) having the
most flexibility to be partially applied.
Aside 2: Arities and kind inference
Most of the examples of poly-kinded type families I presented earlier in this post used explicit return kinds, which make it straightforward to figure out their arities. If a type family doesn’t have an explicit return kind, however, then the arity isn’t always so clear. Here is a particularly tricky example of this in action:
What is the arity of
MyProxy? We know that its kind is
forall k. k -> Type,
but as we’ve discovered, the arity depends on where
k is bound. There are
two reasonable guesses for where
k might be bound:
As it turns out, GHC will infer Guess A in practice. I’m not quite sure as to GHC’s rationale for this choice, but them’s the breaks. If you want the behavior of Guess B, you’ll simply have to write out an explicit return kind.
Aside 3: What about type synonyms?
I’ve restricted my focus in this blog post to type families, but much of what I’ve written also applies to type synonyms. Type synonyms, after all, can be thought of as a very special case of type families: they always have exactly one equation, they cannot match on their arguments, and they are not allowed to recursive.
Moreover, type synonyms also have a saturation requirement like
type families, which means that type synonyms also have arities. Here are
some examples of type synonyms, complete with their arities (I will use
-fprint-explicit-kinds syntax once more for poly-kinded definitions):
If I want to be really pedantic about my definition of arity, I need to pay mention to type synonyms. So here is my final attempt at defining arity (for real this time):
Definition 4: the arity of a type family or type synonym is the number of parameters that are either:
- Bound before the return kind in its definition (in the case of a type family), or
- Bound before the equals sign (in the case of a type synonym).
A parameter may either be bound visibly (through a user-written type variable binder) or invisibly (through implicit quantification).
Through a series of increasingly complex examples, we have seen how arity impacts the usability and power of type families. It was a somewhat long and winding path to get here, but I hope you learned a thing or two along the way.
If the saturation restriction makes you a bit squeamish, you’re not alone. There are others who have pondered ways to drop the saturation restriction altogether, which I’ll briefly mention below:
One way to “partially apply” type families in today’s GHC is through a technique called defunctionalization, which involves encoding type families (and partial applications thereof) as datatypes and “evaluating” them with a special-purpose type family. Defunctionalization requires quite a bit of boilerplate, but it does get the job done. Refer to the blog posts Defunctionalization for the win and Haskell with only one type family for two different approaches to defunctionalization.
Earlier in this post, I remarked that “the kind of a type family doesn’t tell you everything”. This fact proved annoying enough that it convinced multiple academics to develop alternative typing rules for type families.
Richard Eisenberg’s thesis
and the more recent paper
Higher-order Type-level Programming in Haskell
propose systems that, among other things, would enable partially applying any
type family, regardless of what its arity may be.
To preserve type soundess, the latter paper proposes a new
->> that corresponds to arguments that count towards arities
in today’s GHC. In other words, the arity of a type family is now just a property
of its kind.
Here are some examples of type families, along with their kinds , to demonstrate the idea:
Since the saturation requirement is not present in their
system, the arity of a type family is no longer that interesting. Instead,
the main purpose of
->> is to guide type inference. For example, this program,
which uses the normal
-> function arrow in the kind of
f, is valid:
-> is swapped out for
d will no longer typecheck,
f could be instantiated with something like
which would be unsound.
There’s much more than can be said about this new
->> arrow, but that’s
beyond the scope of this post. Hopefully, a system like this will one day
make all type families partially applicable like they were meant to be.
I recommend using
-fprint-explicit-kindson GHC 8.8 or later, since it displays invisible arguments using
@syntax. You could use earlier versions of GHC if you wish, but it renders invisible arguments without
@syntax, so you’ll have to discern for yourself which arguments were originally visible to start with and which ones were not. ↩