Introduction to Singletons (Part 2)

SourceMarkdownLaTeXPosted in HaskellComments


Welcome back to our journey through the singleton design pattern and the great singletons library!

This post is a direct continuation of Part 1, so be sure to check that out first if you haven’t already! If you hare just jumping in now, I suggest taking some time to to through the exercises if you haven’t already!

Again, code is built on GHC 8.2.2 with the lts-10.0 snapshot (so, singletons-2.3.1).

Review

Let’s return to our Door type:

First, this derives the type DoorState with the values Opened, Closed, and Locked, and also the kind DoorState with the types 'Opened, 'Closed, and 'Locked. We then also derive the singletons (and implicit-style typeclass instances, reflectors, etc.) with the template haskell.

Then, there’s Door. Door is great! It is an indexed data type (indexed by a type of kind DoorState) in that picking a different type variable gives a different “type” of Door:

  • Door 'Opened is a type that represents the type of an opened door
  • Door 'Closed is a different type that represents the type of a closed door
  • Door 'Locked is yet another (third) type that represents the type of a locked door.

So, really, when we define Door s, we really are defining three distinct types1.

This is great and all, but isn’t Haskell a language with static, compile-time types? Doesn’t that mean that we have to know if our doors are opened, closed, or locked at compile-time?

This is something we can foresee being a big issue. It’s easy enough to create a Door s if you know s at compile-time by just typing in a type annotation (UnsafeMkDoor "Oak" :: Door 'Opened) or by using a monomorphic constructor (mkDoor @SOpened "Oak"). But what if we don’t know s at compile-time?

To learn how to do this, we first need to learn how to not care.

Ditching the Phantom

Sometimes we don’t actually care about the state of the door in the type of the door. We don’t want Door 'Opened and Door 'Closed…we want a type to just represent a door, without the status in its type.

This might come about a bunch of different ways. Maybe you’re reading a Door data from a serialization format, and you want to be able to parse any door (whatever door is serialized).

To learn how to not care, we can describe a type for a door that does not have its status in its type.

We have a couple of options here. First, we can create a new type SomeDoor that is the same as Door, except instead of keeping its status in its type, it keeps it as a runtime value:

Note the similarity of SomeDoor’s declaration to Door’s declaration above. It’s mostly the same, except, instead of DoorState being a type parameter, it is instead a runtime value inside SomeDoor.

Now, this is actually a type that we could have been using this entire time, if we didn’t care about type safety. In the real world and in real applications, we actually might have written SomeDoor before we ever thought about Door with a phantom type. It’s definitely the more typical “standard” Haskell thing.

SomeDoor is great. But because it’s a completely different type, we can’t re-use any of our Door functions on this SomeDoor. We potentially have to write the same function twice for both Door and SomeDoor, because they have different implementations.

The Existential Datatype

However, there’s another path we can take. With the power of singletons, we can actually implement SomeDoor in terms of Door, using an existential data type:

MkSomeDoor is a constructor for an existential data type, meaning that the data type “hides” a type variable s. Note the type (Sing s -> Door s -> SomeDoor) and how the result type (SomeDoor) forgets the s and hides all traces of it. Think of it like a type variable sponge – type variable goes in, but it’s absorbed opaquely into the result type.

Note the similarities between our original SomeDoor and this one.

Basically, our type before re-implements Door. But the new one actually directly uses the original Door s. This means we can directly re-use our Door functions on SomeDoors, without needing to write completely new implementations.

In Haskell, existential data types are pretty nice, syntactically, to work with. Let’s write some basic functions to see. First, a function to “make” a SomeDoor from a Door:

So that’s how we make one…how do we use it? Let’s port our Door functions to SomeDoor, by re-using our pre-existing functions whenever we can, and pattern matching on MkSomeDoor:

Using an existential wrapper with a singleton makes this pretty simple – just a simple unwrapping and re-wrapping! Imagine having to re-implement all of these functions for a completely different type, and having to re-implement all of our previous Door functions.

It’s important to remember that the secret ingredient here is the Sing s we store inside MkSomeDoor – it gives our pattern matchers the ability to deduce the s type. Without it, the s would be lost forever.

If MkSomeDoor did not have the Sing:

It would then be impossible to write closeSomeOpenedDoor in a way that only works on opened doors:

It’s important to remember that our original separate-implementation SomeDoor is, functionally, identical to the new code-reusing Door. All of the contents are isomorphic with each other, and you could write a function converting one to the other. This is because having an existentially quantified singleton is the same as having a value of the corresponding type. Having an existentially quantified SingDS s is the same as having a value of type DoorState.

In fact, the singletons library gives us a direct existential wrapper:

There are three values of type SomeSing DoorState:

A value of type SomeSing DoorState (which contains an existentially quantified Sing s – a SingDS) is the same as a value of type DoorState. The two types are identical! (Or, well, isomorphic. As a fun exercise, write out the explicit isomorphism – the SomeSing DoorState -> DoorState and the DoorState -> SomeSing DoorState).

Our new SomeDoor containing an existentially quantified Sing s is the same as our first SomeDoor containing just a DoorState.

Why do we sing?

If they’re identical, why use a Sing or the new SomeDoor at all? Why not just use a DoorState value?

One main reason (besides allowing code-reuse like we did earlier) is that using the singleton lets us directly recover the type. Essentially, a Sing s not only contains whether it is Opened/Closed/Locked (like a DoorState would), but also it contains it in a way that GHC can use to bring it all back to the type level.

A forall s. SomeDoor (Sing s) (Door s) essentially contains s with Door s. When you see this, you should read this as forall s. SomeDoor s (Door s) (and, indeed, this is similar to how it is written in dependently typed languages.)

It’s kind of like how, when you’re used to reading Applicative style, you start seeing f <$> x <*> y and reading it like f x y. When you see forall s. SomeDoor (Sing s) (Door s), you should read (the pseudo-haskell) forall s. SomeDoor s (Door s). The role of Sing s there is, like in Part 1, simply to be a run-time stand-in for the type s itself.

So, for our original Door s functions, we need to know s at runtime – storing the Sing s gives GHC exactly that. Once you get the Sing s back, you can now use it in all of our type-safe functions from Part 1, and you’re back in type-safe land.2

Some Lingo

In the language of dependently typed programming, we call SomeDoor a dependent sum, because you can imagine it basically as a sum type:

A three-way sum between a Door 'Opened, a Door 'Closed, and a Door 'Locked, essentially. If you have a SomeDoor, it’s either an opened door, a closed door, or a locked door. Try looking at this new SomeDoor until you realize that this type is the same type as the previous SomeDoor!

You might also see SomeDoor called a dependent pair – it’s a “tuple” where the type of the second item (our Door s) is determined by the value of the first item (our Sing s).

In Idris, we could write SomeDoor as a type alias, using its native dependent pair syntactic sugar, as (s ** Door s). The value of the first item reveals to us (through a pattern match, in Haskell) the type of the second.

Types at Runtime

With this new tool, we finally have enough to build a function to “make” a door with the status unknown until runtime:

Using mkSomeDoor, we can truly pass in a DoorState that we generate at runtime (from IO, or a user prompt, or a configuration file, maybe), and create a Door based on it.

Take that, type erasure! :D

The Existential Type

An existentially quantified type is one that is hidden to the user/consumer, but directly chosen by the producer. The producer chooses the type, and the user has to handle any possible type that the producer gave.

This is in direct contrast to the universally quantified type (which most Haskellers are used to seeing), where the type is directly chosen by the user. The user chooses the type, and the producer has to handle any possible type that the user asks for.

For example, a function like:

Is universally quantified over a: The caller of read gets to pick which type is given. The burden is on the implementor of read to be able to handle whatever a the user picks.

But, for a value like:

The type variable s is existentially quantified. The person who made myDoor picked what s was. And, if you use myDoor, you have to be ready to handle any s they could have chosen.

In Haskell, there’s another way to express an existentially quantified type: the CPS-style encoding. This way is useful because it doesn’t require creating an intermediate helper data type. To help us understand it, let’s compare a basic function in both styles. We saw earlier mkSomeDoor, which takes a DoorState and a String and returns an existentially quantified Door in the form of SomeDoor:

The caller of the function can then break open the SomeDoor and must handle whatever s they find inside.

We can write the same function using a CPS-style existential instead:

With a Rank-N Type, withDoor takes a DoorState and a String and a function to handle a Door s polymorphically. The caller of withDoor must provide a handler that can handle any s, in a uniform and parametrically polymorphic way. The function then gives the result of the handler function called on the resulting Sing s and Door s.

The key to making this work is that your handler function has to be polymorphic over all possible ss. This way, it can handle any potential s that the producer gives. Essentially, the producer is “returning” an s – existentially quantified.

Reification

The general pattern we are exploring here is called reification – we’re taking a dynamic run-time value, and lifting it to the type level as a type (here, the type variable s). You can think of reification as the opposite of reflection, and imagine the two as being the “gateway” between the type-safe and unsafe world. In the dynamic world of a DoorState term-level value, you have no type safety. You live in the world of SomeDoor, closeSomeOpenedDoor, lockAnySomeDoor, etc. But, you can reify your DoorState value to a type, and enter the type-safe world of Door s, closeDoor, lockDoor, and lockAnyDoor.

The singletons library automatically generates functions to directly reify DoorState values:

The first one reifies a DoorState as an existentially quantified data type, and the second one reifies one in CPS-style, without the intermediate data type.

We can actually use these to write mkSomeDoor and withDoor in a nicer way, without directly pattern matching on our constructors:

Zooming Out

Alright! We’ve spent two blog posts going over a lot of different things in the context of our humble Door s type. Let’s zoom out and take a large-scale look at how singletons (the design pattern, and the library) helps us in general.

Sing

The crux of everything is the Sing :: Type -> Type indexed type. If you see a value of type Sing s, you should really just think “a runtime witness for s”. If you see:

You should read it as (in pseudo-Haskell)

This is seen clearly if we look at the partially applied type signatures:

If you squint, this kinda looks like:

And indeed, when we get real dependent types in Haskell, we will really be directly passing types (that act as their own runtime values) instead of singletons.

It is important to remember that Sing is poly-kinded, so we can have Sing 'Opened, but also Sing 'True, Sing 5, and Sing '['Just 3, 'Nothing, 'Just 0] as well. This is the real benefit of using the singletons library instead of writing our own singletons – we get to work uniformly with singletons of all kinds.

