| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.SOP.Index
Synopsis
- newtype Index (xs ∷ [k]) (x ∷ k) where
- dictIndexAll ∷ ∀ {k} (c ∷ k → Constraint) (xs ∷ [k]) (x ∷ k). All c xs ⇒ Proxy c → Index xs x → Dict c x
- indices ∷ ∀ {k} (xs ∷ [k]). SListI xs ⇒ NP (Index xs) xs
- injectNS ∷ ∀ {k} f (x ∷ k) (xs ∷ [k]). All (Top ∷ k → Constraint) xs ⇒ Index xs x → f x → NS f xs
- injectNS' ∷ ∀ {k} (f ∷ k → Type) a b (x ∷ k) (xs ∷ [k]). (All (Top ∷ k → Constraint) xs, Coercible a (f x), Coercible b (NS f xs)) ⇒ Proxy f → Index xs x → a → b
- projectNP ∷ ∀ {k} (xs ∷ [k]) (x ∷ k) f. All (Top ∷ k → Constraint) xs ⇒ Index xs x → NP f xs → f x
- hcimap ∷ ∀ {k} h c (xs ∷ [k]) proxy f1 f2. (HAp h, All c xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ Index xs a → f1 a → f2 a) → h f1 xs → h f2 xs
- hcizipWith ∷ ∀ {k} h c (xs ∷ [k]) proxy f1 f2 f3. (HAp h, All c xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ Index xs a → f1 a → f2 a → f3 a) → NP f1 xs → h f2 xs → h f3 xs
- hcizipWith3 ∷ ∀ {k} h c (xs ∷ [k]) proxy f1 f2 f3 f4. (HAp h, All c xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ Index xs a → f1 a → f2 a → f3 a → f4 a) → NP f1 xs → NP f2 xs → h f3 xs → h f4 xs
- hcizipWith4 ∷ ∀ {k} h c (xs ∷ [k]) proxy f1 f2 f3 f4 f5. (HAp h, All c xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ Index xs a → f1 a → f2 a → f3 a → f4 a → f5 a) → NP f1 xs → NP f2 xs → NP f3 xs → h f4 xs → h f5 xs
- himap ∷ ∀ {k} h (xs ∷ [k]) f1 f2. (HAp h, SListI xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ (∀ (a ∷ k). Index xs a → f1 a → f2 a) → h f1 xs → h f2 xs
- hizipWith ∷ ∀ {k} h (xs ∷ [k]) f1 f2 f3. (HAp h, SListI xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ (∀ (a ∷ k). Index xs a → f1 a → f2 a → f3 a) → NP f1 xs → h f2 xs → h f3 xs
- hizipWith3 ∷ ∀ {k} h (xs ∷ [k]) f1 f2 f3 f4. (HAp h, SListI xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ (∀ (a ∷ k). Index xs a → f1 a → f2 a → f3 a → f4 a) → NP f1 xs → NP f2 xs → h f3 xs → h f4 xs
- hizipWith4 ∷ ∀ {k} h (xs ∷ [k]) f1 f2 f3 f4 f5. (HAp h, SListI xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ (∀ (a ∷ k). Index xs a → f1 a → f2 a → f3 a → f4 a → f5 a) → NP f1 xs → NP f2 xs → NP f3 xs → h f4 xs → h f5 xs
- npWithIndices ∷ ∀ {k} (xs ∷ [k]). SListI xs ⇒ NP (K Word8 ∷ k → Type) xs
- nsFromIndex ∷ ∀ {k} (xs ∷ [k]). SListI xs ⇒ Word8 → Maybe (NS (K () ∷ k → Type) xs)
- nsToIndex ∷ ∀ {k} (xs ∷ [k]) (f ∷ k → Type). SListI xs ⇒ NS f xs → Word8
- toWord8 ∷ ∀ {k} (xs ∷ [k]) (x ∷ k). Index xs x → Word8
Indexing SOP types
dictIndexAll ∷ ∀ {k} (c ∷ k → Constraint) (xs ∷ [k]) (x ∷ k). All c xs ⇒ Proxy c → Index xs x → Dict c x Source #
injectNS ∷ ∀ {k} f (x ∷ k) (xs ∷ [k]). All (Top ∷ k → Constraint) xs ⇒ Index xs x → f x → NS f xs Source #
injectNS' ∷ ∀ {k} (f ∷ k → Type) a b (x ∷ k) (xs ∷ [k]). (All (Top ∷ k → Constraint) xs, Coercible a (f x), Coercible b (NS f xs)) ⇒ Proxy f → Index xs x → a → b Source #
projectNP ∷ ∀ {k} (xs ∷ [k]) (x ∷ k) f. All (Top ∷ k → Constraint) xs ⇒ Index xs x → NP f xs → f x Source #
Zipping with indices
hcimap ∷ ∀ {k} h c (xs ∷ [k]) proxy f1 f2. (HAp h, All c xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ Index xs a → f1 a → f2 a) → h f1 xs → h f2 xs Source #
hcizipWith ∷ ∀ {k} h c (xs ∷ [k]) proxy f1 f2 f3. (HAp h, All c xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ Index xs a → f1 a → f2 a → f3 a) → NP f1 xs → h f2 xs → h f3 xs Source #
hcizipWith3 ∷ ∀ {k} h c (xs ∷ [k]) proxy f1 f2 f3 f4. (HAp h, All c xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ Index xs a → f1 a → f2 a → f3 a → f4 a) → NP f1 xs → NP f2 xs → h f3 xs → h f4 xs Source #
hcizipWith4 ∷ ∀ {k} h c (xs ∷ [k]) proxy f1 f2 f3 f4 f5. (HAp h, All c xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ Index xs a → f1 a → f2 a → f3 a → f4 a → f5 a) → NP f1 xs → NP f2 xs → NP f3 xs → h f4 xs → h f5 xs Source #
himap ∷ ∀ {k} h (xs ∷ [k]) f1 f2. (HAp h, SListI xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ (∀ (a ∷ k). Index xs a → f1 a → f2 a) → h f1 xs → h f2 xs Source #
hizipWith ∷ ∀ {k} h (xs ∷ [k]) f1 f2 f3. (HAp h, SListI xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ (∀ (a ∷ k). Index xs a → f1 a → f2 a → f3 a) → NP f1 xs → h f2 xs → h f3 xs Source #
hizipWith3 ∷ ∀ {k} h (xs ∷ [k]) f1 f2 f3 f4. (HAp h, SListI xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ (∀ (a ∷ k). Index xs a → f1 a → f2 a → f3 a → f4 a) → NP f1 xs → NP f2 xs → h f3 xs → h f4 xs Source #
hizipWith4 ∷ ∀ {k} h (xs ∷ [k]) f1 f2 f3 f4 f5. (HAp h, SListI xs, Prod h ~ (NP ∷ (k → Type) → [k] → Type)) ⇒ (∀ (a ∷ k). Index xs a → f1 a → f2 a → f3 a → f4 a → f5 a) → NP f1 xs → NP f2 xs → NP f3 xs → h f4 xs → h f5 xs Source #
Indices with Word
nsFromIndex ∷ ∀ {k} (xs ∷ [k]). SListI xs ⇒ Word8 → Maybe (NS (K () ∷ k → Type) xs) Source #
We only allow up to 23, see npWithIndices.