| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Ouroboros.Consensus.Util.DepPair
Synopsis
- type DepPair = GenDepPair I
- data GenDepPair (g ∷ k → Type) (f ∷ k → Type) where
- GenDepPair ∷ ∀ {k} (f ∷ k → Type) (a ∷ k) (g ∷ k → Type). !(f a) → !(g a) → GenDepPair g f
- pattern DepPair ∷ () ⇒ f a → a → DepPair f
- depPairFirst ∷ ∀ {k} f f' (g ∷ k → Type). (∀ (a ∷ k). f a → f' a) → GenDepPair g f → GenDepPair g f'
- class SameDepIndex (f ∷ k → Type) where
- sameDepIndex ∷ ∀ (a ∷ k) (b ∷ k). f a → f b → Maybe (a :~: b)
- class SameDepIndex2 (f ∷ k1 → k2 → Type) where
- sameDepIndex2 ∷ ∀ (x ∷ k1) (a ∷ k2) (y ∷ k1) (b ∷ k2). f x a → f y b → Maybe ('(x, a) :~: '(y, b))
- class TrivialDependency (f ∷ k → Type) where
- type TrivialIndex (f ∷ k → Type) ∷ k1
- hasSingleIndex ∷ ∀ (a ∷ k) (b ∷ k). f a → f b → a :~: b
- indexIsTrivial ∷ f (TrivialIndex f ∷ k)
- fromTrivialDependency ∷ TrivialDependency f ⇒ f a → a → TrivialIndex f ∷ Type
- toTrivialDependency ∷ TrivialDependency f ⇒ f a → (TrivialIndex f ∷ Type) → a
- data Proxy (t ∷ k) = Proxy
- data (a ∷ k) :~: (b ∷ k) where
Dependent pairs
type DepPair = GenDepPair I Source #
Dependent pair
A dependent pair is a pair of values where the type of the value depends on the first value.
data GenDepPair (g ∷ k → Type) (f ∷ k → Type) where Source #
Generalization of DepPair
This adds an additional functor g around the second value in the pair.
Constructors
| GenDepPair ∷ ∀ {k} (f ∷ k → Type) (a ∷ k) (g ∷ k → Type). !(f a) → !(g a) → GenDepPair g f |
Instances
depPairFirst ∷ ∀ {k} f f' (g ∷ k → Type). (∀ (a ∷ k). f a → f' a) → GenDepPair g f → GenDepPair g f' Source #
Compare indices
class SameDepIndex (f ∷ k → Type) where Source #
Minimal complete definition
Nothing
Methods
sameDepIndex ∷ ∀ (a ∷ k) (b ∷ k). f a → f b → Maybe (a :~: b) Source #
default sameDepIndex ∷ ∀ (a ∷ k) (b ∷ k). TrivialDependency f ⇒ f a → f b → Maybe (a :~: b) Source #
Instances
class SameDepIndex2 (f ∷ k1 → k2 → Type) where Source #
Methods
sameDepIndex2 ∷ ∀ (x ∷ k1) (a ∷ k2) (y ∷ k1) (b ∷ k2). f x a → f y b → Maybe ('(x, a) :~: '(y, b)) Source #
Instances
| All SingleEraBlock xs ⇒ SameDepIndex2 (QueryIfCurrent xs ∷ QueryFootprint → Type → Type) Source # | |
Defined in Ouroboros.Consensus.HardFork.Combinator.Ledger.Query Methods sameDepIndex2 ∷ ∀ (x ∷ QueryFootprint) a (y ∷ QueryFootprint) b. QueryIfCurrent xs x a → QueryIfCurrent xs y b → Maybe ('(x, a) :~: '(y, b)) Source # | |
| All SingleEraBlock xs ⇒ SameDepIndex2 (BlockQuery (HardForkBlock xs) ∷ QueryFootprint → Type → Type) Source # | |
Defined in Ouroboros.Consensus.HardFork.Combinator.Ledger.Query Methods sameDepIndex2 ∷ ∀ (x ∷ QueryFootprint) a (y ∷ QueryFootprint) b. BlockQuery (HardForkBlock xs) x a → BlockQuery (HardForkBlock xs) y b → Maybe ('(x, a) :~: '(y, b)) Source # | |
| SameDepIndex2 (BlockQuery (DualBlock m a) ∷ QueryFootprint → Type → Type) Source # | |
Defined in Ouroboros.Consensus.Ledger.Dual Methods sameDepIndex2 ∷ ∀ (x ∷ QueryFootprint) a0 (y ∷ QueryFootprint) b. BlockQuery (DualBlock m a) x a0 → BlockQuery (DualBlock m a) y b → Maybe ('(x, a0) :~: '(y, b)) Source # | |
Trivial dependency
class TrivialDependency (f ∷ k → Type) where Source #
A dependency is trivial if it always maps to the same type b
Associated Types
type TrivialIndex (f ∷ k → Type) ∷ k1 Source #
Methods
hasSingleIndex ∷ ∀ (a ∷ k) (b ∷ k). f a → f b → a :~: b Source #
indexIsTrivial ∷ f (TrivialIndex f ∷ k) Source #
Instances
| TrivialDependency (NestedCtxt_ blk f) ⇒ TrivialDependency (NestedCtxt f blk ∷ Type → Type) Source # | |
Defined in Ouroboros.Consensus.Block.NestedContent Methods hasSingleIndex ∷ NestedCtxt f blk a → NestedCtxt f blk b → a :~: b Source # indexIsTrivial ∷ NestedCtxt f blk (TrivialIndex (NestedCtxt f blk) ∷ Type) Source # | |
fromTrivialDependency ∷ TrivialDependency f ⇒ f a → a → TrivialIndex f ∷ Type Source #
toTrivialDependency ∷ TrivialDependency f ⇒ f a → (TrivialIndex f ∷ Type) → a Source #
Convenience re-exports
Proxy is a type that holds no data, but has a phantom parameter of
arbitrary type (or even kind). Its use is to provide type information, even
though there is no value available of that type (or it may be too costly to
create one).
Historically, Proxy :: Proxy aundefined :: a
>>>Proxy :: Proxy (Void, Int -> Int)Proxy
Proxy can even hold types of higher kinds,
>>>Proxy :: Proxy EitherProxy
>>>Proxy :: Proxy FunctorProxy
>>>Proxy :: Proxy complicatedStructureProxy
Constructors
| Proxy |
Instances
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
Instances
| Category ((:~:) ∷ k → k → Type) | Since: base-4.7.0.0 |
| TestEquality ((:~:) a ∷ k → Type) | Since: base-4.7.0.0 |
Defined in GHC.Internal.Data.Type.Equality | |
| GCompare ((:~:) a ∷ k → Type) | |
| GEq ((:~:) a ∷ k → Type) | |
| GRead ((:~:) a ∷ k → Type) | |
Defined in Data.GADT.Internal | |
| GShow ((:~:) a ∷ k → Type) | |
Defined in Data.GADT.Internal | |
| 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 | |
| NFData (a :~: b) | 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 |
| a ~ b ⇒ Read (a :~: b) | Since: base-4.7.0.0 |
| Show (a :~: b) | Since: base-4.7.0.0 |
| Eq (a :~: b) | Since: base-4.7.0.0 |
| Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in GHC.Internal.Data.Type.Equality | |