Introduction to Singletons (Part 4)
Introduction to Singletons
functional programming, dependent types, haskell, singletons, types
Hi again! Welcome back; let's jump right into the fourth and final part of our journey through the singleton design pattern and the great singletons library.
Please check out the first three parts of the series and make sure you are comfortable with them before reading on. I definitely also recommend trying out some or all of the exercises, since we are going to be building on the concepts in those posts in a pretty heavy way.
Today we're going to jump straight into functional programming at the type level. Code in this post is built on GHC 8.6.1 with the nightly-2018-09-29 snapshot (so, singletons-2.5). However, unless noted, all of the code should still work with GHC 8.4 and singletons-2.4.
Just as a quick review, this entire series we have been working with a
!!!singletons/Door4.hs "$(singletons " "data Door " "mkDoor"
And we talked about using
Sing s, or
SDoorState s, to represent the state
of the door (in its type) as a run-time value. We've been using a wrapper to
existentially hide the door state type, but also stuffing in a singleton to let
us recover the type information once we want it again:
data SomeDoor :: Type where MkSomeDoor :: Sing s -> Door s -> SomeDoor mkSomeDoor :: DoorState -> String -> SomeDoor mkSomeDoor ds mat = withSomeSing ds $ \dsSing -> MkSomeDoor dsSing (mkDoor dsSing mat)
In Part 3 we talked about a
Pass data type that we used to talk about whether
or not we can walk through or knock on a door:
$(singletons [d| data Pass = Obstruct | Allow deriving (Show, Eq, Ord) |])
And we defined type-level functions on it using singletons Template Haskell:
$(singletons [d| statePass :: DoorState -> Pass statePass Opened = Allow statePass Closed = Obstruct statePass Locked = Obstruct |])
This essentially generates these three things:
statePass :: DoorState -> Pass statePass Opened = Allow statePass Closed = Obstruct statePass Locked = Obstruct type family StatePass (s :: DoorState) :: Pass where StatePass 'Opened = 'Allow StatePass 'Closed = 'Obstruct StatePass 'Locked = 'Obstruct sStatePass :: Sing s -> Sing (StatePass s) sStatePass = \case SOpened -> SAllow SClosed -> SObstruct SLocked -> SObstruct
And we can use
StatePass as a type-level function while using
manipulate the singletons representing
We used this as a constraint to restrict how we can call our functions:
But then we wondered...is there a way to not only restrict our functions, but to describe how the inputs and outputs are related to each other?
Inputs and Outputs
In the past we have settled with very simple relationships, like:
closeDoor :: Door 'Opened -> Door 'Closed
This means that the relationship between the input and output is that the input is opened...and is then closed.
However, armed with promotion of type-level functions, writing more complex relationships becomes fairly straightforward!
We can write a function
mergeDoor that "merges" two doors together, in
mergeDoor :: Door s -> Door t -> Door ???? mergeDoor d e = UnsafeMkDoor $ doorMaterial d ++ " and " ++ doorMaterial e
A merged door will have a material that is composite of the original materials.
But, what will the new
DoorState be? What goes in the
Well, if we can write the function as a normal function in values...singletons lets us use it as a function on types. Let's write that relationship. Let's say merging takes on the higher "security" option --- merging opened with locked is locked, merging closed with opened is closed, merging locked with closed is locked.
$(singletons [d| mergeState :: DoorState -> DoorState -> DoorState mergeState Opened d = d mergeState Closed Opened = Closed mergeState Closed Closed = Closed mergeState Closed Locked = Locked mergeState Locked _ = Locked |]) -- Alternatively, taking advantage of the derived Ord instance: $(singletons [d| mergeState :: DoorState -> DoorState -> DoorState mergeState = max |])
This makes writing
mergeDoor's type clean to read:
And, with the help of singletons, we can also write this for our doors where we don't know the types until runtime:
To see why this typechecks properly, compare the types of
sMergeState :: Sing s -> Sing t -> Sing (MergeState s t) mergeDoor :: Door s -> Door t -> Sing (MergeState s t) MkSomeDoor :: Sing (MergeState s t) -> Door (MergeState s t) -> SomeDoor
Because the results both create types
MergeState s t,
MkSomeDoor is happy
to apply them to each other, and everything typechecks. However, if, say, we
MkSomeDoor, things would fall apart and not
And so now we have full expressiveness in determining input and output relationships! Once we unlock the power of type-level functions with singletons, writing type-level relationships become as simple as writing value-level ones. If you can write a value-level function, you can write a type-level function.
Kicking it up a notch
How far we can really take this?
Let's make a data type that represents a series of hallways, each linked by a door. A hallway is either an empty stretch with no door, or two hallways linked by a door. We'll structure it like a linked list, and store the list of all door states as a type-level list as a type parameter:
!!!singletons/Door4.hs "data Hallway"
So we might have:
ghci> let door1 = mkDoor SClosed "Oak" ghci> let door2 = mkDoor SOpened "Spruce" ghci> let door3 = mkDoor SLocked "Acacia" ghci> :t door1 :<# door2 :<# door3 :<# HEnd Hallway '[ 'Closed, 'Opened, 'Locked ]
That is, a
Hallway '[ s, t, u ] is a hallway consisting of a
Door s, a
Door t, and a
Door u, constructed like a linked list in Haskell.
Now, let's write a function to collapse all doors in a hallway down to a single door:
collapseHallway :: Hallway ss -> Door ?????
Basically, we want to merge all of the doors one after the other, collapsing it
until we have a single door state. Luckily,
MergeState is both commutative
and associative and has an identity, so this can be defined sensibly.
First, let's think about the type we want. What will the result of merging
We can pattern match and collapse an entire list down item-by-item:
$(singletons [d| mergeStateList :: [DoorState] -> DoorState mergeStateList  = Opened -- ^ the identity of mergeState mergeStateList (s:ss) = s `mergeState` mergeStateList ss |])
Again, remember that this also defines the type family
MergeStateList and the
sMergeStateList :: Sing ss -> Sing (MergeStateList ss).
With this, we can write
Now, because the structure of
collapseHallway perfectly mirrors the structure
mergeStateList, this all typechecks, and we're done!
ghci> collapseHallway (door1 :<# door2 :<# door3 :<# HEnd) UnsafeMkDoor "Oak and Spruce and Acacia and End of Hallway" :: Door 'Locked
Note one nice benefit -- the door state of
collapseHallway (door1 :<# door2 :<# door3 :<# HEnd) is known at compile-time
Door 'Locked, if the types of all of the component doors are also known!
We went over that all a bit fast, but some of you might have noticed that the
mergeStateList bears a really strong resemblance to a very common
Haskell list processing pattern:
mergeStateList :: [DoorState] -> DoorState mergeStateList  = Opened -- ^ the identity of mergeState mergeStateList (s:ss) = s `mergeState` mergeStateList ss
The algorithm is to basically
Opened, and all
If this sounds familiar, that's because this is exactly a right fold! (In
fact, hlint actually made this suggestion to me while I was writing this)
mergeStateList :: [DoorState] -> DoorState mergeStateList = foldr mergeState Opened
In Haskell, we are always encouraged to use higher-order functions whenever possible instead of explicit recursion, both because explicit recursion opens you up to a lot of potential bugs, and also because using established higher-order functions make your code more readable.
So, as Haskellers, let us hold ourselves to a higher standard and not be
satisfied with a
MergeState written using explicit recursion. Let us instead
go full fold --- ONWARD HO!
Initial attempts to write a higher-order type-level function as a type family, however, serve to temper our enthusiasm.
type family Foldr (f :: j -> k -> k) (z :: k) (xs :: [j]) :: k where Foldr f z ' = z Foldr f z (x ': xs) = f x (Foldr f z xs)
So far so good right? So we should expect to be able to write
type MergeStateList ss = Foldr MergeState 'Opened ss
Ah, but the compiler is here to tell you this isn't allowed in Haskell:
• The type family ‘MergeState’ should have 2 arguments, but has been given none • In the equations for closed type family ‘MergeStateList’ In the type family declaration for ‘MergeStateList’
What happened? To figure out, we have to remember that pesky restriction on
type synonyms and type families: they can not be used partially applied
("unsaturated"), and must always be fully applied ("saturated"). For the most
part, only type constructors (like
IO) and lifted
DataKinds data constructors (like
'(:)) in Haskell can ever be
partially applied at the type level. We therefore can't use
MergeState as an
MergeState must always be fully applied.
Unfortunately for us, this makes our
Foldr effectively useless. That's
because we're always going to want to pass in type families (like
MergeState), so there's pretty much literally no way to ever actually call
Foldr except with type constructors or lifted DataKinds data constructors.
So...back to the drawing board?
I like to mentally think of the singletons library as having two parts: the first is linking lifted DataKinds types with run-time values to allow us to manipulate types at runtime as first-class values. The second is a system for effective functional programming at the type level.
To make a working
Foldr, we're going to have to jump into that second half:
Defunctionalization is a technique invented in the early 70's as a way of compiling higher-order functions into first-order functions in target languages. The main idea is:
- Instead of working with functions, work with symbols representing functions.
- Build your final functions and values by composing and combining these symbols.
- At the end of it all, have a single
Applyfunction interpret all of your symbols and produce the value you want.
In singletons these symbols are implemented as "dummy" empty data
Apply is a type family.
To help us understand singleton's defunctionalization system better, let's build our own defunctionalization system from scratch.
First, a little trick to make things easier to read:
!!!singletons/Defunctionalization.hs "data TyFun" "infixr 0 ~>"
Our First Symbols
Now we can define a dummy data type like
Id, which represents the identity
!!!singletons/Defunctionalization.hs "data Id"1
The "actual" kind of
Id :: TyFun a a -> Type; you can imagine
TyFun a a as a phantom parameter that signifies that
Id represents a function from
a. It's essentially a nice trick to allow you to write
Id :: a ~> a
as a kind signature.
Id is not a function...it's a dummy type constructor that
represents a function
a -> a. A type constructor of kind
a ~> a
represents a defunctionalization symbol -- a type constructor that represents
a function from
To interpret it, we need to write our global interpreter function:
!!!singletons/Defunctionalization.hs "type family Apply"
That's the syntax for the definition of an open type family in Haskell: users are free to add their own instances, just like how type classes are normally open in Haskell.
Apply how to interpret
!!!singletons/Defunctionalization.hs "type instance Apply Id"
The above is the actual function definition, like writing
id x = x. We can
Id to get an actual type in return:
ghci> :kind! Apply Id 'True 'True
:kind! is the ghci command to evaluate a type family)
Let's define another one! We'll implement
!!!singletons/Defunctionalization.hs "data Not"
We can try it out:
ghci> :kind! Apply Not 'True 'False ghci> :kind! Apply Not 'False 'True
It can be convenient to define an infix synonym for
!!!singletons/Defunctionalization.hs "type f @@ a" "infixl 9 @@"
Then we can write:
ghci> :kind! Not @@ 'False 'True ghci> :kind! Id @@ 'True 'True
Not are not actual functions --- they're just dummy data
types ("defunctionalization symbols"), and we define the functions they
represent through the global
Apply type function.
A Bit of Principle
So we've got the basics of defunctionalization --- instead of using functions
directly, use dummy symbols that encode your functions that are interpreted
Apply. Let's add a bit of principle to make this all a bit more
The singletons library adopts a few conventions for linking all of these
together. Using the
Not function as an example, if we wanted to lift the
not :: Bool -> Bool not False = True not True = Flse
We already know about the type family and singleton function this would produce:
type family Not (x :: Bool) :: Bool where Not 'False = 'True Not 'True = 'False sNot :: Sing x -> Sing (Not x) sNot SFalse = STrue sNot STrue = SFalse
But the singletons library also produces the following defunctionalization symbols, according to a naming convention:
data NotSym0 :: Bool ~> Bool type instance Apply NotSym0 x = Not x -- also generated for consistency type NotSym1 x = Not x
NotSym0 is the defunctionalization symbol associated with the
family, defined so that
NotSym0 @@ x = Not x. Its purpose is to allow us to
Not as an un-applied function. The
Sym0 suffix is a naming
convention, and the 0 stands for "expects 0 arguments". Similarly for
NotSym1 -- the 1 stands for "expects 1 argument".
Let's look at a slightly more complicated example -- a two-argument function. Let's define the boolean "and":
$(singletons [d| and :: Bool -> (Bool -> Bool) and False _ = False and True x = x ])
this will generate:
type family And (x :: Bool) (y :: Bool) :: Bool where And 'False x = 'False And 'True x = x sAnd :: Sing x -> Sing y -> Sing (And x y) sAnd SFalse x = SFalse sAnd STrue x = x
And the defunctionalization symbols:
data AndSym0 :: Bool ~> (Bool ~> Bool) type instance Apply AndSym0 x = AndSym1 x data AndSym1 (x :: Bool) :: (Bool ~> Bool) -- or data AndSym1 :: Bool -> (Bool ~> Bool) type instance Apply (AndSym1 x) y = And x y type AndSym2 x y = And x y
AndSym0 is a defunctionalization symbol representing a "fully unapplied"
("completely unsaturated") version of
AndSym1 x is a
defunctionalization symbol representing a "partially applied" version of
--- partially applied to
x (its kind is
AndSym1 :: Bool -> (Bool ~> Bool)).
The application of
x gives you
ghci> :kind! AndSym0 @@ 'False AndSym1 'False
Remember its kind
AndSym0 :: Bool ~> (Bool ~> Bool)
AndSym0 :: Bool ~> Bool ~> Bool): it takes a
Bool, and returns a
Bool ~> Bool defunctionalization symbol.
The application of
AndSym1 x to
y gives you
And x y:
ghci> :kind! AndSym1 'False @@ 'True 'False -- or FalseSym0, which is a synonym for 'False ghci> :kind! AndSym1 'True @@ 'True 'True
A note to remember:
AndSym1 'True is the defunctionalization symbol, and
AndSym1 has kind
Bool -> (Bool ~> Bool), but
AndSym1 'True has kind
Bool ~> Bool --- the kind of a defunctionalization
AndSym1 is a sort of "defunctionalization symbol constructor".
Also note here that we encounter the fact that singletons also provides
"defunctionalization symbols" for "nullary" type functions like
type FalseSym0 = 'False type TrueSym0 = 'True
Just like how it defines
AndSym0 for consistency, as well.
Symbols for type constructors
One extra interesting defunctionalization symbol we can write: we turn lift any type constructor into a "free" defunctionalization symbol:
!!!singletons/Defunctionalization.hs "data TyCon1" "type instance Apply (TyCon1 t)"
Apply instance just applies the type constructor
t to its
ghci> :kind! TyCon1 Maybe @@ Int Maybe Int ghci> :kind! TyCon1 'Right @@ 'False 'Right 'False
We can use this to give a normal
j -> k type constructor to a function that
j ~> k defunctionalization symbol.
Bring Me a Higher Order
Okay, so now we have these tokens that represent "unapplied" versions of functions. So what?
Well, remember the problem with our implementation of
Foldr? We couldn't
pass in a type family, since type families must be passed fully applied. So,
instead of having
Foldr expect a type family...we can make it expect a
defunctionalization symbol instead. Remember, defunctionalization symbols
represent the "unapplied" versions of type families, so they are exactly the
tools we need!
!!!singletons/Defunctionalization.hs "type family Foldr"
The difference is that instead of taking a type family or type constructor
f :: j -> k -> k, we have it take the defunctionalization symbol
f :: j ~> (k ~> k).
Instead of taking a type family or type constructor, we take that dummy type constructor.
Now we just need to have our defunctionalization symbols for
!!!singletons/Defunctionalization.hs "data MergeStateSym0" "data MergeStateSym1" "type MergeStateSym2"
And now we can write
!!!singletons/Defunctionalization.hs "type MergeStateList"
(If you "see"
MergeStateSym0, you should read it was
ghci> :kind! MergeStateList '[ 'Closed, 'Opened, 'Locked ] 'Locked ghci> :kind! MergeStateList '[ 'Closed, 'Opened ] 'Closed
(Note: Unfortunately, we do have to use our our own
Foldr here, that we
just defined, instead of using the one that comes with singletons, because of
some outstanding issues with how the singletons TH processes
alternative implementations of
foldr from Prelude. In general, the issue is
that we should only expect type families to work with singletons if the
definition of the type family perfectly matches the structure of how we
implement our value-level functions like
Singletons to make things nicer
Admittedly this is all a huge mess of boilerplate. The code we had to write
more than tripled, and we also have an unsightly number of defunctionalization
Apply instance boilerplate for every function.
Luckily, the singletons library is here to help. You can just write:
$(singletons [d| data DoorState = Opened | Closed | Locked deriving (Show, Eq, Ord) mergeState :: DoorState -> DoorState -> DoorState mergeState = max foldr :: (a -> b -> b) -> b -> [a] -> b foldr _ z  = z foldr f z (x:xs) = f x (foldr f z xs) mergeStateList :: [DoorState] -> DoorState mergeStateList = foldr mergeState Opened |])
And all of these defunctionalization symbols are generated for you;
singletons is also able to recognize that
foldr is a higher-order function
and translate its lifted version to take a defunctionalization
a ~> b ~> b.
That the template haskell also generates
SingI instances for all of your
defunctionalization symbols, too (more on that in a bit).
It's okay to stay "in the world of singletons" for the most part, and let singletons handle the composition of functions for you. However, it's still important to know what the singletons library generates, because sometimes it's still useful to manually create defunctionalization symbols and work with them.
The naming convention for non-symbolic names (non-operators) like
are just to call them
MyFunctionSym0 for the completely unapplied
MyFunctionSym1 for the type constructor that
expects one argument before returning a defunctionalization symbol,
MyFunctionSym2 for the type constructor that expects two arguments before
returning a defunctionalization symbol, etc.
For operator names like
++, the naming convention is to have
++@#@$ be the
completely unapplied defunctionalization symbol,
++@#@$$ be the type
constructor that expects one argument before returning a defunctionalization
++@#@$$$ be the type constructor that takes two arguments before
returning a defunctionalization symbol, etc.
Another helpful thing that singletons does is that it also generates defunctionalization symbols for type families and type synonyms you define in the Template Haskell, as well --- so if you write
$(singletons [d| type MyTypeFamily (b :: Bool) :: Type where MyTypeFamily 'False = Int MyTypeFamily 'True = String |])
$(singletons [d| type MyTypeSynonym a = (a, [a]) |])
singletons will generate:
data MyTypeFamilySym0 :: Bool ~> Type type instance Apply MyTypeFamilySym0 b = MyTypeFamily b type MyTypeFamilySym1 b = MyTypeFamily b
data MyTypeSynonymSym0 :: Type ~> Type type instance Apply MyTypeSynonym b = MyTypeSynonym a type MyTypeSynonymSym1 a = MyTypeSynonym a
Bringing it All Together
Just to show off the library, remember that singletons also promotes typeclasses?
DoorState is a monoid with respect to merging, we can actually write
and promote a
Monoid instance: (requires singletons-2.5 or higher)
$(singletons [d| instance Semigroup DoorState where (<>) = mergeState instance Monoid DoorState where mempty = Opened mappend = (<>) |])
We can promote
$(singletons [d| fold :: Monoid b => [b] -> b fold  = mempty fold (x:xs) = x <> fold xs |])
And we can write
collapseHallway in terms of those instead :)
!!!singletons/Door4Final.hs "collapseHallway'" "collapseSomeHallway'"
(Note again unfortunately that we have to define our own
fold instead of
using the one from singletons and the
SFoldable typeclass, because of
Thoughts on Symbols
Defunctionalization symbols may feel like a bit of a mess, and the naming convention is arguably less than aesthetically satisfying. But, as you work with them more and more, you start to appreciate them on a deeper level.
At the end of the day, you can compare defunctionalization as turning "functions" into just constructors you can match on, just like any other data or type constructor. That's because they are just type constructors!
In a sense, defining defunctionalization symbols is a lot like working with pattern synonyms of your functions, instead of directly passing the functions themselves. At the type family and type class level, you can "pattern match" on these functions.
For a comparison at the value level -- you can't pattern match on
-- Doesn't work like you think it does invertOperation :: (Double -> Dobule -> Double) -> (Double -> Double -> Double) invertOperation (+) = (-) invertOperation (-) = (+) invertOperation (*) = (/) invertOperation (/) = (*)
You can't quite match on the equality of functions to some list of patterns. But, what you can do is create constructors representing your functions, and match on those.
This essentially fixes the "type lambda problem" of type inference and typeclass resolution. You can't match on arbitrary lambdas, but you can match on dummy constructors representing type functions.
And a bit of the magic here, also, is the fact that you don't always need to make our own defunctionalization symbols from scratch --- you can create them based on other ones in a compositional way. This is the basis of libraries like decidable.
For example, suppose we wanted to build defunctionalization symbols for
MergeStateList. We can actually build them directly from defunctionalization
Check out the defunctionalization symbols for
!!!singletons/Defunctionalization.hs "data FoldrSym0" "data FoldrSym1" "data FoldrSym2" "type FoldrSym3"
We can actually use these to define our
symbols, since defunctionalization symbols are first-class:
!!!singletons/Defunctionalization.hs "type MergeStateListSym0"
And you can just write
collapseHallway :: Hallway ss -> Door (MergeStateListSym0 @@ ss) -- or collapseHallway :: Hallway ss -> Door (FoldrSym2 MergeStateSym0 'Opened @@ ss)
You never have to actually define
MergeStateList as a function or type
The whole time, we're just building defunctionalization symbols in terms of
other defunctionalization symbols. And, at the end, when we finally want to
interpret the complex function we construct, we use
You can think of
FoldrSym2 as defunctionalization
symbol constructors -- they're combinators that take in defunctionalization
MergeStateSym0) and return new ones.
Let's look at a nice tool that is made possible using defunctionalization symbols: dependent pairs. I talk a bit about dependent pairs (or dependent sums) in part 2 of this series, and also in my dependent types in Haskell series.
Essentially, a dependent pair is a tuple where the type of the second
field depends on the value of the first one. This is basically what
data SomeDoor :: Type where MkSomeDoor :: Sing x -> Door x -> SomeDoor
The type of the
Door x depends on the value of the
Sing x, which you
can read as essentially storing the
SomeDoor pretty ad-hoc. But what if we wanted to make some other
predicate? Well, we can make a generic dependent pair by parameterizing it
on the dependence between the first and second field. Singletons provides the
Sigma type, in the Data.Singletons.Sigma module:
data Sigma k :: (k ~> Type) -> Type where (:&:) :: Sing x -> (f @@ x) -> Sigma k f -- also available through fancy type synonym type Σ k = Sigma k
If you squint carefully, you can see that
Sigma k is just
but parameterized over
Door. Instead of always holding
Door x, we can have
it parameterized on an arbitrary function
f and have it hold an
f @@ x.
We can actually define
SomeDoor in terms of
!!!singletons/Door4Final.hs "type SomeDoor" "mkSomeDoor"
TyCon1 is the defunctionalization symbol constructor that turns any
normal type constructor
j -> k into a defunctionalization symbol
j ~> k)
That's because a
Sigma DoorState (TyCon1 Door) contains a
Sing (x :: DoorState) and a
TyCon1 Door @@ x, or a
This is a simple relationship, but one can imagine a
Sigma parameterized on
an even more complex type-level function. We'll explore more of these in the
For some context,
Sigma is an interesting data type (the "dependent sum")
that is ubiquitous in dependently typed programming.
Singletons of Defunctionalization Symbols
One last thing to tie it all together -- let's write
collapseHallway in a way
that we don't know the types of the doors.
Luckily, we now have a
SomeHallway type for free:
!!!singletons/Door4Final.hs "type SomeHallway"
The easy way would be to just use
sMergeStateList that we defined:
But what if we didn't write
sMergeStateList, and we constructed our
defunctionalization symbols from scratch?
!!!singletons/Door4Final.hs "collapseHallway''" collapseSomeHallway'' :: SomeHallway -> SomeDoor collapseSomeHallway'' (ss :&: d) = ??? -- what goes here? :&: collapseHallway'' d
This will be our final defunctionalization lesson. How do we turn a singleton
ss into a singleton of
FoldrSym2 MergeStateSym0 'Opened @@ s ?
First -- we have
Foldr at the value level, as
sFoldr. We glossed over this
earlier, but singletons generates the following function for us:
type family Foldr (f :: j ~> k ~> k) (z :: k) (xs :: [j]) :: k where Foldr f z ' = z Foldr f z (x ': xs) = (f @@ x) @@ Foldr f z xs sFoldr :: Sing (f :: j ~> k ~> k) -> Sing (z :: k) -> Sing (xs :: [j]) -> Sing (Foldr f z xs :: k) sFoldr f z SNil = z sFoldr f z (x `SCons` xs) = (f @@ x) @@ sFoldr f z xs
(@@) :: Sing f -> Sing x -> Sing (f @@ x) (or
applySing) is the
singleton/value-level counterpart of
(@@) (and as we see shortly, the
singFun functions) are all
implemented in terms of
SLambda, the "singleton" for functions. Understanding
the details of the implementation of
SLambda aren't particularly important
for the purposes of this introduction.
So we can write:
collapseSomeHallway'' :: SomeHallway -> SomeDoor collapseSomeHallway'' (ss :&: d) = sFoldr ???? SOpened ss :&: collapseHallwa''y d
But how do we get a
We can use the
singFun family of functions:
singFun2 @MergeStateSym0 sMergeState :: Sing MergeStateSym0
But, also, conveniently, the singletons library generates a
MergeStateSym0, if you defined
mergeState using the singletons
sing :: Sing MergeStateSym0 -- or sing @_ @MergeStateSym0 -- singletons 2.4 sing @MergeStateSym0 -- singletons 2.5
And finally, we get our answer:
Woo! Congratulations, you've made it to the end of the this Introduction to Singletons tetralogy! This last and final part understandably ramps things up pretty quickly, so don't be afraid to re-read it a few times until it all sinks in before jumping into the exercises.
I hope you enjoyed this journey deep into the motivation, philosophy, mechanics, and usage of this great library. Hopefully these toy examples have been able to show you a lot of ways that type-level programming can help your programs today, both in type safety and in writing more expressive programs. And also, I hope that you can also see now how to leverage the full power of the singletons library to make those gains a reality.
There are a few corners of the library we haven't gone over (like the TypeLits- and TypeRep-based singletons -- if you're interested, check out this post where I talk a lot about them), but I'd like to hope as well that this series has equipped you to be able to dive into the library documentation and decipher what it holds, armed with the knowledge you now have. (We also look at TypeLits briefly in the exercises)
You can download the source code here --- [Door4Final.hs][source-final] contains the final versions of all our definitions, and [Defunctionalization.hs] contains all of our defunctionalization-from-scratch work. These are designed as stack scripts that you can load into ghci. Just execute the scripts:
$ ./Door4Final.hs ghci>
And you'll be dropped into a ghci session with all of the definitions in scope.
As always, please try out the exercises, which are designed to help solidify
the concepts we went over here! And if you ever have any future questions,
feel free to leave a comment or find me on twitter or in freenode
#haskell, where I idle as jle`.
Some final things to note before truly embracing singletons: remember that, as a library, singletons was always meant to become obsolete. It's a library that only exists because Haskell doesn't have real dependent types yet.
Dependent Haskell is coming some day! It's mostly driven by one solo man, Richard Eisenberg, but every year buzz does get bigger. In a recent progress report, we do know that we realistically won't have dependent types before 2020. That means that this tutorial will still remain relevant for at least another two years :)
How will things be different in a world of Haskell with real dependent types? Well, for a good guess, take a look at Richard Eisenberg's Dissertation!
One day, hopefully, we won't need singletons to work with types at the value-level; we would just be able to directly pattern match and manipulate the types within the language and use them as first-class values, with a nice story for dependent sums. And some day, I hope we won't need any more dances with defunctionalization symbols to write higher-order functions at the type level --- maybe we'll have a nicer way to work with partially applied type-level functions (maybe they'll just be normal functions?), and we don't need to think any different about higher-order or first-order functions.
So, as a final word --- Happy Haskelling, everyone! May you leverage the great singletons library to its full potential, and may we also all dream of a day where singletons becomes obsolete. But may we all enjoy the wonderful journey along the way.
Until next time!
Here are your final exercises for this series! Start from [this sample source
code][source-final], which has all of the definitions that the exercises and
their solutions require. Just make sure to delete all of the parts after the
-- Exercises comment if you don't want to be spoiled. Remember again to
-Wall to ensure that all of your
functions are total.
!!![solution1]:singletons/Door4Final.hs "-- | 1."1 !!![solution2]:singletons/Door4Final.hs "-- | 2."1 !!![solution3]:singletons/Door4Final.hs "-- | 3."1 !!![solution4]:singletons/Door4Final.hs "-- | 4."1 !!![solution5]:singletons/Door4Final.hs "-- | 5."1 !!![solution6]:singletons/Door4Final.hs "-- | 6."1
Let's try combining type families with proofs! In doing so, hopefully we can also see the value of using dependent proofs to show how we can manipulate proofs as first-class values that the compiler can verify.
Knockablefrom Part 3?
!!!singletons/Door4Final.hs "data Knockable"
Closed and Locked doors are knockable. But, if you merge two knockable doors...is the result also always knockable?
I say yes, but don't take my word for it. Prove it using
mergedIsKnockableis only implementable if the merging of two DoorStates that are knockable is also knockable. See if you can write the implementation!
Write a function to append two hallways together.
appendHallways :: Hallway ss -> Hallway ts -> Hallway ????
from singletons --- implement any type families you might need from scratch!
Remember the important principle that your type family must mirror the implementation of the functions that use it.
Next, for fun, use
!!!singletons/Door4Final.hs "type SomeHallway" "appendSomeHallways"4
Can you use
Sigmato define a door that must be knockable?
To do this, try directly defining the defunctionalization symbol
KnockableDoor :: DoorState ~> Type(or use singletons to generate it for you --- remember that singletons can also promote type families) so that:
type SomeKnockableDoor = Sigma DoorState KnockableDoor
will contain a
Doorthat must be knockable.
Try doing it for both (a) the "dependent proof" version (with the
Knockabledata type) and for (b) the type family version (with the
[Solutions here!][solution3] I gave four different ways of doing it, for a full range of manual vs. auto-promoted defunctionalization symbols and
Hint: Look at the definition of
SomeDoorin terms of
type SomeDoor = Sigma DoorState (TyCon1 Door)
Hint: Try having
KnockableDoorreturn a tuple.
Using this, you can use
Sigmato create a predicate that a given
Natnumber is even:
data IsHalfOf :: Nat -> Nat ~> Type type instance Apply (IsHalfOf n) m = n :~: (m * 2) type IsEven n = Sigma Nat (IsHalfOf n)
(*)is multiplication from the Data.Singletons.Prelude.Num module. (You must have the -XNoStarIsType extension on for this to work in GHC 8.6+), and
:~:is the predicate of equality from Part 3:
data (:~:) :: k -> k -> Type where Refl :: a :~: a
(It's only possible to make a value of type
a :~: busing
Refl :: a :~: a, so it's only possible to make a value of that type when
bare equal. I like to use
Reflwith type application syntax, like
Refl @a, so it's clear what we are saying is the same on both sides;
Refl @a :: a :~: a)
The only way to construct an
IsEven nis to provide a number
m * 2is
n. We can do this by using
SNat @m, which is the singleton constructor for the
Natkind (just like how
SFalseare the singleton constructors for the
tenIsEven :: IsEven 10 tenIsEven = SNat @5 :&: Refl @10 -- Refl is the constructor of type n :~: (m * 2) -- here, we use it as Refl @10 :: 10 :~: 10 -- won't compile sevenIsEven :: IsEven 10 sevenIsEven = SNat @4 :&: Refl -- won't compile, because we need something of type `(4 * 2) :~: 7`, -- but Refl must have type `a :~: a`; `8 :~: 7` is not constructable -- using `Refl`. Neither `Refl @8` nor `Refl @7` will work.
Write a similar type
IsOdd nthat can only be constructed if
type IsOdd n = Sigma Nat (???? n)
And construct a proof that
On a sad note, one exercise I'd like to be able to add is to ask you to write decision functions and proofs for
Natis not rich enough to support this out of the box without a lot of extra tooling!
A common beginner Haskeller exercise is to implement
mapin terms of
map :: (a -> b) -> [a] _> [b] map f = foldr ((:) . f) 
Let's do the same thing at the type level, manually.
Directly implement a type-level
Map, with kind
(j ~> k) -> [j] -> [k], in terms of
type Map f xs = Foldr ???? ???? xs
Try to mirror the value-level definition, passing in
(:) . f, and use the promoted version of
(.)from the singletons library, in Data.Singletons.Prelude. You might find
SomeHallwayfrom a list of
!!!singletons/Door4Final.hs "type SomeDoor" "type SomeHallway" "mkSomeHallway"1
Remember that the singleton constructors for list are
I am very humbled to be supported by an amazing community, who make it possible for me to devote time to researching and writing these posts. Very special thanks to my two supporters at the "Amazing" level on patreon, Sam Stites and Josh Vera! :)
Thanks also to Koz Ross for helping proofread this post!