Copyright | (C) 2017 Ryan Scott |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Ryan Scott |
Stability | Experimental |
Portability | GHC |
Safe Haskell | Trustworthy |
Language | GHC2021 |
Data.Eliminator
Contents
Description
Dependently typed elimination functions using singletons
.
This module exports a combination of eliminators whose names are known not to clash with each other. Potential name conflicts have been resolved by putting the conflicting names in separate modules:
- Data.Eliminator defines
elimNat
, which works over theNat
data type from Data.Nat. For an eliminator that works overNat
from GHC.TypeNats, see Data.Eliminator.TypeNats. - Data.Eliminator avoids exporting eliminators for
First
andLast
data types, as there are multiple data types with these names. If you want eliminators for theFirst
andLast
data types from Data.Monoid, import them from Data.Eliminator.Monoid. If you want eliminators for theFirst
andLast
data types from Data.Semigroup, import them from Data.Eliminator.Semigroup. - Data.Eliminator avoids exporting eliminators for
Product
andSum
data types, as there are multiple data types with these names. If you want eliminators for theProduct
andSum
data types from Data.Monoid or Data.Semigroup, import them from Data.Eliminator.Monoid or Data.Eliminator.Semigroup. If you want eliminators for theProduct
andSum
data types from Data.Functor.Product and Data.Functor.Sum, respectively, import them from Data.Eliminator.Functor.
Synopsis
- elimAll :: forall (p :: (~>) All Type) (s :: All). Sing s -> (forall (f0 :: Bool). Sing f0 -> Apply p ('All f0)) -> Apply p s
- type family ElimAll p s p where ...
- elimAny :: forall (p :: (~>) Any Type) (s :: Any). Sing s -> (forall (f0 :: Bool). Sing f0 -> Apply p ('Any f0)) -> Apply p s
- type family ElimAny p s p where ...
- elimArg :: forall (a :: Type) (b :: Type) (p :: (~>) (Arg a b) Type) (s :: Arg a b). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> Apply p ('Arg f0 f1)) -> Apply p s
- type family ElimArg p s p where ...
- elimBool :: forall (p :: (~>) Bool Type) (s :: Bool). Sing s -> Apply p 'False -> Apply p 'True -> Apply p s
- type family ElimBool p s p p where ...
- elimConst :: forall (a :: Type) (k :: Type) (b :: k) (p :: (~>) (Const a b) Type) (s :: Const a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Const f0)) -> Apply p s
- type family ElimConst p s p where ...
- elimDown :: forall (a :: Type) (p :: (~>) (Down a) Type) (s :: Down a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Down f0)) -> Apply p s
- type family ElimDown p s p where ...
- elimDual :: forall (a :: Type) (p :: (~>) (Dual a) Type) (s :: Dual a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Dual f0)) -> Apply p s
- type family ElimDual p s p where ...
- elimEither :: forall (a :: Type) (b :: Type) (p :: (~>) (Either a b) Type) (s :: Either a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Left f0)) -> (forall (f0 :: b). Sing f0 -> Apply p ('Right f0)) -> Apply p s
- type family ElimEither p s p p where ...
- elimIdentity :: forall (a :: Type) (p :: (~>) (Identity a) Type) (s :: Identity a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Identity f0)) -> Apply p s
- type family ElimIdentity p s p where ...
- elimList :: forall (a :: Type) (p :: (~>) ([] a) Type) (s :: [] a). Sing s -> Apply p '[] -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> Apply p f1 -> Apply p ('(:) f0 f1)) -> Apply p s
- type family ElimList p s p p where ...
- elimMax :: forall (a :: Type) (p :: (~>) (Max a) Type) (s :: Max a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Max f0)) -> Apply p s
- type family ElimMax p s p where ...
- elimMaybe :: forall (a :: Type) (p :: (~>) (Maybe a) Type) (s :: Maybe a). Sing s -> Apply p 'Nothing -> (forall (f0 :: a). Sing f0 -> Apply p ('Just f0)) -> Apply p s
- type family ElimMaybe p s p p where ...
- elimMin :: forall (a :: Type) (p :: (~>) (Min a) Type) (s :: Min a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Min f0)) -> Apply p s
- type family ElimMin p s p where ...
- elimNat :: forall (p :: (~>) Nat Type) (s :: Nat). Sing s -> Apply p 'Z -> (forall (f0 :: Nat). Sing f0 -> Apply p f0 -> Apply p ('S f0)) -> Apply p s
- type family ElimNat p s p p where ...
- elimNonEmpty :: forall (a :: Type) (p :: (~>) (NonEmpty a) Type) (s :: NonEmpty a). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> Apply p ('(:|) f0 f1)) -> Apply p s
- type family ElimNonEmpty p s p where ...
- elimOrdering :: forall (p :: (~>) Ordering Type) (s :: Ordering). Sing s -> Apply p 'LT -> Apply p 'EQ -> Apply p 'GT -> Apply p s
- type family ElimOrdering p s p p p where ...
- elimProxy :: forall (k :: Type) (t :: k) (p :: (~>) (Proxy t) Type) (s :: Proxy t). Sing s -> Apply p 'Proxy -> Apply p s
- type family ElimProxy p s p where ...
- elimTuple0 :: forall (p :: (~>) () Type) (s :: ()). Sing s -> Apply p '() -> Apply p s
- type family ElimTuple0 p s p where ...
- elimTuple2 :: forall (a :: Type) (b :: Type) (p :: (~>) ((,) a b) Type) (s :: (,) a b). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> Apply p ('(,) f0 f1)) -> Apply p s
- type family ElimTuple2 p s p where ...
- elimTuple3 :: forall (a :: Type) (b :: Type) (c :: Type) (p :: (~>) ((,,) a b c) Type) (s :: (,,) a b c). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> Apply p ('(,,) f0 f1 f2)) -> Apply p s
- type family ElimTuple3 p s p where ...
- elimTuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: (~>) ((,,,) a b c d) Type) (s :: (,,,) a b c d). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> Apply p ('(,,,) f0 f1 f2 f3)) -> Apply p s
- type family ElimTuple4 p s p where ...
- elimTuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: (~>) ((,,,,) a b c d e) Type) (s :: (,,,,) a b c d e). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> Apply p ('(,,,,) f0 f1 f2 f3 f4)) -> Apply p s
- type family ElimTuple5 p s p where ...
- elimTuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: (~>) ((,,,,,) a b c d e f) Type) (s :: (,,,,,) a b c d e f). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> forall (f5 :: f). Sing f5 -> Apply p ('(,,,,,) f0 f1 f2 f3 f4 f5)) -> Apply p s
- type family ElimTuple6 p s p where ...
- elimTuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (p :: (~>) ((,,,,,,) a b c d e f g) Type) (s :: (,,,,,,) a b c d e f g). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> forall (f5 :: f). Sing f5 -> forall (f6 :: g). Sing f6 -> Apply p ('(,,,,,,) f0 f1 f2 f3 f4 f5 f6)) -> Apply p s
- type family ElimTuple7 p s p where ...
- elimVoid :: forall (p :: (~>) Void Type) (s :: Void). Sing s -> Apply p s
- type family ElimVoid p s where ...
- elimWrappedMonoid :: forall (m :: Type) (p :: (~>) (WrappedMonoid m) Type) (s :: WrappedMonoid m). Sing s -> (forall (f0 :: m). Sing f0 -> Apply p ('WrapMonoid f0)) -> Apply p s
- type family ElimWrappedMonoid p s p where ...
Eliminator functions
These eliminators are defined with propositions of kind <Datatype> ~>
(that is, using the Type
(
kind). These eliminators are designed for
defunctionalized (i.e., "partially applied") types as predicates,
and as a result, the predicates must be applied manually with ~>
)Apply
.
The naming conventions are:
- If the datatype has an alphanumeric name, its eliminator will have that name
with
elim
prepended. - If the datatype has a symbolic name, its eliminator will have that name
with
~>
prepended.
elimAll :: forall (p :: (~>) All Type) (s :: All). Sing s -> (forall (f0 :: Bool). Sing f0 -> Apply p ('All f0)) -> Apply p s Source #
elimAny :: forall (p :: (~>) Any Type) (s :: Any). Sing s -> (forall (f0 :: Bool). Sing f0 -> Apply p ('Any f0)) -> Apply p s Source #
elimArg :: forall (a :: Type) (b :: Type) (p :: (~>) (Arg a b) Type) (s :: Arg a b). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> Apply p ('Arg f0 f1)) -> Apply p s Source #
elimBool :: forall (p :: (~>) Bool Type) (s :: Bool). Sing s -> Apply p 'False -> Apply p 'True -> Apply p s Source #
elimConst :: forall (a :: Type) (k :: Type) (b :: k) (p :: (~>) (Const a b) Type) (s :: Const a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Const f0)) -> Apply p s Source #
elimDown :: forall (a :: Type) (p :: (~>) (Down a) Type) (s :: Down a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Down f0)) -> Apply p s Source #
elimDual :: forall (a :: Type) (p :: (~>) (Dual a) Type) (s :: Dual a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Dual f0)) -> Apply p s Source #
elimEither :: forall (a :: Type) (b :: Type) (p :: (~>) (Either a b) Type) (s :: Either a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Left f0)) -> (forall (f0 :: b). Sing f0 -> Apply p ('Right f0)) -> Apply p s Source #
type family ElimEither p s p p where ... Source #
Equations
ElimEither @a @b p ('Left s0) useThis _p1 = useThis s0 | |
ElimEither @a @b p ('Right s0) _p0 useThis = useThis s0 |
elimIdentity :: forall (a :: Type) (p :: (~>) (Identity a) Type) (s :: Identity a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Identity f0)) -> Apply p s Source #
type family ElimIdentity p s p where ... Source #
Equations
ElimIdentity @a p ('Identity s0) useThis = useThis s0 |
elimList :: forall (a :: Type) (p :: (~>) ([] a) Type) (s :: [] a). Sing s -> Apply p '[] -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> Apply p f1 -> Apply p ('(:) f0 f1)) -> Apply p s Source #
elimMax :: forall (a :: Type) (p :: (~>) (Max a) Type) (s :: Max a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Max f0)) -> Apply p s Source #
elimMaybe :: forall (a :: Type) (p :: (~>) (Maybe a) Type) (s :: Maybe a). Sing s -> Apply p 'Nothing -> (forall (f0 :: a). Sing f0 -> Apply p ('Just f0)) -> Apply p s Source #
elimMin :: forall (a :: Type) (p :: (~>) (Min a) Type) (s :: Min a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Min f0)) -> Apply p s Source #
elimNat :: forall (p :: (~>) Nat Type) (s :: Nat). Sing s -> Apply p 'Z -> (forall (f0 :: Nat). Sing f0 -> Apply p f0 -> Apply p ('S f0)) -> Apply p s Source #
elimNonEmpty :: forall (a :: Type) (p :: (~>) (NonEmpty a) Type) (s :: NonEmpty a). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> Apply p ('(:|) f0 f1)) -> Apply p s Source #
type family ElimNonEmpty p s p where ... Source #
Equations
ElimNonEmpty @a p ('(:|) s0 s1) useThis = useThis s0 s1 |
elimOrdering :: forall (p :: (~>) Ordering Type) (s :: Ordering). Sing s -> Apply p 'LT -> Apply p 'EQ -> Apply p 'GT -> Apply p s Source #
type family ElimOrdering p s p p p where ... Source #
Equations
ElimOrdering p 'LT useThis _p1 _p2 = useThis | |
ElimOrdering p 'EQ _p0 useThis _p2 = useThis | |
ElimOrdering p 'GT _p0 _p1 useThis = useThis |
elimProxy :: forall (k :: Type) (t :: k) (p :: (~>) (Proxy t) Type) (s :: Proxy t). Sing s -> Apply p 'Proxy -> Apply p s Source #
type family ElimTuple0 p s p where ... Source #
Equations
ElimTuple0 p '() useThis = useThis |
elimTuple2 :: forall (a :: Type) (b :: Type) (p :: (~>) ((,) a b) Type) (s :: (,) a b). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> Apply p ('(,) f0 f1)) -> Apply p s Source #
type family ElimTuple2 p s p where ... Source #
Equations
ElimTuple2 @a @b p ('(,) s0 s1) useThis = useThis s0 s1 |
elimTuple3 :: forall (a :: Type) (b :: Type) (c :: Type) (p :: (~>) ((,,) a b c) Type) (s :: (,,) a b c). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> Apply p ('(,,) f0 f1 f2)) -> Apply p s Source #
type family ElimTuple3 p s p where ... Source #
Equations
ElimTuple3 @a @b @c p ('(,,) s0 s1 s2) useThis = useThis s0 s1 s2 |
elimTuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: (~>) ((,,,) a b c d) Type) (s :: (,,,) a b c d). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> Apply p ('(,,,) f0 f1 f2 f3)) -> Apply p s Source #
type family ElimTuple4 p s p where ... Source #
Equations
ElimTuple4 @a @b @c @d p ('(,,,) s0 s1 s2 s3) useThis = useThis s0 s1 s2 s3 |
elimTuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: (~>) ((,,,,) a b c d e) Type) (s :: (,,,,) a b c d e). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> Apply p ('(,,,,) f0 f1 f2 f3 f4)) -> Apply p s Source #
type family ElimTuple5 p s p where ... Source #
Equations
ElimTuple5 @a @b @c @d @e p ('(,,,,) s0 s1 s2 s3 s4) useThis = useThis s0 s1 s2 s3 s4 |
elimTuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: (~>) ((,,,,,) a b c d e f) Type) (s :: (,,,,,) a b c d e f). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> forall (f5 :: f). Sing f5 -> Apply p ('(,,,,,) f0 f1 f2 f3 f4 f5)) -> Apply p s Source #
type family ElimTuple6 p s p where ... Source #
Equations
ElimTuple6 @a @b @c @d @e @f p ('(,,,,,) s0 s1 s2 s3 s4 s5) useThis = useThis s0 s1 s2 s3 s4 s5 |
elimTuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (p :: (~>) ((,,,,,,) a b c d e f g) Type) (s :: (,,,,,,) a b c d e f g). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> forall (f5 :: f). Sing f5 -> forall (f6 :: g). Sing f6 -> Apply p ('(,,,,,,) f0 f1 f2 f3 f4 f5 f6)) -> Apply p s Source #
type family ElimTuple7 p s p where ... Source #
Equations
ElimTuple7 @a @b @c @d @e @f @g p ('(,,,,,,) s0 s1 s2 s3 s4 s5 s6) useThis = useThis s0 s1 s2 s3 s4 s5 s6 |
elimWrappedMonoid :: forall (m :: Type) (p :: (~>) (WrappedMonoid m) Type) (s :: WrappedMonoid m). Sing s -> (forall (f0 :: m). Sing f0 -> Apply p ('WrapMonoid f0)) -> Apply p s Source #
type family ElimWrappedMonoid p s p where ... Source #
Equations
ElimWrappedMonoid @m p ('WrapMonoid s0) useThis = useThis s0 |