Safe Haskell | None |
---|---|
Language | Haskell2010 |
Data.SOP.Strict.NS
Contents
Description
Strict variant of NS
See sop-core
's
NS.
Synopsis
- data NS (f ∷ k → Type) (xs ∷ [k]) where
- index_NS ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). NS f xs → Int
- partition_NS ∷ ∀ {k} (xs ∷ [k]) (f ∷ k → Type). SListI xs ⇒ [NS f xs] → NP ([] :.: f) xs
- sequence_NS' ∷ ∀ {k} (xs ∷ [k]) f (g ∷ k → Type). Functor f ⇒ NS (f :.: g) xs → f (NS g xs)
- unZ ∷ ∀ {k} f (x ∷ k). NS f '[x] → f x
- type Injection (f ∷ k → Type) (xs ∷ [k]) = f -.-> (K (NS f xs) ∷ k → Type)
- injections ∷ ∀ {k} (xs ∷ [k]) (f ∷ k → Type). SListI xs ⇒ NP (Injection f xs) xs
NS
data NS (f ∷ k → Type) (xs ∷ [k]) where Source #
Constructors
Z ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (xs1 ∷ [k]). !(f x) → NS f (x ': xs1) | |
S ∷ ∀ {k} (f ∷ k → Type) (xs1 ∷ [k]) (x ∷ k). !(NS f xs1) → NS f (x ': xs1) |
Instances
HTrans (NS ∷ (k1 → Type) → [k1] → Type) (NS ∷ (k2 → Type) → [k2] → Type) Source # | |
Defined in Data.SOP.Strict.NS Methods htrans ∷ ∀ c (xs ∷ [k1]) (ys ∷ [k2]) proxy f g. AllZipN (Prod (NS ∷ (k1 → Type) → [k1] → Type)) c xs ys ⇒ proxy c → (∀ (x ∷ k1) (y ∷ k2). c x y ⇒ f x → g y) → NS f xs → NS g ys Source # hcoerce ∷ ∀ (f ∷ k1 → Type) (g ∷ k2 → Type) (xs ∷ [k1]) (ys ∷ [k2]). AllZipN (Prod (NS ∷ (k1 → Type) → [k1] → Type)) (LiftedCoercible f g) xs ys ⇒ NS f xs → NS g ys Source # | |
HAp (NS ∷ (k → Type) → [k] → Type) Source # | |
HCollapse (NS ∷ (k → Type) → [k] → Type) Source # | |
HExpand (NS ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict.NS Methods hexpand ∷ ∀ (xs ∷ [k]) f. SListIN (Prod (NS ∷ (k → Type) → [k] → Type)) xs ⇒ (∀ (x ∷ k). f x) → NS f xs → Prod (NS ∷ (k → Type) → [k] → Type) f xs Source # hcexpand ∷ ∀ c (xs ∷ [k]) proxy f. AllN (Prod (NS ∷ (k → Type) → [k] → Type)) c xs ⇒ proxy c → (∀ (x ∷ k). c x ⇒ f x) → NS f xs → Prod (NS ∷ (k → Type) → [k] → Type) f xs Source # | |
HSequence (NS ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Strict.NS Methods hsequence' ∷ ∀ (xs ∷ [k]) f (g ∷ k → Type). (SListIN (NS ∷ (k → Type) → [k] → Type) xs, Applicative f) ⇒ NS (f :.: g) xs → f (NS g xs) Source # hctraverse' ∷ ∀ c (xs ∷ [k]) g proxy f f'. (AllN (NS ∷ (k → Type) → [k] → Type) c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g (f' a)) → NS f xs → g (NS f' xs) Source # htraverse' ∷ ∀ (xs ∷ [k]) g f f'. (SListIN (NS ∷ (k → Type) → [k] → Type) xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g (f' a)) → NS f xs → g (NS f' xs) Source # | |
All (Compose Show f) xs ⇒ Show (NS f xs) Source # | |
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 # | |
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.NS | |
type CollapseTo (NS ∷ (k → Type) → [k] → Type) a Source # | |
Defined in Data.SOP.Strict.NS | |
type AllN (NS ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
Defined in Data.SOP.Strict.NS |
sequence_NS' ∷ ∀ {k} (xs ∷ [k]) f (g ∷ k → Type). Functor f ⇒ NS (f :.: g) xs → f (NS g xs) Source #
Version of sequence_NS
that requires only Functor
The version in the library requires Applicative
, which is unnecessary.