Safe Haskell	None
Language	Haskell2010

Data.SOP.Strict.NS

Contents

NS
Injections

Description

Strict variant of NS

See sop-core's NS.

Synopsis

data NS (f ∷ k → Type) (xs ∷ [k]) where
- 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)
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

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 ∷ [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 #
Instance details Defined in Data.SOP.Strict.NS Methods hap ∷ ∀ (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). Prod (NS ∷ (k → Type) → [k] → Type) (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 ∷ [k]) a. SListIN (NS ∷ (k → Type) → [k] → Type) xs ⇒ NS (K a ∷ k → Type) xs → CollapseTo (NS ∷ (k → Type) → [k] → Type) a Source #
HExpand (NS ∷ (k → Type) → [k] → Type) Source #
Instance details 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 #
Instance details 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 #
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 ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). NS f xs → Int Source #

partition_NS ∷ ∀ {k} (xs ∷ [k]) (f ∷ k → Type). SListI xs ⇒ [NS f xs] → NP ([] :.: f) xs Source #

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.

unZ ∷ ∀ {k} f (x ∷ k). NS f '[x] → f x Source #

Injections

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

injections ∷ ∀ {k} (xs ∷ [k]) (f ∷ k → Type). SListI xs ⇒ NP (Injection f xs) xs Source #