Safe Haskell	None
Language	Haskell2010

Data.SOP.OptNP

Contents

View
Combining

Description

NP with optional values

Intended for qualified import

import           Data.SOP.OptNP (OptNP (..), ViewOptNP (..))
import qualified Data.SOP.OptNP as OptNP

Synopsis

type NonEmptyOptNP = OptNP 'False ∷ (k → Type) → [k] → Type
data OptNP (empty ∷ Bool) (f ∷ k → Type) (xs ∷ [k]) where
- OptNil ∷ ∀ {k} (f ∷ k → Type). OptNP 'True f ('[] ∷ [k])
- OptCons ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (empty1 ∷ Bool) (xs1 ∷ [k]). !(f x) → !(OptNP empty1 f xs1) → OptNP 'False f (x ': xs1)
- OptSkip ∷ ∀ {k} (empty ∷ Bool) (f ∷ k → Type) (xs1 ∷ [k]) (x ∷ k). !(OptNP empty f xs1) → OptNP empty f (x ': xs1)
at ∷ ∀ {k} (xs ∷ [k]) f (x ∷ k). SListI xs ⇒ f x → Index xs x → NonEmptyOptNP f xs
empty ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). SListI xs ⇒ OptNP 'True f xs
fromNP ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]) r. (∀ (empty ∷ Bool). OptNP empty f xs → r) → NP f xs → r
fromNonEmptyNP ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). IsNonEmpty xs ⇒ NP f xs → NonEmptyOptNP f xs
fromSingleton ∷ ∀ {k} f (x ∷ k). NonEmptyOptNP f '[x] → f x
singleton ∷ ∀ {k} f (x ∷ k). f x → NonEmptyOptNP f '[x]
toNP ∷ ∀ {k} (empty ∷ Bool) (f ∷ k → Type) (xs ∷ [k]). OptNP empty f xs → NP (Maybe :.: f) xs
data ViewOptNP (f ∷ k → Type) (xs ∷ [k]) where
- OptNP_ExactlyOne ∷ ∀ {k} (f ∷ k → Type) (x ∷ k). f x → ViewOptNP f '[x]
- OptNP_AtLeastTwo ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (y ∷ k) (zs ∷ [k]). ViewOptNP f (x ': (y ': zs))
view ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). NonEmptyOptNP f xs → ViewOptNP f xs
combine ∷ ∀ (f ∷ Type → Type) (xs ∷ [Type]). (SListI xs, HasCallStack) ⇒ Maybe (NonEmptyOptNP f xs) → Maybe (NonEmptyOptNP f xs) → Maybe (NonEmptyOptNP f xs)
combineWith ∷ ∀ (xs ∷ [Type]) (f ∷ Type → Type) (g ∷ Type → Type) h. SListI xs ⇒ (∀ a. These1 f g a → h a) → Maybe (NonEmptyOptNP f xs) → Maybe (NonEmptyOptNP g xs) → Maybe (NonEmptyOptNP h xs)
zipWith ∷ ∀ (f ∷ Type → Type) (g ∷ Type → Type) h (xs ∷ [Type]). (∀ a. These1 f g a → h a) → NonEmptyOptNP f xs → NonEmptyOptNP g xs → NonEmptyOptNP h xs

Documentation

type NonEmptyOptNP = OptNP 'False ∷ (k → Type) → [k] → Type Source #

data OptNP (empty ∷ Bool) (f ∷ k → Type) (xs ∷ [k]) where Source #

Like an NP, but with optional values

Constructors

