Modulesop-extras-0.4.1.1Haskell2010

Data.SOP.Match

Intended for qualified import

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

datadata Mismatch (f :: k -> Type) (g :: k -> Type) (xs :: [k]) where

We have a mismatch in the index between two NS

ML :: 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 :: 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 :: Mismatch f g xs1 -> Mismatch f g (x ': xs1)
There is a mismatch later on in the xs

Instances10HTrans, HAp, Eq, Ord, Show, NoThunks, …

(forall (x :: k2) (y :: k2). LiftedCoercible p p x y) => HTrans (Mismatch p) (Mismatch p)Defined in sop-extras-0.4.1.1 · Data.SOP.Match
HAp (Mismatch f)Defined in sop-extras-0.4.1.1 · Data.SOP.Match
(All (Compose Eq f) xs, All (Compose Eq g) xs) => Eq (Mismatch f g xs)Defined in sop-extras-0.4.1.1 · Data.SOP.Match
(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)Defined in sop-extras-0.4.1.1 · Data.SOP.Match
(All (Compose Show f) xs, All (Compose Show g) xs) => Show (Mismatch f g xs)Defined in sop-extras-0.4.1.1 · Data.SOP.Match
(All (Compose NoThunks f) xs, All (Compose NoThunks g) xs) => NoThunks (Mismatch f g xs)Defined in sop-extras-0.4.1.1 · Data.SOP.Match
type Prod (Mismatch f) = NPDefined in sop-extras-0.4.1.1 · Data.SOP.Match
type AllN (Mismatch f) c = All cDefined in sop-extras-0.4.1.1 · Data.SOP.Match
type Same (Mismatch f) = Mismatch fDefined in sop-extras-0.4.1.1 · Data.SOP.Match
type SListIN (Mismatch f) = SListIDefined in sop-extras-0.4.1.1 · Data.SOP.Match

valueflipMatch :: Mismatch f g xs -> Mismatch g f xs

valuematchNS

valuematchTelescope

valuetelescopesMismatch

Utilities

7 declarations

valuemismatchNotEmpty

:: Mismatch f g xs
-> forall (x :: k) (xs' :: [k]). xs ~ (x ': xs') => Mismatch f g (x ': xs') -> a
-> a

valuemismatchNotFirst :: Mismatch f g (x ': xs) -> Either (NS f xs) (NS g xs)

valuemismatchOne :: Mismatch f g '[x] -> Void

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

valuemismatchToNS :: Mismatch f g xs -> (NS f xs, NS g xs)

Project two NS from a Mismatch

We should have the property that

uncurry matchNS (mismatchToNS m) == Left m

valuemismatchTwo :: Mismatch f g '[x, y] -> Either (f x, g y) (f y, g x)

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

valuemkMismatchTwo :: Either (f x, g y) (f y, g x) -> Mismatch f g '[x, y]

valuemustMatchNS

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

3 declarations

valuebihap

valuebihcmap

Bifunctor analogue of hcmap

valuebihmap