bimap -package:Agda

Map over both arguments at the same time.

bimap f g ≡ first f . second g

Examples

>>> bimap toUpper (+1) ('j', 3)
('J',4)

>>> bimap toUpper (+1) (Left 'j')
Left 'J'

>>> bimap toUpper (+1) (Right 3)
Right 4

Bidirectional mapping between two key types A data structure representing a bidirectional mapping between two key types. Each value in the bimap is associated with exactly one value of the opposite type.

Transform a graph by applying given functions to the vertices of each part. Complexity: O((n + m) * log(n)) time.

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)

Map over both sides of a symbolic Either at the same time

>>> 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.

An implementation of bidirectional maps between values of two key types. A Bimap is essentially a bijection between subsets of its two argument types. Each element of the left-hand type is associated with an element of the right-hand type, and vice-versa, such that the two mappings are inverses. Deleting an element will cause its twin to be deleted, and inserting a pair of elements will cause any overlapping bindings to be deleted. Most functions implicitly consider the left-hand type to be the key, and the right-hand type to be the value. Functions with an R suffix reverse this convention, treating the right-hand type as the key and the left-hand type as the value.

A bidirectional map between values of types a and b.

Bidirectional map. Essentially, a bijection between subsets of its two argument types. For one value of the left-hand type this map contains one value of the right-hand type and vice versa.

Type-level bimap.

Example

>>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions

>>> :kind! Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural))
Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural)) :: Example
= Ex '(3, 3)

Implementation of Tagged Partial Bidirectional Isomorphism. This module contains the BiMap type that represents conversion between two types with the possibility of failure. See Toml.Codec.BiMap.Conversion for examples of BiMap with specific types. The BiMap concept is general and is not specific to TOML, but in this package most usages of BiMap are between TOML values and Haskell values.

Partial bidirectional isomorphism. BiMap a b contains two function:

1. a -> Either e b

2. b -> Either e a

If you think of types as sets then this data type can be illustrated by the following picture: BiMap also implements Category typeclass. And this instance can be described clearly by this illustration:

Bijection between finite sets. Both data types are strict here.

Alias for bitraverse_.

The bimapAccumL function behaves like a combination of bimap and bifoldl; it traverses a structure from left to right, threading a state of type a and using the given actions to compute new elements for the structure.

Examples

Basic usage:

>>> bimapAccumL (\acc bool -> (acc + 1, show bool)) (\acc string -> (acc * 2, reverse string)) 3 (True, "foo")
(8,("True","oof"))

The bimapAccumR function behaves like a combination of bimap and bifoldr; it traverses a structure from right to left, threading a state of type a and using the given actions to compute new elements for the structure.

Examples

Basic usage:

>>> bimapAccumR (\acc bool -> (acc + 1, show bool)) (\acc string -> (acc * 2, reverse string)) 3 (True, "foo")
(7,("True","oof"))

A default definition of bimap in terms of the Bitraversable operations.

bimapDefault f g ≡
runIdentity . bitraverse (Identity . f) (Identity . g)