Safe Haskell	None
Language	Haskell2010

Data.SOP.Match

Contents

Utilities
SOP operators

Description

Intended for qualified import

import           Data.SOP.Match (Mismatch(..))
import qualified Data.SOP.Match as Match

Synopsis

data Mismatch (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]) where
- ML ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (g ∷ k → Type) (xs1 ∷ [k]). f x → NS g xs1 → Mismatch f g (x ': xs1)
- MR ∷ ∀ {k} (f ∷ k → Type) (xs1 ∷ [k]) (g ∷ k → Type) (x ∷ k). NS f xs1 → g x → Mismatch f g (x ': xs1)
- MS ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs1 ∷ [k]) (x ∷ k). Mismatch f g xs1 → Mismatch f g (x ': xs1)
flipMatch ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). Mismatch f g xs → Mismatch g f xs
matchNS ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]) (g ∷ k → Type). NS f xs → NS g xs → Either (Mismatch f g xs) (NS (Product f g) xs)
matchTelescope ∷ ∀ {k} (h ∷ k → Type) (xs ∷ [k]) (g ∷ k → Type) (f ∷ k → Type). NS h xs → Telescope g f xs → Either (Mismatch h f xs) (Telescope g (Product h f) xs)
telescopesMismatch ∷ ∀ {k} (a ∷ k → Type) (b ∷ k → Type) (xs ∷ [k]) (g ∷ k → Type) (f ∷ k → Type). Telescope a b xs → Telescope g f xs → Maybe (Mismatch b f xs)
mismatchNotEmpty ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]) a. Mismatch f g xs → (∀ (x ∷ k) (xs' ∷ [k]). xs ~ (x ': xs') ⇒ Mismatch f g (x ': xs') → a) → a
mismatchNotFirst ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (x ∷ k) (xs ∷ [k]). Mismatch f g (x ': xs) → Either (NS f xs) (NS g xs)
mismatchOne ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (x ∷ k). Mismatch f g '[x] → Void
mismatchToNS ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). Mismatch f g xs → (NS f xs, NS g xs)
mismatchTwo ∷ ∀ {k} f g (x ∷ k) (y ∷ k). Mismatch f g '[x, y] → Either (f x, g y) (f y, g x)
mkMismatchTwo ∷ ∀ {k} f (x ∷ k) g (y ∷ k). Either (f x, g y) (f y, g x) → Mismatch f g '[x, y]
mustMatchNS ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). HasCallStack ⇒ String → NS f xs → NS g xs → NS (Product f g) xs
bihap ∷ ∀ {k} (f ∷ k → Type) (f' ∷ k → Type) (xs ∷ [k]) (g ∷ k → Type) (g' ∷ k → Type). NP (f -.-> f') xs → NP (g -.-> g') xs → Mismatch f g xs → Mismatch f' g' xs
bihcmap ∷ ∀ {k} c (xs ∷ [k]) proxy f f' g g'. All c xs ⇒ proxy c → (∀ (x ∷ k). c x ⇒ f x → f' x) → (∀ (x ∷ k). c x ⇒ g x → g' x) → Mismatch f g xs → Mismatch f' g' xs
bihmap ∷ ∀ {k} (xs ∷ [k]) f f' g g'. SListI xs ⇒ (∀ (x ∷ k). f x → f' x) → (∀ (x ∷ k). g x → g' x) → Mismatch f g xs → Mismatch f' g' xs

Documentation

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

We have a mismatch in the index between two NS

Constructors

ML ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (g ∷ k → Type) (xs1 ∷ [k]). f x → NS g xs1 → Mismatch f g (x ': xs1)	The left is at the current `x` and the right is somewhere in the later `xs`
MR ∷ ∀ {k} (f ∷ k → Type) (xs1 ∷ [k]) (g ∷ k → Type) (x ∷ k). NS f xs1 → g x → Mismatch f g (x ': xs1)	The right is at the current `x` and the left is somewhere in the later `xs`
MS ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs1 ∷ [k]) (x ∷ k). Mismatch f g xs1 → Mismatch f g (x ': xs1)	There is a mismatch later on in the `xs`

Instances

Instances details

(∀ (x ∷ k2) (y ∷ k2). LiftedCoercible p p x y) ⇒ HTrans (Mismatch p ∷ (k2 → Type) → [k2] → Type) (Mismatch p ∷ (k2 → Type) → [k2] → Type) Source #
Instance details Defined in Data.SOP.Match Methods htrans ∷ ∀ c (xs ∷ [k2]) (ys ∷ [k2]) proxy f g. AllZipN (Prod (Mismatch p)) c xs ys ⇒ proxy c → (∀ (x ∷ k2) (y ∷ k2). c x y ⇒ f x → g y) → Mismatch p f xs → Mismatch p g ys Source # hcoerce ∷ ∀ (f ∷ k2 → Type) (g ∷ k2 → Type) (xs ∷ [k2]) (ys ∷ [k2]). AllZipN (Prod (Mismatch p)) (LiftedCoercible f g) xs ys ⇒ Mismatch p f xs → Mismatch p g ys Source #
HAp (Mismatch f ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Match Methods hap ∷ ∀ (f0 ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). Prod (Mismatch f) (f0 -.-> g) xs → Mismatch f f0 xs → Mismatch f g xs Source #
(All (Compose Show f) xs, All (Compose Show g) xs) ⇒ Show (Mismatch f g xs) Source #
Instance details Defined in Data.SOP.Match Methods showsPrec ∷ Int → Mismatch f g xs → ShowS # show ∷ Mismatch f g xs → String # showList ∷ [Mismatch f g xs] → ShowS #
(All (Compose Eq f) xs, All (Compose Eq g) xs) ⇒ Eq (Mismatch f g xs) Source #
Instance details Defined in Data.SOP.Match Methods (==) ∷ Mismatch f g xs → Mismatch f g xs → Bool # (/=) ∷ Mismatch f g xs → Mismatch f g xs → Bool #
(All (Compose Eq f) xs, All (Compose Ord f) xs, All (Compose Eq g) xs, All (Compose Ord g) xs) ⇒ Ord (Mismatch f g xs) Source #
Instance details Defined in Data.SOP.Match Methods compare ∷ Mismatch f g xs → Mismatch f g xs → Ordering # (<) ∷ Mismatch f g xs → Mismatch f g xs → Bool # (<=) ∷ Mismatch f g xs → Mismatch f g xs → Bool # (>) ∷ Mismatch f g xs → Mismatch f g xs → Bool # (>=) ∷ Mismatch f g xs → Mismatch f g xs → Bool # max ∷ Mismatch f g xs → Mismatch f g xs → Mismatch f g xs # min ∷ Mismatch f g xs → Mismatch f g xs → Mismatch f g xs #
(All (Compose NoThunks f) xs, All (Compose NoThunks g) xs) ⇒ NoThunks (Mismatch f g xs) Source #
Instance details Defined in Data.SOP.Match Methods noThunks ∷ Context → Mismatch f g xs → IO (Maybe ThunkInfo) Source # wNoThunks ∷ Context → Mismatch f g xs → IO (Maybe ThunkInfo) Source # showTypeOf ∷ Proxy (Mismatch f g xs) → String Source #
type Same (Mismatch f ∷ (k2 → Type) → [k2] → Type) Source #
Instance details Defined in Data.SOP.Match type Same (Mismatch f ∷ (k2 → Type) → [k2] → Type) = Mismatch f
type Prod (Mismatch f ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Match type Prod (Mismatch f ∷ (k → Type) → [k] → Type) = NP ∷ (k → Type) → [k] → Type
type SListIN (Mismatch f ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Match type SListIN (Mismatch f ∷ (k → Type) → [k] → Type) = SListI ∷ [k] → Constraint
type AllN (Mismatch f ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source #
Instance details Defined in Data.SOP.Match type AllN (Mismatch f ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) = All c

flipMatch ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). Mismatch f g xs → Mismatch g f xs Source #

matchNS ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]) (g ∷ k → Type). NS f xs → NS g xs → Either (Mismatch f g xs) (NS (Product f g) xs) Source #

matchTelescope ∷ ∀ {k} (h ∷ k → Type) (xs ∷ [k]) (g ∷ k → Type) (f ∷ k → Type). NS h xs → Telescope g f xs → Either (Mismatch h f xs) (Telescope g (Product h f) xs) Source #

telescopesMismatch ∷ ∀ {k} (a ∷ k → Type) (b ∷ k → Type) (xs ∷ [k]) (g ∷ k → Type) (f ∷ k → Type). Telescope a b xs → Telescope g f xs → Maybe (Mismatch b f xs) Source #

Utilities

mismatchNotEmpty ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]) a. Mismatch f g xs → (∀ (x ∷ k) (xs' ∷ [k]). xs ~ (x ': xs') ⇒ Mismatch f g (x ': xs') → a) → a Source #

mismatchNotFirst ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (x ∷ k) (xs ∷ [k]). Mismatch f g (x ': xs) → Either (NS f xs) (NS g xs) Source #

mismatchOne ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (x ∷ k). Mismatch f g '[x] → Void Source #

We cannot give a mismatch if we have only one type variable

mismatchToNS ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). Mismatch f g xs → (NS f xs, NS g xs) Source #

Project two NS from a Mismatch

We should have the property that

uncurry matchNS (mismatchToNS m) == Left m

mismatchTwo ∷ ∀ {k} f g (x ∷ k) (y ∷ k). Mismatch f g '[x, y] → Either (f x, g y) (f y, g x) Source #

If we only have two eras, only two possibilities for a mismatch

mkMismatchTwo ∷ ∀ {k} f (x ∷ k) g (y ∷ k). Either (f x, g y) (f y, g x) → Mismatch f g '[x, y] Source #

mustMatchNS ∷ ∀ {k} (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). HasCallStack ⇒ String → NS f xs → NS g xs → NS (Product f g) xs Source #

Variant of matchNS for when we know the two NSs must match. Otherwise an error, mentioning the given String, is thrown.

SOP operators

bihap ∷ ∀ {k} (f ∷ k → Type) (f' ∷ k → Type) (xs ∷ [k]) (g ∷ k → Type) (g' ∷ k → Type). NP (f -.-> f') xs → NP (g -.-> g') xs → Mismatch f g xs → Mismatch f' g' xs Source #

bihcmap ∷ ∀ {k} c (xs ∷ [k]) proxy f f' g g'. All c xs ⇒ proxy c → (∀ (x ∷ k). c x ⇒ f x → f' x) → (∀ (x ∷ k). c x ⇒ g x → g' x) → Mismatch f g xs → Mismatch f' g' xs Source #

Bifunctor analogue of hcmap

bihmap ∷ ∀ {k} (xs ∷ [k]) f f' g g'. SListI xs ⇒ (∀ (x ∷ k). f x → f' x) → (∀ (x ∷ k). g x → g' x) → Mismatch f g xs → Mismatch f' g' xs Source #