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"