I just returned from yet another fantastic ICFP week. I always have a blast at the conference. It would be easy to take the conversations I had there and turn them into a full-blown research program that would easily take me to next year’s ICFP… and then rinse and repeat!

But in this post, I want to focus on one particlar thorn in my side that started bothering me more than it had before: type families. I’ve realized, in the course of many conversations, that I don’t really understand them. This post will be more questions than answers as I try to write down what ails me.

This post is Literate Haskell.

```
> {-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances, GADTs,
> MultiParamTypeClasses, FunctionalDependencies,
> FlexibleInstances, FlexibleContexts #-}
> module WhatAreTypeFamilies where
```

## Total type families are OK

A total type family feels quite comfortable. By *total* here, I mean a type family whose equations cover all the possible cases and which is guaranteed to terminate. That is, a total type family is properly a function on types. Those other dependently typed languages have functions on types, and they seem to work nicely. I am completely unbothered by total type families.

## Non-covering type families are strange

A *non-covering* type family is a type family whose patterns do not cover the whole space. Let’s consider closed and open families separately, because the issues that come up are different.

### Closed type families

For example:

```
> type family F1 a where
> F1 Int = Bool
```

Note that `F1`

is closed – we won’t ever be adding more equations. `F1`

is clearly non-covering. Yet, the type `F1 Char`

is perfectly well formed.

```
> sillyId :: F1 Char -> F1 Char
> sillyId x = x
```

But `sillyId`

can’t ever be called on a value. This doesn’t stop us from doing chicanery with `F1`

though.

```
> data SillyGadt a where
> MkSillyGadt1 :: Int -> SillyGadt (F1 Char)
> MkSillyGadt2 :: Float -> SillyGadt (F1 Double)
```

Now, even though `F1 Char`

is nonsense, `SillyGadt (F1 Char)`

is inhabited. And GHC distinguishes between `F1 Char`

and `F1 Double`

.

In GHC, a type family that can’t reduce is considered “stuck”. Such a type is effectively a new type, equal only to itself, like empty datatypes a programmer might declare. The only thing different about something like `F1 Char`

from something like `Maybe Char`

is that `F1 Char`

cannot be used in a type pattern (that is, the left-hand side of a type family equation or data family instance). That’s the only difference. So, when we declare `F1`

, we create an infinite family of unique types containing `F1`

applied to all types of kind `*`

, **except for Int**, because

`F1 Int`

is identically `Bool`

.I find this treatment of non-covering closed type families rather bizarre. Compare against term-level behavior. When a term-level function is non-covering, passing an argument for which there are no equations immediately results in a call to `error`

. Yet the same thing in types behaves very differently.

I’m not the only one who finds this strange: Lennart Augustsson posted GHC bug #9636 about this very issue. Indeed, my current views on the subject are strongly influenced by Lennart’s comments.

#### But, sometimes you want stuckness

Sadly, sometimes authors want stuck type families. I know of two examples.

- The bowels of GHC defines this:
`type family Any :: k where {}`

Thus,

`Any`

is a closed type family, available at any kind, with no equations. GHC makes convenient use for`Any`

. Consider the expression`length []`

. This expression has some pointless polymorphism in it:`length`

can be applied to a list of any type, and`[]`

can be a list of any type. Yet, GHC must choose precisely which type these polymorphic definitions are specialized to. Not to play favorites, GHC chooses`Any :: *`

. Such pointless polymorphism can indeed happen at any kind, so`Any`

is polymorphic in its return kind. (Before kind polymorphism,`Any`

existed as a special form. It’s not so special any more.)It’s quite important that

`Any`

is a type family, not a datatype. If it were a datatype (and we forget about the weirdness of a datatype polymorphic in its return kind), then it could be matched in type patterns, making this strangeness possible:`type family ThreeBools (b :: Bool) :: Nat where ThreeBools 'True = 1 ThreeBools 'False = 2 ThreeBools Any = 3`

Bizarre! And yet this was possible in GHC 7.6 and below (modulo the closed type family, which didn’t exist yet). And it caused problems.

Of course, with

`Any`

, we really want it to be stuck. We don’t want`Any`

to reduce to some other type, and we don’t want uses of`Any`

