{-# 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 nil cons =
  cpara_SList (Proxy :: Proxy Top) nil 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 nil cons =
  ccase_SList (Proxy :: Proxy Top) nil 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 = ccase_SList (Proxy :: Proxy Top) SNil 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 = case sList :: SList xs of
          SNil  -> ShapeNil
          SCons -> ShapeCons shape

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