Copyright | (C) 2021 Ryan Scott |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Ryan Scott |
Stability | Experimental |
Portability | GHC |
Safe Haskell | Trustworthy |
Language | GHC2021 |
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 #
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 #
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 #
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 #
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 |