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 t a b = 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.

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

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

Category ((:~:) :: k -> k -> Type)

Since: base-4.7.0.0

Defined in Control.Category

Methods

id :: forall (a :: k0). a :~: a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~: c) -> (a :~: b) -> a :~: c

Semigroupoid ((:~:) :: k -> k -> Type)

Defined in Data.Semigroupoid

Methods

o :: forall (j :: k0) (k1 :: k0) (i :: k0). (j :~: k1) -> (i :~: j) -> i :~: k1

TestCoercion ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in Data.Type.Coercion

Methods

testCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b)

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

NFData2 ((:~:) :: Type -> Type -> Type)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> ()

NFData1 ((:~:) a)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf :: (a0 -> ()) -> (a :~: a0) -> ()

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

Eq (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

(a ~ b, Data a) => Data (a :~: b)

Since: base-4.7.0.0

Defined in Data.Data

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b)

toConstr :: (a :~: b) -> Constr

dataTypeOf :: (a :~: b) -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

Ord (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

NFData (a :~: b)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

rnf :: (a :~: b) -> ()

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

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

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

We can use Equality to do substitution into anything.

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

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

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.

Iso-like functions

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

Construct an Equality from explicit equality evidence.

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

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

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

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

The opposite of working overEquality is working underEquality.

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

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

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

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

Implementation Details

data Identical a b s t where

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

Constructors

Identical :: Identical a b a b