to be errors. - In his work implementing a units-of-measure library via type-checker plugins, Adam Gundry uses closed type families to define type functions whose behavior is specified only via a plugin, not by GHC’s built-in type family reduction rules. He wanted
*empty*closed type families specifically, and so implemented them within GHC. The idea is that units-of-measure with their integer powers form an abelian group, which can be solved via custom machinery but not by GHC’s rather limited left-to-right rewriting used in type family reduction.Once again, we want a closed type family that is stuck but is not an error. The existence of multiple such things got me ruminating on all of this some time ago. I attempted to figure this all out in a post on a GHC ticket, but that didn’t get me very far. And I won’t claim to have made any real progress since that post.

### Open type families

Having a stuck open type family makes moderately more sense than a stuck closed type family. Suppose we have this:

```
> type family F2 a
> type instance F2 Int = Bool
```

Because new equations can be added to open type families at any time, talking about `F2 Char`

isn’t utterly bogus. But it might be nice to have to assert that an equation for `F2 Char`

is in scope before we use it in a type.

### Injective type families

Injective type families are a new feature that just got merged with GHC head. Jan Stolarek, Simon Peyton Jones, and I had a paper at Haskell Symposium about them.

The idea is that you can put an injectivity annotation on a type family declaration, which is rather like a functional dependency. (The injective type family code in this post is not runnable, as it works only with GHC HEAD. The feature will be available with GHC 8.0, due out early 2016.)

```
type family F3 a = r | r -> a where
F3 Int = Bool
F3 Bool = Int
F3 a = a
```

Note that if you know the value of `F3 a`

, then you can discover the value of `a`

: that’s what injectivity is all about.

Now consider this:

```
type family F4 a = r | r -> a where
F4 (Maybe a) = a
```

Looks injective, right? Wrong. The problem is that, if this were injective, we could take a proof that `F4 a ~ F4 b`

and get a proof of `a ~ b`

. Now, consider `F4 (Maybe (F4 Int))`

. This reduces to `F4 Int`

. Thus, we have `F4 (Maybe (F4 Int)) ~ F4 Int`

. And now, by injectivity, we get `Maybe (F4 Int) ~ Int`

. That is, a `Maybe <blah>`

equals an `Int`

. Terrible!

So, in our implementation of injectivity, we exclude type families like `F4`

. But it’s really unexpected that `F4`

should be rejected (at least to me). The problem, at its core, is about partiality. Note that we needed `F4 Int`

– an un-covered case – to make the bad equality proof.

## Looping type families are strange

At first blush, it seems that a looping type families cause chiefly one problem: a looping GHC. But I’m very unconcerned about a looping GHC. After all, if a user has written a non-terminating type family, that amounts to a non-terminating program to be run at compile time. No one should be very surprised when a program that contains a loop does, in fact, loop.

The problem is that looping type families can actually create effectively infinite types. GHC has various protections against actually running off to infinity, but a clever programmer can defeat these protections. And infinite types can cause unsoundness. Indeed, while writing the closed type family paper, we uncovered one such unsoundness, closing bug #8162.

However, even with #8162 gone, we still have a lingering problem. Consider

```
> type family F5 a b where
> F5 a a = 'True
> F5 a b = 'False
```

This is a straightforward equality test, and it works in many cases. But if we ask `F5 a (Maybe a)`

(for some unknown `a`

), the type family doesn’t reduce. It really should! There is no way a finite `a`

can be the same as `Maybe a`

. But we can have an *infinite* `a`

, instantiated to `MaybeInf`

:

```
> type family MaybeInf where MaybeInf = Maybe MaybeInf
```

`MaybeInf`

here is a perfectly well-formed nullary (0-argument) type family. If the `a`

in `F5 a (Maybe a)`

were instantiated with `MaybeInf`

, then reducing to `'True`

would be correct. And thus GHC can’t reduce `F5 a (Maybe a)`

to `'False`

, as one might like.

And this isn’t purely an academic concern. I don’t have links I can share, but this has bitten real programmers doing real work. Once again, the problem boils down to partiality: GHC must be conservative about reducing closed type families (such as `F5`

) because of the possibility that someone, somewhere will write a non-terminating type family. If `F5 a (Maybe a)`

were to reduce to `'False`

, I’m confident that a clever enough person could use this behavior to implement `unsafeCoerce`

. Similar concerns prevent certain type families from being considered injective – see the paper for the example. If we could somehow be sure that there were no non-terminating type families, these concerns would go away.

## Contrast with functional dependencies

