Singletons of singletons

[RyanGlScott]

Can you single a singleton? Currently the answer is "no", since there's no Sing instances for Sings. But should there be? Recently, I found myself wanting something like this when trying to write a Sing instance for Sigma. As a refresher, here's the definition of Sigma:

data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t

Here's what a Sing instance for Sigma ought to look like:

data instance Sing :: forall s (t :: s ~> Type). Sigma s t -> Type where
  (:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst).
            Sing sfst -> Sing snd -> Sing (sfst :&: snd :: Sigma s t)

However, notice that we have a field of type Sing (sfst :: Sing fst)—a singleton of a singleton! Thus, while you can define a Sing instance for Sigma, it's currently impossible to use in practice, since you can't reasonably construct things of type Sing (sfst :: Sing fst).

I used to think that in order to make this work, I had to define instances like this:

data instance Sing :: forall (b :: Bool). Sing b -> Bool where
  SSFalse :: Sing SFalse
  SSTrue  :: Sing STrue

This is unfortunate, since:

1. This would require essentially doubling the number of Sing instances in use today. Plus, if we ever needed a singleton of a singleton of a singleton (e.g., SSSFalse), then we'd need to triple the number of Sing instances in use, and so on.
2. As of GHC 8.6, you can't actually promote data family instance constructors to the type level, so that makes this entire plan impossible.

However, there is another way forward here. You can define a single instance (no pun intended) for all Sings like this:

newtype instance Sing :: forall k (a :: k). Sing a -> Type where
  SSing :: forall k (a :: k) (s :: Sing a). Sing a -> Sing s
type SSing = (Sing :: Sing (a :: k) -> Type)

That's it! Now you can profitably use the Sing instance for Sigma like so:

type family ProjSigma1 (sig :: Sigma s t) :: s where
  ProjSigma1 ((_ :: Sing fst) :&: _) = fst

projSigma2 :: forall s t (sig :: Sigma s t).
              SingKind (t @@ ProjSigma1 sig)
           => Sing sig -> Demote (t @@ ProjSigma1 sig)
projSigma2 (_ :%&: b) = fromSing b

example :: IO ()
example =
  let f :: Sing (sb :: Sing False) -> Sing (sb :&: True :: Sigma Bool (ConstSym1 Bool))
      f sb = sb :%&: STrue
  in print $ projSigma2 $ f $ SSing SFalse

