| Copyright | (c) Justin Le 2019 |
|---|---|
| License | BSD3 |
| Maintainer | justin@jle.im |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.Functor.Contravariant.Night
Description
Synopsis
- data Night :: (Type -> Type) -> (Type -> Type) -> Type -> Type where
- night :: f a -> g b -> Night f g (Either a b)
- runNight :: Decide h => (f ~> h) -> (g ~> h) -> Night f g ~> h
- necide :: Decide f => Night f f ~> f
- assoc :: Night f (Night g h) ~> Night (Night f g) h
- unassoc :: Night (Night f g) h ~> Night f (Night g h)
- swapped :: Night f g ~> Night g f
- trans1 :: (f ~> h) -> Night f g ~> Night h g
- trans2 :: (g ~> h) -> Night f g ~> Night f h
- intro1 :: g ~> Night Not g
- intro2 :: f ~> Night f Not
- elim1 :: Contravariant g => Night Not g ~> g
- elim2 :: Contravariant f => Night f Not ~> f
- newtype Not a = Not {}
- refuted :: Not Void
Documentation
data Night :: (Type -> Type) -> (Type -> Type) -> Type -> Type where Source #
A pairing of contravariant functors to create a new contravariant functor that represents the "choice" between the two.
A is a contravariant "consumer" of Night f g aa, and it does this
by either feeding the a to f, or feeding the a to g. Which one
it gives it to happens at runtime depending what a is actually
given.
For example, if we have x :: f a (a consumer of as) and y :: g b
(a consumer of bs), then .
This is a consumer of night x y :: Night f g (Either a b)s, and it consumes Either a bLeft branches
by feeding it to x, and Right branches by feeding it to y.
Mathematically, this is a contravariant day convolution, except with
a different choice of bifunctor (Either) than the typical one we talk
about in Haskell (which uses (,)). Therefore, it is an alternative to
the typical Day convolution --- hence, the name Night.
Instances
trans1 :: (f ~> h) -> Night f g ~> Night h g Source #
Hoist a function over the left side of a Night.
trans2 :: (g ~> h) -> Night f g ~> Night f h Source #
Hoist a function over the right side of a Night.
A value of type is "proof" that Not aa is uninhabited.