{-# LANGUAGE PolyKinds, StandaloneDeriving #-}
#if __GLASGOW_HASKELL__ < 806
-- Before GHC 8.6, TypeInType was required to explicitly quantify kind variables.
-- After GHC 8.6, this feature was incorporated into PolyKinds.
{-# LANGUAGE TypeInType #-}
#endif
-- | Singleton types corresponding to type-level data structures.
--
-- The implementation is similar, but subtly different to that of the
-- @<https://hackage.haskell.org/package/singletons singletons>@ package.
-- See the <http://www.andres-loeh.de/TrueSumsOfProducts "True Sums of Products">
-- paper for details.
--
module Data.SOP.Sing
  ( -- * Singletons
    SList(..)
  , SListI
  , sList
  , para_SList
  , case_SList
    -- ** Shape of type-level lists
  , Shape(..)
  , shape
  , lengthSList
  ) where

import Data.Kind (Type)
import Data.Proxy (Proxy(..))

import Data.SOP.Constraint

-- * Singletons

-- | Explicit singleton list.
--
-- A singleton list can be used to reveal the structure of
-- a type-level list argument that the function is quantified
-- over. For every type-level list @xs@, there is one non-bottom
-- value of type @'SList' xs@.
--
-- Note that these singleton lists are polymorphic in the
-- list elements; we do not require a singleton representation
-- for them.
--
-- @since 0.2
--
data SList :: [k] -> Type where
  SNil  :: SList '[]
  SCons :: SListI xs => SList (x ': xs)

deriving instance Show (SList (xs :: [k]))
deriving instance Eq   (SList (xs :: [k]))
deriving instance Ord  (SList (xs :: [k]))

-- | Paramorphism for a type-level list.
--
-- @since 0.4.0.0
--
para_SList ::
     SListI xs
  => r '[]
  -> (forall y ys . (SListI ys) => r ys -> r (y ': ys))
  -> r xs
para_SList :: r '[]
-> (forall (y :: k) (ys :: [k]). SListI ys => r ys -> r (y : ys))
-> r xs
para_SList r '[]
nil forall (y :: k) (ys :: [k]). SListI ys => r ys -> r (y : ys)
cons =
  Proxy Top
-> r '[]
-> (forall (y :: k) (ys :: [k]).
    (Top y, All Top ys) =>
    r ys -> r (y : ys))
-> r xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (r :: [k] -> *).
All c xs =>
proxy c
-> r '[]
-> (forall (y :: k) (ys :: [k]).
    (c y, All c ys) =>
    r ys -> r (y : ys))
-> r xs
cpara_SList (forall k. Proxy Top
forall k (t :: k). Proxy t
Proxy :: Proxy Top) r '[]
nil forall (y :: k) (ys :: [k]).
(Top y, All Top ys) =>
r ys -> r (y : ys)
forall (y :: k) (ys :: [k]). SListI ys => r ys -> r (y : ys)
cons
{-# INLINE para_SList #-}

-- | Case distinction on a type-level list.
--
-- @since 0.4.0.0
--
case_SList ::
     SListI xs
  => r '[]
  -> (forall y ys . (SListI ys) => r (y ': ys))
  -> r xs
case_SList :: r '[]
-> (forall (y :: k) (ys :: [k]). SListI ys => r (y : ys)) -> r xs
case_SList r '[]
nil forall (y :: k) (ys :: [k]). SListI ys => r (y : ys)
cons =
  Proxy Top
-> r '[]
-> (forall (y :: k) (ys :: [k]). (Top y, All Top ys) => r (y : ys))
-> r xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (r :: [k] -> *).
All c xs =>
proxy c
-> r '[]
-> (forall (y :: k) (ys :: [k]). (c y, All c ys) => r (y : ys))
-> r xs
ccase_SList (forall k. Proxy Top
forall k (t :: k). Proxy t
Proxy :: Proxy Top) r '[]
nil forall (y :: k) (ys :: [k]). (Top y, All Top ys) => r (y : ys)
forall (y :: k) (ys :: [k]). SListI ys => r (y : ys)
cons
{-# INLINE case_SList #-}

-- | Get hold of an explicit singleton (that one can then
-- pattern match on) for a type-level list
--
sList :: SListI xs => SList xs
sList :: SList xs
sList = Proxy Top
-> SList '[]
-> (forall (y :: k) (ys :: [k]).
    (Top y, All Top ys) =>
    SList (y : ys))
-> SList xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (r :: [k] -> *).
All c xs =>
proxy c
-> r '[]
-> (forall (y :: k) (ys :: [k]). (c y, All c ys) => r (y : ys))
-> r xs
ccase_SList (forall k. Proxy Top
forall k (t :: k). Proxy t
Proxy :: Proxy Top) SList '[]
forall k. SList '[]
SNil forall (y :: k) (ys :: [k]). (Top y, All Top ys) => SList (y : ys)
forall k (xs :: [k]) (x :: k). SListI xs => SList (x : xs)
SCons

-- * Shape of type-level lists

-- | Occasionally it is useful to have an explicit, term-level, representation
-- of type-level lists (esp because of https://ghc.haskell.org/trac/ghc/ticket/9108 )
--
data Shape :: [k] -> Type where
  ShapeNil  :: Shape '[]
  ShapeCons :: SListI xs => Shape xs -> Shape (x ': xs)

deriving instance Show (Shape xs)
deriving instance Eq   (Shape xs)
deriving instance Ord  (Shape xs)

-- | The shape of a type-level list.
shape :: forall k (xs :: [k]). SListI xs => Shape xs
shape :: Shape xs
shape = case SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList :: SList xs of
          SList xs
SNil  -> Shape xs
forall k. Shape '[]
ShapeNil
          SList xs
SCons -> Shape xs -> Shape (x : xs)
forall k (xs :: [k]) (x :: k).
SListI xs =>
Shape xs -> Shape (x : xs)
ShapeCons Shape xs
forall k (xs :: [k]). SListI xs => Shape xs
shape

-- | The length of a type-level list.
--
-- @since 0.2
--
lengthSList :: forall k (xs :: [k]) proxy. SListI xs => proxy xs -> Int
lengthSList :: proxy xs -> Int
lengthSList proxy xs
_ = Shape xs -> Int
forall k (xs' :: [k]). Shape xs' -> Int
lengthShape (Shape xs
forall k (xs :: [k]). SListI xs => Shape xs
shape :: Shape xs)
  where
    lengthShape :: forall xs'. Shape xs' -> Int
    lengthShape :: Shape xs' -> Int
lengthShape Shape xs'
ShapeNil      = Int
0
    lengthShape (ShapeCons Shape xs
s) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Shape xs -> Int
forall k (xs' :: [k]). Shape xs' -> Int
lengthShape Shape xs
s