As you can see in that code snippet, one nice advantage of this is that we can define projSigma2 in essentially the same way that real dependently typed languages do (instead of the Church-style elimination definition that we're forced to use currently).

---

Now that I've extolled the virtues of this idea, it's time to mention the drawbacks. In particular, this whole trick relies on the fact that Sing is currently a data family. However, if we were to make Sing a type family, as proposed in #318, then we would run into GHC limitations. To see why, consider the Sing-as-a-type-family equivalent of the Sing instance for Sings:

type instance Sing = (Sing :: Sing (a :: k) -> Type)

If you compile this, then GHC will give up:

$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive -fprint-explicit-kinds Bug.hs
GHCi, version 8.7.20181007: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:42:15: error:
    • Illegal type synonym family application ‘Sing k’ in instance:
        Sing (Sing k a)
    • In the type instance declaration for ‘Sing’
   |
42 | type instance Sing = (Sing :: Sing (a :: k) -> Type)
   |               ^^^^

Blast, foiled by Trac #12564 once again. Unfortunately, I don't know how to work around this, which means that if we switch Sing over to become a type family, then this idea is imperiled.

[int-index]

We will fix Trac #12564 sooner or later. Perhaps we should keep Sing a data family until we do?

[RyanGlScott]

We will fix Trac #12564 sooner or later.

I certainly hope so! But my understanding is that it's blocked on Trac #14119, which is a monstrously large refactoring that doesn't appear to have made much progress since the ticket was opened a year ago.

Perhaps we should keep Sing a data family until we do?

That's one option, I suppose. It might also be the case that there's a better way to make a Sing instance for Sigma than what I'm proposing, which would obviate the need for SSing altogether. But I certainly can't think of any alternatives to this design at the moment.

[RyanGlScott]

It turns out that there you can work around Trac #12564 here if you're willing to apply some elbow grease. The trick is not to define type Sing = (Sing :: Sing a -> Type), but rather an instance for a newtype wrapper around Sing:

newtype WrappedSing (a :: k) = WrapSing (Sing a)
newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where
  SWrapSing :: forall k (a :: k) (ws :: WrappedSing a).
               Sing a -> SWrappedSing ws
type instance Sing = SWrappedSing

With this, we can tweak the definition of SSigma slightly:

data SSigma :: forall s (t :: s ~> Type). Sigma s t -> Type where
  (:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst).
            Sing (WrapSing sfst) -> Sing snd -> SSigma (sfst :&: snd :: Sigma s t)

Notice that the first field is now of type Sing @(WrappedSing fst) (WrapSing sfst) instead of Sing @(Sing fst) sfst. This is essentially the entire trick, as now we're dealing with a singleton type for a plain old newtype instead of a type family. Here is what the example looks like with this design:

example :: IO ()
example =
  let f :: Sing (SFalse :&: True :: Sigma Bool (ConstSym1 Bool))
      f = SWrapSing SFalse :%&: STrue
  in print $ projSigma2 f

And it works! The downside of this hack is that instead of being able to just use Sing s (where s it iself a singleton), one needs to apply WrapSing/SWrapSing n number of times if you want a singleton type that's n Sings deep. That being said, I doubt most people will ever need to go beyond Sing (WrapSing s), so perhaps this wouldn't be that annoying in practice.

[RyanGlScott]

For the sake of posterity, I'd like to also make mention of an alternative way to solve the singletons-of-singletons problem that doesn't make use of SWrappedSing. This technique was adapted from this StackOverflow question (and answer). The general idea is to have a type family that lifts regular data constructors to their singleton counterparts:

type family ToSing (a :: k) :: Sing a

Here are some examples of ToSing instances:

data SBool :: Bool -> Type where
  SFalse :: SBool False
  STrue  :: SBool True
type instance Sing = SBool

$(pure [])
type instance ToSing False = SFalse
type instance ToSing True  = STrue

data SList :: forall a. [a] -> Type where
  SNil  :: SList '[]
  SCons :: Sing x -> Sing xs -> SList (x:xs)
type instance Sing = SList

$(pure [])
type instance ToSing '[]    = SNil
type instance ToSing (x:xs) = SCons (ToSing x) (ToSing xs)

(Yes, those $(pure []) splices are required. More on this in a second.)

Now, any time you feel the need to reach for a singleton of a singleton, you can instead use ToSing to take your type-level thing and lift it to a type-level singleton. For instance, here is how you would now define the singleton for Sigma:

data SSigma :: forall s (t :: s ~> Type). Sigma s t -> Type where
  (:%&:) :: forall s t (fst :: s) (snd :: t @@ fst).
            Sing fst -> Sing snd -> SSigma (ToSing fst :&: snd :: Sigma s t)

example :: IO ()
example =
  let f :: Sing (SFalse :&: True :: Sigma Bool (ConstSym1 Bool))
      f = SFalse :%&: STrue
  in print $ projSigma2 f

Notice that we no longer need to wrap the first field of (:%&:) with SWrapSing, as ToSing takes care of the heavy lifting for us.

---

At this point, you're probably wondering: what's the catch? From a quick glance, ToSing comes has two major drawbacks that make it unsuitable for use in singletons (at least, at present):

1. Due to Trac #12088, one has to use explicit Template Haskell splices (such as the $(pure [])s in my code above) in order to define ToSing instances alongside the singletons themselves. This makes it extremely annoying to use in practice.
2. It's unclear how one would define ToSing instances for Nat, Symbol, and (~>). It might well be impossible, in fact. I'm also not sure how one would define a ToSing instance for a type like Sigma, although perhaps we'd need to fix Promote GADTs #150 before that is possible.

For these reasons, I'm still of the belief that WrappedSing has a useful role to play.

[RyanGlScott]

I'm forced to take back what I said in #366 (comment): ToSing might be needed after all to make (S)WrappedSing work. The reason I say this is because I realized recently that SWrappedSing doesn't really work as advertised. To see why, consider the following example from #460:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Control.Monad.Trans.Class
import Data.Singletons.TH
import Data.Singletons.TH.Options

$(withOptions defaultOptions{genSingKindInsts = False} $
  singletons $ lift [d|
    data Nat = Z | S Nat
    data Vec n a where
      VNil  :: Vec 'Z a
      (:::) :: a -> Vec n a -> Vec ('S n) a
  |])

vReplicate :: SNat n -> a -> Vec n a
vReplicate SZ _ = VNil
vReplicate (SS n) x = x ::: vReplicate n x

What would a singled version of vReplicate look like if WrappedSing were used? First, we would need to define a promoted version of VReplicate, which is straightforward:

type VReplicate :: SNat n -> a -> Vec n a
type family VReplicate sn x where
  VReplicate SZ     _ = VNil
  VReplicate (SS n) x = x ::: VReplicate n x

Things get trickier when we try to define sVReplicate. We end up stumbling over on the first equation:

sVReplicate :: forall n a (sn :: SNat n) (x :: a).
               Sing ('WrapSing sn) -> Sing x -> Sing (VReplicate sn x)
sVReplicate (SWrapSing SZ) _ = SVNil
-- sVReplicate (SWrapSing (SS sn)) sx = ...

This fails to typecheck with:

Foo.hs:35:32: error:
    • Could not deduce: VReplicate sn x ~ 'VNil
      from the context: n ~ 'Z
        bound by a pattern with constructor: SZ :: SNat 'Z,
                 in an equation for ‘sVReplicate’
        at Foo.hs:35:24-25
      Expected type: Sing (VReplicate sn x)
        Actual type: SVec 'VNil
    • In the expression: SVNil
      In an equation for ‘sVReplicate’:
          sVReplicate (SWrapSing SZ) _ = SVNil
    • Relevant bindings include
        sVReplicate :: Sing ('WrapSing sn)
                       -> Sing x -> Sing (VReplicate sn x)
          (bound at Foo.hs:35:1)
   |
35 | sVReplicate (SWrapSing SZ) _ = SVNil
   |                                ^^^^^

Eek! It turns out that matching on SWrapSing SZ only brings into scope evidence that n ~ Z, but not evidence that sn ~ SZ. Put another way, SWrappedSing (sn :: Sing n) works as a singleton type for n, but not for sn.

How can we repair SWrappedSing so that the example above typechecks? The only way I've figured out thus far is to bring back ToSing from #366 (comment):

type ToSing :: forall k. forall (a :: k) -> Sing a
type family ToSing a

type WrappedSing :: k -> Type
newtype WrappedSing a where
  WrapSing :: forall k (a :: k). Sing a -> WrappedSing a

type SWrappedSing :: forall k (a :: k). WrappedSing a -> Type
data SWrappedSing ws where
  SWrapSing :: forall k (a :: k). Sing a -> SWrappedSing (WrapSing (ToSing a))
type instance Sing = SWrappedSing

Notice that SWrappedSing is no longer a newtype, as the return type of SWrapSing is now SWrappedSing (WrapSing (ToSing a)). The use of ToSing is crucial so that pattern matching on SWrapSing (x :: Sing z) brings into scope evidence that Sing z is equal to ToSing x. Next, we define a ToSing instance for Nats:

type ToSingNat :: forall (n :: Nat) -> SNat n
type family ToSingNat n where
  ToSingNat Z     = SZ
  ToSingNat (S n) = SS (ToSingNat n)
type instance ToSing n = ToSingNat n

Finally, we can define a working version of sVReplicate:

sVReplicate :: forall n a (sn :: SNat n) (x :: a).
               Sing ('WrapSing sn) -> Sing x -> Sing (VReplicate sn x)
sVReplicate (SWrapSing SZ)      _  = SVNil
sVReplicate (SWrapSing (SS sn)) sx = sx :%:: sVReplicate (SWrapSing sn) sx

It works! Or does it? We have lost some things along the way:

1. My original goal was to avoid having to define Sing instances for every singleton type. While that is technically true in the small example above, we now need to define a ToSing instance instead, which is almost like defining a singleton anyway. Moreover, if we wanted to single sVReplicate, we would have to define another ToSing instance for SNat, which in turn would require defining an SSNat type! In this sense, we're back to where we started.

2. If we're going to bother with introducing a ToSing type family, do we really even need WrappedSing? Note that sVReplicate can equivalently be defined like so:

   sVReplicateAux :: forall n a (x :: a).
                     SNat n -> Sing x -> Sing (VReplicate (ToSing n) x)
   sVReplicateAux SZ      _  = SVNil
   sVReplicateAux (SS sn) sx = sx :%:: sVReplicateAux sn sx
   
   sVReplicate :: forall n a (sn :: SNat n) (x :: a).
                  Sing ('WrapSing sn) -> Sing x -> Sing (VReplicate sn x)
   sVReplicate (SWrapSing sn) sx = sVReplicateAux sn sx

   But then again, sVReplicateAux is arguably a cleaner way to define sVReplicate in the first place, as it doesn't require sprinkling uses of SWrapSing all over the place. Perhaps this is a sign that SWrapSing isn't that useful to begin with? I'm not sure.

Something is not quite right with the current design. I'm not quite sure what the right fix is yet, but in the meantime, I'll reopen this issue to invite further discussion.

[RyanGlScott]

This is slightly tangential to the discussion at hand, but assuming that we do introduce a ToSing type family, do we also need a FromSing type family? Actually, we don't—we can get away with making FromSing an ordinary type synonym:

type FromSing :: forall k (a :: k). Sing a -> k
type FromSing (x :: Sing a) = a

This is an interesting observation that I hadn't seen made anywhere before. The closest thing I found was @goldfirere's earlier prototypes of ToSing (which he called "Singleton") here and here. These also feature FromSing, but as an associated type family rather than a type synonym.

[RyanGlScott]

OK, back to the discussion at hand. Another factor to consider in the singletons-of-singletons debate is that in certain situations, you don't need singletons-of-singletons at all. For instance, #460 (comment) observes that given the function below:

vReplicate :: SNat n -> a -> Vec n a
vReplicate SZ _ = VNil
vReplicate (SS n) x = x ::: vReplicate n x

You can successfully single it without ever needing anything like ToSing (x :: Nat) or SSNat:

type VReplicate :: forall a. forall n -> a -> Vec n a
type family VReplicate n a where
  VReplicate 'Z _ = 'VNil
  VReplicate ('S n) x = x '::: VReplicate n x

sVReplicate :: SNat n -> Sing (x :: a) -> SVec (VReplicate n x)
sVReplicate SZ _ = SVNil
sVReplicate (SS n) x = x :%:: sVReplicate n x

Perhaps this can offer a more appealing alternative to ToSing and/or WrappedSing. However, it is not quite feasible in today's GHC for the same reasons as I originally opened this issue for: Sigma. Recall that Sigma is defined like so:

type Sigma :: forall s -> (s ~> Type) -> Type
data Sigma s t where
  (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t

If we wanted to promote this without defining a singleton for Sing (fst :: s), we'd have to do something like this:

type PSigma :: forall s -> (s ~> Type) -> Type
data PSigma s t where
  (:^&:) :: forall s t. forall (fst :: s) -> t @@ fst -> PSigma s t

Unfortunately, this won't work, since today's GHC does not permit visible dependent quantification in data constructor types. Until the day arrives where this is possible, there is still a need for a way to single other singletons.