Some API additions and reorganization for Data.Singletons.Sigma (#400)

* `SSigma`, the singleton type for `Sigma`, has been added.
  This fixes #366.
* A `Show` instance has been added for `Sigma` (and `SSigma`) by
  using copious amounts of quantified constraints. The behavior of
  these instances closely resembles the `Show` implementation for
  `DPair` in Idris' standard library:
  https://github.com/idris-lang/Idris-dev/blob/dbe521ff74189df85121abe454f86894de7fd75c/libs/prelude/Prelude/Show.idr#L195-L196
* New functions `fstSigma` and `sndSigma` (as well as their
  type-level counterparts) have been added. To avoid being a
  duplicate of `fstSigma`, `projSigma1` has been redefined to have a
  new type signature that uses continuation-passing style, much like
  its cousin `projSigma2`.
* New functions `currySigma` and `uncurrySigma` have been added. This
  fixes #359 and supersedes #360.

CHANGES.md

@@ -121,15 +121,31 @@ Changelog for singletons project
   As a result, `singletons` no longer generates instances for `SingI` instances
   for applications of `TyCon{N}` to particular type constructors, as they have
   been superseded by the instances above.
-* Redefine `Σ` such that it is now a partial application of `Sigma`, like so:
+* Changes to `Data.Singletons.Sigma`:
+  * `SSigma`, the singleton type for `Sigma`, is now defined.
+  * New functions `fstSigma`, `sndSigma`, `FstSigma`, `SndSigma`, `currySigma`,
+    and `uncurrySigma` have been added. A `Show` instance for `Sigma` has also
+    been added.
+  * `projSigma1` has been redefined to use continuation-passing style to more
+    closely resemble its cousin `projSigma2`. The new type signature of
+    `projSigma1` is:
+
+    ```hs
+    projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r
+    ```
 
-  ```haskell
-  type Σ = Sigma
-  ```
+    The old type signature of `projSigma1` can be found in the `fstSigma`
+    function.
+  * `Σ` has been redefined such that it is now a partial application of
+    `Sigma`, like so:
+
+    ```haskell
+    type Σ = Sigma
+    ```
 
-  One benefit of this change is that one no longer needs defunctionalization
-  symbols in order to partially apply `Σ`. As a result, `ΣSym0`, `ΣSym1`,
-  and `ΣSym2` have been removed.
+    One benefit of this change is that one no longer needs defunctionalization
+    symbols in order to partially apply `Σ`. As a result, `ΣSym0`, `ΣSym1`,
+    and `ΣSym2` have been removed.
 * In line with corresponding changes in `base-4.13`, the `Fail`/`sFail` methods
   of `{P,S}Monad` have been removed in favor of new `{P,S}MonadFail` classes
   introduced in the `Data.Singletons.Prelude.Monad.Fail` module. These classes

src/Data/Singletons/ShowSing.hs

@@ -268,12 +268,17 @@ ultimately went with.
 -}
 
 ------------------------------------------------------------
--- WrappedSing instance
+-- (S)WrappedSing instances
 ------------------------------------------------------------
 
 instance ShowSing k => Show (WrappedSing (a :: k)) where
-  showsPrec p (WrapSing s) =
-    showParen (p > 10) $ showString "WrapSing " . showsPrec 11 s
+  showsPrec p (WrapSing s) = showParen (p >= 11) $
+    showString "WrapSing {unwrapSing = " . showsPrec 0 s . showChar '}'
+      :: ShowSing' a => ShowS
+
+instance ShowSing k => Show (SWrappedSing (ws :: WrappedSing (a :: k))) where
+  showsPrec p (SWrapSing s) = showParen (p >= 11) $
+    showString "SWrapSing {sUnwrapSing = " . showsPrec 0 s . showChar '}'
       :: ShowSing' a => ShowS
 
 ------------------------------------------------------------

src/Data/Singletons/Sigma.hs

@@ -1,12 +1,18 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ImpredicativeTypes #-} -- See Note [Impredicative Σ?]
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -22,18 +28,34 @@
 ----------------------------------------------------------------------------
 
 module Data.Singletons.Sigma
