Control.Lens.Equality

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 Equality' s a = Equality s s a a

A Simple Equality.

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 k1 k2 (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.

The Trivial Equality

simple :: Equality' a a

Composition with this isomorphism is occasionally useful when your Lens, Traversal or Iso has a constraint on an unused argument to force that argument to agree with the type of a used argument and avoid ScopedTypeVariables or other ugliness.

Implementation Details

data Identical a b s t where

Provides witness that (s ~ a, b ~ t) holds.

Constructors

Identical :: Identical a b a b