Portability | Rank2Types |
---|---|

Stability | provisional |

Maintainer | Edward Kmett <ekmett@gmail.com> |

Safe Haskell | Safe-Inferred |

- type Equality s t a b = forall p f. p a (f b) -> p s (f t)
- type Equality' s a = Equality s s a a
- type AnEquality s t a b = Identical a (Identity b) a (Identity b) -> Identical a (Identity b) s (Identity t)
- type AnEquality' s a = AnEquality s s a a
- runEq :: AnEquality s t a b -> Identical s t a b
- substEq :: AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
- mapEq :: AnEquality s t a b -> f s -> f a
- fromEq :: AnEquality s t a b -> Equality b a t s
- simply :: (Optic' p f s a -> r) -> Optic' p f s a -> r
- simple :: Equality' a a
- data Identical a b s t where

# Type Equality

type Equality s t a b = forall p f. p a (f b) -> p s (f t)Source

A witness that `(a ~ s, b ~ t)`

.

Note: Composition with an `Equality`

is index-preserving.

type AnEquality s t a b = Identical a (Identity b) a (Identity b) -> Identical a (Identity b) s (Identity t)Source

When you see this as an argument to a function, it expects an `Equality`

.

type AnEquality' s a = AnEquality s s a aSource

A `Simple`

`AnEquality`

.

runEq :: AnEquality s t a b -> Identical s t a bSource

Extract a witness of type `Equality`

.

substEq :: AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> rSource

Substituting types with `Equality`

.

mapEq :: AnEquality s t a b -> f s -> f aSource

We can use `Equality`

to do substitution into anything.

fromEq :: AnEquality s t a b -> Equality b a t sSource

`Equality`

is symmetric.

simply :: (Optic' p f s a -> r) -> Optic' p f s a -> rSource

This is an adverb that can be used to modify many other `Lens`

combinators to make them require
simple lenses, simple traversals, simple prisms or simple isos as input.