-    ( Sigma(..), Σ
+    ( -- * The 'Sigma' type
+      Sigma(..), Σ
+    , Sing, SSigma(..), SΣ
+
+      -- * Operations over 'Sigma'
+    , fstSigma, FstSigma, sndSigma, SndSigma
     , projSigma1, projSigma2
     , mapSigma, zipSigma
+    , currySigma, uncurrySigma
+
+      -- * Internal utilities
+      -- $internalutilities
+    , ShowApply,  ShowSingApply
+    , ShowApply', ShowSingApply'
     ) where
 
 import Data.Kind (Type)
 import Data.Singletons.Internal
+import Data.Singletons.ShowSing
 
 -- | A dependent pair.
 data Sigma (s :: Type) :: (s ~> Type) -> Type where
   (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t
 infixr 4 :&:
+instance (ShowSing s, ShowApply t) => Show (Sigma s t) where
+  showsPrec p ((a :: Sing (fst :: s)) :&: b) = showParen (p >= 5) $
+    showsPrec 5 a . showString " :&: " . showsPrec 5 b
+      :: (ShowSing' fst, ShowApply' t fst) => ShowS
 
 -- | Unicode shorthand for 'Sigma'.
 type Σ = Sigma
@@ -48,20 +70,54 @@ case, and the only reason that GHC currently requires this is due to Trac
 ImpredicativeTypes.
 -}
 
+-- | The singleton type for 'Sigma'.
+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)
+infixr 4 :%&:
+
+type instance Sing = SSigma
+instance forall s (t :: s ~> Type) (sig :: Sigma s t).
+         (ShowSing s, ShowSingApply t)
+      => Show (SSigma sig) where
+  showsPrec p ((sa :: Sing ('WrapSing (sfst :: Sing fst))) :%&: (sb :: Sing snd)) =
+    showParen (p >= 5) $
+      showsPrec 5 sa . showString " :&: " . showsPrec 5 sb
+        :: (ShowSing' fst, ShowSingApply' t fst snd) => ShowS
+
+instance forall s t (fst :: s) (a :: Sing fst) (b :: t @@ fst).
+       (SingI fst, SingI b)
+    => SingI (a ':&: b :: Sigma s t) where
+  sing = sing :%&: sing
+
+-- | Unicode shorthand for 'SSigma'.
+type SΣ = SSigma
+
+-- | Project the first element out of a dependent pair.
+fstSigma :: forall s t. SingKind s => Sigma s t -> Demote s
+fstSigma (a :&: _) = fromSing a
+
 -- | Project the first element out of a dependent pair.
-projSigma1 :: forall s t. SingKind s => Sigma s t -> Demote s
-projSigma1 (a :&: _) = fromSing a
+type family FstSigma (sig :: Sigma s t) :: s where
+  FstSigma ((_ :: Sing fst) ':&: _) = fst
 
 -- | Project the second element out of a dependent pair.
---
--- In an ideal setting, the type of 'projSigma2' would be closer to:
---
--- @
--- 'projSigma2' :: 'Sing' (sig :: 'Sigma' s t) -> t @@ ProjSigma1 sig
--- @
---
--- But promoting 'projSigma1' to a type family is not a simple task. Instead,
--- we do the next-best thing, which is to use Church-style elimination.
+sndSigma :: forall s t (sig :: Sigma s t).
+            SingKind (t @@ FstSigma sig)
+         => SSigma sig -> Demote (t @@ FstSigma sig)
+sndSigma (_ :%&: b) = fromSing b
+
+-- | Project the second element out of a dependent pair.
+type family SndSigma (sig :: Sigma s t) :: t @@ FstSigma sig where
+  SndSigma (_ ':&: b) = b
+
+-- | Project the first element out of a dependent pair using
+-- continuation-passing style.
+projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r
+projSigma1 f (a :&: _) = f a
+
+-- | Project the second element out of a dependent pair using
+-- continuation-passing style.
 projSigma2 :: forall s t r. (forall (fst :: s). t @@ fst -> r) -> Sigma s t -> r
 projSigma2 f ((_ :: Sing (fst :: s)) :&: b) = f @fst b
 
@@ -76,3 +132,58 @@ zipSigma :: Sing (f :: a ~> b ~> c)
          -> Sigma a p -> Sigma b q -> Sigma c r
 zipSigma f g ((a :: Sing (fstA :: a)) :&: p) ((b :: Sing (fstB :: b)) :&: q) =
   (f @@ a @@ b) :&: (g @fstA @fstB p q)
+
+-- | Convert an uncurried function on 'Sigma' to a curried one.
+--
+-- Together, 'currySigma' and 'uncurrySigma' witness an isomorphism such that
+-- the following identities hold:
+--
+-- @
+-- id1 :: forall a (b :: a ~> Type) (c :: 'Sigma' a b ~> Type).
+--        (forall (p :: Sigma a b). 'SSigma' p -> c @@ p)
+--     -> (forall (p :: Sigma a b). 'SSigma' p -> c @@ p)
+-- id1 f = 'uncurrySigma' @a @b @c ('currySigma' @a @b @c f)
+--
+-- id2 :: forall a (b :: a ~> Type) (c :: 'Sigma' a b ~> Type).
+--        (forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing' sx) -> Sing y -> c @@ (sx :&: y))
+--     -> (forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing' sx) -> Sing y -> c @@ (sx :&: y))
+-- id2 f = 'currySigma' @a @b @c ('uncurrySigma' @a @b @c f)
+-- @
+currySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
+              (forall (p :: Sigma a b). SSigma p -> c @@ p)
+           -> (forall (x :: a) (sx :: Sing x) (y :: b @@ x).
+                 Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y))
+currySigma f x y = f (x :%&: y)
+
+-- | Convert a curried function on 'Sigma' to an uncurried one.
+--
+-- Together, 'currySigma' and 'uncurrySigma' witness an isomorphism.
+-- (Refer to the documentation for 'currySigma' for more details.)
+uncurrySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
+                (forall (x :: a) (sx :: Sing x) (y :: b @@ x).
+                   Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y))
+             -> (forall (p :: Sigma a b). SSigma p -> c @@ p)
+uncurrySigma f (x :%&: y) = f x y
+
+------------------------------------------------------------
+-- Internal utilities
+------------------------------------------------------------
+
+{- $internal-utilities
+
+See the documentation in "Data.Singletons.ShowSing"—in particular, the
+Haddocks for 'ShowSing' and `ShowSing'`—for an explanation for why these
+classes exist.
+-}
+
+class    (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)
+instance (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)
+
+class    Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)
+instance Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)
+
+class    (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type)
+instance (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type)
+
+class    Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)
+instance Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)