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

``````> {-# 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
``````

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 = ()``````

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

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.

# Coincident Overlap in Type Families

Haskell allows what I will call coincident overlap among type family instances. Coincident overlap occurs when two (or more) type family instances might be applicable to a given type family usage site, but they would evaluate to the same right-hand side. This post, inspired by Andy Adams-Moran’s comment to an earlier blog post, explores coincident overlap and how to extend it (or not!) to branched instances.

This post is a literate Haskell file (though there really isn’t that much code). Paste it into a .lhs file and load it into GHCi. Because the post uses branched instances, you will need the HEAD version of GHC. (Branched instances will be included in GHC 7.8, but not before.)

``````> {-# LANGUAGE TypeFamilies, DataKinds, GADTs, TypeOperators #-}
``````

Our examples will be over `Bool`s, and we need some way to get GHC to evaluate our type families. The easiest way is to use the following singleton GADT:

``````> data SBool :: Bool -> * where
>   SFalse :: SBool False
>   STrue  :: SBool True
``````

## Conflict checking with type family instances

When compiling type family instances, GHC checks the instances for conflicts. To know if two instances conflict (i.e., could both match the same usage site), GHC unifies the two left-hand sides. For example, the following code is bad and is rejected:

``````type family F x
type instance F Int = Bool
type instance F a   = Double``````

Compiling the above instances gives the following error message:

``````Conflicting family instance declarations:
F Int -- Defined at ...
F a -- Defined at ...``````

This check is a good thing, because otherwise it would be possible to equate two incompatible types, such as `Int` and `Bool`.

## Coincident overlap among unbranched instances

Here is a nice example of how coincident overlap is useful:

``````> type family (x :: Bool) && (y :: Bool) :: Bool
> type instance False && a     = False   -- 1
> type instance True  && b     = b       -- 2
> type instance c     && False = False   -- 3
> type instance d     && True  = d       -- 4
``````

Although the first two equations fully define the `&&` operation, the last two instances allow GHC to reduce a use of `&&` that could not otherwise be reducible. For example:

``````> and1 :: SBool a -> SBool (True && a)
> and1 x = x
>
> and2 :: SBool a -> SBool (a && True)
> and2 x = x
``````

`and1` uses the second instance of `&&`, but `and2` requires the fourth instance. If we comment that instance out, `and2` fails to compile, because GHC cannot figure out that `a && True` must be `a` for all values of `a`. For various good reasons, perhaps to be explored in another post, GHC does not do case analysis on types during type inference.

How does GHC know that overlap is coincident? During the conflict check, GHC looks for a substitution that unifies two potentially-conflicting instances. In our case, the fourth and first instances would conflict under the substitution `{a |-> True, d |-> False}`. However, after finding the unifying substitution, GHC checks the right-hand sides under that same substitution. If they are the same, then GHC considers the overlap to be coincident and allows the instance pair. In our case, applies the substitution `{a |-> True, d |-> False}` to `False` and `d` and discovers that both are `False`, and so the instances are allowed.

## Coincident overlap within branched instances

When thinking about branched instances and coincident overlap, there are two possibilities to consider: coincident overlap within a branched instance and coincident overlap among two separate branched instances. Let’s consider the first case here.

Imagine we define `||` analogously to `&&`, but using one branched instance:

``````> type family (x :: Bool) || (y :: Bool) :: Bool
> type instance where
>   False || a     = a     -- 1
>   True  || b     = True  -- 2
>   c     || False = c     -- 3
>   d     || True  = True  -- 4
``````

Now, let’s consider simplifying the type `e || False`. The first two branches don’t match, but the third does. Now, following the rule for branched instance simplification (as stated in the Haskell wiki), we check to see if any previous branches might be applicable to `e || False`, for any possible instantiation of `e`. The first branch certainly might apply, and so `e || False` fails to simplify. This is surely counterintuitive, because the third branch matches `e || False` exactly!

Just to prove this behavior, I tried running this code through GHC:

``````bar :: SBool a -> SBool (a || False)
bar x = x``````

Here is the error:

``Couldn't match type ‛a’ with ‛a || 'False’``

At first blush, it seems I’ve missed something important here in the implementation — allowing coincident overlap within a branched instance. But, there is a major problem with such overlap in this setting. Let’s think about how coincident overlap would work in this setting. After selecting the third branch to simplify `e || False` (with the substitution `{c |-> e}`), GHC checks to see if any previous branch could be applicable to `e || False`. The first branch, `False || a`, unifies with `e || False`, so it might be applicable later on. The unifying substitution is `{a |-> False, e |-> False}`. Now, if we wanted to check for coincident overlap, we would apply both substitutions (`{c |-> e}` and `{a |-> False, e |-> False}`) to the right-hand sides. In this case, we would see that both right-hand sides would become `False`, and it seems we should allow the simplification of `e || False` to `e`.

Let’s try a harder case. What if we want to simplify `(G f) || False`, for some type family `G`? The third branch matches, with the substitution `{c |-> G f}`. Now, we check earlier branches for applicability. The first branch is potentially applicable, if `G f` simplifies to `False`. But, we can’t produce a substitution over type variables to witness to check right-hand sides. In this case, it wouldn’t be hard to imagine a substitution like `{(G f) |-> False}`, but that’s a slippery slope to slide down. What if `f` appears multiple times in the type, perhaps under different type family applications? How do we deal with this? There may well be an answer, but it would be subtle and likely quite fragile from the programmer’s point of view. So, we decided to ignore the possibility of coincident overlap within a branch. We were unable to come up with a compelling example of why anyone would want this feature, it seemed hard to get right, and we can just write `||` using separate instances, anyway.

## Coincident overlap between branched instances

Consider the following (contrived) example:

``````type family F (x :: Bool) (y :: Bool) :: *
type instance where
F False True = Int
F a     a    = Int
F b     c    = Bool
type instance F d True = Int``````

I believe that this set of instances wouldn’t produce any conflicts. Anything that matches `F d True` would have to match one of the first two branches of the branched instance, meaning that the right-hand sides coincide. However, it is difficult to reason about such cases, for human and GHC alike. So, for the sake of simplicity, we also forbid coincident overlap whenever even one instance is branched. This means that

``type instance F Int = Bool``

and

``type instance where F Int = Bool``

are very subtly different.

This post was partially inspired by Andy Adams-Moran’s comment in which Andy poses this example, paraphrased slightly:

``````> data T a
> type family Equiv x y :: Bool
> type instance where
>    Equiv a      a     = True        -- 1
>    Equiv (T b)  (T c) = True        -- 2
>    Equiv (t d)  (t e) = Equiv d e   -- 3
>    Equiv f      g     = False       -- 4
``````

Alas, this does not work as well as one would like. The problem is that we cannot simplify, say, `Equiv (T a) (T b)` to `True`, because this matches the second branch but might later match the first branch. Simplifying this use would require coincident overlap checking within branched instances. We could move the first branch to the third position, and that would help, but not solve the problem. With that change, `Equiv x x` would not simplify, until the head of `x` were known.

So, is this the “compelling example” we were looking for? Perhaps. Andy, why do you want this? Can your use case be achieved with other means? Do you (anyone out there) have a suggestion for how to deal with coincident overlap within branched instances in a simple, easy-to-explain manner?

# Defunctionalization for the win

I enjoy using a type system to help make sure my term level code is unimpeachably correct. This is where my interest in writing the `singletons` library came from. This library allows you to write some dependently typed code in Haskell, using singleton types. I didn’t invent this idea, but I did write a nice library to remove some of the pain of using this encoding. SHE can be considered an ancestor of `singletons`.

At my Haskell Symposium (2012) presentation of the singletons work, an attendee asked if singleton generation works for higher-order functions, like `map`. I innocently answered “yes”, at which point Conor McBride, sitting in the back, stood up and said “I don’t believe you!” I wasn’t lying — `singletons` does indeed handle higher-order functions. However, Conor’s skepticism isn’t unfounded: a “singletonized” higher-order function isn’t so useful.

This blog post explores why singletonized higher-order functions aren’t useful and suggests defunctionalization as a way to fix the problem.

Before we get too much further, this blog post is a literate Haskell file, so we have some necessary throat-clearing:

``````> {-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, TypeFamilies,
>              GADTs, FlexibleContexts, RankNTypes, TypeOperators #-}
> import Prelude hiding (map)
> import Data.Singletons
``````

I should also warn that some of the code rendered as Haskell in this blog post does not have bird-tracks. This code is not intended as part of the executable code. I should finally note that this code does not compile with the current HEAD of GHC (but it does compile with 7.6.1, at least). The new ambiguity check overzealously flags some of the code here as inherently ambiguous, which it is not. I have filed bug report #7804.

## Introduction to singletons

First off, what is a singleton? I will give a brief introduction here, but I refer you to the singletons paper on the subject. A singleton is a type with exactly one value. Let’s make a singleton for the natural numbers:

``````> data Nat = Zero | Succ Nat
> \$(genSingletons [''Nat])
``````

The second line above generates the following singleton definition for `Nat`:

``````data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)``````

(Well, it doesn’t quite generate that, but let’s pretend it does. See the paper [or use `-ddump-splices`!] for more details.) According to this definition, there is exactly one value for every `SNat n`. For example, the type `SNat (Succ Zero)` has one value: `SSucc SZero`. This is interesting because it means that once we identify a value, say in a `case` expression, we also know a type index. This interplay between term-level matching and type-level information is what makes singletons enable something like dependently typed programming.

The `singletons` library provides a singleton for `[]`, but with alphanumeric names. We can pretend this is the definition:

``````data SList :: [k] -> * where
SNil  :: SList '[]
SCons :: Sing h -> SList t -> SList (h ': t)``````

The `Sing` in there (the first parameter to `SCons`) is defined thus:

``data family Sing (a :: k)``

Using a data family allows GHC to choose the correct singleton type, depending on the kind `k`. An instance of this family is defined for every singleton type we create. So, actually, the list type built into the `singletons` library is more like

``````data instance Sing (list :: [k]) where
SNil  :: Sing '[]
SCons :: Sing h -> Sing t -> Sing (h ': t)``````

The `singletons` library also provides a synonym `SList` to refer to this instance of the `Sing` family. Again, you may find more clarity in the singletons paper, which spends a little more time drawing all of this out.

## Singleton first-order functions

We can singletonize more than just datatypes. We can singletonize functions. Consider the following predecessor function on `Nat`s, defined in such a way that we get the singleton definition generated for us:

``````> \$(singletons [d|
>   pred :: Nat -> Nat
>   pred Zero     = Zero
>   pred (Succ n) = n
>   |])
``````

A definition of `pred` that works on singleton `Nat`s is generated for us. It looks something like

``````sPred :: SNat n -> SNat ???
sPred SZero     = SZero
sPred (SSucc n) = n``````

The problem is those pesky `???` marks. Because the type indices of a singleton mirror the computation of singleton values, every function on singletons must be mirrored at the type level. So, to define `sPred`, we must have the type family `Pred` as well:

``````type family Pred (n :: Nat) :: Nat
type instance Pred Zero     = Zero
type instance Pred (Succ n) = n

sPred :: SNat n -> SNat (Pred n)
...``````

The `singletons` library generates both the type-level `Pred` and the singletonized `sPred`.

## Singleton higher-order functions

But what about `map`?

``````> \$(singletons [d|
>   map :: (a -> b) -> [a] -> [b]
>   map _ []      = []
>   map f (h : t) = f h : map f t
>   |])
``````

The `singletons` library generates these definitions (but with some extra class constraints that don’t concern us):

``````type family Map (f :: k1 -> k2) (list :: [k1]) :: [k2]
type instance Map f '[]      = '[]
type instance Map f (h ': t) = ((f h) ': (Map f t)

sMap :: (forall a. Sing a -> Sing (f a)) -> Sing list -> Sing (Map f list)
sMap _ SNil        = SNil
sMap f (SCons h t) = SCons (f h) (sMap f t)``````

Whoa! What’s the bizarre type doing in `sMap`? The `forall` declares that the function passed into `sMap` must be valid for any `a`. That’s not so strange, when we think about the fact the index `a` must be isomorphic to the term `Sing a`. We’re used to having functions that work for any term. Here, because of the relationship between term values and type indices, the function must also work for any type index `a`. This is particularly important, because `Map` will apply `f` to all the `a`s in the list `list`. If we leave off the `forall`, the function won’t type check.

This is all well and good, but this definition of `sMap` isn’t useful. This is because the type of that first parameter is quite restrictive. We must have a function of that type, and `f` must be inferrable. Let’s look at some examples. We can write the following just fine:

``````> sOne   = SSucc SZero
> sTwo   = SSucc sOne
> sThree = SSucc sTwo
> sNums  = SCons sOne \$ SCons sTwo \$ SCons sThree SNil -- [1,2,3]
>
> two_three_four = sMap sSucc sNums
``````

(`sSucc` is a so-called “smart” constructor. It is equivalent to `SSucc`, but adds extra class constraints that don’t concern us here. See Section 3.1 of the singletons paper.) The type of `SSucc` is `forall a. Sing a -> Sing (Succ a)`, so the call to `sMap` type checks just fine. `SSucc` is perfect here. Let’s try something else:

``zero_one_two = sMap sPred sNums``

The type of `sPred` is `forall n. Sing n -> Sing (Pred n)`, as written above, so one would think all is good. All is not good. The problem is that `Pred` is a type family, not a regular type constructor like good old `Succ`. Thus, GHC does not (and cannot, with good reason) infer that `f` in the type of `sMap` should be `Pred`:

``````Couldn't match type `Pred t1' with `t t1'
Expected type: Sing Nat t1 -> Sing Nat (t t1)
Actual type: Sing Nat t1 -> Sing Nat (Pred t1)``````

The reason this inference is bogus is that GHC will not let a type variable unify with a type family. In its internal constraint-solving machinery, GHC assumes that all type variables are both injective and generative. Injective means that from an assumption of `t a ~ t b`, (where `~` denotes type equality) we can derive `a ~ b`. Generative means that from an assumption of `t a ~ s b`, we can derive `t ~ s`. Type families, in general, have neither property. So, GHC won’t let a type variable unify with a type family.

This problem — called the saturation requirement of type families — is what Conor was thinking about when he disbelieved that `singletons` handled `map`.

## Defunctionalization

Defunctionalization is an old technique of dealing with higher-order functions. The idea is that, instead of making a closure or other pointer to code, represent a function with some symbol that can be looked up and linked to the code later. Danvy and Nielsen wrote a more recent paper explaining how the whole thing works. One drawback of the technique that they outline is that defunctionalization tends to require whole-program translation. That is, the transformation requires looking at the entire codebase to do the translation. This is generally necessary so that the table of function “symbols”, encoded as an algebraic datatype, can be matched on. However, in Haskell, we have open type functions, so this problem does not limit us.

Another drawback of defunctionalization is that it is generally poorly-typed. If we are just using some symbol to denote a function, how can we be sure that a function application is well-typed? Pottier and Gauthier address this issue in their paper on the topic by using generalized algebraic datatypes (GADTs). But, given the way type families work in Haskell, we don’t need the power of GADTs to do this for us.

## Encoding defunctionalization in Haskell type families

At the heart of any defunctionalization scheme is an `apply` function:

``type family Apply (f :: k1 -> k2) (a :: k1) :: k2``

But wait, we don’t really want `Apply` to have that kind, because then we would have to pass `Pred` in as the function, and `Pred` all on its own is unsaturated. What we need is some symbol that can represent `Pred`:

``````type family Apply (f :: *) (a :: k1) :: k2
data PredSym :: *
type instance Apply PredSym n = Pred n``````

This is progress. We can now pass `PredSym` around all by itself, and when we apply it, we get the desired behavior. But, this is weakly kinded. We would like to be able to define many symbols akin to `PredSym`, and we would like GHC to be able to make sure that we use these symbols appropriately — that is, we don’t say `Apply PredSym '[Int, Bool]`.

Yet, we still want to be able to create new symbols at will. So, we want to use `data` declarations to create the symbols. Thus, the kind of these symbols must end in `-> *`. But, we have complete freedom as to what appears to the left of that arrow. We will use this definition to store the kinds:

``````> data TyFun :: * -> * -> *
``````

Now, we can make our richly kinded `Apply`:

``````> type family Apply (f :: (TyFun k1 k2) -> *) (x :: k1) :: k2
> data PredSym :: (TyFun Nat Nat) -> *
> type instance Apply PredSym x = Pred x
``````

This one works. But, we want it to work also for real type constructors (like `Succ`), not just type families. We have to wrap these type constructors in an appropriately kinded wrapper:

``````> data TyCon :: (k1 -> k2) -> (TyFun k1 k2) -> *
> type instance Apply (TyCon tc) x = tc x
``````

Then, we define a new version of `sMap` that works with `Apply`:

``````> type family DFMap (f :: (TyFun k1 k2) -> *) (ls :: [k1]) :: [k2]
> type instance DFMap f '[]      = '[]
> type instance DFMap f (h ': t) = (Apply f h ': DFMap f t)
```
```sDFMap :: forall (f :: TyFun k1 k2 -> *) (ls :: [k1]).
(forall a. Sing a -> Sing (Apply f a)) -> Sing ls -> Sing (DFMap f ls)
sDFMap _ SNil        = SNil
sDFMap f (SCons h t) = SCons (f h) (sDFMap f t)``````

We’re close, but we’re not there yet. This `sDFMap` function has a major problem: it is inherently ambiguous. The type variable `f` appears only inside of type family applications, and so there’s no way for GHC to infer its value. This problem has a straightforward solution: use a proxy.

``````> data Proxy a = P
```
```sDFMap :: forall (f :: TyFun k1 k2 -> *) (ls :: [k1]).
Proxy f -> (forall a. Sing a -> Sing (Apply f a)) ->
Sing ls -> Sing (DFMap f ls)
sDFMap _ _ SNil        = SNil
sDFMap p f (SCons h t) = SCons (f h) (sDFMap p f t)``````

This one really does work, but we can still do better. The problem is that some plumbing is exposed. When calling this version of `sDFMap` with `sPred`, we still have to explicitly create the proxy argument and give it the correct type, even though we would like to be able to infer it from `sPred`. The trick is that, while we do need to have `f` exposed in the type of `sDFMap`, the location where it is exposed doesn’t matter. It can actually be in an argument to the callback function. This next, final version also contains those pesky class constraints that we’ve been trying to avoid this whole time.

``````> sDFMap :: forall (f :: TyFun k1 k2 -> *) (ls :: [k1]).
>           SingKind (KindParam :: OfKind k2) =>
>           (forall a. Proxy f -> Sing a -> Sing (Apply f a)) ->
>           Sing ls -> Sing (DFMap f ls)
> sDFMap _ SNil        = sNil
> sDFMap f (SCons h t) = sCons (f P h) (sDFMap f t)
``````

To call this function, we will need to create wrappers around, say, `sPred` and `sSucc` that explicitly relate the functions to their defunctionalization symbols:

``````> sPred' :: Proxy PredSym -> Sing n -> Sing (Pred n)
> sPred' _ = sPred
> sSucc' :: Proxy (TyCon Succ) -> Sing n -> Sing (Succ n)
> sSucc' _ = sSucc
``````

Now, finally, we can use `sDFMap` as desired:

``````> two_three_four' = sDFMap sSucc' sNums
> zero_one_two = sDFMap sPred' sNums
``````

## Conclusions

This whole thing is a bit of a hack, but it’s one that seems to follow a nice pattern that could be automated. In particular, I believe it should be relatively straightforward to incorporate this kind of encoding into a future version of `singletons`. This would allow more code to be singletonized and support dependently typed programming better.

One clear drawback of this approach is that the arity of a defunctionalized function must be a part of the encoding. In some future world with kind families, it may be possible to generalize the arities. One idea I have for a future blog post is to grapple with higher-arity and partially applied functions, which may be a bit icky. And, what about defunctionalizing higher-order functions?

The question at the end of all of this is: could this be an approach to desaturating type families in Haskell? In other words, could an approach based on the ideas here be incorporated into GHC to make all of this Just Work? I’ve thought about it a bit, but not long enough or hard enough to really have an opinion. What do you think?

And, if I write this functionality into `singletons`, will it be useful to you? We all have limited time, and it’s helpful to know if such an improvement will be put to use.