Control.Arrow

This module provides a compatibility layer between the traditional
Haskell arrow hierarchy and the categorical interfaces of this
library. These functions may be easier to write code with for users
who are already familiar with arrows.

Currently, the `Arrow`, `ArrowChoice` and `ArrowLoop` interfaces
are fully defined. `ArrowPlus` may also be defined in the future
if I ever get around to adding support for enriched categories.

`ArrowApply` will most likely never be added, as it is not very
well-behaved categorically and is also essentially useless.

Reexports

Definitions

0 Arrow : Hom Type0 -> Type

Totality: total
Visibility: public export

0 ArrowChoice : Hom Type0 -> Type

Totality: total
Visibility: public export

0 ArrowLoop : Hom Type0 -> Type

Totality: total
Visibility: public export

arrow : Arrow arr => (a -> b) -> arr (W0 a) (W0 b)

Totality: total
Visibility: public export

first : Arrow arr => arr (W0 a) (W0 b) -> arr (W0 (a, c)) (W0 (b, c))

Totality: total
Visibility: public export

second : Arrow arr => arr (W0 a) (W0 b) -> arr (W0 (c, a)) (W0 (c, b))

Totality: total
Visibility: public export

(***) : Arrow arr => arr (W0 a) (W0 b) -> arr (W0 a') (W0 b') -> arr (W0 (a, a')) (W0 (b, b'))

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

(&&&) : Arrow arr => arr (W0 a) (W0 b) -> arr (W0 a) (W0 b') -> arr (W0 a) (W0 (b, b'))

Totality: total
Visibility: public export
Fixity Declarations:
infixr operator, level 7
infixr operator, level 7

liftA2 : Arrow arr => (a -> b -> c) -> arr (W0 d) (W0 a) -> arr (W0 d) (W0 b) -> arr (W0 d) (W0 c)

Totality: total
Visibility: public export

left : ArrowChoice arr => arr (W0 a) (W0 b) -> arr (W0 (Either a c)) (W0 (Either b c))

Totality: total
Visibility: public export

right : ArrowChoice arr => arr (W0 a) (W0 b) -> arr (W0 (Either c a)) (W0 (Either c b))

Totality: total
Visibility: public export

(+++) : ArrowChoice arr => arr (W0 a) (W0 b) -> arr (W0 a') (W0 b') -> arr (W0 (Either a a')) (W0 (Either b b'))

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 6

(\|/) : ArrowChoice arr => arr (W0 a) (W0 b) -> arr (W0 a') (W0 b) -> arr (W0 (Either a a')) (W0 b)

Totality: total
Visibility: public export
Fixity Declarations:
infixr operator, level 6
infixr operator, level 6

loop : ArrowLoop arr => arr (W0 (a, c)) (W0 (b, c)) -> arr (W0 a) (W0 b)

Totality: total
Visibility: public export