Simply, functional dependencies don’t suffer from these problems. Let’s look at the issue around injectivity, as it’s representative. First, recast in terms of functional dependencies:

```
> class F4' a r | a -> r, r -> a
> instance F4' (Maybe a) a
```

Note the bidirectional functional dependency. The left-to-right dependency is the built-in dependency inherent in type families. The right-to-left dependency arises from the injectivity annotation.

Our problem case above was `F4 (Maybe (F4 Int))`

. This case maps to

```
fundep :: (F4' Int f4_int, F4' (Maybe f4_int) result) => ()
fundep = ()
```

GHC helpfully tells us

```
Couldn't match type ‘Maybe f4_int’ with ‘Int’
arising from a functional dependency between:
constraint ‘F4' Int f4_int’
arising from the type signature for
fundep :: (F4' Int f4_int, F4' (Maybe f4_int) result) => Int
instance ‘F4' (Maybe a) a’
```

So GHC notices that there is a problem. But even if it didn’t, we’d be OK. That’s because the `F4' Int f4_int`

constraint essentially asserts that there is *some* value for `F4' Int`

. Of course, there isn’t any such value, and so `fundep`

would never be callable. Indeed, we can’t write any more instances of `F4'`

, as anything we could write would violate the dependencies.

The bottom line here is that there is no way to get into trouble here because the constraints necessary to use bogus functional dependencies can never be satisfied.

## A radical proposal

So, what should we do about all of this? I’m inspired by the non-problems with functional dependencies. I thus propose the following. (Actually, I don’t. This is too radical. But I’m trying to provoke discussion. So take this all with a heap of salt.)

- Remove unassociated open type families. They’re quite awkward anyway – either they should be closed and define some sort of concrete function, or they will need a class constraint nearby to be useful.
- Require class constraints to use associated type families. That is, if
`F a`

is associated with a class`C a`

, writing`F Int`

without a`C Int`

constraint in scope is an error. This means that the use of an associated type family in the right-hand side of another associated type family will require the class constraint in the instance context. - Require closed type families to be total, with an improved termination checker. Naturally, closed type families would be unable to call partial type families.
- Devise a mechanism to associate a closed type family with a class. This would allow for partial closed type families, which indeed are useful.

The bottom line to all of this is that any partial type family should be associated with a class constraint. If the constraint can be satisfied, this means that the type family is defined and well-behaved at the arguments provided. With this, I believe all the problems above go away.

Another way to see this proposal is that functional dependencies are the Right Way to do this, and type families (at least partial ones) are wonky. But type families have much better syntax, and I’d like to keep that.

So, where to go from here? I’m not sure. This proposal is pretty radical, but it could potentially be implemented with the requisite deprecation period, etc. But, mostly, I’m curious to see what conversation this all provokes.

Derek ElkinsI added a comment to #9636, https://ghc.haskell.org/trac/ghc/ticket/9636#comment:26

First, I’m happy to see some love going FunDeps’ way. This suggests that one could reformulate type families as a source-to-source translation into MPTCs and FunDeps and then find where the translation goes awry.

One thing I briefly suggested in the Trac comment is considering the codes of types. I.e. we have a (normal) data type Code of codes for data types, which will typically be just a tree of some sort, and a decode function that goes from Code -> *. You can model this with a Haskell data type and a total closed type family, but it’s probably better to do this in Agda (or Coq or whatever). At any rate, the semantics people want for type families, is that they are type level functions. This is trivial with Code and decode. Our decode function just interprets the type family constructor as a function. However, this must be a total function (i.e. covers all cases and is terminating). Indeed, when the type family is a total function, there are no issues.

So, for type families that would be non-terminating as functions, they should just be disallowed. If for convenience the termination check could be disabled, the compiler would be obligated to actually normalize terms to maintain soundness. In this case, the compiler is justified ignoring infinite terms: either they don’t exist or the compiler will go into a loop before it could actually use them. This should justify F5 working the way you want (albeit only if a termination check is done or types are normalized, which I don’t think GHC does either with UndecidableInstances, so it’s NOT justified in that case).

The other case is incomplete definitions. In the comment I made sounds about uninterpreted functions. Well, decode is exactly an interpretation of such functions, so what interpretation do we provide for something that explicitly has no interpretation? We allow any interpretation. I.e. for F4 we put a big forall cF4 :: * -> * around our entire program and we add a default case to make the F4 type family total.

type family F4 a = r | r -> a where

F4 (Maybe a) = a

