Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- data Lens f xs a = Lens {}
- allComposeShowK ∷ (SListI xs, Show a) ⇒ Proxy xs → Proxy a → Dict (All (Compose Show (K a))) xs
- fn_5 ∷ (f0 a → f1 a → f2 a → f3 a → f4 a → f5 a) → (f0 -.-> (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5))))) a
- lenses_NP ∷ ∀ f xs. SListI xs ⇒ NP (Lens f xs) xs
- map_NP' ∷ ∀ f g xs. (∀ a. f a → g a) → NP f xs → NP g xs
- npToSListI ∷ NP a xs → (SListI xs ⇒ r) → r
- npWithIndices ∷ SListI xs ⇒ NP (K Word8) xs
- nsFromIndex ∷ SListI xs ⇒ Word8 → Maybe (NS (K ()) xs)
- nsToIndex ∷ SListI xs ⇒ NS f xs → Word8
- partition_NS ∷ ∀ xs f. SListI xs ⇒ [NS f xs] → NP ([] :.: f) xs
- sequence_NS' ∷ ∀ xs f g. Functor f ⇒ NS (f :.: g) xs → f (NS g xs)
- class IsNonEmpty xs where
- isNonEmpty ∷ proxy xs → ProofNonEmpty xs

- data ProofNonEmpty ∷ [a] → Type where
- ProofNonEmpty ∷ Proxy x → Proxy xs → ProofNonEmpty (x ': xs)

- checkIsNonEmpty ∷ ∀ xs. SListI xs ⇒ Proxy xs → Maybe (ProofNonEmpty xs)
- data Index xs x where
- dictIndexAll ∷ All c xs ⇒ Proxy c → Index xs x → Dict c x
- indices ∷ ∀ xs. SListI xs ⇒ NP (Index xs) xs
- injectNS ∷ ∀ f x xs. Index xs x → f x → NS f xs
- injectNS' ∷ ∀ f a b x xs. (Coercible a (f x), Coercible b (NS f xs)) ⇒ Proxy f → Index xs x → a → b
- projectNP ∷ Index xs x → NP f xs → f x
- hcimap ∷ (HAp h, All c xs, Prod h ~ NP) ⇒ proxy c → (∀ a. c a ⇒ Index xs a → f1 a → f2 a) → h f1 xs → h f2 xs
- hcizipWith ∷ (HAp h, All c xs, Prod h ~ NP) ⇒ proxy c → (∀ a. c a ⇒ Index xs a → f1 a → f2 a → f3 a) → NP f1 xs → h f2 xs → h f3 xs
- hcizipWith3 ∷ (HAp h, All c xs, Prod h ~ NP) ⇒ proxy c → (∀ a. 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 ∷ (HAp h, All c xs, Prod h ~ NP) ⇒ proxy c → (∀ a. 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 ∷ (HAp h, SListI xs, Prod h ~ NP) ⇒ (∀ a. Index xs a → f1 a → f2 a) → h f1 xs → h f2 xs
- hizipWith ∷ (HAp h, SListI xs, Prod h ~ NP) ⇒ (∀ a. Index xs a → f1 a → f2 a → f3 a) → NP f1 xs → h f2 xs → h f3 xs
- hizipWith3 ∷ (HAp h, SListI xs, Prod h ~ NP) ⇒ (∀ a. Index xs a → f1 a → f2 a → f3 a → f4 a) → NP f1 xs → NP f2 xs → h f3 xs → h f4 xs
- hizipWith4 ∷ (HAp h, SListI xs, Prod h ~ NP) ⇒ (∀ 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

# Minor variations on standard SOP operators

Simple lens to access an element of an n-ary product.

allComposeShowK ∷ (SListI xs, Show a) ⇒ Proxy xs → Proxy a → Dict (All (Compose Show (K a))) xs Source #

fn_5 ∷ (f0 a → f1 a → f2 a → f3 a → f4 a → f5 a) → (f0 -.-> (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5))))) a Source #

lenses_NP ∷ ∀ f xs. SListI xs ⇒ NP (Lens f xs) xs Source #

Generate all lenses to access the element of an n-ary product.

map_NP' ∷ ∀ f g xs. (∀ a. f a → g a) → NP f xs → NP g xs Source #

Version of `map_NP`

that does not require a singleton

nsFromIndex ∷ SListI xs ⇒ Word8 → Maybe (NS (K ()) xs) Source #

We only allow up to 23, see `npWithIndices`

.

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.

# Type-level non-empty lists

class IsNonEmpty xs where Source #

isNonEmpty ∷ proxy xs → ProofNonEmpty xs Source #

#### Instances

IsNonEmpty (x ': xs ∷ [a]) Source # | |

Defined in Ouroboros.Consensus.Util.SOP isNonEmpty ∷ proxy (x ': xs) → ProofNonEmpty (x ': xs) Source # |

data ProofNonEmpty ∷ [a] → Type where Source #

ProofNonEmpty ∷ Proxy x → Proxy xs → ProofNonEmpty (x ': xs) |

checkIsNonEmpty ∷ ∀ xs. SListI xs ⇒ Proxy xs → Maybe (ProofNonEmpty xs) Source #

# Indexing SOP types

injectNS' ∷ ∀ f a b x xs. (Coercible a (f x), Coercible b (NS f xs)) ⇒ Proxy f → Index xs x → a → b Source #

# Zipping with indices

hcimap ∷ (HAp h, All c xs, Prod h ~ NP) ⇒ proxy c → (∀ a. c a ⇒ Index xs a → f1 a → f2 a) → h f1 xs → h f2 xs Source #

hcizipWith ∷ (HAp h, All c xs, Prod h ~ NP) ⇒ proxy c → (∀ a. c a ⇒ Index xs a → f1 a → f2 a → f3 a) → NP f1 xs → h f2 xs → h f3 xs Source #

hcizipWith3 ∷ (HAp h, All c xs, Prod h ~ NP) ⇒ proxy c → (∀ a. 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 ∷ (HAp h, All c xs, Prod h ~ NP) ⇒ proxy c → (∀ a. 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 ∷ (HAp h, SListI xs, Prod h ~ NP) ⇒ (∀ a. Index xs a → f1 a → f2 a) → h f1 xs → h f2 xs Source #

hizipWith ∷ (HAp h, SListI xs, Prod h ~ NP) ⇒ (∀ a. Index xs a → f1 a → f2 a → f3 a) → NP f1 xs → h f2 xs → h f3 xs Source #