What are type families?

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.

  1. 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.

  2. 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.)

  1. 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.
  2. 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.
  3. Require closed type families to be total, with an improved termination checker. Naturally, closed type families would be unable to call partial type families.
  4. 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.

Advertisements

8 thoughts on “What are type families?

  1. Derek Elkins

    I 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.

    Reply
    1. Derek Elkins

      So 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.

      Reply
      1. Richard Eisenberg Post author

        I 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.

    2. Richard Eisenberg Post author

      Wow — 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.

      Reply
      1. Derek Elkins

        I 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.

  2. 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.

    Reply
  3. Janek

    I’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.

    Reply
  4. Ørjan

    For 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).

    Reply

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s