This tutorial assumes you're already familiar with Haskell's kind system and extensions like
If not, please read my blog post first
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.
DataKinds, we create a new
ConnectionStatus kind with two possible types,
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
'Closed) in scope, but we can't pattern match on it!
How do we find out whether
We need a value to pattern match on. Singleton types to the rescue!
'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
-- | 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
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"
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
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
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
-- | 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
-- | 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"