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