Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.SOP.Strict.NS

Contents

NS
Injections

Description

Strict variant of NS

See sop-core's NS.

Synopsis

data NS f xs where
- Z ∷ !(f x) → NS f (x ': xs)
- S ∷ !(NS f xs) → NS f (x ': xs)
index_NS ∷ ∀ f xs. NS f xs → Int
partition_NS ∷ ∀ xs f. SListI xs ⇒ [NS f xs] → NP (List :.: f) xs
sequence_NS' ∷ ∀ xs f g. Functor f ⇒ NS (f :.: g) xs → f (NS g xs)
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

NS

data NS f xs where Source #

Constructors

Z ∷ !(f x) → NS f (x ': xs)
S ∷ !(NS f xs) → NS f (x ': xs)

Instances

Instances details

HTrans (NS ∷ (k1 → Type) → [k1] → Type) (NS ∷ (k2 → Type) → [k2] → Type) Source #
Instance details Defined in Data.SOP.Strict.NS Methods htrans ∷ ∀ c (xs ∷ l1) (ys ∷ l2) proxy f g. AllZipN (Prod NS) c xs ys ⇒ proxy c → (∀ (x ∷ k10) (y ∷ k20). c x y ⇒ f x → g y) → NS f xs → NS g ys Source # hcoerce ∷ ∀ (f ∷ k10 → Type) (g ∷ k20 → Type) (xs ∷ l1) (ys ∷ l2). AllZipN (Prod NS) (LiftedCoercible f g) xs ys ⇒ NS f xs → NS g ys Source #
HAp (NS ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NS Methods hap ∷ ∀ (f ∷ k0 → Type) (g ∷ k0 → Type) (xs ∷ l). Prod NS (f -.-> g) xs → NS f xs → NS g xs Source #
HCollapse (NS ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NS Methods hcollapse ∷ ∀ (xs ∷ l) a. SListIN NS xs ⇒ NS (K a) xs → CollapseTo NS a Source #
HExpand (NS ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NS Methods hexpand ∷ ∀ (xs ∷ l) f. SListIN (Prod NS) xs ⇒ (∀ (x ∷ k0). f x) → NS f xs → Prod NS f xs Source # hcexpand ∷ ∀ c (xs ∷ l) proxy f. AllN (Prod NS) c xs ⇒ proxy c → (∀ (x ∷ k0). c x ⇒ f x) → NS f xs → Prod NS f xs Source #
HSequence (NS ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NS Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN NS xs, Applicative f) ⇒ NS (f :.: g) xs → f (NS g xs) Source # 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) Source # 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) Source #
All (Compose Show f) xs ⇒ Show (NS f xs) Source #
Instance details Defined in Data.SOP.Strict.NS Methods showsPrec ∷ Int → NS f xs → ShowS # show ∷ NS f xs → String # showList ∷ [NS f xs] → ShowS #
All (Compose Eq f) xs ⇒ Eq (NS f xs) Source #
Instance details Defined in Data.SOP.Strict.NS Methods (==) ∷ NS f xs → NS f xs → Bool # (/=) ∷ NS f xs → NS f xs → Bool #
(All (Compose Eq f) xs, All (Compose Ord f) xs) ⇒ Ord (NS f xs) Source #
Instance details Defined in Data.SOP.Strict.NS Methods compare ∷ NS f xs → NS f xs → Ordering # (<) ∷ NS f xs → NS f xs → Bool # (<=) ∷ NS f xs → NS f xs → Bool # (>) ∷ NS f xs → NS f xs → Bool # (>=) ∷ NS f xs → NS f xs → Bool # max ∷ NS f xs → NS f xs → NS f xs # min ∷ NS f xs → NS f xs → NS f xs #
All (Compose NoThunks f) xs ⇒ NoThunks (NS f xs) Source #
Instance details Defined in Data.SOP.Strict.NS Methods noThunks ∷ Context → NS f xs → IO (Maybe ThunkInfo) Source # wNoThunks ∷ Context → NS f xs → IO (Maybe ThunkInfo) Source # showTypeOf ∷ Proxy (NS f xs) → String Source #
type Same (NS ∷ (k1 → Type) → [k1] → Type) Source #
Instance details Defined in Data.SOP.Strict.NS type Same (NS ∷ (k1 → Type) → [k1] → Type) = NS ∷ (k2 → Type) → [k2] → Type
type Prod (NS ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NS type Prod (NS ∷ (k → Type) → [k] → Type) = NP ∷ (k → Type) → [k] → Type
type SListIN (NS ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NS type SListIN (NS ∷ (k → Type) → [k] → Type) = SListI ∷ [k] → Constraint
type CollapseTo (NS ∷ (k → Type) → [k] → Type) a Source #
Instance details Defined in Data.SOP.Strict.NS type CollapseTo (NS ∷ (k → Type) → [k] → Type) a = a
type AllN (NS ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source #
Instance details Defined in Data.SOP.Strict.NS type AllN (NS ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) = All c

index_NS ∷ ∀ f xs. NS f xs → Int Source #

partition_NS ∷ ∀ xs f. SListI xs ⇒ [NS f xs] → NP (List :.: f) xs Source #

sequence_NS' ∷ ∀ xs f g. 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.

unZ ∷ NS f '[x] → f x Source #

Injections

type Injection (f ∷ k → Type) (xs ∷ [k]) = f -.-> K (NS f xs) Source #

injections ∷ ∀ xs f. SListI xs ⇒ NP (Injection f xs) xs Source #