# singletons v0.9 Released!

I just uploaded singletons-0.9.2 to hackage. This is a significant upgrade from previous versions, and it gives me a good chance to explain some of its features here.

This post is a literate Haskell file. Copy and paste it into a .lhs file, and you’re off to the races. But first, of course, a little throat-clearing:

``````> {-# LANGUAGE TemplateHaskell, PolyKinds, DataKinds, TypeFamilies,
>              ScopedTypeVariables, GADTs, StandaloneDeriving, RankNTypes,
>              TypeOperators #-}
>
> import Data.Singletons.TH
> import Unsafe.Coerce    -- don't hate me yet! keep reading!
``````

The singletons library was developed as part of the research behind this paper, published at the Haskell Symposium, 2012.

## What are singletons?

Singleton types are a technique for “faking” dependent types in non-dependent languages, such as Haskell. They have been known for some time – please see the original research paper for more history and prior work. A singleton type is a type with exactly one value. (Note that `undefined` is not a value!) Because of this curious fact, learning something about the value of a singleton type tells you about the type, and vice versa.

A few lines of example is worth several paragraphs of awkward explanation, so here we go (the underscores are to differentiate from our second version, below):

``````> data Nat_ = Zero_ | Succ_ Nat_
> data SNat_ :: Nat_ -> * where
>   SZero_ :: SNat_ Zero_
>   SSucc_ :: SNat_ n -> SNat_ (Succ_ n)
>
> plus_ :: Nat_ -> Nat_ -> Nat_
> plus_ Zero_     n = n
> plus_ (Succ_ m) n = Succ_ (plus_ m n)
>
> type family Plus_ (m :: Nat_) (n :: Nat_) :: Nat_
> type instance Plus_ Zero_     n = n
> type instance Plus_ (Succ_ m) n = Succ_ (Plus_ m n)
>
> sPlus_ :: SNat_ m -> SNat_ n -> SNat_ (Plus_ m n)
> sPlus_ SZero_     n = n
> sPlus_ (SSucc_ m) n = SSucc_ (sPlus_ m n)
``````

Here, `SNat_` defines a singleton family of types. Note that, for any `n`, there is exactly one value of `SNat_ n`. This means that when we pattern-match on a `SNat_`, we learn about the type variable along with the term-level variable. This, in turn, allows for more type-level reasoning to show correctness for our code. See the paper for more explanation here.

Using singletons, we can pretend Haskell is dependently typed. For example, I have written a richly-typed database client and a provably* correct sorting algorithm using singletons.

*Of course, Haskell is not a total language (that is, it has `undefined` and friends), so any proof should be viewed with suspicion. More accurately, it is a proof of partial correctness. When the sorting algorithm compiles in finite time and when it runs in finite time, the result it produces is indeed a sorted list.

## Don’t Repeat Yourself

The above definitions are neat and all, but they sure are annoying. Haskell’s built-in promotion mechanism duplicates `Nat_` at the type and kind level for us, but we have to be responsible for all three versions of `plus_`. Let’s use the singletons library to help us!

``````> \$(singletons [d|
>   data Nat = Zero | Succ Nat
>     deriving Eq
>
>   plus :: Nat -> Nat -> Nat
>   plus Zero     n = n
>   plus (Succ m) n = Succ (plus m n)
>   |])
``````

The code above is a Template Haskell splice, containing a call to the `singletons` function (exported from `Data.Singletons.TH`). That function’s one argument is a Template Haskell quote, containing the abstract syntax tree of the definitions in the quote. The singletons library chews on those definitions to produce all the definitions above, and more.

To demonstrate the usefulness of singletons, we’ll need length-indexed vectors:

``````> data Vec :: * -> Nat -> * where
>   VNil  :: Vec a Zero
>   VCons :: a -> Vec a n -> Vec a (Succ n)
>
> instance Show a => Show (Vec a n) where
>   show VNil        = "VNil"
>   show (VCons h t) = show h ++ " : " ++ show t
``````

Now, we can write a well-typed `vReplicate` function:

``````> vReplicate :: SNat n -> a -> Vec a n
> vReplicate SZero      _ = VNil
> vReplicate (SSucc n') x = VCons x (vReplicate n' x)
``````

This works as expected:

``````ghci> vReplicate (SSucc (SSucc (SSucc SZero))) "hi"
"hi" : "hi" : "hi" : VNil
``````

Even better, we can make the numerical argument to `vReplicate` implicit, using `SingI`. The `SingI` class is very simple:

``````class SingI (a :: k) where
sing :: Sing a``````

A dictionary for (that is, a class constraint of) `SingI` just holds an implicit singleton. (See the paper for more info about `Sing`, which I won’t go over in this post.) Now, we can define the improved `vReplicateI`:

``````> vReplicateI :: forall a n. SingI n => a -> Vec a n
> vReplicateI x =
>   case sing :: SNat n of
>     SZero    -> VNil
>     SSucc n' -> VCons x (withSingI n' \$ vReplicateI x)
```
```ghci> vReplicateI "hi" :: Vec String (Succ (Succ (Succ Zero)))

"hi" : "hi" : "hi" : VNil
``````

Cool!

At this point, you may also want to check out the generated documentation for the singletons library to see a little more of what’s going on. The rest of this post will focus on some of the strange and wonderful new features of v0.9.

## Magic `SingI` dictionaries

Previous versions of singletons had definitions like this:

``````data instance Sing (n :: Nat) where
SZero :: Sing Zero
SSucc :: SingI n => Sing n -> Sing (Succ n)``````

