Data.Eliminator

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 the Nat data type from Data.Nat. For an eliminator that works over Nat from GHC.TypeNats, see Data.Eliminator.TypeNats.
• Data.Eliminator avoids exporting eliminators for First and Last data types, as there are multiple data types with these names. If you want eliminators for the First and Last data types from Data.Monoid, import them from Data.Eliminator.Monoid. If you want eliminators for the First and Last data types from Data.Semigroup, import them from Data.Eliminator.Semigroup.
• Data.Eliminator avoids exporting eliminators for Product and Sum data types, as there are multiple data types with these names. If you want eliminators for the Product and Sum data types from Data.Monoid or Data.Semigroup, import them from Data.Eliminator.Monoid or Data.Eliminator.Semigroup. If you want eliminators for the Product and Sum data types from Data.Functor.Product and Data.Functor.Sum, respectively, import them from Data.Eliminator.Functor.

Eliminator functions

These eliminators are defined with propositions of kind <Datatype> ~> Type (that is, using the (~>) 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

type family ElimAll p s p where ...

Equations

ElimAll p ('All s0) useThis = useThis s0

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 ...

Equations

ElimAny p ('Any s0) useThis = useThis s0

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 ...

Equations

ElimArg @a @b p ('Arg s0 s1) useThis = useThis s0 s1

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 ...

Equations

ElimBool p 'False useThis _p1 = useThis

ElimBool p 'True _p0 useThis = useThis

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 ...

Equations

ElimConst @a @k @b p ('Const s0) useThis = useThis s0

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 ...

Equations

ElimDown @a p ('Down s0) useThis = useThis s0

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 ...

Equations

ElimDual @a p ('Dual s0) useThis = useThis s0

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 ...

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

type family ElimIdentity p s p where ...

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

type family ElimList p s p p where ...

Equations

ElimList @a p '[] useThis _p1 = useThis

ElimList @a p ('(:) s0 s1) _p0 useThis = Apply (useThis s0 s1) (ElimList @a p s1 _p0 useThis)

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 ...

Equations

ElimMax @a p ('Max s0) useThis = useThis s0

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 ...

Equations

ElimMaybe @a p 'Nothing useThis _p1 = useThis

ElimMaybe @a p ('Just s0) _p0 useThis = useThis s0

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 ...

Equations

ElimMin @a p ('Min s0) useThis = useThis s0

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 ...

Equations

ElimNat p 'Z useThis _p1 = useThis

ElimNat p ('S s0) _p0 useThis = Apply (useThis s0) (ElimNat p s0 _p0 useThis)

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 ...

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

type family ElimOrdering p s p p p where ...

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

type family ElimProxy p s p where ...

Equations

ElimProxy @k @t p 'Proxy useThis = useThis

elimTuple0 :: forall (p :: (~>) () Type) (s :: ()). Sing s -> Apply p '() -> Apply p s

type family ElimTuple0 p s p where ...

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

type family ElimTuple2 p s p where ...

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

type family ElimTuple3 p s p where ...

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

type family ElimTuple4 p s p where ...

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

type family ElimTuple5 p s p where ...

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

type family ElimTuple6 p s p where ...

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

type family ElimTuple7 p s p where ...

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

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 ...

Equations

ElimWrappedMonoid @m p ('WrapMonoid s0) useThis = useThis s0