Safe Haskell	None
Language	Haskell2010

Data.SOP.Strict.NP

Contents

NP

Description

Strict variant of NP

See sop-core's NP.

Synopsis

data NP (f ∷ k → Type) (xs ∷ [k]) where
- Nil ∷ ∀ {k} (f ∷ k → Type). NP f ('[] ∷ [k])
- (:*) ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (xs1 ∷ [k]). !(f x) → !(NP f xs1) → NP f (x ': xs1)
hd ∷ ∀ {k} f (x ∷ k) (xs ∷ [k]). NP f (x ': xs) → f x
map_NP' ∷ ∀ {k} f g (xs ∷ [k]). (∀ (a ∷ k). f a → g a) → NP f xs → NP g xs
npToSListI ∷ ∀ {k} (a ∷ k → Type) (xs ∷ [k]) r. NP a xs → (SListI xs ⇒ r) → r
singletonNP ∷ ∀ {k} f (x ∷ k). f x → NP f '[x]
tl ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (xs ∷ [k]). NP f (x ': xs) → NP f xs

NP

data NP (f ∷ k → Type) (xs ∷ [k]) where Source #

Constructors

Nil ∷ ∀ {k} (f ∷ k → Type). NP f ('[] ∷ [k])
(:*) ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (xs1 ∷ [k]). !(f x) → !(NP f xs1) → NP f (x ': xs1) infixr 5

Instances

Instances details

HTrans (NP ∷ (k1 → Type) → [k1] → Type) (NP ∷ (k2 → Type) → [k2] → Type) Source #
Instance details Defined in Data.SOP.Strict.NP Methods htrans ∷ ∀ c (xs ∷ [k1]) (ys ∷ [k2]) proxy f g. AllZipN (Prod (NP ∷ (k1 → Type) → [k1] → Type)) c xs ys ⇒ proxy c → (∀ (x ∷ k1) (y ∷ k2). c x y ⇒ f x → g y) → NP f xs → NP g ys Source # hcoerce ∷ ∀ (f ∷ k1 → Type) (g ∷ k2 → Type) (xs ∷ [k1]) (ys ∷ [k2]). AllZipN (Prod (NP ∷ (k1 → Type) → [k1] → Type)) (LiftedCoercible f g) xs ys ⇒ NP f xs → NP g ys Source #
HAp (NP ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NP Methods hap ∷ ∀ (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). Prod (NP ∷ (k → Type) → [k] → Type) (f -.-> g) xs → NP f xs → NP g xs Source #
HCollapse (NP ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NP Methods hcollapse ∷ ∀ (xs ∷ [k]) a. SListIN (NP ∷ (k → Type) → [k] → Type) xs ⇒ NP (K a ∷ k → Type) xs → CollapseTo (NP ∷ (k → Type) → [k] → Type) a Source #
HPure (NP ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NP Methods hpure ∷ ∀ (xs ∷ [k]) f. SListIN (NP ∷ (k → Type) → [k] → Type) xs ⇒ (∀ (a ∷ k). f a) → NP f xs Source # hcpure ∷ ∀ c (xs ∷ [k]) proxy f. AllN (NP ∷ (k → Type) → [k] → Type) c xs ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a) → NP f xs Source #
HSequence (NP ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NP Methods hsequence' ∷ ∀ (xs ∷ [k]) f (g ∷ k → Type). (SListIN (NP ∷ (k → Type) → [k] → Type) xs, Applicative f) ⇒ NP (f :.: g) xs → f (NP g xs) Source # hctraverse' ∷ ∀ c (xs ∷ [k]) g proxy f f'. (AllN (NP ∷ (k → Type) → [k] → Type) c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g (f' a)) → NP f xs → g (NP f' xs) Source # htraverse' ∷ ∀ (xs ∷ [k]) g f f'. (SListIN (NP ∷ (k → Type) → [k] → Type) xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g (f' a)) → NP f xs → g (NP f' xs) Source #
HTraverse_ (NP ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NP Methods hctraverse_ ∷ ∀ c (xs ∷ [k]) g proxy f. (AllN (NP ∷ (k → Type) → [k] → Type) c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g ()) → NP f xs → g () Source # htraverse_ ∷ ∀ (xs ∷ [k]) g f. (SListIN (NP ∷ (k → Type) → [k] → Type) xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g ()) → NP f xs → g () Source #
All (Compose Show f) xs ⇒ Show (NP f xs) Source #	Copied from sop-core Not derived, since derived instance ignores associativity info
Instance details Defined in Data.SOP.Strict.NP Methods showsPrec ∷ Int → NP f xs → ShowS # show ∷ NP f xs → String # showList ∷ [NP f xs] → ShowS #
All (Compose Eq f) xs ⇒ Eq (NP f xs) Source #
Instance details Defined in Data.SOP.Strict.NP Methods (==) ∷ NP f xs → NP f xs → Bool # (/=) ∷ NP f xs → NP f xs → Bool #
(All (Compose Eq f) xs, All (Compose Ord f) xs) ⇒ Ord (NP f xs) Source #
Instance details Defined in Data.SOP.Strict.NP Methods compare ∷ NP f xs → NP f xs → Ordering # (<) ∷ NP f xs → NP f xs → Bool # (<=) ∷ NP f xs → NP f xs → Bool # (>) ∷ NP f xs → NP f xs → Bool # (>=) ∷ NP f xs → NP f xs → Bool # max ∷ NP f xs → NP f xs → NP f xs # min ∷ NP f xs → NP f xs → NP f xs #
All (Compose NoThunks f) xs ⇒ NoThunks (NP f xs) Source #
Instance details Defined in Data.SOP.Strict.NP Methods noThunks ∷ Context → NP f xs → IO (Maybe ThunkInfo) Source # wNoThunks ∷ Context → NP f xs → IO (Maybe ThunkInfo) Source # showTypeOf ∷ Proxy (NP f xs) → String Source #
type AllZipN (NP ∷ (k → Type) → [k] → Type) (c ∷ a → b → Constraint) Source #
Instance details Defined in Data.SOP.Strict.NP type AllZipN (NP ∷ (k → Type) → [k] → Type) (c ∷ a → b → Constraint) = AllZip c
type Same (NP ∷ (k1 → Type) → [k1] → Type) Source #
Instance details Defined in Data.SOP.Strict.NP type Same (NP ∷ (k1 → Type) → [k1] → Type) = NP ∷ (k2 → Type) → [k2] → Type
type Prod (NP ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NP type Prod (NP ∷ (k → Type) → [k] → Type) = NP ∷ (k → Type) → [k] → Type
type SListIN (NP ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Strict.NP type SListIN (NP ∷ (k → Type) → [k] → Type) = SListI ∷ [k] → Constraint
type CollapseTo (NP ∷ (k → Type) → [k] → Type) a Source #
Instance details Defined in Data.SOP.Strict.NP type CollapseTo (NP ∷ (k → Type) → [k] → Type) a = [a]
type AllN (NP ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source #
Instance details Defined in Data.SOP.Strict.NP type AllN (NP ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) = All c

hd ∷ ∀ {k} f (x ∷ k) (xs ∷ [k]). NP f (x ': xs) → f x Source #

map_NP' ∷ ∀ {k} f g (xs ∷ [k]). (∀ (a ∷ k). f a → g a) → NP f xs → NP g xs Source #

Version of map_NP that does not require a singleton

npToSListI ∷ ∀ {k} (a ∷ k → Type) (xs ∷ [k]) r. NP a xs → (SListI xs ⇒ r) → r Source #

Conjure up an SListI constraint from an NP

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

tl ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (xs ∷ [k]). NP f (x ': xs) → NP f xs Source #