{-# LANGUAGE PolyKinds, StandaloneDeriving #-}
#if MIN_VERSION_base(4,7,0)
{-# LANGUAGE NoAutoDeriveTypeable #-}
#endif
-- | Singleton types corresponding to type-level data structures.
--
-- The implementation is similar, but subtly different to that of the
-- @@ package.
-- See the
-- paper for details.
--
module Generics.SOP.Sing
( -- * Singletons
SList(..)
, SListI(..)
, Sing
, SingI(..)
-- ** Shape of type-level lists
, Shape(..)
, shape
, lengthSList
, lengthSing
) where
-- * 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] -> * 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]))
-- | Implicit singleton list.
--
-- A singleton list can be used to reveal the structure of
-- a type-level list argument that the function is quantified
-- over.
--
-- The class 'SListI' should have instances that match the
-- constructors of 'SList'.
--
-- @since 0.2
--
class SListI (xs :: [k]) where
-- | Get hold of the explicit singleton (that one can then
-- pattern match on).
sList :: SList xs
instance SListI '[] where
sList = SNil
instance SListI xs => SListI (x ': xs) where
sList = SCons
-- | General class for implicit singletons.
--
-- Just provided for limited backward compatibility.
--
{-# DEPRECATED SingI "Use 'SListI' instead." #-}
{-# DEPRECATED sing "Use 'sList' instead." #-}
class SListI xs => SingI (xs :: [k]) where
sing :: Sing xs
-- | Explicit singleton type.
--
-- Just provided for limited backward compatibility.
{-# DEPRECATED Sing "Use 'SList' instead." #-}
type Sing = SList
-- * Shape of type-level lists
-- | Occassionally 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] -> * 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 (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 (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
-- | Old name for 'lengthSList'.
{-# DEPRECATED lengthSing "Use 'lengthSList' instead." #-}
lengthSing :: SListI xs => proxy xs -> Int
lengthSing = lengthSList