lens-5.0.1: Lenses, Folds and Traversals

Control.Lens.Equality

Description

Synopsis

# 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) Source #

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

Note: Composition with an Equality is index-preserving.

type Equality' s a = Equality s s a a Source #

A Simple Equality.

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

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

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

A Simple AnEquality.

data (a :: k) :~: (b :: k) where infix 4 Source #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

 Refl :: forall k (a :: k). a :~: a

#### Instances

Instances details
 Category ((:~:) :: k -> k -> Type) Since: base-4.7.0.0 Instance detailsDefined in Control.Category Methodsid :: forall (a :: k0). a :~: a Source #(.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~: c) -> (a :~: b) -> a :~: c Source # Semigroupoid ((:~:) :: k -> k -> Type) Instance detailsDefined in Data.Semigroupoid Methodso :: forall (j :: k0) (k1 :: k0) (i :: k0). (j :~: k1) -> (i :~: j) -> i :~: k1 Source # TestCoercion ((:~:) a :: k -> Type) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion MethodstestCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) Source # TestEquality ((:~:) a :: k -> Type) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality MethodstestEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source # NFData2 ((:~:) :: Type -> Type -> Type) Since: deepseq-1.4.3.0 Instance detailsDefined in Control.DeepSeq MethodsliftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> () Source # NFData1 ((:~:) a) Since: deepseq-1.4.3.0 Instance detailsDefined in Control.DeepSeq MethodsliftRnf :: (a0 -> ()) -> (a :~: a0) -> () Source # a ~ b => Bounded (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality MethodsminBound :: a :~: b Source #maxBound :: a :~: b Source # a ~ b => Enum (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality Methodssucc :: (a :~: b) -> a :~: b Source #pred :: (a :~: b) -> a :~: b Source #toEnum :: Int -> a :~: b Source #fromEnum :: (a :~: b) -> Int Source #enumFrom :: (a :~: b) -> [a :~: b] Source #enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source # Eq (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality Methods(==) :: (a :~: b) -> (a :~: b) -> Bool Source #(/=) :: (a :~: b) -> (a :~: b) -> Bool Source # (a ~ b, Data a) => Data (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Data Methodsgfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) Source #gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Source #toConstr :: (a :~: b) -> Constr Source #dataTypeOf :: (a :~: b) -> DataType Source #dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Source #dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Source #gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source #gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source #gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source #gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source #gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # Ord (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality Methodscompare :: (a :~: b) -> (a :~: b) -> Ordering Source #(<) :: (a :~: b) -> (a :~: b) -> Bool Source #(<=) :: (a :~: b) -> (a :~: b) -> Bool Source #(>) :: (a :~: b) -> (a :~: b) -> Bool Source #(>=) :: (a :~: b) -> (a :~: b) -> Bool Source #max :: (a :~: b) -> (a :~: b) -> a :~: b Source #min :: (a :~: b) -> (a :~: b) -> a :~: b Source # a ~ b => Read (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality MethodsreadsPrec :: Int -> ReadS (a :~: b) Source #readList :: ReadS [a :~: b] Source # Show (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality MethodsshowsPrec :: Int -> (a :~: b) -> ShowS Source #show :: (a :~: b) -> String Source #showList :: [a :~: b] -> ShowS Source # NFData (a :~: b) Since: deepseq-1.4.3.0 Instance detailsDefined in Control.DeepSeq Methodsrnf :: (a :~: b) -> () Source #

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

Extract a witness of type Equality.

substEq :: forall s t a b rep (r :: TYPE rep). AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r Source #

Substituting types with Equality.

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

We can use Equality to do substitution into anything.

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

Equality is symmetric.

simply :: forall p f s a rep (r :: TYPE rep). (Optic' p f s a -> r) -> Optic' p f s a -> r Source #

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

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.

# Iso-like functions

equality :: (s :~: a) -> (b :~: t) -> Equality s t a b Source #

Construct an Equality from explicit equality evidence.

equality' :: (a :~: b) -> Equality' a b Source #

A Simple version of equality

withEquality :: forall s t a b rep (r :: TYPE rep). AnEquality s t a b -> ((s :~: a) -> (b :~: t) -> r) -> r Source #

A version of substEq that provides explicit, rather than implicit, equality evidence.

underEquality :: AnEquality s t a b -> p t s -> p b a Source #

The opposite of working overEquality is working underEquality.

overEquality :: AnEquality s t a b -> p a b -> p s t Source #

Recover a "profunctor lens" form of equality. Reverses fromLeibniz.

fromLeibniz :: (Identical a b a b -> Identical a b s t) -> Equality s t a b Source #

Convert a "profunctor lens" form of equality to an equality. Reverses overEquality.

The type should be understood as

fromLeibniz :: (forall p. p a b -> p s t) -> Equality s t a b

fromLeibniz' :: ((s :~: s) -> s :~: a) -> Equality' s a Source #

Convert Leibniz equality to equality. Reverses mapEq in Simple cases.

The type should be understood as

fromLeibniz' :: (forall f. f s -> f a) -> Equality' s a

cloneEquality :: AnEquality s t a b -> Equality s t a b Source #

# Implementation Details

data Identical a b s t where Source #

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

Constructors

 Identical :: Identical a b a b