OptNil ∷ ∀ {k} (f ∷ k → Type). OptNP 'True f ('[] ∷ [k])
OptCons ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (empty1 ∷ Bool) (xs1 ∷ [k]). !(f x) → !(OptNP empty1 f xs1) → OptNP 'False f (x ': xs1)
OptSkip ∷ ∀ {k} (empty ∷ Bool) (f ∷ k → Type) (xs1 ∷ [k]) (x ∷ k). !(OptNP empty f xs1) → OptNP empty f (x ': xs1)

Instances

Instances details

HTrans (OptNP empty ∷ (k1 → Type) → [k1] → Type) (OptNP empty ∷ (k2 → Type) → [k2] → Type) Source #
Instance details Defined in Data.SOP.OptNP Methods htrans ∷ ∀ c (xs ∷ [k1]) (ys ∷ [k2]) proxy f g. AllZipN (Prod (OptNP empty ∷ (k1 → Type) → [k1] → Type)) c xs ys ⇒ proxy c → (∀ (x ∷ k1) (y ∷ k2). c x y ⇒ f x → g y) → OptNP empty f xs → OptNP empty g ys Source # hcoerce ∷ ∀ (f ∷ k1 → Type) (g ∷ k2 → Type) (xs ∷ [k1]) (ys ∷ [k2]). AllZipN (Prod (OptNP empty ∷ (k1 → Type) → [k1] → Type)) (LiftedCoercible f g) xs ys ⇒ OptNP empty f xs → OptNP empty g ys Source #
HAp (OptNP empty ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.OptNP Methods hap ∷ ∀ (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). Prod (OptNP empty ∷ (k → Type) → [k] → Type) (f -.-> g) xs → OptNP empty f xs → OptNP empty g xs Source #
HSequence (OptNP empty ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.OptNP Methods hsequence' ∷ ∀ (xs ∷ [k]) f (g ∷ k → Type). (SListIN (OptNP empty ∷ (k → Type) → [k] → Type) xs, Applicative f) ⇒ OptNP empty (f :.: g) xs → f (OptNP empty g xs) Source # hctraverse' ∷ ∀ c (xs ∷ [k]) g proxy f f'. (AllN (OptNP empty ∷ (k → Type) → [k] → Type) c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g (f' a)) → OptNP empty f xs → g (OptNP empty f' xs) Source # htraverse' ∷ ∀ (xs ∷ [k]) g f f'. (SListIN (OptNP empty ∷ (k → Type) → [k] → Type) xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g (f' a)) → OptNP empty f xs → g (OptNP empty f' xs) Source #
All (Compose Show f) xs ⇒ Show (OptNP empty f xs) Source #
Instance details Defined in Data.SOP.OptNP Methods showsPrec ∷ Int → OptNP empty f xs → ShowS # show ∷ OptNP empty f xs → String # showList ∷ [OptNP empty f xs] → ShowS #
All (Compose Eq f) xs ⇒ Eq (OptNP empty f xs) Source #
Instance details Defined in Data.SOP.OptNP Methods (==) ∷ OptNP empty f xs → OptNP empty f xs → Bool # (/=) ∷ OptNP empty f xs → OptNP empty f xs → Bool #
type Same (OptNP empty ∷ (k1 → Type) → [k1] → Type) Source #
Instance details Defined in Data.SOP.OptNP type Same (OptNP empty ∷ (k1 → Type) → [k1] → Type) = OptNP empty ∷ (k2 → Type) → [k2] → Type
type Prod (OptNP empty ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.OptNP type Prod (OptNP empty ∷ (k → Type) → [k] → Type) = NP ∷ (k → Type) → [k] → Type
type SListIN (OptNP empty ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.OptNP type SListIN (OptNP empty ∷ (k → Type) → [k] → Type) = SListI ∷ [k] → Constraint
type AllN (OptNP empty ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source #
Instance details Defined in Data.SOP.OptNP type AllN (OptNP empty ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) = All c

at ∷ ∀ {k} (xs ∷ [k]) f (x ∷ k). SListI xs ⇒ f x → Index xs x → NonEmptyOptNP f xs Source #

empty ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). SListI xs ⇒ OptNP 'True f xs Source #

fromNP ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]) r. (∀ (empty ∷ Bool). OptNP empty f xs → r) → NP f xs → r Source #

fromNonEmptyNP ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). IsNonEmpty xs ⇒ NP f xs → NonEmptyOptNP f xs Source #

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

If OptNP is not empty, it must contain at least one value

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

toNP ∷ ∀ {k} (empty ∷ Bool) (f ∷ k → Type) (xs ∷ [k]). OptNP empty f xs → NP (Maybe :.: f) xs Source #

View

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

Constructors

OptNP_ExactlyOne ∷ ∀ {k} (f ∷ k → Type) (x ∷ k). f x → ViewOptNP f '[x]
OptNP_AtLeastTwo ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (y ∷ k) (zs ∷ [k]). ViewOptNP f (x ': (y ': zs))

view ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). NonEmptyOptNP f xs → ViewOptNP f xs Source #

Combining

combine ∷ ∀ (f ∷ Type → Type) (xs ∷ [Type]). (SListI xs, HasCallStack) ⇒ Maybe (NonEmptyOptNP f xs) → Maybe (NonEmptyOptNP f xs) → Maybe (NonEmptyOptNP f xs) Source #

Precondition: there is no overlap between the two given lists: if there is a Just at a given position in one, it must be Nothing at the same position in the other.

combineWith ∷ ∀ (xs ∷ [Type]) (f ∷ Type → Type) (g ∷ Type → Type) h. SListI xs ⇒ (∀ a. These1 f g a → h a) → Maybe (NonEmptyOptNP f xs) → Maybe (NonEmptyOptNP g xs) → Maybe (NonEmptyOptNP h xs) Source #

zipWith ∷ ∀ (f ∷ Type → Type) (g ∷ Type → Type) h (xs ∷ [Type]). (∀ a. These1 f g a → h a) → NonEmptyOptNP f xs → NonEmptyOptNP g xs → NonEmptyOptNP h xs Source #