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 | None |
Language | Haskell2010 |
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
- data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where
- runEq :: AnEquality s t a b -> Identical s t a b
- substEq :: forall s t a b rep (r :: TYPE rep). AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r
- mapEq :: forall k1 k2 (s :: k1) (t :: k2) (a :: k1) (b :: k2) (f :: k1 -> Type). AnEquality s t a b -> f s -> f a
- fromEq :: AnEquality s t a b -> Equality b a t s
- simply :: forall p f s a rep (r :: TYPE rep). (Optic' p f s a -> r) -> Optic' p f s a -> r
- simple :: Equality' a a
- equality :: (s :~: a) -> (b :~: t) -> Equality s t a b
- equality' :: (a :~: b) -> Equality' a b
- withEquality :: forall s t a b rep (r :: TYPE rep). AnEquality s t a b -> ((s :~: a) -> (b :~: t) -> r) -> r
- underEquality :: AnEquality s t a b -> p t s -> p b a
- overEquality :: AnEquality s t a b -> p a b -> p s t
- fromLeibniz :: (Identical a b a b -> Identical a b s t) -> Equality s t a b
- fromLeibniz' :: ((s :~: s) -> s :~: a) -> Equality' s a
- cloneEquality :: AnEquality s t a b -> Equality s t a b
- 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) Source #
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) 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) :: forall k. k -> k -> Type 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
Instances
Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0 |
Semigroupoid ((:~:) :: k -> k -> Type) | |
TestCoercion ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Coercion | |
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
NFData1 ((:~:) a) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
Eq (a :~: b) | Since: base-4.7.0.0 |
(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Data 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 :: (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 | |
a ~ b => Read (a :~: b) | Since: base-4.7.0.0 |
Show (a :~: b) | Since: base-4.7.0.0 |
NFData (a :~: b) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq |
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.
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
Iso
-like functions
equality :: (s :~: a) -> (b :~: t) -> Equality s t a b Source #
Construct an Equality
from explicit equality evidence.
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
cloneEquality :: AnEquality s t a b -> Equality s t a b Source #