SingI

SingI is a bit of typeclass trickery that lets us implicitly pass Sings to functions:

If you see:

These are identical in power to

Either way, you’re passing in the ability to get a runtime witness on s – just in one way, it is asked for as an explicit argument, and the second way, it is passed in using a typeclass.

We can convert from SingI s -> style to SingI s => style using sing:

And we can convert from SingI s => style to SingI s -> style using withSingI:

Again, the same function – just two different styles of calling them.

Reflection and Reification

Reflection is the process of bringing a type-level thing to a value at the term level (“losing” the type information in the process) and reification is the process of bringing a value at the term level to the type level.

Reflection and reification can be thought of as the gateways between the untyped/unsafe world and the typed/safe world. Reflection takes you from the typed world to the untyped world (from Sing s to DoorState) and reification takes you from the untyped world to the typed world (from DoorState to Sing s).

One limitation in Haskell is that there is no actual link between the type DoorState and its values with the kind DoorState with its types. Sure, the constructors have the same names, but the language doesn’t actually link them together for us.

SingKind

The singletons library handles this by using a typeclass with associated types to implement a generalized reflection and reification process. It gives us the SingKind “kindclass”:

Instances of SingKind are (promoted) kinds like Bool-the-kind, DoorState-the-kind, etc., and Demote is an associated type/type family that associates each instance with the type it is promoted from. (Note – writing these type signatures requires the -XTypeInType extension, which lets us treat kinds as types)

