singleton-types.md

singleton-types.md

This tutorial assumes you're already familiar with Haskell's kind system and extensions like DataKinds. If not, please read my blog post first </shameless-plug>.

Say you want to model a TCP connection, and it can be in either an "open" or "closed" status.

data Connection = MkConnection ...

-- | If the connection is closed, open it.
-- If it's already open, throw an exception.
open :: Connection -> IO Connection
open = _

-- | If the connection is open, close it.
-- If it's already closed, throw an exception.
close :: Connection -> IO Connection
close = _

We immediately face a problem: this API allows users to open connections which are already open, or close connections that are already closed. And this can lead to exceptions and buggy programs.

So we want to allow the user to open a connection only if it's closed, and close a connection only if it's open.

We can do this by parameterizing Connection over its status.

Using DataKinds, we create a new ConnectionStatus kind with two possible types, 'Open and 'Closed.

data ConnectionStatus where
  Open :: ConnectionStatus
  Closed :: ConnectionStatus

data Connection (st :: ConnectionStatus) = MkConnection

open :: Connection 'Closed -> IO (Connection 'Open)
open = undefined

close :: Connection 'Open -> IO (Connection 'Closed)
close = undefined

Let's test this out. We create some dummy connections:

someOpenConn :: Connection 'Open
someOpenConn = MkConnection @'Open

someClosedConn :: Connection 'Closed
someClosedConn = MkConnection @'Closed

And we attempt to open or close them:

res1 :: IO (Connection 'Open)
res1 = open someClosedConn

res2 :: IO (Connection 'Closed)
res2 = close someOpenConn

-- • Couldn't match type ‘'Open’ with ‘'Closed’
--   Expected type: Connection 'Closed
--     Actual type: Connection 'Open
wontCompile = open anOpenConn

Next, let's try to implement a function that prints the connection's status, so we can display it on the terminal.

showConnectionStatus :: forall st. Connection st -> String
showConnectionStatus conn =
  "The connection is " <> ???

Here's the problem: we have a type st (which is either 'Open or 'Closed) in scope, but we can't pattern match on it! How do we find out whether st is 'Open or 'Closed?

We need a value to pattern match on. Singleton types to the rescue!

Remember, 'Open and 'Closed are uninhabited types - there are no values of these types!

kinds:    ConnectionStatus
                ↑
                |
types:        'Open
                ↑
                |
values:        N/A

But we can create a correspondence between, for example, the uninhabited type 'Open and a type SConnectionStatus 'Open, inhabited by a single value SOpen.

-- | Singleton type for 'ConnectionStatus'.
--
-- It's named "singleton" because it's a type with exactly one single value.
-- E.g: the type 'SConnectionStatus Open' has exactly one value: `SOpen`
--      the type 'SConnectionStatus Closed' has exactly one value: `SClosed`
data SConnectionStatus (st :: ConnectionStatus) where
  SOpen :: SConnectionStatus 'Open
  SClosed :: SConnectionStatus 'Closed

We now have the following correspondence:

kinds:    ConnectionStatus               Data.Kind.Type
                ↑                              ↑
                |                              |
types:        'Open    ------------> SConnectionStatus 'Open
                                               ↑
                                               |
values:                                      SOpen

Now we can change our showConnectionStatus function to accept a Connection st and the corresponding singleton for that connection's status st.

showConnectionStatus :: forall st. SConnectionStatus st -> Connection st -> String
showConnectionStatus singleton _ = do
  case singleton of
    SOpen -> "The connection is open"
    SClosed -> "The connection is closed"

Let's try it out:

>>> showConnectionStatus SOpen someOpenConn
"The connection is open"

>>> showConnectionStatus SClosed someClosedConn
"The connection is closed"

It works!

---

However, we have to actually pass the value SConnectionStatus st around with the connection all the time, and this can be a bit annoying.

To solve this, we can create a typeclass that lets us summon the singleton for a given st.

class ConnectionStatusSingletonImplicit st where
  sing :: SConnectionStatus st

instance ConnectionStatusSingletonImplicit 'Open where
  sing :: SConnectionStatus 'Open
  sing = SOpen
instance ConnectionStatusSingletonImplicit 'Closed where
  sing :: SConnectionStatus 'Closed
  sing = SClosed

We can now change our showConnectionStatus to accept a typeclass instance instead of a singleton type:

showConnectionStatus2 :: forall st. ConnectionStatusSingletonImplicit st => Connection st -> String
showConnectionStatus2 _ = do
  case sing @st of
    SOpen -> "The connection is open"
    SClosed -> "The connection is closed"

Now, we don't have to pass SOpen and SClosed around. We can simply let GHC do the hard work for us and figure out which singleton should be used:

>>> showConnectionStatus2 someOpenConn
"The connection is open"

>>> showConnectionStatus2 someClosedConn
"The connection is closed"

---

Turns out this is a very common pattern, so the singletons library gives us abstractions to work with singeton types in general, so we don't have to keep re-inventing the wheel.

It provides a Sing type family, that maps a promoted data type (like 'Open) to its corresponding singleton type SConnectionStatus 'Open:

-- | Abstracts over any singleton type `a` of any kind `k`
type family Sing (a :: k)

-- The singleton type for `'Open :: ConnectionStatus` is `SConnectionStatus 'Open`
type instance Sing (st :: ConnectionStatus) = SConnectionStatus st

Furthermore, it generalizes our ConnectionStatusSingletonImplicit as SingI:

-- | Generalized version of 'ConnectionStatusSingletonImplicit'
class SingI a where
  sing :: Sing a

instance SingI 'Open where
  sing = SOpen
instance SingI 'Closed where
  sing = SClosed

Now we can modify our showConnectionStatus function to use the generalized SingI constraint instead:

showConnectionStatus3 :: forall st. SingI st => Connection st -> String
showConnectionStatus3 _ = do
  case sing @st of
    SOpen -> "The connection is open"
    SClosed -> "The connection is closed"

>>> showConnectionStatus3 someOpenConn
"The connection is open"

>>> showConnectionStatus3 someClosedConn
"The connection is closed"