The key difference here is the `SingI` constraint in the `SSucc` constructor. This constraint meant that if you pattern-matched on an `SNat` and got a `SSucc`, you would get both an explicit singleton for (n-1) and an implicit singleton (that is, a `SingI` dictionary) for (n-1). This was useful, and it meant that the old version of `vReplicateI` wouldn’t need the `withSingI` business. But, it also meant that every node in a singleton had duplicated information. Since this was true at every (interior) node, singleton trees were exponentially larger than necessary. Yuck. Somehow, none of my advisor, our reviewers, nor me noticed this before. My advisor (Stephanie Weirich) and I somehow convinced ourselves that the duplication would lead to trees that were double the necessary size, which we deemed acceptable. Oops!

In singletons 0.9, though, a singleton just contains the explicit version. We then needed a way to convert from explicit ones to implicit ones. To do this, I used a trick I learned from Edward Kmett at ICFP this year: take advantage of the fact that classes with exactly one method (and no superclass) are represented solely by the method, and nothing else. Thus, a dictionary for `SingI` is actually the same, in memory, as a real singleton! To go from explicit to implicit, then, we just have to wave a magic wand and change the type of a singleton from `Sing a` to `SingI a`.

The magic wand is easy; it’s called `unsafeCoerce`. What’s a little trickier is the fact that, of course, we can’t have dictionaries in the same place as normal datatypes in Haskell code. The first step is to create a way to explicitly talk about dictionaries. We make a datatype wrapper:

``````> data SingInstance (a :: k) where
>   SingInstance :: SingI a => SingInstance a
``````

To call the `SingInstance` constructor, we need to have a `SingI a` lying around. When we pattern-match on a `SingInstance`, we get that `SingI a` back. Perfect.

Now, we need a way to call the `SingInstance` constructor when we have an explicit singleton. Naively, we could imagine saying something like

``... (unsafeCoerce SingInstance :: Sing a -> SingInstance a) ...``

because, after all, `SingI a => SingInstance a` is the same under the hood as `Sing a -> SingInstance a`. The problem here is that as soon as we say `SingInstance` in Haskell code, GHC helpfully tries to solve the arising `SingI a` constraint – something we do not want here. (Once the `SingInstance` is instantiated, its type is just `SingInstance a`, which is not the same as `Sing a -> SingInstance a`!) The answer is to use a `newtype` the prevents instantiation:

``````> newtype DI a = Don'tInstantiate (SingI a => SingInstance a)
``````

Now, after a call to the `Don'tInstantiate` constructor, GHC will refrain from instantiating. Great – now we just need to connect the dots:

``````> singInstance :: forall (a :: k). Sing a -> SingInstance a
> singInstance s = with_sing_i SingInstance
>   where
>     with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
>     with_sing_i si = unsafeCoerce (Don'tInstantiate si) s
``````

It’s dirty work, but someone’s got to do it. And it saves us from exponential blow-up, so I’d say it’s worth it. The `withSingI` function we saw used above is just a convenient wrapper:

``````> withSingI :: Sing n -> (SingI n => r) -> r
> withSingI sn r =
>   case singInstance sn of
>     SingInstance -> r
``````

## Decidable propositional equality

A previous post on this blog discussed the different between Boolean equality and propositional equality. Previous versions of singletons contained the `SEq` “kind class” to use Boolean equality on singleton types. Singletons 0.9 also contains the `SDecide` class to allow for decidable propositional equality on singleton types.

Before we dive right into `SDecide` though, let’s review a few new definitions in the standard library (`base` package) shipping with GHC 7.8. Under `Data.Type.Equality`, we have these handy definitions:

``````data a :~: b where
Refl :: a :~: a

gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
gcastWith Refl x = x

class TestEquality (f :: k -> *) where
testEquality :: f a -> f b -> Maybe (a :~: b)``````

The idea behind the `TestEquality` class is that it should classify datatypes whose definitions are such that we can (perhaps) learn about the equality of type variables by looking at terms. Singletons are the chief candidates for instances of this class. `Typeable` almost is, but it’s at the wrong kind – `k -> Constraint` instead of `k -> *`. (See the new function `Data.Typeable.eqT` for comparison.)

`SDecide` takes the `TestEquality` idea one step further, providing full decidable propositional equality. See the previous post on propositional equality for more background.

``````data Void
type Refuted a = a -> Void
data Decision a = Proved a
| Disproved (Refuted a)

class (kproxy ~ 'KProxy) => SDecide (kproxy :: KProxy k) where
(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)``````

We can now use `(%~)` to (perhaps) produce an equality that GHC can use to complete type inference. Instances of `SDecide` (and of `SEq`, for that matter) are generated for any datatype passed to the `singletons` Template Haskell function that derive `Eq`. Or, you can use other functions exported by `Data.Singletons.TH` to create these instances; see the generated documentation.

## Future work

While the improvements in v0.9 are substantial, there is still much distance to cover. In particular, I conjecture that almost any function definable at the term level can be promoted to the type level. The exceptions would be unpromotable datatypes (like `Double`, `IO`, or GADTs) and higher-rank functions (there are no higher-rank kinds). Short of that, I think it’s all within reach.

How?

• The th-desugar library desugars Haskell’s fancy constructs into a manageable set.
• Case statements can be straightforwardly encoded using lambda lifting.

But, I don’t seem to have the time to put this all into action. If you’re interested in taking some or all of this on, I’d be very happy to collaborate. I believe some interesting research-y things might come out of it all, too, so there might even be something publishable in it. Drop me a line to discuss!

# 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

Over lunch while at ICFP, I had the good fortune of sitting with Tillmann Rendel, and we got to talking about this problem. He suggested that I think about defunctionalization. I have thought about this, and I think it’s the answer to the problem.

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.