| Copyright | (C) 2017 Ryan Scott |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Ryan Scott |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Singletons.ShowSing
Description
The ShowSing type
class (forall (z :: k). ShowSing' z) => ShowSing k Source #
In addition to the promoted and singled versions of the Show class that
singletons provides, it is also useful to be able to directly define
Show instances for singleton types themselves. Doing so is almost entirely
straightforward, as a derived Show instance does 90 percent of the work.
The last 10 percent—getting the right instance context—is a bit tricky, and
that's where ShowSing comes into play.
As an example, let's consider the singleton type for lists. We want to write an instance with the following shape:
instance ??? =>Show(SList(z :: [k])) where showsPrec pSNil= showString "SNil" showsPrec p (SConssx sxs) = showParen (p > 10) $ showString "SCons " . showsPrec 11 sx . showSpace . showsPrec 11 sxs
To figure out what should go in place of ???, observe that we require the
type of each field to also be Show instances. In other words, we need
something like (. But this isn't quite right, as the
type variable Show (Sing (a :: k)))a doesn't appear in the instance head. In fact, this a
type is really referring to an existentially quantified type variable in the
SCons constructor, so it doesn't make sense to try and use it like this.
Luckily, the QuantifiedConstraints language extension provides a solution
to this problem. This lets you write a context of the form
(forall a. , which demands that there be an instance
for Show (Sing (a :: k)))Show (Sing (a :: k))a.
This lets us write something closer to this:
instance (forall a.Show(Sing(a :: k))) =>SList(Sing(z :: [k])) where ...
The ShowSing class is a thin wrapper around
(forall a. . With Show (Sing (a :: k)))ShowSing, our final instance
declaration becomes this:
instanceShowSingk =>Show(SList(z :: [k])) where showsPrec pSNil= showString "SNil" showsPrec p (SCons(sx ::Singx) (sxs ::Singxs)) = (showParen (p > 10) $ showString "SCons " . showsPrec 11 sx . showSpace . showsPrec 11 sxs) :: (ShowSing' x, ShowSing' xs) => ShowS
(Note that the actual definition of ShowSing is slightly more complicated
than what this documentation might suggest. For the full story, as well as
an explanation of why we need an explicit
(ShowSing' x, ShowSing' xs) => ShowS signature at the end,
refer to the documentation for ShowSing`.)
When singling a derived Show instance, singletons will also generate
a Show instance for the corresponding singleton type using ShowSing.
In other words, if you give singletons a derived Show instance, then
you'll receive the following in return:
- A promoted (
PShow) instance - A singled (
SShow) instance - A
Showinstance for the singleton type
What a bargain!
Instances
| (forall (z :: k). ShowSing' z) => ShowSing k Source # | |
Defined in Data.Singletons.ShowSing | |
Internal utilities
class Show (Sing z) => ShowSing' z Source #
The workhorse that powers ShowSing. The only reason that ShowSing`
exists is to work around GHC's inability to put type families in the head
of a quantified constraint (see
this GHC issue for more
details on this point). In other words, GHC will not let you define
ShowSing like so:
class (forall (z :: k).Show(Singz)) =>ShowSingk
By replacing Show (Sing z)ShowSing' z, we are able to avoid
this restriction for the most part. There is one major downside to using
ShowSing', however: deriving Show instances for singleton types does
not work out of the box. In other words, if you try to do this:
deriving instanceShowSingk =>Show(SList(z :: [k]))
Then GHC will complain to the effect that it could not deduce a
Show (Sing x)ShowSing kShow (Sing (x :: k))
instanceShowSingk =>Show(SList(z :: [k])) where showsPrec pSNil= showString "SNil" showsPrec p (SCons(sx ::Singx) (sxs ::Singxs)) = (showParen (p > 10) $ showString "SCons " . showsPrec 11 sx . showSpace . showsPrec 11 sxs) :: (ShowSing' x, ShowSing' xs) => ShowS
The use of ShowSing' x in the signature is sufficient to make the
constraint solver connect the dots between ShowSing kShow (Sing (x :: k))ShowSing' xs constraint is not strictly
necessary, but it is shown here since that is in fact the code that
singletons will generate for this instance.)
Because deriving will not insert these explicit signatures for us,
it is not possible to derive ShowShow instances for singleton types.
Thankfully, singletons' Template Haskell machinery can do this manual
gruntwork for us 99% of the time, but if you ever find yourself in a
situation where you must define a Show instance for a singleton type by
hand, this is important to keep in mind.
Note that there is one potential future direction that might alleviate this
pain. We could define ShowSing` like this instead:
class (forall sing. sing ~Sing=>Show(sing z)) => ShowSing' z instanceShow(Singz) => ShowSing' z
For many examples, this lets you just derive Show instances for singleton
types like you would expect. Alas, this topples over on Bar in the
following example:
newtype Foo a = MkFoo a data SFoo :: forall a. Foo a -> Type where SMkFoo :: Sing x -> SFoo (MkFoo x) type instance Sing = SFoo deriving instance ShowSing a => Show (SFoo (z :: Foo a)) newtype Bar a = MkBar (Foo a) data SBar :: forall a. Bar a -> Type where SMkBar :: Sing x -> SBar (MkBar x) type instance Sing = SBar deriving instance ShowSing (Foo a) => Show (SBar (z :: Bar a))
This fails because
of—you guessed it—another GHC bug.
Bummer. Unless that bug were to be fixed, the current definition of
ShowSing` is the best that we can do.