Justin Le https://blog.jle.im (justin@jle.im)

Lambdaconf 2017, May 27, 2017

Slide available at https://mstksg.github.io/talks/lambdaconf-2017/singletons/singleton-slides.html.

GHC extensions (potentially) used:

```
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind -- to get type Type = *
import Data.Singletons
```

```
data DoorState = Opened | Closed | Locked
deriving (Show, Eq)
data Door (s :: DoorState) = UnsafeMkDoor
-- alternatively
data Door :: DoorState -> Type where
UnsafeMkDoor :: Door s
```

- State machines (socket connections, file handles, opened/closed)
- Refinement types
- "Tagged" types (santized/unsantized strings)

```
closeDoor :: Door 'Opened -> Door 'Closed
closeDoor UnsafeMkDoor = UnsafeMkDoor
```

```
openDoor :: Door 'Closed -> Door 'Opened
openDoor UnsafeMkDoor = UnsafeMkDoor
```

```
doorStatus :: Door s -> DoorState
doorStatus = -- ????
```

We have a problem.

```
doorStatus :: Door s -> DoorState
doorStatus UnsafeMkDoor = -- s ???
```

```
initalizeDoor :: DoorStatus -> Door s
initializeDoor = \case
Opened -> UnsafeMkDoor
Closed -> UnsafeMkDoor
Locked -> UnsafeMkDoor
```

Neat, but does this work?

```
ghci> :t initializeDoor Opened :: Door 'Closed
initializeDoor Opened :: Door 'Closed
```

Oops.

- In Haskell, types only exist at
*compile-time*. They are**erased**at runtime. - This is a good thing for performance! Types incur no runtime overhead!
- But it makes functions like
`doorStatus`

fundamentally unwritable without fancy typeclasses. - ...or does it?

```
data SingDS :: DoorStatus -> Type where
SOpened :: SingDS 'Opened
SClosed :: SingDS 'Closed
SLocked :: SingDS 'Locked
```

Creates three constructors:

```
SOpened :: SingDS 'Opened
SClosed :: SingDS 'Closed
SLocked :: SingDS 'Locked
```

- A
**singleton**is a type that has exactly one inhabited value. - There is only one value of type
`SingDS 'Opened`

, and only one value of type`SingDS 'Closed`

. - The constructor that a
`SingDS s`

uses reveals to us what`s`

is.

With our new singletons, we can essentially **pattern match** on types:

```
showSingDS :: SingDS s -> String
showSingDS = \case
SOpened -> "Opened"
SClosed -> "Closed"
SLocked -> "Locked"
```

Alone like this, it's a bit boring. We didn't need GADTs for this.

```
doorStatus' :: SingDS s -> Door s -> DoorState
doorStatus' = \case
SOpened -> \_ -> "Door is opened"
SClosed -> \_ -> "Door is closed"
SLocked -> \_ -> "Door is locked"
```

- GADT-ness allows us to enforce that the
`s`

in`SingDS s`

is the same as the`s`

in our`Door`

. - Singleton property means that
`SingDS s`

has a one-to-one correspondence with its constructors. - Pattern matching on that single constructor reveals to us the type of
`Door`

.

```
class SingDSI s where
singDS :: SingDSI s
instance SingDSI 'Opened where
singDS = SOpened
instance SingDSI 'Closed where
singDS = SClosed
instance SingDSI 'Locked where
singDS = SLocked
```

```
doorStatus :: SingDSI s => Door s -> DoorState
doorStatus = doorStatus' singDS
```

```
ghci> doorStatus (UnsafeMkDoor :: Door 'Locked)
Door is locked!
```

```
initializeDoor' :: SingDS s -> Door s
initializeDoor' _ _ = UnsafeMkDoor
```

```
ghci> :t initializeDoor' SOpened
initializeDoor SOpened :: Door 'Opened
ghci> :t initializeDoor' SClosed
initializeDoor SClosed :: Door 'Closed
```

Implicit passing style:

```
initializeDoor :: SingDSI s => Door s
initializeDoor = initializeDoor' singDS
```

- Really,
`SingDS s ->`

is the same as`SingDSI s =>`

