bimap f g empty == empty bimap f g . vertex == vertex . Data.Bifunctor.bimap f g bimap f g (edge x y) == edge (f x) (g y) bimap id id == id bimap f1 g1 . bimap f2 g2 == bimap (f1 . f2) (g1 . g2)
>>> let f = uninterpret "f" :: SInteger -> SInteger >>> let g = uninterpret "g" :: SInteger -> SInteger >>> prove $ \x -> fromLeft (bimap f g (sLeft x)) .== f x Q.E.D. >>> prove $ \x -> fromRight (bimap f g (sRight x)) .== g x Q.E.D.
>>> :kind! Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat) = '(3, 3)
>>> bimapAccumL (\acc bool -> (acc + 1, show bool)) (\acc string -> (acc * 2, reverse string)) 3 (True, "foo") (8,("True","oof"))
>>> bimapAccumR (\acc bool -> (acc + 1, show bool)) (\acc string -> (acc * 2, reverse string)) 3 (True, "foo") (7,("True","oof"))
bimapDefault f g ≡ runIdentity . bitraverse (Identity . f) (Identity . g)