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 :: All ~> Type) (s :: All) (p1 :: forall (f0 :: Bool) -> Apply p ('All f0)) :: Apply p s where ...

Equations

ElimAll p ('All s0) (useThis :: forall (f0 :: Bool) -> Apply p ('All f0)) = 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 :: Any ~> Type) (s :: Any) (p1 :: forall (f0 :: Bool) -> Apply p ('Any f0)) :: Apply p s where ...

Equations

ElimAny p ('Any s0) (useThis :: forall (f0 :: Bool) -> Apply p ('Any f0)) = useThis s0

elimArg :: forall a b (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 :: Arg a b ~> Type) (s :: Arg a b) (p1 :: forall (f0 :: a) (f1 :: b) -> Apply p ('Arg f0 f1)) :: Apply p s where ...

Equations

ElimArg (p :: Arg a b ~> Type) ('Arg s0 s1 :: Arg a b) (useThis :: forall (f0 :: a) (f1 :: b) -> Apply p ('Arg f0 f1)) = 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 :: Bool ~> Type) (s :: Bool) (p1 :: Apply p 'False) (p2 :: Apply p 'True) :: Apply p s where ...

Equations

ElimBool p 'False (useThis :: Apply p 'False) (_p1 :: Apply p 'True) = useThis

ElimBool p 'True (_p0 :: Apply p 'False) (useThis :: Apply p 'True) = useThis

elimConst :: forall a k (b :: k) (p :: Const a b ~> Type) (s :: Const a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Const f0 :: Const a b)) -> Apply p s

