{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE QuantifiedConstraints #-}
#else
{-# LANGUAGE TypeInType #-}
#endif

#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#else
{-# LANGUAGE ImpredicativeTypes #-} -- See Note [Impredicative Σ?]
#endif

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Sigma
-- Copyright   :  (C) 2017 Ryan Scott
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Ryan Scott
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Defines 'Sigma', a dependent pair data type, and related functions.
--
----------------------------------------------------------------------------

module Data.Singletons.Sigma
    ( -- * The 'Sigma' type
      Sigma(..), Σ
    , Sing, SSigma(..), SΣ

      -- * Operations over 'Sigma'
    , fstSigma, FstSigma, sndSigma, SndSigma
    , projSigma1, projSigma2
    , mapSigma, zipSigma
    , currySigma, uncurrySigma

#if __GLASGOW_HASKELL__ >= 806
      -- * Internal utilities
      -- $internalutilities
    , ShowApply,  ShowSingApply
    , ShowApply', ShowSingApply'
#endif
    ) where

import Data.Kind
import Data.Singletons
#if __GLASGOW_HASKELL__ >= 806
import Data.Singletons.ShowSing
#endif

-- | A dependent pair.
#if __GLASGOW_HASKELL__ >= 810
type Sigma :: forall s -> (s ~> Type) -> Type
#endif
data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t
infixr 4 :&:

-- | Unicode shorthand for 'Sigma'.
#if __GLASGOW_HASKELL__ >= 810
type Σ :: forall s -> (s ~> Type) -> Type
#endif
type Σ = Sigma

{-
Note [Impredicative Σ?]
~~~~~~~~~~~~~~~~~~~~~~~
The following definition alone:

  type Σ = Sigma

will not typecheck without the use of ImpredicativeTypes. There isn't a
fundamental reason that this should be the case, and the only reason that GHC
currently requires this is due to GHC#13408. Thankfully, giving Σ a standalone
kind signature works around GHC#13408, so we only have to enable
ImpredicativeTypes on pre-8.10 versions of GHC.
-}

-- | The singleton type for 'Sigma'.
#if __GLASGOW_HASKELL__ >= 810
type SSigma :: Sigma s t -> Type
#endif
data SSigma :: forall s t. 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 (fst :: s) (a :: Sing fst) (b :: t @@ fst).
       (SingI fst, SingI b)
    => SingI (a ':&: b :: Sigma s t) where
  sing :: Sing (a ':&: b)
sing = Sing ('WrapSing a)
forall {k} (a :: k). SingI a => Sing a
sing Sing ('WrapSing a) -> Sing b -> SSigma (a ':&: b)
forall s (t :: s ~> *) (fst :: s) (sfst :: Sing fst)
       (snd :: t @@ fst).
Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd)
:%&: Sing b
forall {k} (a :: k). SingI a => Sing a
sing

-- | Unicode shorthand for 'SSigma'.
#if __GLASGOW_HASKELL__ >= 810
type SΣ :: Sigma s t -> Type
#endif
type SΣ = SSigma

-- | Project the first element out of a dependent pair.
fstSigma :: forall s t. SingKind s => Sigma s t -> Demote s
fstSigma :: forall s (t :: s ~> *). SingKind s => Sigma s t -> Demote s
fstSigma (Sing fst
a :&: t @@ fst
_) = Sing fst -> Demote s
forall (a :: s). Sing a -> Demote s
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing fst
a

-- | Project the first element out of a dependent pair.
#if __GLASGOW_HASKELL__ >= 810
type FstSigma :: Sigma s t -> s
#endif
type family FstSigma (sig :: Sigma s t) :: s where
  FstSigma ((_ :: Sing fst) ':&: _) = fst

-- | Project the second element out of a dependent pair.
sndSigma :: forall s t (sig :: Sigma s t).
            SingKind (t @@ FstSigma sig)
         => SSigma sig -> Demote (t @@ FstSigma sig)
sndSigma :: forall s (t :: s ~> *) (sig :: Sigma s t).
SingKind (t @@ FstSigma sig) =>
SSigma sig -> Demote (t @@ FstSigma sig)
sndSigma (Sing ('WrapSing sfst)
_ :%&: Sing snd
b) = Sing snd -> Demote (Apply t fst)
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Apply t fst). Sing a -> Demote (Apply t fst)
fromSing Sing snd
b

-- | Project the second element out of a dependent pair.
#if __GLASGOW_HASKELL__ >= 810
type SndSigma :: forall s t. forall (sig :: Sigma s t) -> t @@ FstSigma sig
#endif
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 :: forall s r (t :: s ~> *).
(forall (fst :: s). Sing fst -> r) -> Sigma s t -> r
projSigma1 forall (fst :: s). Sing fst -> r
f (Sing fst
a :&: t @@ fst
_) = Sing fst -> r
forall (fst :: s). Sing fst -> r
f Sing fst
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 :: forall s (t :: s ~> *) r.
(forall (fst :: s). (t @@ fst) -> r) -> Sigma s t -> r
projSigma2 forall (fst :: s). (t @@ fst) -> r
f ((Sing fst
_ :: Sing (fst :: s)) :&: t @@ fst
b) = forall (fst :: s). (t @@ fst) -> r
f @fst t @@ fst
b

-- | Map across a 'Sigma' value in a dependent fashion.
mapSigma :: Sing (f :: a ~> b) -> (forall (x :: a). p @@ x -> q @@ (f @@ x))
         -> Sigma a p -> Sigma b q
mapSigma :: forall a b (f :: a ~> b) (p :: a ~> *) (q :: b ~> *).
Sing f
-> (forall (x :: a). (p @@ x) -> q @@ (f @@ x))
-> Sigma a p
-> Sigma b q
mapSigma Sing f
f forall (x :: a). (p @@ x) -> q @@ (f @@ x)
g ((Sing fst
x :: Sing (fst :: a)) :&: p @@ fst
y) = (Sing f
f Sing f -> Sing fst -> Sing (Apply f fst)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing fst
x) Sing (Apply f fst) -> (q @@ Apply f fst) -> Sigma b q
forall s (t :: s ~> *) (fst :: s).
Sing fst -> (t @@ fst) -> Sigma s t
:&: (forall (x :: a). (p @@ x) -> q @@ (f @@ x)
g @fst p @@ fst
y)

-- | Zip two 'Sigma' values together in a dependent fashion.
zipSigma :: Sing (f :: a ~> b ~> c)
         -> (forall (x :: a) (y :: b). p @@ x -> q @@ y -> r @@ (f @@ x @@ y))
         -> Sigma a p -> Sigma b q -> Sigma c r
zipSigma :: forall a b c (f :: a ~> (b ~> c)) (p :: a ~> *) (q :: b ~> *)
       (r :: c ~> *).
Sing f
-> (forall (x :: a) (y :: b).
    (p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y))
-> Sigma a p
-> Sigma b q
-> Sigma c r
zipSigma Sing f
f forall (x :: a) (y :: b).
(p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y)
g ((Sing fst
a :: Sing (fstA :: a)) :&: p @@ fst
p) ((Sing fst
b :: Sing (fstB :: b)) :&: q @@ fst
q) =
  (Sing f
f Sing f -> Sing fst -> Sing (Apply f fst)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing fst
a Sing (Apply f fst) -> Sing fst -> Sing (Apply (Apply f fst) fst)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing fst
b) Sing (Apply (Apply f fst) fst)
-> (r @@ Apply (Apply f fst) fst) -> Sigma c r
forall s (t :: s ~> *) (fst :: s).
Sing fst -> (t @@ fst) -> Sigma s t
:&: (forall (x :: a) (y :: b).
(p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y)
g @fstA @fstB p @@ fst
p q @@ fst
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 :: forall a (b :: a ~> *) (c :: Sigma a b ~> *).
(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 forall (p :: Sigma a b). SSigma p -> c @@ p
f Sing ('WrapSing sx)
x Sing y
y = SSigma (sx ':&: y) -> Apply c (sx ':&: y)
forall (p :: Sigma a b). SSigma p -> c @@ p
f (Sing ('WrapSing sx)
x Sing ('WrapSing sx) -> Sing y -> SSigma (sx ':&: y)
forall s (t :: s ~> *) (fst :: s) (sfst :: Sing fst)
       (snd :: t @@ fst).
Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd)
:%&: Sing y
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 :: forall a (b :: a ~> *) (c :: Sigma a b ~> *).
(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 forall (x :: a) (sx :: Sing x) (y :: b @@ x).
Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)
f (Sing ('WrapSing sfst)
x :%&: Sing snd
y) = Sing ('WrapSing sfst) -> Sing snd -> c @@ (sfst ':&: snd)
forall (x :: a) (sx :: Sing x) (y :: b @@ x).
Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)
f Sing ('WrapSing sfst)
x Sing snd
y

#if __GLASGOW_HASKELL__ >= 806
instance (ShowSing s, ShowApply t) => Show (Sigma s t) where
  showsPrec :: Int -> Sigma s t -> ShowS
showsPrec Int
p ((Sing fst
a :: Sing (fst :: s)) :&: t @@ fst
b) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
5) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Int -> Sing fst -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 Sing fst
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :&: " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (t @@ fst) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 t @@ fst
b
      :: ShowApply' t fst => ShowS

instance forall s (t :: s ~> Type) (sig :: Sigma s t).
         (ShowSing s, ShowSingApply t)
      => Show (SSigma sig) where
  showsPrec :: Int -> SSigma sig -> ShowS
showsPrec Int
p ((Sing ('WrapSing sfst)
sa :: Sing ('WrapSing (sfst :: Sing fst))) :%&: (Sing snd
sb :: Sing snd)) =
    Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
5) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      Int -> SWrappedSing ('WrapSing sfst) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 SWrappedSing ('WrapSing sfst)
Sing ('WrapSing sfst)
sa ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :&: " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Sing snd -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 Sing snd
sb
        :: ShowSingApply' t fst snd => ShowS

------------------------------------------------------------
-- 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.

Note that these classes are only defined on GHC 8.6 or later.
-}

#if __GLASGOW_HASKELL__ >= 810
type ShowApply :: (a ~> Type) -> Constraint
#endif
class    (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)
instance (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)

#if __GLASGOW_HASKELL__ >= 810
type ShowApply' :: (a ~> Type) -> a -> Constraint
#endif
class    Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)
instance Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)

#if __GLASGOW_HASKELL__ >= 810
type ShowSingApply :: (a ~> Type) -> Constraint
#endif
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)

#if __GLASGOW_HASKELL__ >= 810
type ShowSingApply' :: forall a. forall (f :: a ~> Type) (x :: a) -> Apply f x -> Constraint
#endif
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)
#endif