{-# 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 #-}

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

      -- * 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 :: Int -> Sigma s t -> ShowS
showsPrec p :: Int
p ((a :: Sing (fst :: s)) :&: b :: t @@ fst
b) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 5) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Int -> Sing fst -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 5 Sing fst
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " :&: " 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 5 t @@ fst
b
      :: (ShowSing' fst, ShowApply' t fst) => ShowS

-- | Unicode shorthand for 'Sigma'.
type Σ = Sigma

{-
Note [Impredicative Σ?]
~~~~~~~~~~~~~~~~~~~~~~~
The definition of Σ currently 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 Trac
#13408. If someone ever fixes that bug, we could remove the use of
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 :: Int -> SSigma sig -> ShowS
showsPrec p :: Int
p ((sa :: Sing ('WrapSing (sfst :: Sing fst))) :%&: (sb :: Sing snd)) =
    Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 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 5 SWrappedSing ('WrapSing sfst)
Sing ('WrapSing sfst)
sa ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " :&: " 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 5 Sing snd
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 (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'.
type SΣ = SSigma

-- | Project the first element out of a dependent pair.
fstSigma :: forall s t. SingKind s => Sigma s t -> Demote s
fstSigma :: Sigma s t -> Demote s
fstSigma (a :: Sing fst
a :&: _) = Sing fst -> 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.
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 :: SSigma sig -> Demote (t @@ FstSigma sig)
sndSigma (_ :%&: b :: Sing snd
b) = Sing snd -> Demote (t @@ FstSigma sig)
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing snd
Sing snd
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 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r
projSigma1 f :: forall (fst :: s). Sing fst -> r
f (a :: Sing fst
a :&: _) = 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 (fst :: s). (t @@ fst) -> r) -> Sigma s t -> r
projSigma2 f :: forall (fst :: s). (t @@ fst) -> r
f ((_ :: Sing (fst :: s)) :&: b :: t @@ fst
b) = (t @@ fst) -> r
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 :: Sing f
-> (forall (x :: a). (p @@ x) -> q @@ (f @@ x))
-> Sigma a p
-> Sigma b q
mapSigma f :: Sing f
f g :: forall (x :: a). (p @@ x) -> q @@ (f @@ x)
g ((x :: Sing (fst :: a)) :&: y :: p @@ fst
y) = (Sing f
f Sing f -> Sing fst -> Sing (f @@ fst)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing fst
x) Sing (f @@ fst) -> (q @@ (f @@ fst)) -> Sigma b q
forall s (t :: s ~> *) (fst :: s).
Sing fst -> (t @@ fst) -> Sigma s t
:&: ((p @@ fst) -> q @@ (f @@ fst)
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 :: 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 f :: Sing f
f g :: forall (x :: a) (y :: b).
(p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y)
g ((a :: Sing (fstA :: a)) :&: p :: p @@ fst
p) ((b :: Sing (fstB :: b)) :&: q :: 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 f fst @@ fst)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing fst
b) Sing (Apply f fst @@ fst)
-> (r @@ (Apply f fst @@ fst)) -> Sigma c r
forall s (t :: s ~> *) (fst :: s).
Sing fst -> (t @@ fst) -> Sigma s t
:&: ((p @@ fst) -> (q @@ fst) -> r @@ (Apply f fst @@ fst)
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 (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 :: forall (p :: Sigma a b). SSigma p -> c @@ p
f x :: Sing ('WrapSing sx)
x y :: Sing y
y = SSigma (sx ':&: y) -> 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 (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 :: forall (x :: a) (sx :: Sing x) (y :: b @@ x).
Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)
f (x :: Sing ('WrapSing sfst)
x :%&: y :: 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

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