0 | ||| This module provides a compatibility layer between the traditional
 1 | ||| Haskell arrow hierarchy and the categorical interfaces of this
 2 | ||| library. These functions may be easier to write code with for users
 3 | ||| who are already familiar with arrows.
 4 | |||
 5 | ||| Currently, the `Arrow`, `ArrowChoice` and `ArrowLoop` interfaces
 6 | ||| are fully defined. `ArrowPlus` may also be defined in the future
 7 | ||| if I ever get around to adding support for enriched categories.
 8 | |||
 9 | ||| `ArrowApply` will most likely never be added, as it is not very
10 | ||| well-behaved categorically and is also essentially useless.
11 | module Control.Arrow
12 |
13 | import public Control.Category.Core as Control.Category
14 | import Control.Category
15 | import Control.Category.Promonad
16 | import Control.Category.Traced
17 | import Data.Either
18 | import Data.Morphisms
19 | import Data.Wrap0
20 |
21 | %default total
22 |
23 | export infixr 7 ***
24 | export infixr 7 &&&
25 | export infixr 6 +++
26 | export infixr 6 \|/
27 |
28 | ------------------------------------------------------------
29 | -- Interface
30 | ------------------------------------------------------------
31 |
32 | public export
33 | 0 Arrow : (arr : Hom Type0) -> Type
34 | Arrow arr = (Promonad0 arr, EndoBinoidal arr (liftW2 Pair))
35 |
36 | public export
37 | 0 ArrowChoice : (arr : Hom Type0) -> Type
38 | ArrowChoice arr = (Arrow arr, EndoBinoidal arr (liftW2 Either))
39 |
40 | public export
41 | 0 ArrowLoop : (arr : Hom Type0) -> Type
42 | ArrowLoop arr = (Promonad0 arr, Traced arr (liftW2 Pair) (W0 ()))
43 |
44 |
45 | ------------------------------------------------------------
46 | -- Functions
47 | ------------------------------------------------------------
48 |
49 | public export %inline
50 | arrow : Arrow arr => (a -> b) -> arr (W0 a) (W0 b)
51 | arrow = funitW
52 |
53 | public export %inline
54 | first : Arrow arr => arr (W0 a) (W0 b) -> arr (W0 (a, c)) (W0 (b, c))
55 | first = mapl' {f=liftW2 Pair,a=W0 _,b=W0 _,c=W0 _}
56 |
57 | public export %inline
58 | second : Arrow arr => arr (W0 a) (W0 b) -> arr (W0 (c, a)) (W0 (c, b))
59 | second = mapr' {f=liftW2 Pair,a=W0 _,b=W0 _,c=W0 _}
60 |
61 | public export
62 | (***) : Arrow arr => arr (W0 a) (W0 b) -> arr (W0 a') (W0 b') -> arr (W0 (a, a')) (W0 (b, b'))
63 | f *** g = first f >>> second g
64 |
65 | public export
66 | (&&&) : Arrow arr => arr (W0 a) (W0 b) -> arr (W0 a) (W0 b') -> arr (W0 a) (W0 (b, b'))
67 | f &&& g = arrow dup >>> f *** g
68 |
69 | public export
70 | liftA2 : Arrow arr => (a -> b -> c) -> arr (W0 d) (W0 a) -> arr (W0 d) (W0 b) -> arr (W0 d) (W0 c)
71 | liftA2 op f g = (f &&& g) >>> arrow (uncurry op)
72 |
73 |
74 | public export %inline
75 | left : ArrowChoice arr => arr (W0 a) (W0 b) -> arr (W0 $ Either a c) (W0 $ Either b c)
76 | left = mapl' {f=liftW2 Either,a=W0 _,b=W0 _,c=W0 _}
77 |
78 | public export %inline
79 | right : ArrowChoice arr => arr (W0 a) (W0 b) -> arr (W0 $ Either c a) (W0 $ Either c b)
80 | right = mapr' {f=liftW2 Either,a=W0 _,b=W0 _,c=W0 _}
81 |
82 | public export
83 | (+++) : ArrowChoice arr => arr (W0 a) (W0 b) -> arr (W0 a') (W0 b') -> arr (W0 $ Either a a') (W0 $ Either b b')
84 | f +++ g = left f >>> right g
85 |
86 | public export
87 | (\|/) : ArrowChoice arr => arr (W0 a) (W0 b) -> arr (W0 a') (W0 b) -> arr (W0 $ Either a a') (W0 b)
88 | f \|/ g = f +++ g >>> arrow fromEither
89 |
90 |
91 | public export %inline
92 | loop : ArrowLoop arr => arr (W0 (a, c)) (W0 (b, c)) -> arr (W0 a) (W0 b)
93 | loop = tracer {ten=liftW2 Pair,a=W0 _,b=W0 _,c=W0 _}
94 |