- The two are the same way of providing the same information to the compiler, and at runtime.
- We can use the two styles interchangebly.
- One is
**explicitly passing the type**, the other is**explicitly passing the type**.

Sometimes we don't care about what the status of our door is, and we want the type system to relax.

This is essentially the same as saying that the status of our door is a runtime property that we do not want to (or sometimes can't) check at compile-time.

```
data SomeDoor :: Type where
MkSomeDoor :: SingDS s => Door s -> SomeDoor
```

```
ghci> let myDoor = MkSomeDoor (initializeDoor SOpened)
ghci> :t myDoor
myDoor :: SomeDoor
ghci> case myDoor of MkSomeDoor d -> doorStatus d
Door is opened.
```

```
initializeSomeDoor :: DoorStatus -> SomeDoor
initializeSomeDoor = \case
Opened -> SomeDoor (initialiseDoor' SOpened)
Closed -> SomeDoor (initialiseDoor' SClosed)
Locked -> SomeDoor (initialiseDoor' SLocked)
```

```
ghci> let myDoor = initializeSomeDoor Locked
ghci> :t myDoor
myDoor :: SomeDoor
ghci> case myDoor of MkSomeDoor d -> doorStatus d
Door is locked.
```

The singletons library provides a unified framework for creating and working with singletons for different types (not just `DoorStatus`

), and also for functions on those types.

```
$(singletons [d|
data DoorState = Opened | Closed | Locked
deriving (Show, Eq)
|])
```

This creates three types and three constructors:

```
-- not the actual code, but essentially what happens
data Sing :: DoorState -> Type where
SOpened :: Sing 'Opened
SClosed :: Sing 'Closed
SLocked :: Sing 'Locked
```

`Sing`

is a poly-kinded type constructor (family):

And also

```
instance SingI 'Opened where
sing = SOpened
instance SingI 'Closed where
sing = SClosed
instance SingI 'Locked where
sing = SLocked
```

(`SingI`

is a poly-kinded typeclass)

```
STrue :: Sing 'True
SJust SFalse :: Sing ('Just 'True)
SOpened `SCons` SClosed `SCons` SNil :: Sing '[ 'Opened, 'Closed ]
```

```
ghci> sing :: Sing 'True'
STrue
```

Some other convenient features:

```
ghci> fromSing SOpened
Opened
```

```
ghci> let s = toSing Opened
ghci> :t s
s :: SomeSing DoorStatus
ghci> case s of
SomeSing SOpened -> "Opened."
SomeSing SClosed -> "SClosed."
SomeSing SLocked -> "SLocked."
```

```
knock :: Door s -> IO ()
knock = -- ??
```

We want to allow the user to knock on a closed or locked door, but not an opened door.

We can do this simple case using pattern matching, but it's not always feasible or scalable. We want to define a type relationship that can be used by potentially many functions.

```
$(singletons [d|
canKnock :: DoorState -> Bool
canKnock Opened = False
canKnock Closed = True
canKnock Locked = True
|])
```

```
knock :: (CanKnock s ~ True) => Door s -> IO ()
knock _ = putStrLn "knock knock!"
```

```
ghci> knock (initializeDoor SOpened)
Compile Error!!!!
ghci> knock (initializeDoor SClosed)
knock knock!
```

```
tryKnock' :: Sing s -> Door s -> IO ()
tryKnock' s = case sCanKnock s of
STrue -> knock
SFalse -> \_ -> putStrLn "Cannot knock door!"
tryKnock :: SingI s => Door s -> IO ()
tryKnock = tryKnock' sing
```

```
ghci> tryKnock (initializeDoor SOpened)
Cannot knock door!
ghci> tryKnock (initializeDoor SClosed)
knock knock!
```

```
$(singletons [d|
data N = Z | S N
|])
data Vec :: N -> Type -> Type where
VNil :: Vec Z a
(:*) :: a -> Vec n a -> Vec (S n) a
infixr 5 :*
```

```
replicateV'
:: Sing n
-> a
-> Vec n a
replicateV' = \case
SZ -> \_ -> VNil
SS n -> \x -> x :* replicateV' n x
```

```
replicateV
:: SingI n
=> a
-> Vec n a
replicateV = replicateV' sing
```

- Further confusion: https://blog.jle.im/entry/verified-instances-in-haskell.html