type family ElimConst (p :: Const a b ~> Type) (s :: Const a b) (p1 :: forall (f0 :: a) -> Apply p ('Const f0 :: Const a b)) :: Apply p s where ...

Equations

ElimConst (p :: Const a b ~> Type) ('Const s0 :: Const a b) (useThis :: forall (f0 :: a) -> Apply p ('Const f0 :: Const a b)) = useThis s0

elimDown :: forall a (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 :: Down a ~> Type) (s :: Down a) (p1 :: forall (f0 :: a) -> Apply p ('Down f0)) :: Apply p s where ...

Equations

ElimDown (p :: Down a ~> Type) ('Down s0 :: Down a) (useThis :: forall (f0 :: a) -> Apply p ('Down f0)) = useThis s0

elimDual :: forall a (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 :: Dual a ~> Type) (s :: Dual a) (p1 :: forall (f0 :: a) -> Apply p ('Dual f0)) :: Apply p s where ...

Equations

ElimDual (p :: Dual a ~> Type) ('Dual s0 :: Dual a) (useThis :: forall (f0 :: a) -> Apply p ('Dual f0)) = useThis s0

elimEither :: forall a b (p :: Either a b ~> Type) (s :: Either a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Left f0 :: Either a b)) -> (forall (f0 :: b). Sing f0 -> Apply p ('Right f0 :: Either a b)) -> Apply p s

type family ElimEither (p :: Either a b ~> Type) (s :: Either a b) (p1 :: forall (f0 :: a) -> Apply p ('Left f0 :: Either a b)) (p2 :: forall (f0 :: b) -> Apply p ('Right f0 :: Either a b)) :: Apply p s where ...

Equations

ElimEither (p :: Either a b ~> Type) ('Left s0 :: Either a b) (useThis :: forall (f0 :: a) -> Apply p ('Left f0 :: Either a b)) (_p1 :: forall (f0 :: b) -> Apply p ('Right f0 :: Either a b)) = useThis s0

ElimEither (p :: Either a b ~> Type) ('Right s0 :: Either a b) (_p0 :: forall (f0 :: a) -> Apply p ('Left f0 :: Either a b)) (useThis :: forall (f0 :: b) -> Apply p ('Right f0 :: Either a b)) = useThis s0

elimIdentity :: forall a (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 :: Identity a ~> Type) (s :: Identity a) (p1 :: forall (f0 :: a) -> Apply p ('Identity f0)) :: Apply p s where ...

Equations

ElimIdentity (p :: Identity a ~> Type) ('Identity s0 :: Identity a) (useThis :: forall (f0 :: a) -> Apply p ('Identity f0)) = useThis s0

elimList :: forall a (p :: [a] ~> Type) (s :: [a]). Sing s -> Apply p ('[] :: [a]) -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> Apply p f1 -> Apply p (f0 ': f1)) -> Apply p s

type family ElimList (p :: [a] ~> Type) (s :: [a]) (p1 :: Apply p ('[] :: [a])) (p2 :: forall (f0 :: a) (f1 :: [a]) -> Apply p f1 ~> Apply p (f0 ': f1)) :: Apply p s where ...

Equations

ElimList (p :: [a] ~> Type) ('[] :: [a]) (useThis :: Apply p ('[] :: [a])) (_p1 :: forall (f0 :: a) (f1 :: [a]) -> Apply p f1 ~> Apply p (f0 ': f1)) = useThis

ElimList (p :: [a] ~> Type) (s0 ': s1 :: [a]) (_p0 :: Apply p ('[] :: [a])) (useThis :: forall (f0 :: a) (f1 :: [a]) -> Apply p f1 ~> Apply p (f0 ': f1)) = Apply (useThis s0 s1) (ElimList p s1 _p0 useThis)

elimMax :: forall a (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 :: Max a ~> Type) (s :: Max a) (p1 :: forall (f0 :: a) -> Apply p ('Max f0)) :: Apply p s where ...

Equations

ElimMax (p :: Max a ~> Type) ('Max s0 :: Max a) (useThis :: forall (f0 :: a) -> Apply p ('Max f0)) = useThis s0

elimMaybe :: forall a (p :: Maybe a ~> Type) (s :: Maybe a). Sing s -> Apply p ('Nothing :: Maybe a) -> (forall (f0 :: a). Sing f0 -> Apply p ('Just f0)) -> Apply p s

type family ElimMaybe (p :: Maybe a ~> Type) (s :: Maybe a) (p1 :: Apply p ('Nothing :: Maybe a)) (p2 :: forall (f0 :: a) -> Apply p ('Just f0)) :: Apply p s where ...

Equations

ElimMaybe (p :: Maybe a ~> Type) ('Nothing :: Maybe a) (useThis :: Apply p ('Nothing :: Maybe a)) (_p1 :: forall (f0 :: a) -> Apply p ('Just f0)) = useThis

ElimMaybe (p :: Maybe a ~> Type) ('Just s0 :: Maybe a) (_p0 :: Apply p ('Nothing :: Maybe a)) (useThis :: forall (f0 :: a) -> Apply p ('Just f0)) = useThis s0

elimMin :: forall a (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 :: Min a ~> Type) (s :: Min a) (p1 :: forall (f0 :: a) -> Apply p ('Min f0)) :: Apply p s where ...

Equations

ElimMin (p :: Min a ~> Type) ('Min s0 :: Min a) (useThis :: forall (f0 :: a) -> Apply p ('Min f0)) = 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 :: Nat ~> Type) (s :: Nat) (p1 :: Apply p 'Z) (p2 :: forall (f0 :: Nat) -> Apply p f0 ~> Apply p ('S f0)) :: Apply p s where ...

Equations

ElimNat p 'Z (useThis :: Apply p 'Z) (_p1 :: forall (f0 :: Nat) -> Apply p f0 ~> Apply p ('S f0)) = useThis

ElimNat p ('S s0) (_p0 :: Apply p 'Z) (useThis :: forall (f0 :: Nat) -> Apply p f0 ~> Apply p ('S f0)) = Apply (useThis s0) (ElimNat p s0 _p0 useThis)

elimNonEmpty :: forall a (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 :: NonEmpty a ~> Type) (s :: NonEmpty a) (p1 :: forall (f0 :: a) (f1 :: [a]) -> Apply p (f0 ':| f1)) :: Apply p s where ...

Equations

ElimNonEmpty (p :: NonEmpty a ~> Type) (s0 ':| s1 :: NonEmpty a) (useThis :: forall (f0 :: a) (f1 :: [a]) -> Apply p (f0 ':| f1)) = 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 :: Ordering ~> Type) (s :: Ordering) (p1 :: Apply p 'LT) (p2 :: Apply p 'EQ) (p3 :: Apply p 'GT) :: Apply p s where ...

Equations

ElimOrdering p 'LT (useThis :: Apply p 'LT) (_p1 :: Apply p 'EQ) (_p2 :: Apply p 'GT) = useThis

ElimOrdering p 'EQ (_p0 :: Apply p 'LT) (useThis :: Apply p 'EQ) (_p2 :: Apply p 'GT) = useThis

ElimOrdering p 'GT (_p0 :: Apply p 'LT) (_p1 :: Apply p 'EQ) (useThis :: Apply p 'GT) = useThis

elimProxy :: forall k (t :: k) (p :: Proxy t ~> Type) (s :: Proxy t). Sing s -> Apply p ('Proxy :: Proxy t) -> Apply p s

type family ElimProxy (p :: Proxy t ~> Type) (s :: Proxy t) (p1 :: Apply p ('Proxy :: Proxy t)) :: Apply p s where ...

Equations

ElimProxy (p :: Proxy t ~> Type) ('Proxy :: Proxy t) (useThis :: Apply p ('Proxy :: Proxy t)) = useThis

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

type family ElimTuple0 (p :: () ~> Type) (s :: ()) (p1 :: Apply p '()) :: Apply p s where ...

Equations

ElimTuple0 p '() (useThis :: Apply p '()) = useThis

elimTuple2 :: forall a b (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 :: (a, b) ~> Type) (s :: (a, b)) (p1 :: forall (f0 :: a) (f1 :: b) -> Apply p '(f0, f1)) :: Apply p s where ...

Equations

ElimTuple2 (p :: (a, b) ~> Type) ('(s0, s1) :: (a, b)) (useThis :: forall (f0 :: a) (f1 :: b) -> Apply p '(f0, f1)) = useThis s0 s1

elimTuple3 :: forall a b c (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 :: (a, b, c) ~> Type) (s :: (a, b, c)) (p1 :: forall (f0 :: a) (f1 :: b) (f2 :: c) -> Apply p '(f0, f1, f2)) :: Apply p s where ...

Equations

ElimTuple3 (p :: (a, b, c) ~> Type) ('(s0, s1, s2) :: (a, b, c)) (useThis :: forall (f0 :: a) (f1 :: b) (f2 :: c) -> Apply p '(f0, f1, f2)) = useThis s0 s1 s2

elimTuple4 :: forall a b c d (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 :: (a, b, c, d) ~> Type) (s :: (a, b, c, d)) (p1 :: forall (f0 :: a) (f1 :: b) (f2 :: c) (f3 :: d) -> Apply p '(f0, f1, f2, f3)) :: Apply p s where ...

Equations

ElimTuple4 (p :: (a, b, c, d) ~> Type) ('(s0, s1, s2, s3) :: (a, b, c, d)) (useThis :: forall (f0 :: a) (f1 :: b) (f2 :: c) (f3 :: d) -> Apply p '(f0, f1, f2, f3)) = useThis s0 s1 s2 s3

elimTuple5 :: forall a b c d e (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 :: (a, b, c, d, e) ~> Type) (s :: (a, b, c, d, e)) (p1 :: forall (f0 :: a) (f1 :: b) (f2 :: c) (f3 :: d) (f4 :: e) -> Apply p '(f0, f1, f2, f3, f4)) :: Apply p s where ...

Equations

ElimTuple5 (p :: (a, b, c, d, e) ~> Type) ('(s0, s1, s2, s3, s4) :: (a, b, c, d, e)) (useThis :: forall (f0 :: a) (f1 :: b) (f2 :: c) (f3 :: d) (f4 :: e) -> Apply p '(f0, f1, f2, f3, f4)) = useThis s0 s1 s2 s3 s4

elimTuple6 :: forall a b c d e f (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 :: (a, b, c, d, e, f) ~> Type) (s :: (a, b, c, d, e, f)) (p1 :: forall (f0 :: a) (f1 :: b) (f2 :: c) (f3 :: d) (f4 :: e) (f5 :: f) -> Apply p '(f0, f1, f2, f3, f4, f5)) :: Apply p s where ...

Equations

ElimTuple6 (p :: (a, b, c, d, e, f) ~> Type) ('(s0, s1, s2, s3, s4, s5) :: (a, b, c, d, e, f)) (useThis :: forall (f0 :: a) (f1 :: b) (f2 :: c) (f3 :: d) (f4 :: e) (f5 :: f) -> Apply p '(f0, f1, f2, f3, f4, f5)) = useThis s0 s1 s2 s3 s4 s5

elimTuple7 :: forall a b c d e f g (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 :: (a, b, c, d, e, f, g) ~> Type) (s :: (a, b, c, d, e, f, g)) (p1 :: forall (f0 :: a) (f1 :: b) (f2 :: c) (f3 :: d) (f4 :: e) (f5 :: f) (f6 :: g) -> Apply p '(f0, f1, f2, f3, f4, f5, f6)) :: Apply p s where ...

Equations

ElimTuple7 (p :: (a, b, c, d, e, f, g) ~> Type) ('(s0, s1, s2, s3, s4, s5, s6) :: (a, b, c, d, e, f, g)) (useThis :: forall (f0 :: a) (f1 :: b) (f2 :: c) (f3 :: d) (f4 :: e) (f5 :: f) (f6 :: g) -> Apply p '(f0, f1, f2, f3, f4, f5, f6)) = useThis s0 s1 s2 s3 s4 s5 s6

elimVoid :: forall (p :: Void ~> Type) (s :: Void). Sing s -> Apply p s

type family ElimVoid (p :: Void ~> Type) (s :: Void) :: Apply p s where ...

elimWrappedMonoid :: forall m (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 :: WrappedMonoid m ~> Type) (s :: WrappedMonoid m) (p1 :: forall (f0 :: m) -> Apply p ('WrapMonoid f0)) :: Apply p s where ...

Equations

ElimWrappedMonoid (p :: WrappedMonoid m ~> Type) ('WrapMonoid s0 :: WrappedMonoid m) (useThis :: forall (f0 :: m) -> Apply p ('WrapMonoid f0)) = useThis s0