| 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 :: 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 #
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 |
elimProduct :: forall (k :: Type) (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 s p where ... Source #
Equations
| ElimProduct @k @f @g @a p ('Pair s0 s1) useThis = useThis s0 s1 |