Copyright | (C) 2012-16 Edward Kmett |
---|---|

License | BSD-style (see the file LICENSE) |

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

Stability | provisional |

Portability | Rank2Types |

Safe Haskell | Safe |

Language | Haskell98 |

## Synopsis

- type Equality (s :: k1) (t :: k2) (a :: k1) (b :: k2) = forall k3 (p :: k1 -> k3 -> Type) (f :: k2 -> k3). p a (f b) -> p s (f t)
- type Equality' s a = Equality s s a a
- type AnEquality (s :: k1) (t :: k2) (a :: k1) (b :: k2) = Identical a (Proxy b) a (Proxy b) -> Identical a (Proxy b) s (Proxy 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 :: forall (s :: k1) (t :: k2) (a :: k1) (b :: k2) (f :: k1 -> *). 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 :: k1) (t :: k2) (a :: k1) (b :: k2) = forall k3 (p :: k1 -> k3 -> Type) (f :: k2 -> k3). p a (f b) -> p s (f t) #

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

.

Note: Composition with an `Equality`

is index-preserving.

type AnEquality (s :: k1) (t :: k2) (a :: k1) (b :: k2) = Identical a (Proxy b) a (Proxy b) -> Identical a (Proxy b) s (Proxy t) #

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

.

type AnEquality' s a = AnEquality s s a a #

A `Simple`

`AnEquality`

.

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

Extract a witness of type `Equality`

.

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

Substituting types with `Equality`

.

mapEq :: forall (s :: k1) (t :: k2) (a :: k1) (b :: k2) (f :: k1 -> *). AnEquality s t a b -> f s -> f a #

We can use `Equality`

to do substitution into anything.

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

`Equality`

is symmetric.

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

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.