0 | module Data.Contravariant
 1 |
 2 | %default total
 3 |
 4 | export infixl 4 >$, >$<, >&<, $<
 5 |
 6 | ||| Contravariant functors
 7 | public export
 8 | interface Contravariant (0 f : Type -> Type) where
 9 |   contramap : (a -> b) -> f b -> f a
10 |
11 |   (>$) : b -> f b -> f a
12 |   v >$ fb = contramap (const v) fb
13 |
14 | ||| If `f` is both `Functor` and `Contravariant` then by the time you factor in the
15 | ||| laws of each of those classes, it can't actually use its argument in any
16 | ||| meaningful capacity.
17 | public export %inline
18 | phantom : Contravariant f => Functor f => f a -> f b
19 | phantom fa = () >$ (fa $> ())
20 |
21 | ||| This is an infix alias for `contramap`.
22 | public export %inline
23 | (>$<) : Contravariant f => (a -> b) -> f b -> f a
24 | (>$<) = contramap
25 |
26 | ||| This is an infix version of `contramap` with the arguments flipped.
27 | public export %inline
28 | (>&<) : Contravariant f => f b -> (a -> b) -> f a
29 | (>&<) = flip contramap
30 |
31 | ||| This is `>$` with its arguments flipped.
32 | public export %inline
33 | ($<) : Contravariant f => f b -> b -> f a
34 | ($<) = flip (>$)
35 |
36 | ||| Composition of `Contravariant` is a `Functor`.
37 | public export
38 | [Compose] (Contravariant f, Contravariant g) => Functor (f . g) where
39 |   map = contramap . contramap
40 |
41 | ||| Composition of a `Functor` and a `Contravariant` is a `Contravariant`.
42 | public export
43 | [ComposeFC] (Functor f, Contravariant g) => Contravariant (f . g) where
44 |   contramap = map . contramap
45 |
46 | ||| Composition of a `Contravariant` and a `Functor` is a `Contravariant`.
47 | public export
48 | [ComposeCF] (Contravariant f, Functor g) => Contravariant (f . g) where
49 |   contramap = contramap . map
50 |