0 | module Data.Linear.Bifunctor
 1 |
 2 | import Data.Linear.Notation
 3 |
 4 | %default total
 5 |
 6 | ||| A linear bimap on linear pairs.
 7 | ||| There is no general Bifunctor interface because it would not be implementable with
 8 | ||| The same type signature consistently, for example LEither does not consume both
 9 | ||| `f` and `g` linearly.
10 | public export
11 | bimap : (a -@ x) -@ (b -@ y) -@ (LPair a b) -@ (LPair x y)
12 | bimap f g (a # b) = f a # g b
13 |
14 | public export
15 | mapFst : (a -@ x) -@ LPair a b -@ LPair x b
16 | mapFst f = bimap f id
17 |
18 | public export
19 | mapSnd : (b -@ y) -@ LPair a b -@ LPair a y
20 | mapSnd = bimap id
21 |