singletons-2.6: A framework for generating singleton types

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

Contents

- The `ShowSing` type
- Internal utilities
- Orphan instances

Description

Defines the class `ShowSing` type synonym, which is useful for defining `Show` instances for singleton types.

Synopsis

- class (forall (z :: k). ShowSing' z) => ShowSing k
- class Show (Sing z) => ShowSing' z

# 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 p SNil = showString "SNil"
      showsPrec p (SCons sx 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 `(`Show` (`Sing` (a :: k)))`. But this isn't quite right, as the type variable `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. `Show` (`Sing` (a :: k)))`, which demands that there be an instance for ``Show` (`Sing` (a :: k))` that is parametric in the use of `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. `Show` (`Sing` (a :: k)))`. With `ShowSing`, our final instance declaration becomes this:

    instance ShowSing k => Show (SList (z :: [k])) where
      showsPrec p SNil = showString "SNil"
      showsPrec p (SCons (sx :: Sing x) (sxs :: Sing xs)) =
        (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 `Show` instance for the singleton type

What a bargain!

#### Instances

Instances details

(forall (z :: k). ShowSing' z) => ShowSing k Source # |
Instance details 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 (Sing z)) => ShowSing k

By replacing ``Show` (`Sing` z)` with `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 instance ShowSing k => Show (SList (z :: [k]))

Then GHC will complain to the effect that it could not deduce a ``Show` (`Sing` x)` constraint. This is due to another unfortunate GHC bug that prevents GHC from realizing that ``ShowSing` k` implies ``Show` (`Sing` (x :: k))`. The workaround is to force GHC to come to its senses by using an explicit type signature:

    instance ShowSing k => Show (SList (z :: [k])) where
      showsPrec p SNil = showString "SNil"
      showsPrec p (SCons (sx :: Sing x) (sxs :: Sing xs)) =
        (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` k` and ``Show` (`Sing` (x :: k))`. (The `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 `Show`` will not insert these explicit signatures for us, it is not possible to derive `Show` 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
    instance Show (Sing z) => 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.

#### Instances

Instances details

Show (Sing z) => ShowSing' (z :: k) Source # |
Instance details Defined in Data.Singletons.ShowSing

# Orphan instances

Show (STuple0 z) Source # |
Instance details Methods showsPrec :: Int -> STuple0 z -> ShowS show :: STuple0 z -> String showList :: [STuple0 z] -> ShowS
Show (SOrdering z) Source # |
Instance details Methods showsPrec :: Int -> SOrdering z -> ShowS show :: SOrdering z -> String showList :: [SOrdering z] -> ShowS
Show (SBool z) Source # |
Instance details Methods showsPrec :: Int -> SBool z -> ShowS show :: SBool z -> String showList :: [SBool z] -> ShowS
Show (SVoid z) Source # |
Instance details Methods showsPrec :: Int -> SVoid z -> ShowS show :: SVoid z -> String showList :: [SVoid z] -> ShowS
Show (SSymbol s) Source # |
Instance details Methods showsPrec :: Int -> SSymbol s -> ShowS show :: SSymbol s -> String showList :: [SSymbol s] -> ShowS
Show (SNat n) Source # |
Instance details Methods showsPrec :: Int -> SNat n -> ShowS show :: SNat n -> String showList :: [SNat n] -> ShowS
ShowSing k => Show (WrappedSing a) Source # |
Instance details Methods showsPrec :: Int -> WrappedSing a -> ShowS show :: WrappedSing a -> String showList :: [WrappedSing a] -> ShowS
ShowSing a => Show (SIdentity z) Source # |
Instance details Methods showsPrec :: Int -> SIdentity z -> ShowS show :: SIdentity z -> String showList :: [SIdentity z] -> ShowS
(ShowSing a, ShowSing [a]) => Show (SNonEmpty z) Source # |
Instance details Methods showsPrec :: Int -> SNonEmpty z -> ShowS show :: SNonEmpty z -> String showList :: [SNonEmpty z] -> ShowS
(ShowSing a, ShowSing [a]) => Show (SList z) Source # |
Instance details Methods showsPrec :: Int -> SList z -> ShowS show :: SList z -> String showList :: [SList z] -> ShowS
ShowSing a => Show (SMaybe z) Source # |
Instance details Methods showsPrec :: Int -> SMaybe z -> ShowS show :: SMaybe z -> String showList :: [SMaybe z] -> ShowS
ShowSing k => Show (SWrappedSing ws) Source # |
Instance details Methods showsPrec :: Int -> SWrappedSing ws -> ShowS show :: SWrappedSing ws -> String showList :: [SWrappedSing ws] -> ShowS
(ShowSing a, ShowSing b) => Show (STuple2 z) Source # |
Instance details Methods showsPrec :: Int -> STuple2 z -> ShowS show :: STuple2 z -> String showList :: [STuple2 z] -> ShowS
(ShowSing a, ShowSing b) => Show (SEither z) Source # |
Instance details Methods showsPrec :: Int -> SEither z -> ShowS show :: SEither z -> String showList :: [SEither z] -> ShowS
(ShowSing a, ShowSing b, ShowSing c) => Show (STuple3 z) Source # |
Instance details Methods showsPrec :: Int -> STuple3 z -> ShowS show :: STuple3 z -> String showList :: [STuple3 z] -> ShowS
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (STuple4 z) Source # |
Instance details Methods showsPrec :: Int -> STuple4 z -> ShowS show :: STuple4 z -> String showList :: [STuple4 z] -> ShowS
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (STuple5 z) Source # |
Instance details Methods showsPrec :: Int -> STuple5 z -> ShowS show :: STuple5 z -> String showList :: [STuple5 z] -> ShowS
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (STuple6 z) Source # |
Instance details Methods showsPrec :: Int -> STuple6 z -> ShowS show :: STuple6 z -> String showList :: [STuple6 z] -> ShowS
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (STuple7 z) Source # |
Instance details Methods showsPrec :: Int -> STuple7 z -> ShowS show :: STuple7 z -> String showList :: [STuple7 z] -> ShowS