F4 a = cF4 a

When we skolemize, we get exactly the desired uninterpreted functions. Any is exactly a skolem constant and this explains why it serves its purpose well. In terms of decode, this just means it’s parameterized by a *-valued function for each incomplete type family. In terms of the programmer’s view of code, we have to write as if F4 Int could be anything. In particular, it could be Void, so we can’t do anything with it, but it also could be F4 (Maybe B) for some B.

This makes it quite clear why injectivity fails for F4. It’s also obvious from the completed F4 that it is not injective.

Derek ElkinsSo applying the above framework to your questions a little more explicitly. Non-covering type families don’t strike me as particularly strange and their usefulness in the examples you gave seems pretty clear. Essentially, when you make a non-covering type family you aren’t saying that it is defined for some inputs and undefined for others (and thus a type error), you are saying it’s defined for some inputs and you don’t know or care what it is for other inputs. So, an infinite family of codes is generated, but they still get mapped to “normal” types. However, if a compiler plugin happens to introduce some types not expressible with the codes, it is free to map those families to those new types. (* can be bigger than what we can write as type which is why we can’t pattern match on it).

Using this framework, the looping case suggests that the type Code is coinductive (or worse…) which makes decode very awkward. In particular, it is no longer a fold over the codes, i.e. it’s no longer compositional. It changes the whole game. (And at the very least, F5, which you call Equality in your paper, should be called something like Bisimilar.) The natural thing this suggests is making a metatheory where you make coinductive rules about the observations you can make from *. Stretching (maybe?), it’s possible Computational Type Theory is of this form (it’s * is essentially Bohm trees in typical realizations). It’s relatively normal presentation is an inductive characterizations of the experiments that can be done against * in the same spirit as the Take Lemma for streams. I’ll need to do a lot more work to see if this works out. At any rate, all this is to say that I think looping type families really are strange.

Richard EisenbergPost authorI really don’t want * (or Code) to be coinductive. It *should* be finite. Otherwise, we encounter the host of problems you describe here. Which is why I want a better termination checker.

Perhaps one solid way forward is this: improve the termination checker so that you don’t have to disable it for, say, standard Peano multiplication. Then, when it’s disabled, force normalization. That would go a long way, I think.

It does open the question, though, of whether/when we do want coinductive datakinds.

Richard EisenbergPost authorWow — lots to think about here. Thanks!

Re UndecidableInstances: You’re right. With UndecidableInstances on, GHC does not normalize types (this is no different to NoUndecidableInstances). This is seen as an optimization: if we’re trying to prove (F Int ~ F Int), it seems (at first) awfully silly to have to reduce F Int to normal form. But I agree with you that if we staunchly required normalization (with UndecidableInstances), then (F5 a (Maybe a)) could really reduce to False.

Re non-covering functions: When writing the injectivity paper, I started thinking along the lines that you describe here, about adding a closing case. But I didn’t quite figure out what the RHS should be. Perhaps you’re right here, about quantifying over some unknown function. But I don’t see how your argument extends to open type families: the F4 example above is closed, but the same exact problem arises when it is open.

Derek ElkinsI completely agree that we want Code to be inductive.

Can you elaborate on why you don’t think this argument extends to open type families? I’m not sure if it does or not either, but there doesn’t seem to be a big difference from this perspective between open and closed type families assuming you have the “whole program” in front of you. Or is the problem how to handle separate compilation?

Changing topic, one aspect about this interpretation is that I’m essentially saying GHC would add a type family to Code in the same way it would add the type constructor of any data type, the difference would be in the branch of the definition of decode that was added. GHC, knowing that, e.g, decode (T Int) = decode Bool could soundly use equations of the form T Int = Bool, but there’s nothing about Code that implies that. It’s only because GHC is defining decode that it knows that the equation is sound (in a model theoretic sense). One way to enforce this would be to quotient Code by the relation T Int ~ Bool. Then decode would be forced to have decode (T Int) ~ decode Bool. GHC would also be justified at the syntactic level making use of the equation T Int = Bool. There are some maybe insurmountable problems with this view. The first is that the quotiented Code type is probably not inductive. Indeed, what stops us from quotienting by MaybeInf ~ Maybe MaybeInf? I suspect it is possible to separate “good” equations from “bad” ones not just pragmatically but from a principled perspective. (One possible definition of what makes a “good” equation good is that the quotient with respect to it is a subobject of the original type.)

Another possible direction is to interpret the quotient as a higher inductive type a la homotopy type theory. This doesn’t actually solve any of the problems above except possibly by recasting them as not problems. It comes with its own potential issues. The main one is that the images of equations would be isomorphisms not (necessarily) equalities. We would get only that T Int is isomorphic to Bool. GHC would also have to witness equalities, but I think this is what System Fc is already doing. I don’t think GHC is forced to do anything weird in this approach though, so, since GHC is still defining the decode function it is free to make choices where all the isomorphisms are identities. This can justify not having to work as hard with the equality witnesses.

wren romano (@wrengr)As for your modest proposal at the end:

1. The main use for unassociated open type families is when we have a collection of type classes which are all related in that they discuss some particular TF, but where none of the classes can really be considered the “most primitive” class, or the “origin” for the TF itself. This is a pretty rare case, though I wouldn’t be surprised if it actually comes up in a few places. Though I do wonder if we have any good examples out there in the wild? If not, I’d be all for breaking unassociated open type families off into their own special language pragma, which we could maybe deprecate later on.

2. Hmm. Would it be possible to do this internally but without exposing the change at the source-code level? I guess it’d lead to unexpected performance regressions in cases where people don’t realize they’re closing over a type class instance…

3. I’m all for requiring termination, since the current logic of types only makes sense for finitely-large type expressions/codes so the presence of nontermination can’t really do anything desirable. However, as we keep pushing more and more on the syntax of what functions can be defined by TFs we’re going to quickly get into the position where we have a function which is in fact terminating but which the type-checker can’t determine is terminating. This is unavoidable. Thus, we should always allow the escape hatch of UndecidableInstances, throwing up our hands if it doesn’t actually terminate.

However, I’m not a fan of requiring coverage. When we think of TFs as functions it’s natural to expect those functions to have types (i.e., kinds for the inputs and outputs). However, we very often want to discuss subkinds of * (or of other standard kinds). Every non-covering TF is a covering TF on some subkind, and I’d much rather avoid needing to design codes for naming those subkinds. The trick then is how we can effectively behave as if we have all possible subkinds without actually dipping into the machinery of full-blown subtyping.

4. Same comment as for #2.

JanekI’m trying to contrast proposals from this blog post (“Let’s express TFs with TCs+FDs”) with approach presented in this year’s Haskell Symposium paper “Type Families with Class, Type Classes with Family”, Serrano et al. (“Let’s express TCs+FDs with TFs”).

Firstly, I’m not entirely sure what is Serrano’s motivation (other than an exploration of design space). Section 4 shows several features that can be easily added to TCs if we encode them using TFs: non-membership (prevent a type from becoming a member of a class), closed instances, disjointness and instance chains. At ICFP 2014 Alejandro Serrano Mena presented a poster that proposed extending TCs with these features, but when I later asked him about it in private correspondence he said:

“They seem like nice ideas for the type system, but on the ICFP SRC quite some other issues were raised with translation into System FC and so on. Thus, I didn’t get to the point of implementing them in UHC”

So perhaps these features are easy to add if we encode TCs using TFs but are very hard to add to “normal” TCs? But that question is hard to answer without actually knowing what were the issues with System FC translation.

Secondly, section 7.1 of Serrano’s paper says:

“(…) why is our choice any better?

The answer lies in the use of instance improvement by functional

dependencies, as discussed in 3.2. This type of improvement makes

type inference brittle: it depends on the compiler proving that only

one instance is available for some case, which can be influenced by

the addition of another, not related, instance for a class.”

Section 3.2 is about functional dependencies and encoding them with injectivity. (BTW: their encoding of TCs with functional dependencies using injective TFs is a compelling use case for generalized injectivity.) If I understand correctly they are saying that FDs are bad because adding a new instance to a type class can violate that FD. But the same holds true for injective type families: adding a new equation can violate injectivity. What am I missing?

I don’t think that approach presented in “Type Families with Class…” addresses any of the problems that you raised here. But it seems to follow the same direction that your proposals: unify TFs and TCs into a single, uniform mechanism.

ØrjanFor what it’s worth, the new and safer (knock on wood) design for `Data.Constraint.Forall` in the `constraints` package uses stuck type families as skolems. Ideally I’d have made them closed, too (not that it matters much since they’re unexported).

Pingback: Dependent Types | Thirty years tapping a keyboard