For example, remember how data DoorState = Opened | Closed | Locked created the type DoorState (with value constructors Opened, Closed, and Locked), and also the kind DoorState (with type constructors 'Opened, 'Closed, and 'Locked). Our kind DoorState would be the instance of SingKind, and Demote DoorState would be the type DoorState.

The reason we need an explicit Demote associated type is, again, that GHC doesn’t actually link the type and its promoted kind. Demote lets us explicitly specify what type a Kind should expect its term-level reflected values to be. (And, like most things in this post, Demote will hopefully one day become obsolete, along with the rest of SingKind)

Examples

To illustrate explicitly, here is the automatically generated instance of SingKind for the DoorState kind:

If you are unfamiliar with how associated types work, type Demote DoorState = DoorState means that wherever we see Demote DoorState (with DoorState the kind), we replace it with DoorState (the type). That’s why the type of our reflection function fromSing :: Sing s -> Demote DoorState can be simplified to fromSing :: Sing s -> DoorState.

Let’s take a look at the instance for Bool, to compare:

And a more sophisticated example, let’s look at the instance for Maybe:

This definition, I think, is a real testament to the usefulness of having all of our singletons be unified under the same system. Because of how SingKind works, Demote (Maybe DoorState) is evaluated to Maybe (Demote DoorState), which is simplified to Maybe DoorState. This means that if we have a way to reify DoorState values, we also have a way to reify Maybe DoorState values! And, if we have a way to reflect DoorState singletons, we also have a way to reflect Maybe DoorState singletons!

SomeSing

Throughout all of this, we utilize SomeSing as a generic poly-kinded existential wrapper:

Basically, this says that SomeSing k contains a Sing x, where x is of kind k. This is why we had, earlier:

If we use SomeSing with, say, SClosed, we get SomeSing :: Sing 'Closed -> SomeSing DoorState. SomeSing is an indexed type that tells us the kind of the type variable we existentially quantifying over. The value SomeSing STrue would have the type SomeSing Bool. The value SomeSing (SJust SClosed) would have the type SomeSing (Maybe DoorState).

Looking Forward

Between these first two parts, we explored a specific use case that would benefit from dependent types (simple phantom types for state transitions) and explored how the singletons and design pattern help us implement the functionality necessary to make things useful, and snuck in some concepts from dependently typed programming as well. We then took a step back to explore the singletons library in a more “universal” way, and saw how it is generalized to many different types.

The code is available here for you to play around with yourself!

Now that the basics are out of the way, in Part 3 we’ll jump deep into type-level programming and being able to lift our term-level functions on values up to become type-level functions, and how to use this to express complex relationships and enhance our code!

Let me know in the comments if you have any questions! I’m also usually idling on the freenode #haskell channel, as well, as jle`.

And, again, I definitely recommend checking out the original singletons paper for a really nice technical overview of all of these techniques from the source itself.

Exercises

Check out the sample code for solutions!

  1. Let’s revisit our original redundant SomeDoor, compared to our final SomeDoor:

    To help convince yourself that the two are equal, write functions converting between the two:

    Avoid directly pattern matching on the singletons or constructors. Instead, use singletons library tools like toSing, withSomeSing, fromSing, etc.

  2. Previously, we had an unlockDoor function that took an Int (the “password”) with a Door 'Locked and returned a Maybe (Door 'Closed). It returns a Door 'Closed (unlocked door) in Just if an odd number was given, and Nothing otherwise (a failed unlock)

    Use this to implement a that would return a SomeDoor. Re-use the “password” logic from the original unlockDoor. If the door is successfully unlocked (with a Just), return the unlocked door in a SomeDoor. Otherwise, return the original locked door (in a SomeDoor).

  3. Implement openAnyDoor' in the same style, with respect to openAnyDoor:

    Remember to re-use openAnyDoor.

  4. Write the SingKind instance for the promoted kind of a custom list type:

    The singletons for List are:

    Note that the built-in singletons for the list type also uses these same constructor names, for [] and :.


  1. And also a not-so-obvious fourth type, forall s. Door s, which is a subtype of all of those three!

  2. You might have noticed I was a bit sneaky by jumping straight SomeDoor when we already had a perfectly good “I don’t care” option. We used it last post!

    This does work! lockAnyDoor takes a Door s and doesn’t “care” about what s it gets (it’s parametrically polymorphic).

    So, this normal “parametrically polymorphic” way is how we have, in the past, treated functions that can take a Door with an s we don’t want the type system to care about. However, the reason we need SomeDoor and existentially quantified types is for the situation where we want to return something that we want to the type system to not care about.

Comments powered by Disqus