Copyright	(C) 2021 Ryan Scott
License	BSD-style (see the file LICENSE)
Maintainer	Ryan Scott
Stability	Experimental
Portability	GHC
Safe Haskell	Trustworthy
Language	GHC2021

Data.Eliminator.Functor

Description

Eliminator functions for data types in the Data.Functor.* module namespace. All of these are re-exported from Data.Eliminator with the exceptions of Sum and Product, as these clash with eliminators of the same names in Data.Eliminator.Semigroup and Data.Eliminator.Monoid.

Documentation

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

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

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

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

Equations

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

elimProduct :: forall k (f :: k -> Type) (g :: k -> Type) (a :: k) (p :: Product f g a ~> Type) (s :: Product f g a). Sing s -> (forall (f0 :: f a). Sing f0 -> forall (f1 :: g a). Sing f1 -> Apply p ('Pair f0 f1)) -> Apply p s Source #

type family ElimProduct (p :: Product f g a ~> Type) (s :: Product f g a) (p1 :: forall (f0 :: f a) (f1 :: g a) -> Apply p ('Pair f0 f1)) :: Apply p s where ... Source #

Equations

ElimProduct (p :: Product f g a ~> Type) ('Pair s0 s1 :: Product f g a) (useThis :: forall (f0 :: f a) (f1 :: g a) -> Apply p ('Pair f0 f1)) = useThis s0 s1

elimSum :: forall k (f :: k -> Type) (g :: k -> Type) (a :: k) (p :: Sum f g a ~> Type) (s :: Sum f g a). Sing s -> (forall (f0 :: f a). Sing f0 -> Apply p ('InL f0 :: Sum f g a)) -> (forall (f0 :: g a). Sing f0 -> Apply p ('InR f0 :: Sum f g a)) -> Apply p s Source #

type family ElimSum (p :: Sum f g a ~> Type) (s :: Sum f g a) (p1 :: forall (f0 :: f a) -> Apply p ('InL f0 :: Sum f g a)) (p2 :: forall (f0 :: g a) -> Apply p ('InR f0 :: Sum f g a)) :: Apply p s where ... Source #

Equations

ElimSum (p :: Sum f g a ~> Type) ('InL s0 :: Sum f g a) (useThis :: forall (f0 :: f a) -> Apply p ('InL f0 :: Sum f g a)) (_p1 :: forall (f0 :: g a) -> Apply p ('InR f0 :: Sum f g a)) = useThis s0
ElimSum (p :: Sum f g a ~> Type) ('InR s0 :: Sum f g a) (_p0 :: forall (f0 :: f a) -> Apply p ('InL f0 :: Sum f g a)) (useThis :: forall (f0 :: g a) -> Apply p ('InR f0 :: Sum f g a)) = useThis s0