Copyright | (c) Justin Le 2019 |
---|---|
License | BSD3 |
Maintainer | justin@jle.im |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- data Night :: (Type -> Type) -> (Type -> Type) -> Type -> Type where
- newtype Not a = Not {}
- refuted :: Not Void
- night :: f a -> g b -> Night f g (Either a b)
- runNight :: Inalt h => (f ~> h) -> (g ~> h) -> Night f g ~> h
- nerve :: Inalt f => Night f f ~> f
- runNightAlt :: forall f g h. Alt h => (f ~> h) -> (g ~> h) -> Night f g ~> h
- runNightDecide :: forall f g h. Decide h => (f ~> h) -> (g ~> h) -> Night f g ~> h
- toCoNight :: (Functor f, Functor g) => Night f g ~> (f :*: g)
- toCoNight_ :: Night f g ~> (Coyoneda f :*: Coyoneda g)
- toContraNight :: Night f g ~> Night f g
- assoc :: Night f (Night g h) ~> Night (Night f g) h
- unassoc :: Night (Night f g) h ~> Night f (Night g h)
- intro1 :: g ~> Night Not g
- intro2 :: f ~> Night f Not
- elim1 :: Invariant g => Night Not g ~> g
- elim2 :: Invariant f => Night f Not ~> f
- 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
Documentation
data Night :: (Type -> Type) -> (Type -> Type) -> Type -> Type where Source #
A pairing of invariant functors to create a new invariant functor that represents the "choice" between the two.
A
is a invariant "consumer" and "producer" of Night
f g aa
, and
it does this by either feeding the a
to f
, or feeding the a
to
g
, and then collecting the result from whichever one it was fed to.
Which decision of which path to takes happens at runtime depending
what a
is actually given.
For example, if we have x :: f a
and y :: g b
, then
. This is a consumer/producer 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
. It then passes back the single result from the one of
the two that was chosen.
Mathematically, this is a invariant 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
A value of type
is "proof" that Not
aa
is uninhabited.
Instances
A useful shortcut for a common usage: Void
is always not so.
Since: 0.3.1.0
toContraNight :: Night f g ~> Night f g Source #
Convert an invariant Night
into the contravariant version, dropping
the covariant part.