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
- 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 a
s) and y :: g b
(a consumer of b
s), 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.