Safe Haskell | None |
---|---|
Language | Haskell2010 |
Data.SOP.Strict
Description
Strict variant of SOP
This does not currently attempt to be exhaustive.
Synopsis
- data NP ∷ (k → Type) → [k] → Type where
- hd ∷ NP f (x ': xs) → f x
- singletonNP ∷ f x → NP f '[x]
- tl ∷ NP f (x ': xs) → NP f xs
- data NS ∷ (k → Type) → [k] → Type where
- index_NS ∷ ∀ f xs. NS f xs → Int
- unZ ∷ NS f '[x] → f x
- type Injection (f ∷ k → Type) (xs ∷ [k]) = f -.-> K (NS f xs)
- injections ∷ ∀ xs f. SListI xs ⇒ NP (Injection f xs) xs
- data Proxy (t ∷ k) = Proxy
- mapII ∷ (a → b) → I a → I b
- mapIII ∷ (a → b → c) → I a → I b → I c
- mapIIK ∷ ∀ k a b c (d ∷ k). (a → b → c) → I a → I b → K c d
- mapIK ∷ ∀ k a b (c ∷ k). (a → b) → I a → K b c
- mapIKI ∷ ∀ k a b c (d ∷ k). (a → b → c) → I a → K b d → I c
- mapIKK ∷ ∀ k1 k2 a b c (d ∷ k1) (e ∷ k2). (a → b → c) → I a → K b d → K c e
- mapKI ∷ ∀ k a b (c ∷ k). (a → b) → K a c → I b
- mapKII ∷ ∀ k a b c (d ∷ k). (a → b → c) → K a d → I b → I c
- mapKIK ∷ ∀ k1 k2 a b c (d ∷ k1) (e ∷ k2). (a → b → c) → K a d → I b → K c e
- mapKK ∷ ∀ k1 k2 a b (c ∷ k1) (d ∷ k2). (a → b) → K a c → K b d
- mapKKI ∷ ∀ k1 k2 a b c (d ∷ k1) (e ∷ k2). (a → b → c) → K a d → K b e → I c
- mapKKK ∷ ∀ k1 k2 k3 a b c (d ∷ k1) (e ∷ k2) (f ∷ k3). (a → b → c) → K a d → K b e → K c f
- unComp ∷ ∀ l k f (g ∷ k → l) (p ∷ k). (f :.: g) p → f (g p)
- unI ∷ I a → a
- unK ∷ ∀ k a (b ∷ k). K a b → a
- fn ∷ ∀ k f (a ∷ k) f'. (f a → f' a) → (f -.-> f') a
- fn_2 ∷ ∀ k f (a ∷ k) f' f''. (f a → f' a → f'' a) → (f -.-> (f' -.-> f'')) a
- fn_3 ∷ ∀ k f (a ∷ k) f' f'' f'''. (f a → f' a → f'' a → f''' a) → (f -.-> (f' -.-> (f'' -.-> f'''))) a
- fn_4 ∷ ∀ k f (a ∷ k) f' f'' f''' f''''. (f a → f' a → f'' a → f''' a → f'''' a) → (f -.-> (f' -.-> (f'' -.-> (f''' -.-> f'''')))) a
- hcfoldMap ∷ ∀ k l h c (xs ∷ l) m proxy f. (HTraverse_ h, AllN h c xs, Monoid m) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → m) → h f xs → m
- hcfor ∷ ∀ l h c (xs ∷ l) g proxy f. (HSequence h, AllN h c xs, Applicative g) ⇒ proxy c → h f xs → (∀ a. c a ⇒ f a → g a) → g (h I xs)
- hcfor_ ∷ ∀ k l h c (xs ∷ l) g proxy f. (HTraverse_ h, AllN h c xs, Applicative g) ⇒ proxy c → h f xs → (∀ (a ∷ k). c a ⇒ f a → g ()) → g ()
- hcliftA ∷ ∀ k l h c (xs ∷ l) proxy f f'. (AllN (Prod h) c xs, HAp h) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a) → h f xs → h f' xs
- hcliftA2 ∷ ∀ k l h c (xs ∷ l) proxy f f' f''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a → f'' a) → Prod h f xs → h f' xs → h f'' xs
- hcliftA3 ∷ ∀ k l h c (xs ∷ l) proxy f f' f'' f'''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a → f'' a → f''' a) → Prod h f xs → Prod h f' xs → h f'' xs → h f''' xs
- hcmap ∷ ∀ k l h c (xs ∷ l) proxy f f'. (AllN (Prod h) c xs, HAp h) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a) → h f xs → h f' xs
- hctraverse ∷ ∀ l h c (xs ∷ l) g proxy f. (HSequence h, AllN h c xs, Applicative g) ⇒ proxy c → (∀ a. c a ⇒ f a → g a) → h f xs → g (h I xs)
- hczipWith ∷ ∀ k l h c (xs ∷ l) proxy f f' f''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a → f'' a) → Prod h f xs → h f' xs → h f'' xs
- hczipWith3 ∷ ∀ k l h c (xs ∷ l) proxy f f' f'' f'''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a → f'' a → f''' a) → Prod h f xs → Prod h f' xs → h f'' xs → h f''' xs
- hfromI ∷ ∀ l1 k2 l2 h1 (f ∷ k2 → Type) (xs ∷ l1) (ys ∷ l2) h2. (AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2) ⇒ h1 I xs → h2 f ys
- hliftA ∷ ∀ k l h (xs ∷ l) f f'. (SListIN (Prod h) xs, HAp h) ⇒ (∀ (a ∷ k). f a → f' a) → h f xs → h f' xs
- hliftA2 ∷ ∀ k l h (xs ∷ l) f f' f''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) ⇒ (∀ (a ∷ k). f a → f' a → f'' a) → Prod h f xs → h f' xs → h f'' xs
- hliftA3 ∷ ∀ k l h (xs ∷ l) f f' f'' f'''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) ⇒ (∀ (a ∷ k). f a → f' a → f'' a → f''' a) → Prod h f xs → Prod h f' xs → h f'' xs → h f''' xs
- hmap ∷ ∀ k l h (xs ∷ l) f f'. (SListIN (Prod h) xs, HAp h) ⇒ (∀ (a ∷ k). f a → f' a) → h f xs → h f' xs
- hsequence ∷ ∀ l h (xs ∷ l) f. (SListIN h xs, SListIN (Prod h) xs, HSequence h, Applicative f) ⇒ h f xs → f (h I xs)
- hsequenceK ∷ ∀ k l h (xs ∷ l) f a. (SListIN h xs, SListIN (Prod h) xs, Applicative f, HSequence h) ⇒ h (K (f a) ∷ k → Type) xs → f (h (K a ∷ k → Type) xs)
- htoI ∷ ∀ k1 l1 l2 h1 (f ∷ k1 → Type) (xs ∷ l1) (ys ∷ l2) h2. (AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2) ⇒ h1 f xs → h2 I ys
- hzipWith ∷ ∀ k l h (xs ∷ l) f f' f''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) ⇒ (∀ (a ∷ k). f a → f' a → f'' a) → Prod h f xs → h f' xs → h f'' xs
- hzipWith3 ∷ ∀ k l h (xs ∷ l) f f' f'' f'''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) ⇒ (∀ (a ∷ k). f a → f' a → f'' a → f''' a) → Prod h f xs → Prod h f' xs → h f'' xs → h f''' xs
- ccase_SList ∷ ∀ k c (xs ∷ [k]) proxy r. All c xs ⇒ proxy c → r ('[] ∷ [k]) → (∀ (y ∷ k) (ys ∷ [k]). (c y, All c ys) ⇒ r (y ': ys)) → r xs
- fromList ∷ ∀ k (xs ∷ [k]) a. SListI xs ⇒ [a] → Maybe (NP (K a ∷ k → Type) xs)
- hcliftA' ∷ ∀ k (c ∷ k → Constraint) (xss ∷ [[k]]) h proxy f f'. (All2 c xss, Prod h ~ (NP ∷ ([k] → Type) → [[k]] → Type), HAp h) ⇒ proxy c → (∀ (xs ∷ [k]). All c xs ⇒ f xs → f' xs) → h f xss → h f' xss
- hcliftA2' ∷ ∀ k (c ∷ k → Constraint) (xss ∷ [[k]]) h proxy f f' f''. (All2 c xss, Prod h ~ (NP ∷ ([k] → Type) → [[k]] → Type), HAp h) ⇒ proxy c → (∀ (xs ∷ [k]). All c xs ⇒ f xs → f' xs → f'' xs) → Prod h f xss → h f' xss → h f'' xss
- hcliftA3' ∷ ∀ k (c ∷ k → Constraint) (xss ∷ [[k]]) h proxy f f' f'' f'''. (All2 c xss, Prod h ~ (NP ∷ ([k] → Type) → [[k]] → Type), HAp h) ⇒ proxy c → (∀ (xs ∷ [k]). All c xs ⇒ f xs → f' xs → f'' xs → f''' xs) → Prod h f xss → Prod h f' xss → h f'' xss → h f''' xss
- projections ∷ ∀ k (xs ∷ [k]) (f ∷ k → Type). SListI xs ⇒ NP (Projection f xs) xs
- shiftProjection ∷ ∀ a1 (f ∷ a1 → Type) (xs ∷ [a1]) (a2 ∷ a1) (x ∷ a1). Projection f xs a2 → Projection f (x ': xs) a2
- unPOP ∷ ∀ k (f ∷ k → Type) (xss ∷ [[k]]). POP f xss → NP (NP f) xss
- apInjs_NP ∷ ∀ k (xs ∷ [k]) (f ∷ k → Type). SListI xs ⇒ NP f xs → [NS f xs]
- apInjs_POP ∷ ∀ k (xss ∷ [[k]]) (f ∷ k → Type). SListI xss ⇒ POP f xss → [SOP f xss]
- ccompare_NS ∷ ∀ k c proxy r f g (xs ∷ [k]). All c xs ⇒ proxy c → r → (∀ (x ∷ k). c x ⇒ f x → g x → r) → r → NS f xs → NS g xs → r
- ccompare_SOP ∷ ∀ k (c ∷ k → Constraint) proxy r (f ∷ k → Type) (g ∷ k → Type) (xss ∷ [[k]]). All2 c xss ⇒ proxy c → r → (∀ (xs ∷ [k]). All c xs ⇒ NP f xs → NP g xs → r) → r → SOP f xss → SOP g xss → r
- compare_NS ∷ ∀ k r f g (xs ∷ [k]). r → (∀ (x ∷ k). f x → g x → r) → r → NS f xs → NS g xs → r
- compare_SOP ∷ ∀ k r (f ∷ k → Type) (g ∷ k → Type) (xss ∷ [[k]]). r → (∀ (xs ∷ [k]). NP f xs → NP g xs → r) → r → SOP f xss → SOP g xss → r
- shift ∷ ∀ a1 (f ∷ a1 → Type) (xs ∷ [a1]) (a2 ∷ a1) (x ∷ a1). Injection f xs a2 → Injection f (x ': xs) a2
- unSOP ∷ ∀ k (f ∷ k → Type) (xss ∷ [[k]]). SOP f xss → NS (NP f) xss
- case_SList ∷ ∀ k (xs ∷ [k]) r. SListI xs ⇒ r ('[] ∷ [k]) → (∀ (y ∷ k) (ys ∷ [k]). SListI ys ⇒ r (y ': ys)) → r xs
- lengthSList ∷ ∀ k (xs ∷ [k]) proxy. SListI xs ⇒ proxy xs → Int
- para_SList ∷ ∀ k (xs ∷ [k]) r. SListI xs ⇒ r ('[] ∷ [k]) → (∀ (y ∷ k) (ys ∷ [k]). SListI ys ⇒ r ys → r (y ': ys)) → r xs
- sList ∷ ∀ k (xs ∷ [k]). SListI xs ⇒ SList xs
- shape ∷ ∀ k (xs ∷ [k]). SListI xs ⇒ Shape xs
- newtype ((f ∷ l → Type) :.: (g ∷ k → l)) (p ∷ k) = Comp (f (g p))
- newtype I a = I a
- newtype K a (b ∷ k) = K a
- newtype ((f ∷ k → Type) -.-> (g ∷ k → Type)) (a ∷ k) = Fn {
- apFn ∷ f a → g a
- type family CollapseTo (h ∷ (k → Type) → l → Type) x
- class (Prod (Prod h) ~ Prod h, HPure (Prod h)) ⇒ HAp (h ∷ (k → Type) → l → Type) where
- class UnProd (Prod h) ~ h ⇒ HApInjs (h ∷ (k → Type) → l → Type) where
- class HCollapse (h ∷ (k → Type) → l → Type) where
- hcollapse ∷ ∀ (xs ∷ l) a. SListIN h xs ⇒ h (K a ∷ k → Type) xs → CollapseTo h a
- class HExpand (h ∷ (k → Type) → l → Type) where
- class HIndex (h ∷ (k → Type) → l → Type) where
- class HPure (h ∷ (k → Type) → l → Type) where
- class HAp h ⇒ HSequence (h ∷ (k → Type) → l → Type) where
- hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k → Type). (SListIN h xs, Applicative f) ⇒ h (f :.: g) xs → f (h g xs)
- hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN h c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g (f' a)) → h f xs → g (h f' xs)
- htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN h xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g (f' a)) → h f xs → g (h f' xs)
- class ((Same h1 ∷ (k2 → Type) → l2 → Type) ~ h2, (Same h2 ∷ (k1 → Type) → l1 → Type) ~ h1) ⇒ HTrans (h1 ∷ (k1 → Type) → l1 → Type) (h2 ∷ (k2 → Type) → l2 → Type) where
- class HTraverse_ (h ∷ (k → Type) → l → Type) where
- hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN h c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g ()) → h f xs → g ()
- htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN h xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g ()) → h f xs → g ()
- type family Prod (h ∷ (k → Type) → l → Type) ∷ (k → Type) → l → Type
- type family UnProd (h ∷ (k → Type) → l → Type) ∷ (k → Type) → l → Type
- class (AllF c xs, SListI xs) ⇒ All (c ∷ k → Constraint) (xs ∷ [k]) where
- cpara_SList ∷ proxy c → r ('[] ∷ [k]) → (∀ (y ∷ k) (ys ∷ [k]). (c y, All c ys) ⇒ r ys → r (y ': ys)) → r xs
- type All2 (c ∷ k → Constraint) = All (All c)
- type family AllN (h ∷ (k → Type) → l → Type) (c ∷ k → Constraint) ∷ l → Constraint
- class (SListI xs, SListI ys, SameShapeAs xs ys, SameShapeAs ys xs, AllZipF c xs ys) ⇒ AllZip (c ∷ a → b → Constraint) (xs ∷ [a]) (ys ∷ [b])
- class (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) ⇒ AllZip2 (f ∷ a → b → Constraint) (xss ∷ [[a]]) (yss ∷ [[b]])
- type family AllZipN (h ∷ (k → Type) → l → Type) (c ∷ k1 → k2 → Constraint) ∷ l1 → l2 → Constraint
- class (f x, g x) ⇒ And (f ∷ k → Constraint) (g ∷ k → Constraint) (x ∷ k)
- class f (g x) ⇒ Compose (f ∷ k → Constraint) (g ∷ k1 → k) (x ∷ k1)
- class Coercible (f x) (g y) ⇒ LiftedCoercible (f ∷ k → k1) (g ∷ k2 → k1) (x ∷ k) (y ∷ k2)
- type SListI = All (Top ∷ k → Constraint)
- type SListI2 = All (SListI ∷ [k] → Constraint)
- type family SameShapeAs (xs ∷ [a]) (ys ∷ [b]) where ...
- class Top (x ∷ k)
- newtype POP (f ∷ k → Type) (xss ∷ [[k]]) = POP (NP (NP f) xss)
- type Projection (f ∷ k → Type) (xs ∷ [k]) = (K (NP f xs) ∷ k → Type) -.-> f
- newtype SOP (f ∷ k → Type) (xss ∷ [[k]]) = SOP (NS (NP f) xss)
- data SList (a ∷ [k]) where
- data Shape (a ∷ [k]) where
NP
data NP ∷ (k → Type) → [k] → Type where Source #
Instances
HTrans (NP ∷ (k1 → Type) → [k1] → Type) (NP ∷ (k2 → Type) → [k2] → Type) Source # | |
Defined in Data.SOP.Strict | |
HAp (NP ∷ (k → Type) → [k] → Type) Source # | |
HCollapse (NP ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict | |
HPure (NP ∷ (k → Type) → [k] → Type) Source # | |
HSequence (NP ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN NP xs, Applicative f) ⇒ NP (f :.: g) xs → f (NP g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN NP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → NP f xs → g (NP f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN NP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → NP f xs → g (NP f' xs) # | |
HTraverse_ (NP ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict Methods hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN NP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → NP f xs → g () # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN NP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → NP f xs → g () # | |
All (Compose Eq f) xs ⇒ Eq (NP f xs) Source # | |
(All (Compose Eq f) xs, All (Compose Ord f) xs) ⇒ Ord (NP f xs) Source # | |
Defined in Data.SOP.Strict | |
All (Compose Show f) xs ⇒ Show (NP f xs) Source # | Copied from sop-core Not derived, since derived instance ignores associativity info |
All (Compose NoThunks f) xs ⇒ NoThunks (NP f xs) Source # | |
type AllZipN (NP ∷ (k → Type) → [k] → Type) (c ∷ a → b → Constraint) Source # | |
Defined in Data.SOP.Strict | |
type Same (NP ∷ (k1 → Type) → [k1] → Type) Source # | |
type Prod (NP ∷ (k → Type) → [k] → Type) Source # | |
type SListIN (NP ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict | |
type CollapseTo (NP ∷ (k → Type) → [k] → Type) a Source # | |
Defined in Data.SOP.Strict | |
type AllN (NP ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
Defined in Data.SOP.Strict |
singletonNP ∷ f x → NP f '[x] Source #
NS
data NS ∷ (k → Type) → [k] → Type where Source #
Instances
HTrans (NS ∷ (k1 → Type) → [k1] → Type) (NS ∷ (k2 → Type) → [k2] → Type) Source # | |
Defined in Data.SOP.Strict | |
HAp (NS ∷ (k → Type) → [k] → Type) Source # | |
HCollapse (NS ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict | |
HExpand (NS ∷ (k → Type) → [k] → Type) Source # | |
HSequence (NS ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN NS xs, Applicative f) ⇒ NS (f :.: g) xs → f (NS g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN NS c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → NS f xs → g (NS f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN NS xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → NS f xs → g (NS f' xs) # | |
All (Compose Eq f) xs ⇒ Eq (NS f xs) Source # | |
(All (Compose Eq f) xs, All (Compose Ord f) xs) ⇒ Ord (NS f xs) Source # | |
Defined in Data.SOP.Strict | |
All (Compose Show f) xs ⇒ Show (NS f xs) Source # | |
All (Compose NoThunks f) xs ⇒ NoThunks (NS f xs) Source # | |
type Same (NS ∷ (k1 → Type) → [k1] → Type) Source # | |
type Prod (NS ∷ (k → Type) → [k] → Type) Source # | |
type SListIN (NS ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict | |
type CollapseTo (NS ∷ (k → Type) → [k] → Type) a Source # | |
Defined in Data.SOP.Strict | |
type AllN (NS ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
Defined in Data.SOP.Strict |
Injections
Re-exports from sop-core
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,
is a safer alternative to the
Proxy
:: Proxy
a
idiom.undefined
:: a
>>>
Proxy :: Proxy (Void, Int -> Int)
Proxy
Proxy can even hold types of higher kinds,
>>>
Proxy :: Proxy Either
Proxy
>>>
Proxy :: Proxy Functor
Proxy
>>>
Proxy :: Proxy complicatedStructure
Proxy
Constructors
Proxy |
Instances
Generic1 (Proxy ∷ k → Type) | Since: base-4.6.0.0 |
SemialignWithIndex Void (Proxy ∷ Type → Type) | |
Defined in Data.Semialign.Internal Methods ialignWith ∷ (Void → These a b → c) → Proxy a → Proxy b → Proxy c | |
ZipWithIndex Void (Proxy ∷ Type → Type) | |
RepeatWithIndex Void (Proxy ∷ Type → Type) | |
Defined in Data.Semialign.Internal | |
Monad (Proxy ∷ Type → Type) | Since: base-4.7.0.0 |
Functor (Proxy ∷ Type → Type) | Since: base-4.7.0.0 |
Applicative (Proxy ∷ Type → Type) | Since: base-4.7.0.0 |
Foldable (Proxy ∷ Type → Type) | Since: base-4.7.0.0 |
Defined in Data.Foldable Methods fold ∷ Monoid m ⇒ Proxy m → m Source # foldMap ∷ Monoid m ⇒ (a → m) → Proxy a → m Source # foldMap' ∷ Monoid m ⇒ (a → m) → Proxy a → m Source # foldr ∷ (a → b → b) → b → Proxy a → b Source # foldr' ∷ (a → b → b) → b → Proxy a → b Source # foldl ∷ (b → a → b) → b → Proxy a → b Source # foldl' ∷ (b → a → b) → b → Proxy a → b Source # foldr1 ∷ (a → a → a) → Proxy a → a Source # foldl1 ∷ (a → a → a) → Proxy a → a Source # toList ∷ Proxy a → [a] Source # null ∷ Proxy a → Bool Source # length ∷ Proxy a → Int Source # elem ∷ Eq a ⇒ a → Proxy a → Bool Source # maximum ∷ Ord a ⇒ Proxy a → a Source # minimum ∷ Ord a ⇒ Proxy a → a Source # | |
Traversable (Proxy ∷ Type → Type) | Since: base-4.7.0.0 |
Contravariant (Proxy ∷ Type → Type) | |
Eq1 (Proxy ∷ Type → Type) | Since: base-4.9.0.0 |
Ord1 (Proxy ∷ Type → Type) | Since: base-4.9.0.0 |
Defined in Data.Functor.Classes | |
Read1 (Proxy ∷ Type → Type) | Since: base-4.9.0.0 |
Defined in Data.Functor.Classes | |
Show1 (Proxy ∷ Type → Type) | Since: base-4.9.0.0 |
Alternative (Proxy ∷ Type → Type) | Since: base-4.9.0.0 |
MonadPlus (Proxy ∷ Type → Type) | Since: base-4.9.0.0 |
NFData1 (Proxy ∷ Type → Type) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
Hashable1 (Proxy ∷ Type → Type) | |
Defined in Data.Hashable.Class | |
Align (Proxy ∷ Type → Type) | |
Defined in Data.Semialign.Internal | |
Semialign (Proxy ∷ Type → Type) | |
Zip (Proxy ∷ Type → Type) | |
Unalign (Proxy ∷ Type → Type) | |
Defined in Data.Semialign.Internal | |
Repeat (Proxy ∷ Type → Type) | |
Defined in Data.Semialign.Internal | |
Unzip (Proxy ∷ Type → Type) | |
Bounded (Proxy t) | Since: base-4.7.0.0 |
Enum (Proxy s) | Since: base-4.7.0.0 |
Defined in Data.Proxy Methods succ ∷ Proxy s → Proxy s Source # pred ∷ Proxy s → Proxy s Source # toEnum ∷ Int → Proxy s Source # fromEnum ∷ Proxy s → Int Source # enumFrom ∷ Proxy s → [Proxy s] Source # enumFromThen ∷ Proxy s → Proxy s → [Proxy s] Source # enumFromTo ∷ Proxy s → Proxy s → [Proxy s] Source # enumFromThenTo ∷ Proxy s → Proxy s → Proxy s → [Proxy s] Source # | |
Eq (Proxy s) | Since: base-4.7.0.0 |
Ord (Proxy s) | Since: base-4.7.0.0 |
Defined in Data.Proxy | |
Read (Proxy t) | Since: base-4.7.0.0 |
Show (Proxy s) | Since: base-4.7.0.0 |
Ix (Proxy s) | Since: base-4.7.0.0 |
Generic (Proxy t) | Since: base-4.6.0.0 |
Semigroup (Proxy s) | Since: base-4.9.0.0 |
Monoid (Proxy s) | Since: base-4.7.0.0 |
NFData (Proxy a) | Since: deepseq-1.4.0.0 |
Defined in Control.DeepSeq | |
Hashable (Proxy a) | |
Defined in Data.Hashable.Class | |
Serialise (Proxy a) | |
Defined in Codec.Serialise.Class | |
type Rep1 (Proxy ∷ k → Type) | |
type Rep (Proxy t) | |
fn_3 ∷ ∀ k f (a ∷ k) f' f'' f'''. (f a → f' a → f'' a → f''' a) → (f -.-> (f' -.-> (f'' -.-> f'''))) a #
fn_4 ∷ ∀ k f (a ∷ k) f' f'' f''' f''''. (f a → f' a → f'' a → f''' a → f'''' a) → (f -.-> (f' -.-> (f'' -.-> (f''' -.-> f'''')))) a #
hcfoldMap ∷ ∀ k l h c (xs ∷ l) m proxy f. (HTraverse_ h, AllN h c xs, Monoid m) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → m) → h f xs → m #
hcfor ∷ ∀ l h c (xs ∷ l) g proxy f. (HSequence h, AllN h c xs, Applicative g) ⇒ proxy c → h f xs → (∀ a. c a ⇒ f a → g a) → g (h I xs) #
hcfor_ ∷ ∀ k l h c (xs ∷ l) g proxy f. (HTraverse_ h, AllN h c xs, Applicative g) ⇒ proxy c → h f xs → (∀ (a ∷ k). c a ⇒ f a → g ()) → g () #
hcliftA ∷ ∀ k l h c (xs ∷ l) proxy f f'. (AllN (Prod h) c xs, HAp h) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a) → h f xs → h f' xs #
hcliftA2 ∷ ∀ k l h c (xs ∷ l) proxy f f' f''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a → f'' a) → Prod h f xs → h f' xs → h f'' xs #
hcliftA3 ∷ ∀ k l h c (xs ∷ l) proxy f f' f'' f'''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a → f'' a → f''' a) → Prod h f xs → Prod h f' xs → h f'' xs → h f''' xs #
hcmap ∷ ∀ k l h c (xs ∷ l) proxy f f'. (AllN (Prod h) c xs, HAp h) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a) → h f xs → h f' xs #
hctraverse ∷ ∀ l h c (xs ∷ l) g proxy f. (HSequence h, AllN h c xs, Applicative g) ⇒ proxy c → (∀ a. c a ⇒ f a → g a) → h f xs → g (h I xs) #
hczipWith ∷ ∀ k l h c (xs ∷ l) proxy f f' f''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a → f'' a) → Prod h f xs → h f' xs → h f'' xs #
hczipWith3 ∷ ∀ k l h c (xs ∷ l) proxy f f' f'' f'''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → f' a → f'' a → f''' a) → Prod h f xs → Prod h f' xs → h f'' xs → h f''' xs #
hfromI ∷ ∀ l1 k2 l2 h1 (f ∷ k2 → Type) (xs ∷ l1) (ys ∷ l2) h2. (AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2) ⇒ h1 I xs → h2 f ys #
hliftA ∷ ∀ k l h (xs ∷ l) f f'. (SListIN (Prod h) xs, HAp h) ⇒ (∀ (a ∷ k). f a → f' a) → h f xs → h f' xs #
hliftA2 ∷ ∀ k l h (xs ∷ l) f f' f''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) ⇒ (∀ (a ∷ k). f a → f' a → f'' a) → Prod h f xs → h f' xs → h f'' xs #
hliftA3 ∷ ∀ k l h (xs ∷ l) f f' f'' f'''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) ⇒ (∀ (a ∷ k). f a → f' a → f'' a → f''' a) → Prod h f xs → Prod h f' xs → h f'' xs → h f''' xs #
hmap ∷ ∀ k l h (xs ∷ l) f f'. (SListIN (Prod h) xs, HAp h) ⇒ (∀ (a ∷ k). f a → f' a) → h f xs → h f' xs #
hsequence ∷ ∀ l h (xs ∷ l) f. (SListIN h xs, SListIN (Prod h) xs, HSequence h, Applicative f) ⇒ h f xs → f (h I xs) #
hsequenceK ∷ ∀ k l h (xs ∷ l) f a. (SListIN h xs, SListIN (Prod h) xs, Applicative f, HSequence h) ⇒ h (K (f a) ∷ k → Type) xs → f (h (K a ∷ k → Type) xs) #
htoI ∷ ∀ k1 l1 l2 h1 (f ∷ k1 → Type) (xs ∷ l1) (ys ∷ l2) h2. (AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2) ⇒ h1 f xs → h2 I ys #
hzipWith ∷ ∀ k l h (xs ∷ l) f f' f''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) ⇒ (∀ (a ∷ k). f a → f' a → f'' a) → Prod h f xs → h f' xs → h f'' xs #
hzipWith3 ∷ ∀ k l h (xs ∷ l) f f' f'' f'''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) ⇒ (∀ (a ∷ k). f a → f' a → f'' a → f''' a) → Prod h f xs → Prod h f' xs → h f'' xs → h f''' xs #
ccase_SList ∷ ∀ k c (xs ∷ [k]) proxy r. All c xs ⇒ proxy c → r ('[] ∷ [k]) → (∀ (y ∷ k) (ys ∷ [k]). (c y, All c ys) ⇒ r (y ': ys)) → r xs #
hcliftA' ∷ ∀ k (c ∷ k → Constraint) (xss ∷ [[k]]) h proxy f f'. (All2 c xss, Prod h ~ (NP ∷ ([k] → Type) → [[k]] → Type), HAp h) ⇒ proxy c → (∀ (xs ∷ [k]). All c xs ⇒ f xs → f' xs) → h f xss → h f' xss #
hcliftA2' ∷ ∀ k (c ∷ k → Constraint) (xss ∷ [[k]]) h proxy f f' f''. (All2 c xss, Prod h ~ (NP ∷ ([k] → Type) → [[k]] → Type), HAp h) ⇒ proxy c → (∀ (xs ∷ [k]). All c xs ⇒ f xs → f' xs → f'' xs) → Prod h f xss → h f' xss → h f'' xss #
hcliftA3' ∷ ∀ k (c ∷ k → Constraint) (xss ∷ [[k]]) h proxy f f' f'' f'''. (All2 c xss, Prod h ~ (NP ∷ ([k] → Type) → [[k]] → Type), HAp h) ⇒ proxy c → (∀ (xs ∷ [k]). All c xs ⇒ f xs → f' xs → f'' xs → f''' xs) → Prod h f xss → Prod h f' xss → h f'' xss → h f''' xss #
projections ∷ ∀ k (xs ∷ [k]) (f ∷ k → Type). SListI xs ⇒ NP (Projection f xs) xs #
shiftProjection ∷ ∀ a1 (f ∷ a1 → Type) (xs ∷ [a1]) (a2 ∷ a1) (x ∷ a1). Projection f xs a2 → Projection f (x ': xs) a2 #
ccompare_NS ∷ ∀ k c proxy r f g (xs ∷ [k]). All c xs ⇒ proxy c → r → (∀ (x ∷ k). c x ⇒ f x → g x → r) → r → NS f xs → NS g xs → r #
ccompare_SOP ∷ ∀ k (c ∷ k → Constraint) proxy r (f ∷ k → Type) (g ∷ k → Type) (xss ∷ [[k]]). All2 c xss ⇒ proxy c → r → (∀ (xs ∷ [k]). All c xs ⇒ NP f xs → NP g xs → r) → r → SOP f xss → SOP g xss → r #
compare_NS ∷ ∀ k r f g (xs ∷ [k]). r → (∀ (x ∷ k). f x → g x → r) → r → NS f xs → NS g xs → r #
compare_SOP ∷ ∀ k r (f ∷ k → Type) (g ∷ k → Type) (xss ∷ [[k]]). r → (∀ (xs ∷ [k]). NP f xs → NP g xs → r) → r → SOP f xss → SOP g xss → r #
shift ∷ ∀ a1 (f ∷ a1 → Type) (xs ∷ [a1]) (a2 ∷ a1) (x ∷ a1). Injection f xs a2 → Injection f (x ': xs) a2 #
case_SList ∷ ∀ k (xs ∷ [k]) r. SListI xs ⇒ r ('[] ∷ [k]) → (∀ (y ∷ k) (ys ∷ [k]). SListI ys ⇒ r (y ': ys)) → r xs #
lengthSList ∷ ∀ k (xs ∷ [k]) proxy. SListI xs ⇒ proxy xs → Int #
para_SList ∷ ∀ k (xs ∷ [k]) r. SListI xs ⇒ r ('[] ∷ [k]) → (∀ (y ∷ k) (ys ∷ [k]). SListI ys ⇒ r ys → r (y ': ys)) → r xs #
newtype ((f ∷ l → Type) :.: (g ∷ k → l)) (p ∷ k) #
Constructors
Comp (f (g p)) |
Instances
Constructors
I a |
Instances
Constructors
K a |
Instances
type family CollapseTo (h ∷ (k → Type) → l → Type) x #
Instances
type CollapseTo (NP ∷ (k → Type) → [k] → Type) a Source # | |
Defined in Data.SOP.Strict | |
type CollapseTo (NS ∷ (k → Type) → [k] → Type) a Source # | |
Defined in Data.SOP.Strict | |
type CollapseTo (NS ∷ (k → Type) → [k] → Type) a | |
Defined in Data.SOP.NS | |
type CollapseTo (SOP ∷ (k → Type) → [[k]] → Type) a | |
Defined in Data.SOP.NS | |
type CollapseTo (NP ∷ (k → Type) → [k] → Type) a | |
Defined in Data.SOP.NP | |
type CollapseTo (POP ∷ (k → Type) → [[k]] → Type) a | |
Defined in Data.SOP.NP | |
type CollapseTo (SimpleTelescope ∷ (k → Type) → [k] → Type) a Source # | |
type CollapseTo HardForkState a Source # | |
class (Prod (Prod h) ~ Prod h, HPure (Prod h)) ⇒ HAp (h ∷ (k → Type) → l → Type) where #
Instances
HAp (NP ∷ (k → Type) → [k] → Type) Source # | |
HAp (NS ∷ (k → Type) → [k] → Type) Source # | |
HAp (SimpleTelescope ∷ (k → Type) → [k] → Type) Source # | |
Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hap ∷ ∀ (f ∷ k0 → Type) (g ∷ k0 → Type) (xs ∷ l). Prod SimpleTelescope (f -.-> g) xs → SimpleTelescope f xs → SimpleTelescope g xs # | |
HAp (NP ∷ (k → Type) → [k] → Type) | |
HAp (SOP ∷ (k → Type) → [[k]] → Type) | |
HAp (NS ∷ (k → Type) → [k] → Type) | |
HAp (POP ∷ (k → Type) → [[k]] → Type) | |
HAp (OptNP empty ∷ (k → Type) → [k] → Type) Source # | |
HAp (Telescope g ∷ (k → Type) → [k] → Type) Source # | |
HAp (Mismatch f ∷ (k → Type) → [k] → Type) Source # | |
HAp HardForkState Source # | |
Defined in Ouroboros.Consensus.HardFork.Combinator.State.Instances Methods hap ∷ ∀ (f ∷ k → Type) (g ∷ k → Type) (xs ∷ l). Prod HardForkState (f -.-> g) xs → HardForkState f xs → HardForkState g xs # |
class UnProd (Prod h) ~ h ⇒ HApInjs (h ∷ (k → Type) → l → Type) where #
class HCollapse (h ∷ (k → Type) → l → Type) where #
Methods
hcollapse ∷ ∀ (xs ∷ l) a. SListIN h xs ⇒ h (K a ∷ k → Type) xs → CollapseTo h a #
Instances
class HExpand (h ∷ (k → Type) → l → Type) where #
Methods
hexpand ∷ ∀ (xs ∷ l) f. SListIN (Prod h) xs ⇒ (∀ (x ∷ k). f x) → h f xs → Prod h f xs #
hcexpand ∷ ∀ c (xs ∷ l) proxy f. AllN (Prod h) c xs ⇒ proxy c → (∀ (x ∷ k). c x ⇒ f x) → h f xs → Prod h f xs #
class HPure (h ∷ (k → Type) → l → Type) where #
Methods
hpure ∷ ∀ (xs ∷ l) f. SListIN h xs ⇒ (∀ (a ∷ k). f a) → h f xs #
hcpure ∷ ∀ c (xs ∷ l) proxy f. AllN h c xs ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a) → h f xs #
class HAp h ⇒ HSequence (h ∷ (k → Type) → l → Type) where #
Methods
hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k → Type). (SListIN h xs, Applicative f) ⇒ h (f :.: g) xs → f (h g xs) #
hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN h c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g (f' a)) → h f xs → g (h f' xs) #
htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN h xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g (f' a)) → h f xs → g (h f' xs) #
Instances
HSequence (NP ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN NP xs, Applicative f) ⇒ NP (f :.: g) xs → f (NP g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN NP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → NP f xs → g (NP f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN NP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → NP f xs → g (NP f' xs) # | |
HSequence (NS ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN NS xs, Applicative f) ⇒ NS (f :.: g) xs → f (NS g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN NS c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → NS f xs → g (NS f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN NS xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → NS f xs → g (NS f' xs) # | |
HSequence (SimpleTelescope ∷ (k → Type) → [k] → Type) Source # | |
Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN SimpleTelescope xs, Applicative f) ⇒ SimpleTelescope (f :.: g) xs → f (SimpleTelescope g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN SimpleTelescope c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → SimpleTelescope f xs → g (SimpleTelescope f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN SimpleTelescope xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → SimpleTelescope f xs → g (SimpleTelescope f' xs) # | |
HSequence (SOP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NS Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN SOP xs, Applicative f) ⇒ SOP (f :.: g) xs → f (SOP g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN SOP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → SOP f xs → g (SOP f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN SOP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → SOP f xs → g (SOP f' xs) # | |
HSequence (NS ∷ (k → Type) → [k] → Type) | |
Defined in Data.SOP.NS Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN NS xs, Applicative f) ⇒ NS (f :.: g) xs → f (NS g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN NS c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → NS f xs → g (NS f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN NS xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → NS f xs → g (NS f' xs) # | |
HSequence (POP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NP Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN POP xs, Applicative f) ⇒ POP (f :.: g) xs → f (POP g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN POP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → POP f xs → g (POP f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN POP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → POP f xs → g (POP f' xs) # | |
HSequence (NP ∷ (k → Type) → [k] → Type) | |
Defined in Data.SOP.NP Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN NP xs, Applicative f) ⇒ NP (f :.: g) xs → f (NP g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN NP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → NP f xs → g (NP f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN NP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → NP f xs → g (NP f' xs) # | |
HSequence (OptNP empty ∷ (k → Type) → [k] → Type) Source # | |
Defined in Ouroboros.Consensus.Util.OptNP Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN (OptNP empty) xs, Applicative f) ⇒ OptNP empty (f :.: g) xs → f (OptNP empty g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN (OptNP empty) c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → OptNP empty f xs → g (OptNP empty f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN (OptNP empty) xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → OptNP empty f xs → g (OptNP empty f' xs) # | |
HSequence (Telescope g ∷ (k → Type) → [k] → Type) Source # | |
Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hsequence' ∷ ∀ (xs ∷ l) f (g0 ∷ k0 → Type). (SListIN (Telescope g) xs, Applicative f) ⇒ Telescope g (f :.: g0) xs → f (Telescope g g0 xs) # hctraverse' ∷ ∀ c (xs ∷ l) g0 proxy f f'. (AllN (Telescope g) c xs, Applicative g0) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g0 (f' a)) → Telescope g f xs → g0 (Telescope g f' xs) # htraverse' ∷ ∀ (xs ∷ l) g0 f f'. (SListIN (Telescope g) xs, Applicative g0) ⇒ (∀ (a ∷ k0). f a → g0 (f' a)) → Telescope g f xs → g0 (Telescope g f' xs) # | |
HSequence HardForkState Source # | |
Defined in Ouroboros.Consensus.HardFork.Combinator.State.Instances Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k → Type). (SListIN HardForkState xs, Applicative f) ⇒ HardForkState (f :.: g) xs → f (HardForkState g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN HardForkState c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g (f' a)) → HardForkState f xs → g (HardForkState f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN HardForkState xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g (f' a)) → HardForkState f xs → g (HardForkState f' xs) # |
class ((Same h1 ∷ (k2 → Type) → l2 → Type) ~ h2, (Same h2 ∷ (k1 → Type) → l1 → Type) ~ h1) ⇒ HTrans (h1 ∷ (k1 → Type) → l1 → Type) (h2 ∷ (k2 → Type) → l2 → Type) where #
Methods
htrans ∷ ∀ c (xs ∷ l1) (ys ∷ l2) proxy f g. AllZipN (Prod h1) c xs ys ⇒ proxy c → (∀ (x ∷ k1) (y ∷ k2). c x y ⇒ f x → g y) → h1 f xs → h2 g ys #
hcoerce ∷ ∀ (f ∷ k1 → Type) (g ∷ k2 → Type) (xs ∷ l1) (ys ∷ l2). AllZipN (Prod h1) (LiftedCoercible f g) xs ys ⇒ h1 f xs → h2 g ys #
Instances
HTrans (NP ∷ (k1 → Type) → [k1] → Type) (NP ∷ (k2 → Type) → [k2] → Type) Source # | |
Defined in Data.SOP.Strict | |
HTrans (NS ∷ (k1 → Type) → [k1] → Type) (NS ∷ (k2 → Type) → [k2] → Type) Source # | |
Defined in Data.SOP.Strict | |
HTrans (SOP ∷ (k1 → Type) → [[k1]] → Type) (SOP ∷ (k2 → Type) → [[k2]] → Type) | |
Defined in Data.SOP.NS | |
HTrans (NS ∷ (k1 → Type) → [k1] → Type) (NS ∷ (k2 → Type) → [k2] → Type) | |
Defined in Data.SOP.NS | |
HTrans (POP ∷ (k1 → Type) → [[k1]] → Type) (POP ∷ (k2 → Type) → [[k2]] → Type) | |
Defined in Data.SOP.NP | |
HTrans (NP ∷ (k1 → Type) → [k1] → Type) (NP ∷ (k2 → Type) → [k2] → Type) | |
Defined in Data.SOP.NP |
class HTraverse_ (h ∷ (k → Type) → l → Type) where #
Methods
hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN h c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g ()) → h f xs → g () #
htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN h xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g ()) → h f xs → g () #
Instances
HTraverse_ (NP ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict Methods hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN NP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → NP f xs → g () # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN NP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → NP f xs → g () # | |
HTraverse_ (SimpleTelescope ∷ (k → Type) → [k] → Type) Source # | |
Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN SimpleTelescope c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → SimpleTelescope f xs → g () # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN SimpleTelescope xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → SimpleTelescope f xs → g () # | |
HTraverse_ (SOP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NS Methods hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN SOP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → SOP f xs → g () # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN SOP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → SOP f xs → g () # | |
HTraverse_ (NS ∷ (k → Type) → [k] → Type) | |
Defined in Data.SOP.NS Methods hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN NS c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → NS f xs → g () # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN NS xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → NS f xs → g () # | |
HTraverse_ (POP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NP Methods hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN POP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → POP f xs → g () # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN POP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → POP f xs → g () # | |
HTraverse_ (NP ∷ (k → Type) → [k] → Type) | |
Defined in Data.SOP.NP Methods hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN NP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → NP f xs → g () # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN NP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → NP f xs → g () # | |
HTraverse_ (Telescope g ∷ (k → Type) → [k] → Type) Source # | |
Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hctraverse_ ∷ ∀ c (xs ∷ l) g0 proxy f. (AllN (Telescope g) c xs, Applicative g0) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g0 ()) → Telescope g f xs → g0 () # htraverse_ ∷ ∀ (xs ∷ l) g0 f. (SListIN (Telescope g) xs, Applicative g0) ⇒ (∀ (a ∷ k0). f a → g0 ()) → Telescope g f xs → g0 () # |
type family Prod (h ∷ (k → Type) → l → Type) ∷ (k → Type) → l → Type #
Instances
type Prod (NP ∷ (k → Type) → [k] → Type) Source # | |
type Prod (NS ∷ (k → Type) → [k] → Type) Source # | |
type Prod (NS ∷ (k → Type) → [k] → Type) | |
type Prod (SOP ∷ (k → Type) → [[k]] → Type) | |
type Prod (NP ∷ (k → Type) → [k] → Type) | |
type Prod (POP ∷ (k → Type) → [[k]] → Type) | |
type Prod (SimpleTelescope ∷ (k → Type) → [k] → Type) Source # | |
type Prod (OptNP empty ∷ (k → Type) → [k] → Type) Source # | |
type Prod (Telescope g ∷ (k → Type) → [k] → Type) Source # | |
type Prod (Mismatch f ∷ (k → Type) → [k] → Type) Source # | |
type Prod HardForkState Source # | |
class (AllF c xs, SListI xs) ⇒ All (c ∷ k → Constraint) (xs ∷ [k]) where #
Methods
cpara_SList ∷ proxy c → r ('[] ∷ [k]) → (∀ (y ∷ k) (ys ∷ [k]). (c y, All c ys) ⇒ r ys → r (y ': ys)) → r xs #
Instances
All (c ∷ k → Constraint) ('[] ∷ [k]) | |
Defined in Data.SOP.Constraint Methods cpara_SList ∷ proxy c → r '[] → (∀ (y ∷ k0) (ys ∷ [k0]). (c y, All c ys) ⇒ r ys → r (y ': ys)) → r '[] # | |
(c x, All c xs) ⇒ All (c ∷ a → Constraint) (x ': xs ∷ [a]) | |
Defined in Data.SOP.Constraint Methods cpara_SList ∷ proxy c → r '[] → (∀ (y ∷ k) (ys ∷ [k]). (c y, All c ys) ⇒ r ys → r (y ': ys)) → r (x ': xs) # |
type All2 (c ∷ k → Constraint) = All (All c) #
type family AllN (h ∷ (k → Type) → l → Type) (c ∷ k → Constraint) ∷ l → Constraint #
Instances
type AllN (NP ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
Defined in Data.SOP.Strict | |
type AllN (NS ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
Defined in Data.SOP.Strict | |
type AllN (NS ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) | |
Defined in Data.SOP.NS | |
type AllN (SOP ∷ (k → Type) → [[k]] → Type) (c ∷ k → Constraint) | |
Defined in Data.SOP.NS | |
type AllN (NP ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) | |
Defined in Data.SOP.NP | |
type AllN (POP ∷ (k → Type) → [[k]] → Type) (c ∷ k → Constraint) | |
Defined in Data.SOP.NP | |
type AllN (SimpleTelescope ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
type AllN (OptNP empty ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
Defined in Ouroboros.Consensus.Util.OptNP | |
type AllN (Telescope g ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
type AllN (Mismatch f ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
type AllN HardForkState (c ∷ Type → Constraint) Source # | |
class (SListI xs, SListI ys, SameShapeAs xs ys, SameShapeAs ys xs, AllZipF c xs ys) ⇒ AllZip (c ∷ a → b → Constraint) (xs ∷ [a]) (ys ∷ [b]) #
Instances
(SListI xs, SListI ys, SameShapeAs xs ys, SameShapeAs ys xs, AllZipF c xs ys) ⇒ AllZip (c ∷ a → b → Constraint) (xs ∷ [a]) (ys ∷ [b]) | |
Defined in Data.SOP.Constraint |
class (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) ⇒ AllZip2 (f ∷ a → b → Constraint) (xss ∷ [[a]]) (yss ∷ [[b]]) #
Instances
(AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) ⇒ AllZip2 (f ∷ a → b → Constraint) (xss ∷ [[a]]) (yss ∷ [[b]]) | |
Defined in Data.SOP.Constraint |
type family AllZipN (h ∷ (k → Type) → l → Type) (c ∷ k1 → k2 → Constraint) ∷ l1 → l2 → Constraint #
Instances
type AllZipN (NP ∷ (k → Type) → [k] → Type) (c ∷ a → b → Constraint) Source # | |
Defined in Data.SOP.Strict | |
type AllZipN (NP ∷ (k → Type) → [k] → Type) (c ∷ a → b → Constraint) | |
Defined in Data.SOP.NP | |
type AllZipN (POP ∷ (k → Type) → [[k]] → Type) (c ∷ a → b → Constraint) | |
Defined in Data.SOP.NP |
class (f x, g x) ⇒ And (f ∷ k → Constraint) (g ∷ k → Constraint) (x ∷ k) #
Instances
(f x, g x) ⇒ And (f ∷ k → Constraint) (g ∷ k → Constraint) (x ∷ k) | |
Defined in Data.SOP.Constraint |
class f (g x) ⇒ Compose (f ∷ k → Constraint) (g ∷ k1 → k) (x ∷ k1) #
Instances
f (g x) ⇒ Compose (f ∷ k1 → Constraint) (g ∷ k2 → k1) (x ∷ k2) | |
Defined in Data.SOP.Constraint |
class Coercible (f x) (g y) ⇒ LiftedCoercible (f ∷ k → k1) (g ∷ k2 → k1) (x ∷ k) (y ∷ k2) #
Instances
Coercible (f x) (g y) ⇒ LiftedCoercible (f ∷ k1 → k2) (g ∷ k3 → k2) (x ∷ k1) (y ∷ k3) | |
Defined in Data.SOP.Constraint |
type SListI = All (Top ∷ k → Constraint) #
type SListI2 = All (SListI ∷ [k] → Constraint) #
type family SameShapeAs (xs ∷ [a]) (ys ∷ [b]) where ... #
Equations
SameShapeAs ('[] ∷ [a]) (ys ∷ [b]) = ys ~ ('[] ∷ [b]) | |
SameShapeAs (x ': xs ∷ [a1]) (ys ∷ [a2]) = ys ~ (Head ys ': Tail ys) |
Instances
Top (x ∷ k) | |
Defined in Data.SOP.Constraint |
newtype POP (f ∷ k → Type) (xss ∷ [[k]]) #
Constructors
POP (NP (NP f) xss) |
Instances
HTrans (POP ∷ (k1 → Type) → [[k1]] → Type) (POP ∷ (k2 → Type) → [[k2]] → Type) | |
Defined in Data.SOP.NP | |
HAp (POP ∷ (k → Type) → [[k]] → Type) | |
HCollapse (POP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NP | |
HPure (POP ∷ (k → Type) → [[k]] → Type) | |
HSequence (POP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NP Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN POP xs, Applicative f) ⇒ POP (f :.: g) xs → f (POP g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN POP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → POP f xs → g (POP f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN POP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → POP f xs → g (POP f' xs) # | |
HTraverse_ (POP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NP Methods hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN POP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → POP f xs → g () # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN POP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → POP f xs → g () # | |
Eq (NP (NP f) xss) ⇒ Eq (POP f xss) | |
Ord (NP (NP f) xss) ⇒ Ord (POP f xss) | |
Defined in Data.SOP.NP | |
Show (NP (NP f) xss) ⇒ Show (POP f xss) | |
Semigroup (NP (NP f) xss) ⇒ Semigroup (POP f xss) | |
Monoid (NP (NP f) xss) ⇒ Monoid (POP f xss) | |
NFData (NP (NP f) xss) ⇒ NFData (POP f xss) | |
Defined in Data.SOP.NP | |
type AllZipN (POP ∷ (k → Type) → [[k]] → Type) (c ∷ a → b → Constraint) | |
Defined in Data.SOP.NP | |
type Same (POP ∷ (k1 → Type) → [[k1]] → Type) | |
type Prod (POP ∷ (k → Type) → [[k]] → Type) | |
type UnProd (POP ∷ (k → Type) → [[k]] → Type) | |
type SListIN (POP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NP | |
type CollapseTo (POP ∷ (k → Type) → [[k]] → Type) a | |
Defined in Data.SOP.NP | |
type AllN (POP ∷ (k → Type) → [[k]] → Type) (c ∷ k → Constraint) | |
Defined in Data.SOP.NP |
newtype SOP (f ∷ k → Type) (xss ∷ [[k]]) #
Constructors
SOP (NS (NP f) xss) |
Instances
HTrans (SOP ∷ (k1 → Type) → [[k1]] → Type) (SOP ∷ (k2 → Type) → [[k2]] → Type) | |
Defined in Data.SOP.NS | |
HAp (SOP ∷ (k → Type) → [[k]] → Type) | |
HApInjs (SOP ∷ (k → Type) → [[k]] → Type) | |
HCollapse (SOP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NS | |
HExpand (SOP ∷ (k → Type) → [[k]] → Type) | |
HIndex (SOP ∷ (k → Type) → [[k]] → Type) | |
HSequence (SOP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NS Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN SOP xs, Applicative f) ⇒ SOP (f :.: g) xs → f (SOP g xs) # hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN SOP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → SOP f xs → g (SOP f' xs) # htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN SOP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → SOP f xs → g (SOP f' xs) # | |
HTraverse_ (SOP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NS Methods hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN SOP c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → SOP f xs → g () # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN SOP xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → SOP f xs → g () # | |
Eq (NS (NP f) xss) ⇒ Eq (SOP f xss) | |
Ord (NS (NP f) xss) ⇒ Ord (SOP f xss) | |
Defined in Data.SOP.NS | |
Show (NS (NP f) xss) ⇒ Show (SOP f xss) | |
NFData (NS (NP f) xss) ⇒ NFData (SOP f xss) | |
Defined in Data.SOP.NS | |
type Same (SOP ∷ (k1 → Type) → [[k1]] → Type) | |
type Prod (SOP ∷ (k → Type) → [[k]] → Type) | |
type SListIN (SOP ∷ (k → Type) → [[k]] → Type) | |
Defined in Data.SOP.NS | |
type CollapseTo (SOP ∷ (k → Type) → [[k]] → Type) a | |
Defined in Data.SOP.NS | |
type AllN (SOP ∷ (k → Type) → [[k]] → Type) (c ∷ k → Constraint) | |
Defined in Data.SOP.NS |
Constructors
SNil ∷ ∀ k. SList ('[] ∷ [k]) | |
SCons ∷ ∀ k (xs ∷ [k]) (x ∷ k). SListI xs ⇒ SList (x ': xs) |
Instances
Eq (SList xs) | |
Ord (SList xs) | |
Show (SList xs) | |
Constructors
ShapeNil ∷ ∀ k. Shape ('[] ∷ [k]) | |
ShapeCons ∷ ∀ k (xs ∷ [k]) (x ∷ k). SListI xs ⇒ Shape xs → Shape (x ': xs) |
Instances
Eq (Shape xs) | |
Ord (Shape xs) | |
Show (Shape xs) | |