generics-sop-0.5.1.4: Generic Programming using True Sums of Products
Safe HaskellNone
LanguageHaskell2010

Generics.SOP.NP

Documentation

data NP (a :: k -> Type) (b :: [k]) where #

Constructors

Nil :: forall {k} (a :: k -> Type). NP a ('[] :: [k]) 
(:*) :: forall {k} (a :: k -> Type) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x ': xs) 

Instances

Instances details
HTrans (NP :: (k1 -> Type) -> [k1] -> Type) (NP :: (k2 -> Type) -> [k2] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

htrans :: forall c (xs :: [k1]) (ys :: [k2]) proxy f g. AllZipN (Prod (NP :: (k1 -> Type) -> [k1] -> Type)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NP f xs -> NP g ys #

hcoerce :: forall (f :: k1 -> Type) (g :: k2 -> Type) (xs :: [k1]) (ys :: [k2]). AllZipN (Prod (NP :: (k1 -> Type) -> [k1] -> Type)) (LiftedCoercible f g) xs ys => NP f xs -> NP g ys #

HAp (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hap :: forall (f :: k -> Type) (g :: k -> Type) (xs :: [k]). Prod (NP :: (k -> Type) -> [k] -> Type) (f -.-> g) xs -> NP f xs -> NP g xs #

HCollapse (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hcollapse :: forall (xs :: [k]) a. SListIN (NP :: (k -> Type) -> [k] -> Type) xs => NP (K a :: k -> Type) xs -> CollapseTo (NP :: (k -> Type) -> [k] -> Type) a #

HPure (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hpure :: forall (xs :: [k]) f. SListIN (NP :: (k -> Type) -> [k] -> Type) xs => (forall (a :: k). f a) -> NP f xs #

hcpure :: forall c (xs :: [k]) proxy f. AllN (NP :: (k -> Type) -> [k] -> Type) c xs => proxy c -> (forall (a :: k). c a => f a) -> NP f xs #

HSequence (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hsequence' :: forall (xs :: [k]) f (g :: k -> Type). (SListIN (NP :: (k -> Type) -> [k] -> Type) xs, Applicative f) => NP (f :.: g) xs -> f (NP g xs) #

hctraverse' :: forall c (xs :: [k]) g proxy f f'. (AllN (NP :: (k -> Type) -> [k] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) #

htraverse' :: forall (xs :: [k]) g f f'. (SListIN (NP :: (k -> Type) -> [k] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs) #

HTraverse_ (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hctraverse_ :: forall c (xs :: [k]) g proxy f. (AllN (NP :: (k -> Type) -> [k] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g () #

htraverse_ :: forall (xs :: [k]) g f. (SListIN (NP :: (k -> Type) -> [k] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g ()) -> NP f xs -> g () #

All (Compose NFData f) xs => NFData (NP f xs) 
Instance details

Defined in Data.SOP.NP

Methods

rnf :: NP f xs -> ()

(All (Compose Monoid f) xs, All (Compose Semigroup f) xs) => Monoid (NP f xs) 
Instance details

Defined in Data.SOP.NP

Methods

mempty :: NP f xs

mappend :: NP f xs -> NP f xs -> NP f xs

mconcat :: [NP f xs] -> NP f xs

All (Compose Semigroup f) xs => Semigroup (NP f xs) 
Instance details

Defined in Data.SOP.NP

Methods

(<>) :: NP f xs -> NP f xs -> NP f xs

sconcat :: NonEmpty (NP f xs) -> NP f xs

stimes :: Integral b => b -> NP f xs -> NP f xs

All (Compose Show f) xs => Show (NP f xs) 
Instance details

Defined in Data.SOP.NP

Methods

showsPrec :: Int -> NP f xs -> ShowS

show :: NP f xs -> String

showList :: [NP f xs] -> ShowS

All (Compose Eq f) xs => Eq (NP f xs) 
Instance details

Defined in Data.SOP.NP

Methods

(==) :: NP f xs -> NP f xs -> Bool

(/=) :: NP f xs -> NP f xs -> Bool

(All (Compose Eq f) xs, All (Compose Ord f) xs) => Ord (NP f xs) 
Instance details

Defined in Data.SOP.NP

Methods

compare :: NP f xs -> NP f xs -> Ordering

(<) :: NP f xs -> NP f xs -> Bool

(<=) :: NP f xs -> NP f xs -> Bool

(>) :: NP f xs -> NP f xs -> Bool

(>=) :: NP f xs -> NP f xs -> Bool

max :: NP f xs -> NP f xs -> NP f xs

min :: NP f xs -> NP f xs -> NP f xs

type AllZipN (NP :: (k -> Type) -> [k] -> Type) (c :: a -> b -> Constraint) 
Instance details

Defined in Data.SOP.NP

type AllZipN (NP :: (k -> Type) -> [k] -> Type) (c :: a -> b -> Constraint) = AllZip c
type Same (NP :: (k1 -> Type) -> [k1] -> Type) 
Instance details

Defined in Data.SOP.NP

type Same (NP :: (k1 -> Type) -> [k1] -> Type) = NP :: (k2 -> Type) -> [k2] -> Type
type Prod (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

type Prod (NP :: (k -> Type) -> [k] -> Type) = NP :: (k -> Type) -> [k] -> Type
type UnProd (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

type UnProd (NP :: (k -> Type) -> [k] -> Type) = NS :: (k -> Type) -> [k] -> Type
type SListIN (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

type SListIN (NP :: (k -> Type) -> [k] -> Type) = SListI :: [k] -> Constraint
type CollapseTo (NP :: (k -> Type) -> [k] -> Type) a 
Instance details

Defined in Data.SOP.NP

type CollapseTo (NP :: (k -> Type) -> [k] -> Type) a = [a]
type AllN (NP :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) 
Instance details

Defined in Data.SOP.NP

type AllN (NP :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) = All c

newtype POP (f :: k -> Type) (xss :: [[k]]) #

Constructors

POP (NP (NP f) xss) 

Instances

Instances details
HTrans (POP :: (k1 -> Type) -> [[k1]] -> Type) (POP :: (k2 -> Type) -> [[k2]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

htrans :: forall c (xs :: [[k1]]) (ys :: [[k2]]) proxy f g. AllZipN (Prod (POP :: (k1 -> Type) -> [[k1]] -> Type)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> POP f xs -> POP g ys #

hcoerce :: forall (f :: k1 -> Type) (g :: k2 -> Type) (xs :: [[k1]]) (ys :: [[k2]]). AllZipN (Prod (POP :: (k1 -> Type) -> [[k1]] -> Type)) (LiftedCoercible f g) xs ys => POP f xs -> POP g ys #

HAp (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hap :: forall (f :: k -> Type) (g :: k -> Type) (xs :: [[k]]). Prod (POP :: (k -> Type) -> [[k]] -> Type) (f -.-> g) xs -> POP f xs -> POP g xs #

HCollapse (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hcollapse :: forall (xs :: [[k]]) a. SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs => POP (K a :: k -> Type) xs -> CollapseTo (POP :: (k -> Type) -> [[k]] -> Type) a #

HPure (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hpure :: forall (xs :: [[k]]) f. SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs => (forall (a :: k). f a) -> POP f xs #

hcpure :: forall c (xs :: [[k]]) proxy f. AllN (POP :: (k -> Type) -> [[k]] -> Type) c xs => proxy c -> (forall (a :: k). c a => f a) -> POP f xs #

HSequence (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hsequence' :: forall (xs :: [[k]]) f (g :: k -> Type). (SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs, Applicative f) => POP (f :.: g) xs -> f (POP g xs) #

hctraverse' :: forall c (xs :: [[k]]) g proxy f f'. (AllN (POP :: (k -> Type) -> [[k]] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> POP f xs -> g (POP f' xs) #

htraverse' :: forall (xs :: [[k]]) g f f'. (SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> POP f xs -> g (POP f' xs) #

HTraverse_ (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hctraverse_ :: forall c (xs :: [[k]]) g proxy f. (AllN (POP :: (k -> Type) -> [[k]] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> POP f xs -> g () #

htraverse_ :: forall (xs :: [[k]]) g f. (SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g ()) -> POP f xs -> g () #

NFData (NP (NP f) xss) => NFData (POP f xss) 
Instance details

Defined in Data.SOP.NP

Methods

rnf :: POP f xss -> ()

Monoid (NP (NP f) xss) => Monoid (POP f xss) 
Instance details

Defined in Data.SOP.NP

Methods

mempty :: POP f xss

mappend :: POP f xss -> POP f xss -> POP f xss

mconcat :: [POP f xss] -> POP f xss

Semigroup (NP (NP f) xss) => Semigroup (POP f xss) 
Instance details

Defined in Data.SOP.NP

Methods

(<>) :: POP f xss -> POP f xss -> POP f xss

sconcat :: NonEmpty (POP f xss) -> POP f xss

stimes :: Integral b => b -> POP f xss -> POP f xss

Show (NP (NP f) xss) => Show (POP f xss) 
Instance details

Defined in Data.SOP.NP

Methods

showsPrec :: Int -> POP f xss -> ShowS

show :: POP f xss -> String

showList :: [POP f xss] -> ShowS

Eq (NP (NP f) xss) => Eq (POP f xss) 
Instance details

Defined in Data.SOP.NP

Methods

(==) :: POP f xss -> POP f xss -> Bool

(/=) :: POP f xss -> POP f xss -> Bool

Ord (NP (NP f) xss) => Ord (POP f xss) 
Instance details

Defined in Data.SOP.NP

Methods

compare :: POP f xss -> POP f xss -> Ordering

(<) :: POP f xss -> POP f xss -> Bool

(<=) :: POP f xss -> POP f xss -> Bool

(>) :: POP f xss -> POP f xss -> Bool

(>=) :: POP f xss -> POP f xss -> Bool

max :: POP f xss -> POP f xss -> POP f xss

min :: POP f xss -> POP f xss -> POP f xss

type AllZipN (POP :: (k -> Type) -> [[k]] -> Type) (c :: a -> b -> Constraint) 
Instance details

Defined in Data.SOP.NP

type AllZipN (POP :: (k -> Type) -> [[k]] -> Type) (c :: a -> b -> Constraint) = AllZip2 c
type Same (POP :: (k1 -> Type) -> [[k1]] -> Type) 
Instance details

Defined in Data.SOP.NP

type Same (POP :: (k1 -> Type) -> [[k1]] -> Type) = POP :: (k2 -> Type) -> [[k2]] -> Type
type Prod (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

type Prod (POP :: (k -> Type) -> [[k]] -> Type) = POP :: (k -> Type) -> [[k]] -> Type
type UnProd (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

type UnProd (POP :: (k -> Type) -> [[k]] -> Type) = SOP :: (k -> Type) -> [[k]] -> Type
type SListIN (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

type SListIN (POP :: (k -> Type) -> [[k]] -> Type) = SListI2 :: [[k]] -> Constraint
type CollapseTo (POP :: (k -> Type) -> [[k]] -> Type) a 
Instance details

Defined in Data.SOP.NP

type CollapseTo (POP :: (k -> Type) -> [[k]] -> Type) a = [[a]]
type AllN (POP :: (k -> Type) -> [[k]] -> Type) (c :: k -> Constraint) 
Instance details

Defined in Data.SOP.NP

type AllN (POP :: (k -> Type) -> [[k]] -> Type) (c :: k -> Constraint) = All2 c

unPOP :: forall {k} (f :: k -> Type) (xss :: [[k]]). POP f xss -> NP (NP f) xss #

hd :: forall {k} f (x :: k) (xs :: [k]). NP f (x ': xs) -> f x #

tl :: forall {k} (f :: k -> Type) (x :: k) (xs :: [k]). NP f (x ': xs) -> NP f xs #

type Projection (f :: k -> Type) (xs :: [k]) = (K (NP f xs) :: k -> Type) -.-> f #

projections :: forall {k} (xs :: [k]) (f :: k -> Type). SListI xs => NP (Projection f xs) xs #

shiftProjection :: forall {a1} (f :: a1 -> Type) (xs :: [a1]) (a2 :: a1) (x :: a1). Projection f xs a2 -> Projection f (x ': xs) a2 #

hcliftA' :: forall {k} (c :: k -> Constraint) (xss :: [[k]]) h proxy f f'. (All2 c xss, Prod h ~ (NP :: ([k] -> Type) -> [[k]] -> Type), HAp h) => proxy c -> (forall (xs :: [k]). All c xs => f xs -> f' xs) -> h f xss -> h f' xss #

hcliftA2' :: forall {k} (c :: k -> Constraint) (xss :: [[k]]) h proxy f f' f''. (All2 c xss, Prod h ~ (NP :: ([k] -> Type) -> [[k]] -> Type), HAp h) => proxy c -> (forall (xs :: [k]). All c xs => f xs -> f' xs -> f'' xs) -> Prod h f xss -> h f' xss -> h f'' xss #

hcliftA3' :: forall {k} (c :: k -> Constraint) (xss :: [[k]]) h proxy f f' f'' f'''. (All2 c xss, Prod h ~ (NP :: ([k] -> Type) -> [[k]] -> Type), HAp h) => proxy c -> (forall (xs :: [k]). All c xs => f xs -> f' xs -> f'' xs -> f''' xs) -> Prod h f xss -> Prod h f' xss -> h f'' xss -> h f''' xss #

fromList :: forall {k} (xs :: [k]) a. SListI xs => [a] -> Maybe (NP (K a :: k -> Type) xs) #

ap_NP :: forall {k} (f :: k -> Type) (g :: k -> Type) (xs :: [k]). NP (f -.-> g) xs -> NP f xs -> NP g xs #

cliftA2'_NP :: forall {k} (c :: k -> Constraint) (xss :: [[k]]) proxy f g h. All2 c xss => proxy c -> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs) -> NP f xss -> NP g xss -> NP h xss #

ana_NP :: forall {k} s f (xs :: [k]). SListI xs => (forall (y :: k) (ys :: [k]). s (y ': ys) -> (f y, s ys)) -> s xs -> NP f xs #

ap_POP :: forall {k} (f :: k -> Type) (g :: k -> Type) (xss :: [[k]]). POP (f -.-> g) xss -> POP f xss -> POP g xss #

cana_NP :: forall {k} c proxy s f (xs :: [k]). All c xs => proxy c -> (forall (y :: k) (ys :: [k]). c y => s (y ': ys) -> (f y, s ys)) -> s xs -> NP f xs #

cata_NP :: forall {a} r f (xs :: [a]). r ('[] :: [a]) -> (forall (y :: a) (ys :: [a]). f y -> r ys -> r (y ': ys)) -> NP f xs -> r xs #

ccata_NP :: forall {a} c proxy r f (xs :: [a]). All c xs => proxy c -> r ('[] :: [a]) -> (forall (y :: a) (ys :: [a]). c y => f y -> r ys -> r (y ': ys)) -> NP f xs -> r xs #

cfoldMap_NP :: forall {k} c (xs :: [k]) m proxy f. (All c xs, Monoid m) => proxy c -> (forall (a :: k). c a => f a -> m) -> NP f xs -> m #

cfoldMap_POP :: forall {k} c (xs :: [[k]]) m proxy f. (All2 c xs, Monoid m) => proxy c -> (forall (a :: k). c a => f a -> m) -> POP f xs -> m #

cliftA2_NP :: forall {k} c (xs :: [k]) proxy f g h. All c xs => proxy c -> (forall (a :: k). c a => f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs #

cliftA2_POP :: forall {k} c (xss :: [[k]]) proxy f g h. All2 c xss => proxy c -> (forall (a :: k). c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss #

cliftA3_NP :: forall {k} c (xs :: [k]) proxy f g h i. All c xs => proxy c -> (forall (a :: k). c a => f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs #

cliftA3_POP :: forall {k} c (xss :: [[k]]) proxy f g h i. All2 c xss => proxy c -> (forall (a :: k). c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss #

cliftA_NP :: forall {k} c (xs :: [k]) proxy f g. All c xs => proxy c -> (forall (a :: k). c a => f a -> g a) -> NP f xs -> NP g xs #

cliftA_POP :: forall {k} c (xss :: [[k]]) proxy f g. All2 c xss => proxy c -> (forall (a :: k). c a => f a -> g a) -> POP f xss -> POP g xss #

cmap_NP :: forall {k} c (xs :: [k]) proxy f g. All c xs => proxy c -> (forall (a :: k). c a => f a -> g a) -> NP f xs -> NP g xs #

cmap_POP :: forall {k} c (xss :: [[k]]) proxy f g. All2 c xss => proxy c -> (forall (a :: k). c a => f a -> g a) -> POP f xss -> POP g xss #

coerce_NP :: forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> Type) (xs :: [k1]) (ys :: [k2]). AllZip (LiftedCoercible f g) xs ys => NP f xs -> NP g ys #

coerce_POP :: forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> Type) (xss :: [[k1]]) (yss :: [[k2]]). AllZip2 (LiftedCoercible f g) xss yss => POP f xss -> POP g yss #

collapse_NP :: forall {k} a (xs :: [k]). NP (K a :: k -> Type) xs -> [a] #

collapse_POP :: forall {k} (xss :: [[k]]) a. SListI xss => POP (K a :: k -> Type) xss -> [[a]] #

cpure_NP :: forall {k} c (xs :: [k]) proxy f. All c xs => proxy c -> (forall (a :: k). c a => f a) -> NP f xs #

cpure_POP :: forall {k} c (xss :: [[k]]) proxy f. All2 c xss => proxy c -> (forall (a :: k). c a => f a) -> POP f xss #

ctraverse'_NP :: forall {k} c proxy (xs :: [k]) f f' g. (All c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) #

ctraverse'_POP :: forall {k} c (xss :: [[k]]) g proxy f f'. (All2 c xss, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> POP f xss -> g (POP f' xss) #

ctraverse_NP :: forall c (xs :: [Type]) g proxy f. (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs) #

ctraverse_POP :: forall c (xs :: [[Type]]) g proxy f. (All2 c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs) #

ctraverse__NP :: forall {k} c proxy (xs :: [k]) f g. (All c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g () #

ctraverse__POP :: forall {k} c proxy (xss :: [[k]]) f g. (All2 c xss, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> POP f xss -> g () #

czipWith3_NP :: forall {k} c (xs :: [k]) proxy f g h i. All c xs => proxy c -> (forall (a :: k). c a => f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs #

czipWith3_POP :: forall {k} c (xss :: [[k]]) proxy f g h i. All2 c xss => proxy c -> (forall (a :: k). c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss #

czipWith_NP :: forall {k} c (xs :: [k]) proxy f g h. All c xs => proxy c -> (forall (a :: k). c a => f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs #

czipWith_POP :: forall {k} c (xss :: [[k]]) proxy f g h. All2 c xss => proxy c -> (forall (a :: k). c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss #

fromI_NP :: forall {k} (f :: k -> Type) (xs :: [Type]) (ys :: [k]). AllZip (LiftedCoercible I f) xs ys => NP I xs -> NP f ys #

fromI_POP :: forall {k} (f :: k -> Type) (xss :: [[Type]]) (yss :: [[k]]). AllZip2 (LiftedCoercible I f) xss yss => POP I xss -> POP f yss #

liftA2_NP :: forall {k} (xs :: [k]) f g h. SListI xs => (forall (a :: k). f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs #

liftA2_POP :: forall {k} (xss :: [[k]]) f g h. All (SListI :: [k] -> Constraint) xss => (forall (a :: k). f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss #

liftA3_NP :: forall {k} (xs :: [k]) f g h i. SListI xs => (forall (a :: k). f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs #

liftA3_POP :: forall {k} (xss :: [[k]]) f g h i. All (SListI :: [k] -> Constraint) xss => (forall (a :: k). f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss #

liftA_NP :: forall {k} (xs :: [k]) f g. SListI xs => (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs #

liftA_POP :: forall {k} (xss :: [[k]]) f g. All (SListI :: [k] -> Constraint) xss => (forall (a :: k). f a -> g a) -> POP f xss -> POP g xss #

map_NP :: forall {k} (xs :: [k]) f g. SListI xs => (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs #

map_POP :: forall {k} (xss :: [[k]]) f g. All (SListI :: [k] -> Constraint) xss => (forall (a :: k). f a -> g a) -> POP f xss -> POP g xss #

pure_NP :: forall {k} f (xs :: [k]). SListI xs => (forall (a :: k). f a) -> NP f xs #

pure_POP :: forall {k} (xss :: [[k]]) f. All (SListI :: [k] -> Constraint) xss => (forall (a :: k). f a) -> POP f xss #

sequence'_NP :: forall {k} f (g :: k -> Type) (xs :: [k]). Applicative f => NP (f :.: g) xs -> f (NP g xs) #

sequence'_POP :: forall {k} (xss :: [[k]]) f (g :: k -> Type). (SListI xss, Applicative f) => POP (f :.: g) xss -> f (POP g xss) #

sequence_NP :: forall (xs :: [Type]) f. (SListI xs, Applicative f) => NP f xs -> f (NP I xs) #

sequence_POP :: forall (xss :: [[Type]]) f. (All (SListI :: [Type] -> Constraint) xss, Applicative f) => POP f xss -> f (POP I xss) #

toI_NP :: forall {k} (f :: k -> Type) (xs :: [k]) (ys :: [Type]). AllZip (LiftedCoercible f I) xs ys => NP f xs -> NP I ys #

toI_POP :: forall {k} (f :: k -> Type) (xss :: [[k]]) (yss :: [[Type]]). AllZip2 (LiftedCoercible f I) xss yss => POP f xss -> POP I yss #

trans_NP :: forall {k1} {k2} c (xs :: [k1]) (ys :: [k2]) proxy f g. AllZip c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NP f xs -> NP g ys #

trans_POP :: forall {k1} {k2} c (xss :: [[k1]]) (yss :: [[k2]]) proxy f g. AllZip2 c xss yss => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> POP f xss -> POP g yss #

traverse'_NP :: forall {k} (xs :: [k]) f f' g. (SListI xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs) #

traverse'_POP :: forall {k} (xss :: [[k]]) g f f'. (SListI2 xss, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> POP f xss -> g (POP f' xss) #

traverse__NP :: forall {k} (xs :: [k]) f g. (SListI xs, Applicative g) => (forall (a :: k). f a -> g ()) -> NP f xs -> g () #

traverse__POP :: forall {k} (xss :: [[k]]) f g. (SListI2 xss, Applicative g) => (forall (a :: k). f a -> g ()) -> POP f xss -> g () #

zipWith3_NP :: forall {k} (xs :: [k]) f g h i. SListI xs => (forall (a :: k). f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs #

zipWith3_POP :: forall {k} (xss :: [[k]]) f g h i. All (SListI :: [k] -> Constraint) xss => (forall (a :: k). f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss #

zipWith_NP :: forall {k} (xs :: [k]) f g h. SListI xs => (forall (a :: k). f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs #

zipWith_POP :: forall {k} (xss :: [[k]]) f g h. All (SListI :: [k] -> Constraint) xss => (forall (a :: k). f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss #