{-# LANGUAGE PolyKinds, StandaloneDeriving, UndecidableInstances #-}
-- | n-ary products (and products of products)
module Data.SOP.NP
  ( -- * Datatypes
    NP(..)
  , POP(..)
  , unPOP
    -- * Constructing products
  , pure_NP
  , pure_POP
  , cpure_NP
  , cpure_POP
    -- ** Construction from a list
  , fromList
    -- * Application
  , ap_NP
  , ap_POP
    -- * Destructing products
  , hd
  , tl
  , Projection
  , projections
  , shiftProjection
    -- * Lifting / mapping
  , liftA_NP
  , liftA_POP
  , liftA2_NP
  , liftA2_POP
  , liftA3_NP
  , liftA3_POP
  , map_NP
  , map_POP
  , zipWith_NP
  , zipWith_POP
  , zipWith3_NP
  , zipWith3_POP
  , cliftA_NP
  , cliftA_POP
  , cliftA2_NP
  , cliftA2_POP
  , cliftA3_NP
  , cliftA3_POP
  , cmap_NP
  , cmap_POP
  , czipWith_NP
  , czipWith_POP
  , czipWith3_NP
  , czipWith3_POP
    -- * Dealing with @'All' c@
  , hcliftA'
  , hcliftA2'
  , hcliftA3'
  , cliftA2'_NP
    -- * Collapsing
  , collapse_NP
  , collapse_POP
    -- * Folding and sequencing
  , ctraverse__NP
  , ctraverse__POP
  , traverse__NP
  , traverse__POP
  , cfoldMap_NP
  , cfoldMap_POP
  , sequence'_NP
  , sequence'_POP
  , sequence_NP
  , sequence_POP
  , ctraverse'_NP
  , ctraverse'_POP
  , traverse'_NP
  , traverse'_POP
  , ctraverse_NP
  , ctraverse_POP
    -- * Catamorphism and anamorphism
  , cata_NP
  , ccata_NP
  , ana_NP
  , cana_NP
    -- * Transformation of index lists and coercions
  , trans_NP
  , trans_POP
  , coerce_NP
  , coerce_POP
  , fromI_NP
  , fromI_POP
  , toI_NP
  , toI_POP
  ) where

import Data.Coerce
import Data.Kind (Type)
import Data.Proxy (Proxy(..))
import Unsafe.Coerce
import Data.Semigroup (Semigroup (..))

import Control.DeepSeq (NFData(..))

import Data.SOP.BasicFunctors
import Data.SOP.Classes
import Data.SOP.Constraint
import Data.SOP.Sing

-- | An n-ary product.
--
-- The product is parameterized by a type constructor @f@ and
-- indexed by a type-level list @xs@. The length of the list
-- determines the number of elements in the product, and if the
-- @i@-th element of the list is of type @x@, then the @i@-th
-- element of the product is of type @f x@.
--
-- The constructor names are chosen to resemble the names of the
-- list constructors.
--
-- Two common instantiations of @f@ are the identity functor 'I'
-- and the constant functor 'K'. For 'I', the product becomes a
-- heterogeneous list, where the type-level list describes the
-- types of its components. For @'K' a@, the product becomes a
-- homogeneous list, where the contents of the type-level list are
-- ignored, but its length still specifies the number of elements.
--
-- In the context of the SOP approach to generic programming, an
-- n-ary product describes the structure of the arguments of a
-- single data constructor.
--
-- /Examples:/
--
-- > I 'x'    :* I True  :* Nil  ::  NP I       '[ Char, Bool ]
-- > K 0      :* K 1     :* Nil  ::  NP (K Int) '[ Char, Bool ]
-- > Just 'x' :* Nothing :* Nil  ::  NP Maybe   '[ Char, Bool ]
--
data NP :: (k -> Type) -> [k] -> Type where
  Nil  :: NP f '[]
  (:*) :: f x -> NP f xs -> NP f (x ': xs)

infixr 5 :*

-- This is written manually,
-- because built-in deriving doesn't use associativity information!
instance All (Show `Compose` f) xs => Show (NP f xs) where
  showsPrec :: Int -> NP f xs -> ShowS
showsPrec _ Nil       = String -> ShowS
showString "Nil"
  showsPrec d :: Int
d (f :: f x
f :* fs :: NP f xs
fs) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 5)
    (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> f x -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (5 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) f x
f
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " :* "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NP f xs -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 5 NP f xs
fs

deriving instance All (Eq   `Compose` f) xs => Eq   (NP f xs)
deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NP f xs)

-- | @since 0.4.0.0
instance All (Semigroup `Compose` f) xs => Semigroup (NP f xs) where
  <> :: NP f xs -> NP f xs -> NP f xs
(<>) = Proxy (Compose Semigroup f)
-> (forall (a :: k). Compose Semigroup f a => f a -> f a -> f a)
-> NP f xs
-> NP f xs
-> NP f xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *)
       (h :: k -> *).
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_NP (Proxy (Compose Semigroup f)
forall k (t :: k). Proxy t
Proxy :: Proxy (Semigroup `Compose` f)) forall (a :: k). Compose Semigroup f a => f a -> f a -> f a
forall a. Semigroup a => a -> a -> a
(<>)

-- | @since 0.4.0.0
instance (All (Monoid `Compose` f) xs
#if MIN_VERSION_base(4,11,0)
  , All (Semigroup `Compose` f) xs  -- GHC isn't smart enough to figure this out
#endif
  ) => Monoid (NP f xs) where
  mempty :: NP f xs
mempty  = Proxy (Compose Monoid f)
-> (forall (a :: k). Compose Monoid f a => f a) -> NP f xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP (Proxy (Compose Monoid f)
forall k (t :: k). Proxy t
Proxy :: Proxy (Monoid `Compose` f)) forall (a :: k). Compose Monoid f a => f a
forall a. Monoid a => a
mempty
  mappend :: NP f xs -> NP f xs -> NP f xs
mappend = Proxy (Compose Monoid f)
-> (forall (a :: k). Compose Monoid f a => f a -> f a -> f a)
-> NP f xs
-> NP f xs
-> NP f xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *)
       (h :: k -> *).
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_NP (Proxy (Compose Monoid f)
forall k (t :: k). Proxy t
Proxy :: Proxy (Monoid `Compose` f)) forall (a :: k). Compose Monoid f a => f a -> f a -> f a
forall a. Monoid a => a -> a -> a
mappend

-- | @since 0.2.5.0
instance All (NFData `Compose` f) xs => NFData (NP f xs) where
    rnf :: NP f xs -> ()
rnf Nil       = ()
    rnf (x :: f x
x :* xs :: NP f xs
xs) = f x -> ()
forall a. NFData a => a -> ()
rnf f x
x () -> () -> ()
forall a b. a -> b -> b
`seq` NP f xs -> ()
forall a. NFData a => a -> ()
rnf NP f xs
xs

-- | A product of products.
--
-- This is a 'newtype' for an 'NP' of an 'NP'. The elements of the
-- inner products are applications of the parameter @f@. The type
-- 'POP' is indexed by the list of lists that determines the lengths
-- of both the outer and all the inner products, as well as the types
-- of all the elements of the inner products.
--
-- A 'POP' is reminiscent of a two-dimensional table (but the inner
-- lists can all be of different length). In the context of the SOP
-- approach to generic programming, a 'POP' is useful to represent
-- information that is available for all arguments of all constructors
-- of a datatype.
--
newtype POP (f :: (k -> Type)) (xss :: [[k]]) = POP (NP (NP f) xss)

deriving instance (Show (NP (NP f) xss)) => Show (POP f xss)
deriving instance (Eq   (NP (NP f) xss)) => Eq   (POP f xss)
deriving instance (Ord  (NP (NP f) xss)) => Ord  (POP f xss)

-- | @since 0.4.0.0
instance (Semigroup (NP (NP f) xss)) => Semigroup (POP f xss) where
  POP xss :: NP (NP f) xss
xss <> :: POP f xss -> POP f xss -> POP f xss
<> POP yss :: NP (NP f) xss
yss = NP (NP f) xss -> POP f xss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP (NP (NP f) xss
xss NP (NP f) xss -> NP (NP f) xss -> NP (NP f) xss
forall a. Semigroup a => a -> a -> a
<> NP (NP f) xss
yss)

-- | @since 0.4.0.0
instance (Monoid (NP (NP f) xss)) => Monoid (POP f xss) where
  mempty :: POP f xss
mempty                      = NP (NP f) xss -> POP f xss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP NP (NP f) xss
forall a. Monoid a => a
mempty
  mappend :: POP f xss -> POP f xss -> POP f xss
mappend (POP xss :: NP (NP f) xss
xss) (POP yss :: NP (NP f) xss
yss) = NP (NP f) xss -> POP f xss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP (NP (NP f) xss -> NP (NP f) xss -> NP (NP f) xss
forall a. Monoid a => a -> a -> a
mappend NP (NP f) xss
xss NP (NP f) xss
yss)

-- | @since 0.2.5.0
instance (NFData (NP (NP f) xss)) => NFData (POP f xss) where
    rnf :: POP f xss -> ()
rnf (POP xss :: NP (NP f) xss
xss) = NP (NP f) xss -> ()
forall a. NFData a => a -> ()
rnf NP (NP f) xss
xss

-- | Unwrap a product of products.
unPOP :: POP f xss -> NP (NP f) xss
unPOP :: POP f xss -> NP (NP f) xss
unPOP (POP xss :: NP (NP f) xss
xss) = NP (NP f) xss
xss

type instance AllN NP  c = All  c
type instance AllN POP c = All2 c

type instance AllZipN NP  c = AllZip  c
type instance AllZipN POP c = AllZip2 c

type instance SListIN NP  = SListI
type instance SListIN POP = SListI2

-- * Constructing products

-- | Specialization of 'hpure'.
--
-- The call @'pure_NP' x@ generates a product that contains 'x' in every
-- element position.
--
-- /Example:/
--
-- >>> pure_NP [] :: NP [] '[Char, Bool]
-- "" :* [] :* Nil
-- >>> pure_NP (K 0) :: NP (K Int) '[Double, Int, String]
-- K 0 :* K 0 :* K 0 :* Nil
--
pure_NP :: forall f xs. SListI xs => (forall a. f a) -> NP f xs
pure_NP :: (forall (a :: k). f a) -> NP f xs
pure_NP f :: forall (a :: k). f a
f = Proxy Top -> (forall (a :: k). Top a => f a) -> NP f xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP Proxy Top
forall k. Proxy Top
topP forall (a :: k). f a
forall (a :: k). Top a => f a
f
{-# INLINE pure_NP #-}

-- | Specialization of 'hpure'.
--
-- The call @'pure_POP' x@ generates a product of products that contains 'x'
-- in every element position.
--
pure_POP :: All SListI xss => (forall a. f a) -> POP f xss
pure_POP :: (forall (a :: k). f a) -> POP f xss
pure_POP f :: forall (a :: k). f a
f = Proxy Top -> (forall (a :: k). Top a => f a) -> POP f xss
forall k (c :: k -> Constraint) (xss :: [[k]])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All2 c xss =>
proxy c -> (forall (a :: k). c a => f a) -> POP f xss
cpure_POP Proxy Top
forall k. Proxy Top
topP forall (a :: k). f a
forall (a :: k). Top a => f a
f
{-# INLINE pure_POP #-}

topP :: Proxy Top
topP :: Proxy Top
topP = Proxy Top
forall k (t :: k). Proxy t
Proxy

-- | Specialization of 'hcpure'.
--
-- The call @'cpure_NP' p x@ generates a product that contains 'x' in every
-- element position.
--
cpure_NP :: forall c xs proxy f. All c xs
         => proxy c -> (forall a. c a => f a) -> NP f xs
cpure_NP :: proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP p :: proxy c
p f :: forall (a :: k). c a => f a
f = case SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList :: SList xs of
  SNil   -> NP f xs
forall k (f :: k -> *). NP f '[]
Nil
  SCons  -> f x
forall (a :: k). c a => f a
f f x -> NP f xs -> NP f (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* proxy c -> (forall (a :: k). c a => f a) -> NP f xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP proxy c
p forall (a :: k). c a => f a
f

-- | Specialization of 'hcpure'.
--
-- The call @'cpure_NP' p x@ generates a product of products that contains 'x'
-- in every element position.
--
cpure_POP :: forall c xss proxy f. All2 c xss
          => proxy c -> (forall a. c a => f a) -> POP f xss
cpure_POP :: proxy c -> (forall (a :: k). c a => f a) -> POP f xss
cpure_POP p :: proxy c
p f :: forall (a :: k). c a => f a
f = NP (NP f) xss -> POP f xss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP (Proxy (All c)
-> (forall (a :: [k]). All c a => NP f a) -> NP (NP f) xss
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP (proxy c -> Proxy (All c)
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint).
proxy c -> Proxy (All c)
allP proxy c
p) (proxy c -> (forall (a :: k). c a => f a) -> NP f a
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP proxy c
p forall (a :: k). c a => f a
f))

allP :: proxy c -> Proxy (All c)
allP :: proxy c -> Proxy (All c)
allP _ = Proxy (All c)
forall k (t :: k). Proxy t
Proxy

instance HPure NP where
  hpure :: (forall (a :: k). f a) -> NP f xs
hpure  = (forall (a :: k). f a) -> NP f xs
forall k (f :: k -> *) (xs :: [k]).
SListI xs =>
(forall (a :: k). f a) -> NP f xs
pure_NP
  hcpure :: proxy c -> (forall (a :: k). c a => f a) -> NP f xs
hcpure = proxy c -> (forall (a :: k). c a => f a) -> NP f xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP

instance HPure POP where
  hpure :: (forall (a :: k). f a) -> POP f xs
hpure  = (forall (a :: k). f a) -> POP f xs
forall k (xss :: [[k]]) (f :: k -> *).
All SListI xss =>
(forall (a :: k). f a) -> POP f xss
pure_POP
  hcpure :: proxy c -> (forall (a :: k). c a => f a) -> POP f xs
hcpure = proxy c -> (forall (a :: k). c a => f a) -> POP f xs
forall k (c :: k -> Constraint) (xss :: [[k]])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All2 c xss =>
proxy c -> (forall (a :: k). c a => f a) -> POP f xss
cpure_POP

-- ** Construction from a list

-- | Construct a homogeneous n-ary product from a normal Haskell list.
--
-- Returns 'Nothing' if the length of the list does not exactly match the
-- expected size of the product.
--
fromList :: SListI xs => [a] -> Maybe (NP (K a) xs)
fromList :: [a] -> Maybe (NP (K a) xs)
fromList = SList xs -> [a] -> Maybe (NP (K a) xs)
forall k (xs :: [k]) a. SList xs -> [a] -> Maybe (NP (K a) xs)
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: SList xs -> [a] -> Maybe (NP (K a) xs)
    go :: SList xs -> [a] -> Maybe (NP (K a) xs)
go SNil  []     = NP (K a) '[] -> Maybe (NP (K a) '[])
forall (m :: * -> *) a. Monad m => a -> m a
return NP (K a) '[]
forall k (f :: k -> *). NP f '[]
Nil
    go SCons (x :: a
x:xs :: [a]
xs) = do NP (K a) xs
ys <- SList xs -> [a] -> Maybe (NP (K a) xs)
forall k (xs :: [k]) a. SList xs -> [a] -> Maybe (NP (K a) xs)
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList [a]
xs ; NP (K a) (x : xs) -> Maybe (NP (K a) (x : xs))
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> K a x
forall k a (b :: k). a -> K a b
K a
x K a x -> NP (K a) xs -> NP (K a) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP (K a) xs
ys)
    go _     _      = Maybe (NP (K a) xs)
forall a. Maybe a
Nothing

-- * Application

-- | Specialization of 'hap'.
--
-- Applies a product of (lifted) functions pointwise to a product of
-- suitable arguments.
--
ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP Nil           Nil        = NP g xs
forall k (f :: k -> *). NP f '[]
Nil
ap_NP (Fn f :: f x -> g x
f :* fs :: NP (f -.-> g) xs
fs)  (x :: f x
x :* xs :: NP f xs
xs)  = f x -> g x
f f x
f x
x g x -> NP g xs -> NP g (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP (f -.-> g) xs -> NP f xs -> NP g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP NP (f -.-> g) xs
fs NP f xs
NP f xs
xs

-- | Specialization of 'hap'.
--
-- Applies a product of (lifted) functions pointwise to a product of
-- suitable arguments.
--
ap_POP :: POP (f -.-> g) xss -> POP f xss -> POP g xss
ap_POP :: POP (f -.-> g) xss -> POP f xss -> POP g xss
ap_POP (POP fss' :: NP (NP (f -.-> g)) xss
fss') (POP xss' :: NP (NP f) xss
xss') = NP (NP g) xss -> POP g xss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP (NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
forall k (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
go NP (NP (f -.-> g)) xss
fss' NP (NP f) xss
xss')
  where
    go :: NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
    go :: NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
go Nil         Nil         = NP (NP g) xss
forall k (f :: k -> *). NP f '[]
Nil
    go (fs :: NP (f -.-> g) x
fs :* fss :: NP (NP (f -.-> g)) xs
fss) (xs :: NP f x
xs :* xss :: NP (NP f) xs
xss) = NP (f -.-> g) x -> NP f x -> NP g x
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP NP (f -.-> g) x
fs NP f x
NP f x
xs NP g x -> NP (NP g) xs -> NP (NP g) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP (NP (f -.-> g)) xs -> NP (NP f) xs -> NP (NP g) xs
forall k (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
go NP (NP (f -.-> g)) xs
fss NP (NP f) xs
NP (NP f) xs
xss

-- The definition of 'ap_POP' is a more direct variant of
-- '_ap_POP_spec'. The direct definition has the advantage
-- that it avoids the 'SListI' constraint.
_ap_POP_spec :: SListI xss => POP (f -.-> g) xss -> POP  f xss -> POP  g xss
_ap_POP_spec :: POP (f -.-> g) xss -> POP f xss -> POP g xss
_ap_POP_spec (POP fs :: NP (NP (f -.-> g)) xss
fs) (POP xs :: NP (NP f) xss
xs) = NP (NP g) xss -> POP g xss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP ((forall (a :: [k]). NP (f -.-> g) a -> NP f a -> NP g a)
-> NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
forall k (xs :: [k]) (f :: k -> *) (g :: k -> *) (h :: k -> *).
SListI xs =>
(forall (a :: k). f a -> g a -> h a)
-> NP f xs -> NP g xs -> NP h xs
liftA2_NP forall (a :: [k]). NP (f -.-> g) a -> NP f a -> NP g a
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP NP (NP (f -.-> g)) xss
fs NP (NP f) xss
xs)

type instance Same NP  = NP
type instance Same POP = POP

type instance Prod NP  = NP
type instance Prod POP = POP

instance HAp NP  where hap :: Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
hap = Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP
instance HAp POP where hap :: Prod POP (f -.-> g) xs -> POP f xs -> POP g xs
hap = Prod POP (f -.-> g) xs -> POP f xs -> POP g xs
forall k (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
POP (f -.-> g) xss -> POP f xss -> POP g xss
ap_POP

-- * Destructing products

-- | Obtain the head of an n-ary product.
--
-- @since 0.2.1.0
--
hd :: NP f (x ': xs) -> f x
hd :: NP f (x : xs) -> f x
hd (x :: f x
x :* _xs :: NP f xs
_xs) = f x
f x
x

-- | Obtain the tail of an n-ary product.
--
-- @since 0.2.1.0
--
tl :: NP f (x ': xs) -> NP f xs
tl :: NP f (x : xs) -> NP f xs
tl (_x :: f x
_x :* xs :: NP f xs
xs) = NP f xs
NP f xs
xs

-- | The type of projections from an n-ary product.
--
-- A projection is a function from the n-ary product to a single element.
--
type Projection (f :: k -> Type) (xs :: [k]) = K (NP f xs) -.-> f

-- | Compute all projections from an n-ary product.
--
-- Each element of the resulting product contains one of the projections.
--
projections :: forall xs f . SListI xs => NP (Projection f xs) xs
projections :: NP (Projection f xs) xs
projections = case SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList :: SList xs of
  SNil  -> NP (Projection f xs) xs
forall k (f :: k -> *). NP f '[]
Nil
  SCons -> (K (NP f (x : xs)) x -> f x) -> (-.->) (K (NP f (x : xs))) f x
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn (NP f (x : xs) -> f x
forall k (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
hd (NP f (x : xs) -> f x)
-> (K (NP f (x : xs)) x -> NP f (x : xs))
-> K (NP f (x : xs)) x
-> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K (NP f (x : xs)) x -> NP f (x : xs)
forall k a (b :: k). K a b -> a
unK) (-.->) (K (NP f (x : xs))) f x
-> NP (K (NP f (x : xs)) -.-> f) xs
-> NP (K (NP f (x : xs)) -.-> f) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* (forall (a :: k).
 Projection f xs a -> (-.->) (K (NP f (x : xs))) f a)
-> NP (Projection f xs) xs -> NP (K (NP f (x : xs)) -.-> f) xs
forall k (xs :: [k]) (f :: k -> *) (g :: k -> *).
SListI xs =>
(forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
liftA_NP forall (a :: k).
Projection f xs a -> (-.->) (K (NP f (x : xs))) f a
forall a (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
Projection f xs a -> Projection f (x : xs) a
shiftProjection NP (Projection f xs) xs
forall k (xs :: [k]) (f :: k -> *).
SListI xs =>
NP (Projection f xs) xs
projections

shiftProjection :: Projection f xs a -> Projection f (x ': xs) a
shiftProjection :: Projection f xs a -> Projection f (x : xs) a
shiftProjection (Fn f :: K (NP f xs) a -> f a
f) = (K (NP f (x : xs)) a -> f a) -> Projection f (x : xs) a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((K (NP f (x : xs)) a -> f a) -> Projection f (x : xs) a)
-> (K (NP f (x : xs)) a -> f a) -> Projection f (x : xs) a
forall a b. (a -> b) -> a -> b
$ K (NP f xs) a -> f a
f (K (NP f xs) a -> f a)
-> (K (NP f (x : xs)) a -> K (NP f xs) a)
-> K (NP f (x : xs)) a
-> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP f xs -> K (NP f xs) a
forall k a (b :: k). a -> K a b
K (NP f xs -> K (NP f xs) a)
-> (K (NP f (x : xs)) a -> NP f xs)
-> K (NP f (x : xs)) a
-> K (NP f xs) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP f (x : xs) -> NP f xs
forall k (f :: k -> *) (x :: k) (xs :: [k]).
NP f (x : xs) -> NP f xs
tl (NP f (x : xs) -> NP f xs)
-> (K (NP f (x : xs)) a -> NP f (x : xs))
-> K (NP f (x : xs)) a
-> NP f xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K (NP f (x : xs)) a -> NP f (x : xs)
forall k a (b :: k). K a b -> a
unK

-- * Lifting / mapping

-- | Specialization of 'hliftA'.
liftA_NP  :: SListI     xs  => (forall a. f a -> g a) -> NP  f xs  -> NP  g xs
-- | Specialization of 'hliftA'.
liftA_POP :: All SListI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss

liftA_NP :: (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
liftA_NP  = (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hliftA
liftA_POP :: (forall (a :: k). f a -> g a) -> POP f xss -> POP g xss
liftA_POP = (forall (a :: k). f a -> g a) -> POP f xss -> POP g xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hliftA

-- | Specialization of 'hliftA2'.
liftA2_NP  :: SListI     xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP   h xs
-- | Specialization of 'hliftA2'.
liftA2_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP  h xss

liftA2_NP :: (forall (a :: k). f a -> g a -> h a)
-> NP f xs -> NP g xs -> NP h xs
liftA2_NP  = (forall (a :: k). f a -> g a -> h a)
-> NP f xs -> NP g xs -> NP h xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hliftA2
liftA2_POP :: (forall (a :: k). f a -> g a -> h a)
-> POP f xss -> POP g xss -> POP h xss
liftA2_POP = (forall (a :: k). f a -> g a -> h a)
-> POP f xss -> POP g xss -> POP h xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hliftA2

-- | Specialization of 'hliftA3'.
liftA3_NP  :: SListI     xs  => (forall a. f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
-- | Specialization of 'hliftA3'.
liftA3_POP :: All SListI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

liftA3_NP :: (forall (a :: k). f a -> g a -> h a -> i a)
-> NP f xs -> NP g xs -> NP h xs -> NP i xs
liftA3_NP  = (forall (a :: k). f a -> g a -> h a -> i a)
-> NP f xs -> NP g xs -> NP h xs -> NP i xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
hliftA3
liftA3_POP :: (forall (a :: k). f a -> g a -> h a -> i a)
-> POP f xss -> POP g xss -> POP h xss -> POP i xss
liftA3_POP = (forall (a :: k). f a -> g a -> h a -> i a)
-> POP f xss -> POP g xss -> POP h xss -> POP i xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
hliftA3

-- | Specialization of 'hmap', which is equivalent to 'hliftA'.
map_NP  :: SListI     xs  => (forall a. f a -> g a) -> NP  f xs  -> NP  g xs
-- | Specialization of 'hmap', which is equivalent to 'hliftA'.
map_POP :: All SListI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss

map_NP :: (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
map_NP  = (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap
map_POP :: (forall (a :: k). f a -> g a) -> POP f xss -> POP g xss
map_POP = (forall (a :: k). f a -> g a) -> POP f xss -> POP g xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap

-- | Specialization of 'hzipWith', which is equivalent to 'hliftA2'.
zipWith_NP  :: SListI     xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP   h xs
-- | Specialization of 'hzipWith', which is equivalent to 'hliftA2'.
zipWith_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP  h xss

zipWith_NP :: (forall (a :: k). f a -> g a -> h a)
-> NP f xs -> NP g xs -> NP h xs
zipWith_NP  = (forall (a :: k). f a -> g a -> h a)
-> NP f xs -> NP g xs -> NP h xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith
zipWith_POP :: (forall (a :: k). f a -> g a -> h a)
-> POP f xss -> POP g xss -> POP h xss
zipWith_POP = (forall (a :: k). f a -> g a -> h a)
-> POP f xss -> POP g xss -> POP h xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith

-- | Specialization of 'hzipWith3', which is equivalent to 'hliftA3'.
zipWith3_NP  :: SListI     xs  => (forall a. f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
-- | Specialization of 'hzipWith3', which is equivalent to 'hliftA3'.
zipWith3_POP :: All SListI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

zipWith3_NP :: (forall (a :: k). f a -> g a -> h a -> i a)
-> NP f xs -> NP g xs -> NP h xs -> NP i xs
zipWith3_NP  = (forall (a :: k). f a -> g a -> h a -> i a)
-> NP f xs -> NP g xs -> NP h xs -> NP i xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
hzipWith3
zipWith3_POP :: (forall (a :: k). f a -> g a -> h a -> i a)
-> POP f xss -> POP g xss -> POP h xss -> POP i xss
zipWith3_POP = (forall (a :: k). f a -> g a -> h a -> i a)
-> POP f xss -> POP g xss -> POP h xss -> POP i xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
hzipWith3

-- | Specialization of 'hcliftA'.
cliftA_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NP   f xs  -> NP  g xs
-- | Specialization of 'hcliftA'.
cliftA_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP  f xss -> POP g xss

cliftA_NP :: proxy c
-> (forall (a :: k). c a => f a -> g a) -> NP f xs -> NP g xs
cliftA_NP  = proxy c
-> (forall (a :: k). c a => f a -> g a) -> NP f xs -> NP g xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcliftA
cliftA_POP :: proxy c
-> (forall (a :: k). c a => f a -> g a) -> POP f xss -> POP g xss
cliftA_POP = proxy c
-> (forall (a :: k). c a => f a -> g a) -> POP f xss -> POP g xss
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcliftA

-- | Specialization of 'hcliftA2'.
cliftA2_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP  h xs
-- | Specialization of 'hcliftA2'.
cliftA2_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss

cliftA2_NP :: proxy c
-> (forall (a :: k). c a => f a -> g a -> h a)
-> NP f xs
-> NP g xs
-> NP h xs
cliftA2_NP  = proxy c
-> (forall (a :: k). c a => f a -> g a -> h a)
-> NP f xs
-> NP g xs
-> NP h xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hcliftA2
cliftA2_POP :: proxy c
-> (forall (a :: k). c a => f a -> g a -> h a)
-> POP f xss
-> POP g xss
-> POP h xss
cliftA2_POP = proxy c
-> (forall (a :: k). c a => f a -> g a -> h a)
-> POP f xss
-> POP g xss
-> POP h xss
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hcliftA2

-- | Specialization of 'hcliftA3'.
cliftA3_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
-- | Specialization of 'hcliftA3'.
cliftA3_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

cliftA3_NP :: 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_NP  = 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
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs
-> Prod h f' xs
-> h f'' xs
-> h f''' xs
hcliftA3
cliftA3_POP :: 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
cliftA3_POP = 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
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs
-> Prod h f' xs
-> h f'' xs
-> h f''' xs
hcliftA3

-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
cmap_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NP   f xs  -> NP  g xs
-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
cmap_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP  f xss -> POP g xss

cmap_NP :: proxy c
-> (forall (a :: k). c a => f a -> g a) -> NP f xs -> NP g xs
cmap_NP  = proxy c
-> (forall (a :: k). c a => f a -> g a) -> NP f xs -> NP g xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap
cmap_POP :: proxy c
-> (forall (a :: k). c a => f a -> g a) -> POP f xss -> POP g xss
cmap_POP = proxy c
-> (forall (a :: k). c a => f a -> g a) -> POP f xss -> POP g xss
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap

-- | Specialization of 'hczipWith', which is equivalent to 'hcliftA2'.
czipWith_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP  h xs
-- | Specialization of 'hczipWith', which is equivalent to 'hcliftA2'.
czipWith_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss

czipWith_NP :: proxy c
-> (forall (a :: k). c a => f a -> g a -> h a)
-> NP f xs
-> NP g xs
-> NP h xs
czipWith_NP  = proxy c
-> (forall (a :: k). c a => f a -> g a -> h a)
-> NP f xs
-> NP g xs
-> NP h xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hczipWith
czipWith_POP :: proxy c
-> (forall (a :: k). c a => f a -> g a -> h a)
-> POP f xss
-> POP g xss
-> POP h xss
czipWith_POP = proxy c
-> (forall (a :: k). c a => f a -> g a -> h a)
-> POP f xss
-> POP g xss
-> POP h xss
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hczipWith

-- | Specialization of 'hczipWith3', which is equivalent to 'hcliftA3'.
czipWith3_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
-- | Specialization of 'hczipWith3', which is equivalent to 'hcliftA3'.
czipWith3_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

czipWith3_NP :: 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_NP  = 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
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs
-> Prod h f' xs
-> h f'' xs
-> h f''' xs
hczipWith3
czipWith3_POP :: 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
czipWith3_POP = 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
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs
-> Prod h f' xs
-> h f'' xs
-> h f''' xs
hczipWith3

-- * Dealing with @'All' c@

-- | Lift a constrained function operating on a list-indexed structure
-- to a function on a list-of-list-indexed structure.
--
-- This is a variant of 'hcliftA'.
--
-- /Specification:/
--
-- @
-- 'hcliftA'' p f xs = 'hpure' ('fn_2' $ \\ 'AllDictC' -> f) \` 'hap' \` 'allDict_NP' p \` 'hap' \` xs
-- @
--
-- /Instances:/
--
-- @
-- 'hcliftA'' :: 'All2' c xss => proxy c -> (forall xs. 'All' c xs => f xs -> f' xs) -> 'NP' f xss -> 'NP' f' xss
-- 'hcliftA'' :: 'All2' c xss => proxy c -> (forall xs. 'All' c xs => f xs -> f' xs) -> 'Data.SOP.NS.NS' f xss -> 'Data.SOP.NS.NS' f' xss
-- @
--
{-# DEPRECATED hcliftA' "Use 'hcliftA' or 'hcmap' instead." #-}
hcliftA'  :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs)                                                       -> h f   xss -> h f'   xss

-- | Like 'hcliftA'', but for binary functions.
{-# DEPRECATED hcliftA2' "Use 'hcliftA2' or 'hczipWith' instead." #-}
hcliftA2' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs)            -> Prod h f xss                  -> h f'  xss -> h f''  xss

-- | Like 'hcliftA'', but for ternary functions.
{-# DEPRECATED hcliftA3' "Use 'hcliftA3' or 'hczipWith3' instead." #-}
hcliftA3' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. 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

hcliftA' :: proxy c
-> (forall (xs :: [k]). All c xs => f xs -> f' xs)
-> h f xss
-> h f' xss
hcliftA'  p :: proxy c
p = Proxy (All c)
-> (forall (xs :: [k]). All c xs => f xs -> f' xs)
-> h f xss
-> h f' xss
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcliftA  (proxy c -> Proxy (All c)
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint).
proxy c -> Proxy (All c)
allP proxy c
p)
hcliftA2' :: proxy c
-> (forall (xs :: [k]). All c xs => f xs -> f' xs -> f'' xs)
-> Prod h f xss
-> h f' xss
-> h f'' xss
hcliftA2' p :: proxy c
p = Proxy (All c)
-> (forall (xs :: [k]). All c xs => f xs -> f' xs -> f'' xs)
-> Prod h f xss
-> h f' xss
-> h f'' xss
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hcliftA2 (proxy c -> Proxy (All c)
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint).
proxy c -> Proxy (All c)
allP proxy c
p)
hcliftA3' :: 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
hcliftA3' p :: proxy c
p = Proxy (All 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
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a)
-> Prod h f xs
-> Prod h f' xs
-> h f'' xs
-> h f''' xs
hcliftA3 (proxy c -> Proxy (All c)
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint).
proxy c -> Proxy (All c)
allP proxy c
p)

-- | Specialization of 'hcliftA2''.
{-# DEPRECATED cliftA2'_NP "Use 'cliftA2_NP'  instead." #-}
cliftA2'_NP :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NP g xss -> NP h xss

cliftA2'_NP :: proxy c
-> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs)
-> NP f xss
-> NP g xss
-> NP h xss
cliftA2'_NP = proxy c
-> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs)
-> NP f xss
-> NP g xss
-> NP h xss
forall k (c :: k -> Constraint) (xss :: [[k]])
       (h :: ([k] -> *) -> [[k]] -> *) (proxy :: (k -> Constraint) -> *)
       (f :: [k] -> *) (f' :: [k] -> *) (f'' :: [k] -> *).
(All2 c xss, Prod h ~ NP, 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
hcliftA2'

-- * Collapsing

-- | Specialization of 'hcollapse'.
--
-- /Example:/
--
-- >>> collapse_NP (K 1 :* K 2 :* K 3 :* Nil)
-- [1,2,3]
--
collapse_NP  ::              NP  (K a) xs  ->  [a]

-- | Specialization of 'hcollapse'.
--
-- /Example:/
--
-- >>> collapse_POP (POP ((K 'a' :* Nil) :* (K 'b' :* K 'c' :* Nil) :* Nil) :: POP (K Char) '[ '[(a :: Type)], '[b, c] ])
-- ["a","bc"]
--
-- (The type signature is only necessary in this case to fix the kind of the type variables.)
--
collapse_POP :: SListI xss => POP (K a) xss -> [[a]]

collapse_NP :: NP (K a) xs -> [a]
collapse_NP Nil         = []
collapse_NP (K x :: a
x :* xs :: NP (K a) xs
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: NP (K a) xs -> [a]
forall k a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP NP (K a) xs
xs

collapse_POP :: POP (K a) xss -> [[a]]
collapse_POP = NP (K [a]) xss -> [[a]]
forall k a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP (NP (K [a]) xss -> [[a]])
-> (POP (K a) xss -> NP (K [a]) xss) -> POP (K a) xss -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: [k]). NP (K a) a -> K [a] a)
-> NP (NP (K a)) xss -> NP (K [a]) xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hliftA ([a] -> K [a] a
forall k a (b :: k). a -> K a b
K ([a] -> K [a] a) -> (NP (K a) a -> [a]) -> NP (K a) a -> K [a] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K a) a -> [a]
forall k a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP) (NP (NP (K a)) xss -> NP (K [a]) xss)
-> (POP (K a) xss -> NP (NP (K a)) xss)
-> POP (K a) xss
-> NP (K [a]) xss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. POP (K a) xss -> NP (NP (K a)) xss
forall k (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
unPOP

type instance CollapseTo NP  a = [a]
type instance CollapseTo POP a = [[a]]

instance HCollapse NP  where hcollapse :: NP (K a) xs -> CollapseTo NP a
hcollapse = NP (K a) xs -> CollapseTo NP a
forall k a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP
instance HCollapse POP where hcollapse :: POP (K a) xs -> CollapseTo POP a
hcollapse = POP (K a) xs -> CollapseTo POP a
forall k (xss :: [[k]]) a. SListI xss => POP (K a) xss -> [[a]]
collapse_POP

-- * Folding

-- | Specialization of 'hctraverse_'.
--
-- @since 0.3.2.0
--
ctraverse__NP ::
     forall c proxy xs f g. (All c xs, Applicative g)
  => proxy c -> (forall a. c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP _ f :: forall (a :: k). c a => f a -> g ()
f = NP f xs -> g ()
forall (ys :: [k]). All c ys => NP f ys -> g ()
go
  where
    go :: All c ys => NP f ys -> g ()
    go :: NP f ys -> g ()
go Nil       = () -> g ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    go (x :: f x
x :* xs :: NP f xs
xs) = f x -> g ()
forall (a :: k). c a => f a -> g ()
f f x
x g () -> g () -> g ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> NP f xs -> g ()
forall (ys :: [k]). All c ys => NP f ys -> g ()
go NP f xs
xs

-- | Specialization of 'htraverse_'.
--
-- @since 0.3.2.0
--
traverse__NP ::
     forall xs f g. (SListI xs, Applicative g)
  => (forall a. f a -> g ()) -> NP f xs -> g ()
traverse__NP :: (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
traverse__NP f :: forall (a :: k). f a -> g ()
f =
  Proxy Top
-> (forall (a :: k). Top a => f a -> g ()) -> NP f xs -> g ()
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP Proxy Top
forall k. Proxy Top
topP forall (a :: k). f a -> g ()
forall (a :: k). Top a => f a -> g ()
f
{-# INLINE traverse__NP #-}

-- | Specialization of 'hctraverse_'.
--
-- @since 0.3.2.0
--
ctraverse__POP ::
     forall c proxy xss f g. (All2 c xss, Applicative g)
  => proxy c -> (forall a. c a => f a -> g ()) -> POP f xss -> g ()
ctraverse__POP :: proxy c
-> (forall (a :: k). c a => f a -> g ()) -> POP f xss -> g ()
ctraverse__POP p :: proxy c
p f :: forall (a :: k). c a => f a -> g ()
f = Proxy (All c)
-> (forall (a :: [k]). All c a => NP f a -> g ())
-> NP (NP f) xss
-> g ()
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP (proxy c -> Proxy (All c)
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint).
proxy c -> Proxy (All c)
allP proxy c
p) (proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f a -> g ()
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP proxy c
p forall (a :: k). c a => f a -> g ()
f) (NP (NP f) xss -> g ())
-> (POP f xss -> NP (NP f) xss) -> POP f xss -> g ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. POP f xss -> NP (NP f) xss
forall k (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
unPOP

-- | Specialization of 'htraverse_'.
--
-- @since 0.3.2.0
--
traverse__POP ::
     forall xss f g. (SListI2 xss, Applicative g)
  => (forall a. f a -> g ()) -> POP f xss -> g ()
traverse__POP :: (forall (a :: k). f a -> g ()) -> POP f xss -> g ()
traverse__POP f :: forall (a :: k). f a -> g ()
f =
  Proxy Top
-> (forall (a :: k). Top a => f a -> g ()) -> POP f xss -> g ()
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
(All2 c xss, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g ()) -> POP f xss -> g ()
ctraverse__POP Proxy Top
forall k. Proxy Top
topP forall (a :: k). f a -> g ()
forall (a :: k). Top a => f a -> g ()
f
{-# INLINE traverse__POP #-}

instance HTraverse_ NP  where
  hctraverse_ :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
hctraverse_ = proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP
  htraverse_ :: (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
htraverse_  = (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
forall k (xs :: [k]) (f :: k -> *) (g :: * -> *).
(SListI xs, Applicative g) =>
(forall (a :: k). f a -> g ()) -> NP f xs -> g ()
traverse__NP

instance HTraverse_ POP where
  hctraverse_ :: proxy c
-> (forall (a :: k). c a => f a -> g ()) -> POP f xs -> g ()
hctraverse_ = proxy c
-> (forall (a :: k). c a => f a -> g ()) -> POP f xs -> g ()
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
(All2 c xss, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g ()) -> POP f xss -> g ()
ctraverse__POP
  htraverse_ :: (forall (a :: k). f a -> g ()) -> POP f xs -> g ()
htraverse_  = (forall (a :: k). f a -> g ()) -> POP f xs -> g ()
forall k (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
(SListI2 xss, Applicative g) =>
(forall (a :: k). f a -> g ()) -> POP f xss -> g ()
traverse__POP

-- | Specialization of 'hcfoldMap'.
--
-- @since 0.3.2.0
--
cfoldMap_NP :: (All c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> NP f xs -> m
cfoldMap_NP :: proxy c -> (forall (a :: k). c a => f a -> m) -> NP f xs -> m
cfoldMap_NP  = proxy c -> (forall (a :: k). c a => f a -> m) -> NP f xs -> m
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) m (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HTraverse_ h, AllN h c xs, Monoid m) =>
proxy c -> (forall (a :: k). c a => f a -> m) -> h f xs -> m
hcfoldMap

-- | Specialization of 'hcfoldMap'.
--
-- @since 0.3.2.0
--
cfoldMap_POP :: (All2 c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> POP f xs -> m
cfoldMap_POP :: proxy c -> (forall (a :: k). c a => f a -> m) -> POP f xs -> m
cfoldMap_POP = proxy c -> (forall (a :: k). c a => f a -> m) -> POP f xs -> m
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) m (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HTraverse_ h, AllN h c xs, Monoid m) =>
proxy c -> (forall (a :: k). c a => f a -> m) -> h f xs -> m
hcfoldMap

-- * Sequencing

-- | Specialization of 'hsequence''.
sequence'_NP  ::              Applicative f  => NP  (f :.: g) xs  -> f (NP  g xs)
sequence'_NP :: NP (f :.: g) xs -> f (NP g xs)
sequence'_NP Nil         = NP g '[] -> f (NP g '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure NP g '[]
forall k (f :: k -> *). NP f '[]
Nil
sequence'_NP (mx :: (:.:) f g x
mx :* mxs :: NP (f :.: g) xs
mxs) = g x -> NP g xs -> NP g (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
(:*) (g x -> NP g xs -> NP g (x : xs))
-> f (g x) -> f (NP g xs -> NP g (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (:.:) f g x -> f (g x)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp (:.:) f g x
mx f (NP g xs -> NP g (x : xs)) -> f (NP g xs) -> f (NP g (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NP (f :.: g) xs -> f (NP g xs)
forall k (f :: * -> *) (g :: k -> *) (xs :: [k]).
Applicative f =>
NP (f :.: g) xs -> f (NP g xs)
sequence'_NP NP (f :.: g) xs
mxs

-- | Specialization of 'hsequence''.
sequence'_POP :: (SListI xss, Applicative f) => POP (f :.: g) xss -> f (POP g xss)
sequence'_POP :: POP (f :.: g) xss -> f (POP g xss)
sequence'_POP = (NP (NP g) xss -> POP g xss) -> f (NP (NP g) xss) -> f (POP g xss)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NP (NP g) xss -> POP g xss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP (f (NP (NP g) xss) -> f (POP g xss))
-> (POP (f :.: g) xss -> f (NP (NP g) xss))
-> POP (f :.: g) xss
-> f (POP g xss)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (f :.: NP g) xss -> f (NP (NP g) xss)
forall k (f :: * -> *) (g :: k -> *) (xs :: [k]).
Applicative f =>
NP (f :.: g) xs -> f (NP g xs)
sequence'_NP (NP (f :.: NP g) xss -> f (NP (NP g) xss))
-> (POP (f :.: g) xss -> NP (f :.: NP g) xss)
-> POP (f :.: g) xss
-> f (NP (NP g) xss)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: [k]). NP (f :.: g) a -> (:.:) f (NP g) a)
-> NP (NP (f :.: g)) xss -> NP (f :.: NP g) xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hliftA (f (NP g a) -> (:.:) f (NP g) a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (f (NP g a) -> (:.:) f (NP g) a)
-> (NP (f :.: g) a -> f (NP g a))
-> NP (f :.: g) a
-> (:.:) f (NP g) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (f :.: g) a -> f (NP g a)
forall k (f :: * -> *) (g :: k -> *) (xs :: [k]).
Applicative f =>
NP (f :.: g) xs -> f (NP g xs)
sequence'_NP) (NP (NP (f :.: g)) xss -> NP (f :.: NP g) xss)
-> (POP (f :.: g) xss -> NP (NP (f :.: g)) xss)
-> POP (f :.: g) xss
-> NP (f :.: NP g) xss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. POP (f :.: g) xss -> NP (NP (f :.: g)) xss
forall k (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
unPOP

-- | Specialization of 'hctraverse''.
--
-- @since 0.3.2.0
--
ctraverse'_NP  ::
     forall c proxy xs f f' g. (All c xs,  Applicative g)
  => proxy c -> (forall a. c a => f a -> g (f' a)) -> NP f xs  -> g (NP f' xs)
ctraverse'_NP :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
ctraverse'_NP _ f :: forall (a :: k). c a => f a -> g (f' a)
f = NP f xs -> g (NP f' xs)
forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
go where
  go :: All c ys => NP f ys -> g (NP f' ys)
  go :: NP f ys -> g (NP f' ys)
go Nil       = NP f' '[] -> g (NP f' '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure NP f' '[]
forall k (f :: k -> *). NP f '[]
Nil
  go (x :: f x
x :* xs :: NP f xs
xs) = f' x -> NP f' xs -> NP f' (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
(:*) (f' x -> NP f' xs -> NP f' (x : xs))
-> g (f' x) -> g (NP f' xs -> NP f' (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> g (f' x)
forall (a :: k). c a => f a -> g (f' a)
f f x
x g (NP f' xs -> NP f' (x : xs))
-> g (NP f' xs) -> g (NP f' (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NP f xs -> g (NP f' xs)
forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
go NP f xs
xs

-- | Specialization of 'htraverse''.
--
-- @since 0.3.2.0
--
traverse'_NP  ::
     forall xs f f' g. (SListI xs,  Applicative g)
  => (forall a. f a -> g (f' a)) -> NP f xs  -> g (NP f' xs)
traverse'_NP :: (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
traverse'_NP f :: forall (a :: k). f a -> g (f' a)
f =
  Proxy Top
-> (forall (a :: k). Top a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (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'_NP Proxy Top
forall k. Proxy Top
topP forall (a :: k). f a -> g (f' a)
forall (a :: k). Top a => f a -> g (f' a)
f
{-# INLINE traverse'_NP #-}

-- | Specialization of 'hctraverse''.
--
-- @since 0.3.2.0
--
ctraverse'_POP :: (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> POP f xss -> g (POP f' xss)
ctraverse'_POP :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> POP f xss
-> g (POP f' xss)
ctraverse'_POP p :: proxy c
p f :: forall (a :: k). c a => f a -> g (f' a)
f = (NP (NP f') xss -> POP f' xss)
-> g (NP (NP f') xss) -> g (POP f' xss)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NP (NP f') xss -> POP f' xss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP (g (NP (NP f') xss) -> g (POP f' xss))
-> (POP f xss -> g (NP (NP f') xss)) -> POP f xss -> g (POP f' xss)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (All c)
-> (forall (a :: [k]). All c a => NP f a -> g (NP f' a))
-> NP (NP f) xss
-> g (NP (NP f') xss)
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (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'_NP (proxy c -> Proxy (All c)
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint).
proxy c -> Proxy (All c)
allP proxy c
p) (proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f a
-> g (NP f' a)
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (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'_NP proxy c
p forall (a :: k). c a => f a -> g (f' a)
f) (NP (NP f) xss -> g (NP (NP f') xss))
-> (POP f xss -> NP (NP f) xss) -> POP f xss -> g (NP (NP f') xss)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. POP f xss -> NP (NP f) xss
forall k (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
unPOP

-- | Specialization of 'hctraverse''.
--
-- @since 0.3.2.0
--
traverse'_POP :: (SListI2 xss, Applicative g) => (forall a. f a -> g (f' a)) -> POP f xss -> g (POP f' xss)
traverse'_POP :: (forall (a :: k). f a -> g (f' a)) -> POP f xss -> g (POP f' xss)
traverse'_POP f :: forall (a :: k). f a -> g (f' a)
f =
  Proxy Top
-> (forall (a :: k). Top a => f a -> g (f' a))
-> POP f xss
-> g (POP f' xss)
forall k (c :: k -> Constraint) (xss :: [[k]]) (g :: * -> *)
       (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
(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'_POP Proxy Top
forall k. Proxy Top
topP forall (a :: k). f a -> g (f' a)
forall (a :: k). Top a => f a -> g (f' a)
f
{-# INLINE traverse'_POP #-}

instance HSequence NP  where
  hsequence' :: NP (f :.: g) xs -> f (NP g xs)
hsequence'  = NP (f :.: g) xs -> f (NP g xs)
forall k (f :: * -> *) (g :: k -> *) (xs :: [k]).
Applicative f =>
NP (f :.: g) xs -> f (NP g xs)
sequence'_NP
  hctraverse' :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
hctraverse' = proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (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'_NP
  htraverse' :: (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
htraverse'  = (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
forall k (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
(SListI xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
traverse'_NP

instance HSequence POP where
  hsequence' :: POP (f :.: g) xs -> f (POP g xs)
hsequence'  = POP (f :.: g) xs -> f (POP g xs)
forall k (xss :: [[k]]) (f :: * -> *) (g :: k -> *).
(SListI xss, Applicative f) =>
POP (f :.: g) xss -> f (POP g xss)
sequence'_POP
  hctraverse' :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> POP f xs
-> g (POP f' xs)
hctraverse' = proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> POP f xs
-> g (POP f' xs)
forall k (c :: k -> Constraint) (xss :: [[k]]) (g :: * -> *)
       (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
(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'_POP
  htraverse' :: (forall (a :: k). f a -> g (f' a)) -> POP f xs -> g (POP f' xs)
htraverse'  = (forall (a :: k). f a -> g (f' a)) -> POP f xs -> g (POP f' xs)
forall k (xss :: [[k]]) (g :: * -> *) (f :: k -> *) (f' :: k -> *).
(SListI2 xss, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> POP f xss -> g (POP f' xss)
traverse'_POP

-- | Specialization of 'hsequence'.
--
-- /Example:/
--
-- >>> sequence_NP (Just 1 :* Just 2 :* Nil)
-- Just (I 1 :* I 2 :* Nil)
--
sequence_NP  :: (SListI xs,  Applicative f) => NP  f xs  -> f (NP  I xs)

-- | Specialization of 'hsequence'.
--
-- /Example:/
--
-- >>> sequence_POP (POP ((Just 1 :* Nil) :* (Just 2 :* Just 3 :* Nil) :* Nil))
-- Just (POP ((I 1 :* Nil) :* (I 2 :* I 3 :* Nil) :* Nil))
--
sequence_POP :: (All SListI xss, Applicative f) => POP f xss -> f (POP I xss)

sequence_NP :: NP f xs -> f (NP I xs)
sequence_NP   = NP f xs -> f (NP I xs)
forall l (h :: (* -> *) -> l -> *) (xs :: l) (f :: * -> *).
(SListIN h xs, SListIN (Prod h) xs, HSequence h, Applicative f) =>
h f xs -> f (h I xs)
hsequence
sequence_POP :: POP f xss -> f (POP I xss)
sequence_POP  = POP f xss -> f (POP I xss)
forall l (h :: (* -> *) -> l -> *) (xs :: l) (f :: * -> *).
(SListIN h xs, SListIN (Prod h) xs, HSequence h, Applicative f) =>
h f xs -> f (h I xs)
hsequence

-- | Specialization of 'hctraverse'.
--
-- @since 0.3.2.0
--
ctraverse_NP  :: (All  c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> NP  f xs -> g (NP  I xs)

-- | Specialization of 'hctraverse'.
--
-- @since 0.3.2.0
--
ctraverse_POP :: (All2 c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)

ctraverse_NP :: proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs)
ctraverse_NP  = proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs)
forall l (h :: (* -> *) -> l -> *) (c :: * -> Constraint) (xs :: l)
       (g :: * -> *) (proxy :: (* -> Constraint) -> *) (f :: * -> *).
(HSequence h, AllN h c xs, Applicative g) =>
proxy c -> (forall a. c a => f a -> g a) -> h f xs -> g (h I xs)
hctraverse
ctraverse_POP :: proxy c
-> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)
ctraverse_POP = proxy c
-> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)
forall l (h :: (* -> *) -> l -> *) (c :: * -> Constraint) (xs :: l)
       (g :: * -> *) (proxy :: (* -> Constraint) -> *) (f :: * -> *).
(HSequence h, AllN h c xs, Applicative g) =>
proxy c -> (forall a. c a => f a -> g a) -> h f xs -> g (h I xs)
hctraverse

-- * Catamorphism and anamorphism

-- | Catamorphism for 'NP'.
--
-- This is a suitable generalization of 'foldr'. It takes
-- parameters on what to do for 'Nil' and ':*'. Since the
-- input list is heterogeneous, the result is also indexed
-- by a type-level list.
--
-- @since 0.2.3.0
--
cata_NP ::
     forall r f xs .
     r '[]
  -> (forall y ys . f y -> r ys -> r (y ': ys))
  -> NP f xs
  -> r xs
cata_NP :: r '[]
-> (forall (y :: k) (ys :: [k]). f y -> r ys -> r (y : ys))
-> NP f xs
-> r xs
cata_NP nil :: r '[]
nil cons :: forall (y :: k) (ys :: [k]). f y -> r ys -> r (y : ys)
cons = NP f xs -> r xs
forall (ys :: [k]). NP f ys -> r ys
go
  where
    go :: forall ys . NP f ys -> r ys
    go :: NP f ys -> r ys
go Nil       = r ys
r '[]
nil
    go (x :: f x
x :* xs :: NP f xs
xs) = f x -> r xs -> r (x : xs)
forall (y :: k) (ys :: [k]). f y -> r ys -> r (y : ys)
cons f x
x (NP f xs -> r xs
forall (ys :: [k]). NP f ys -> r ys
go NP f xs
xs)

-- | Constrained catamorphism for 'NP'.
--
-- The difference compared to 'cata_NP' is that the function
-- for the cons-case can make use of the fact that the specified
-- constraint holds for all the types in the signature of the
-- product.
--
-- @since 0.2.3.0
--
ccata_NP ::
     forall c proxy r f xs . (All c xs)
  => proxy c
  -> r '[]
  -> (forall y ys . c y => f y -> r ys -> r (y ': ys))
  -> NP f xs
  -> r xs
ccata_NP :: proxy c
-> r '[]
-> (forall (y :: k) (ys :: [k]). c y => f y -> r ys -> r (y : ys))
-> NP f xs
-> r xs
ccata_NP _ nil :: r '[]
nil cons :: forall (y :: k) (ys :: [k]). c y => f y -> r ys -> r (y : ys)
cons = NP f xs -> r xs
forall (ys :: [k]). All c ys => NP f ys -> r ys
go
  where
    go :: forall ys . (All c ys) => NP f ys -> r ys
    go :: NP f ys -> r ys
go Nil       = r ys
r '[]
nil
    go (x :: f x
x :* xs :: NP f xs
xs) = f x -> r xs -> r (x : xs)
forall (y :: k) (ys :: [k]). c y => f y -> r ys -> r (y : ys)
cons f x
x (NP f xs -> r xs
forall (ys :: [k]). All c ys => NP f ys -> r ys
go NP f xs
xs)

-- | Anamorphism for 'NP'.
--
-- In contrast to the anamorphism for normal lists, the
-- generating function does not return an 'Either', but
-- simply an element and a new seed value.
--
-- This is because the decision on whether to generate a
-- 'Nil' or a ':*' is determined by the types.
--
-- @since 0.2.3.0
--
ana_NP ::
     forall s f xs .
     SListI xs
  => (forall y ys . s (y ': ys) -> (f y, s ys))
  -> s xs
  -> NP f xs
ana_NP :: (forall (y :: k) (ys :: [k]). s (y : ys) -> (f y, s ys))
-> s xs -> NP f xs
ana_NP uncons :: forall (y :: k) (ys :: [k]). s (y : ys) -> (f y, s ys)
uncons =
  Proxy Top
-> (forall (y :: k) (ys :: [k]).
    Top y =>
    s (y : ys) -> (f y, s ys))
-> s xs
-> NP f xs
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (s :: [k] -> *) (f :: k -> *) (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
cana_NP Proxy Top
forall k. Proxy Top
topP forall (y :: k) (ys :: [k]). s (y : ys) -> (f y, s ys)
forall (y :: k) (ys :: [k]). Top y => s (y : ys) -> (f y, s ys)
uncons
{-# INLINE ana_NP #-}

-- | Constrained anamorphism for 'NP'.
--
-- Compared to 'ana_NP', the generating function can
-- make use of the specified constraint here for the
-- elements that it generates.
--
-- @since 0.2.3.0
--
cana_NP ::
     forall c proxy s f xs . (All c xs)
  => proxy c
  -> (forall y ys . c y => s (y ': ys) -> (f y, s ys))
  -> s xs
  -> NP f xs
cana_NP :: proxy c
-> (forall (y :: k) (ys :: [k]). c y => s (y : ys) -> (f y, s ys))
-> s xs
-> NP f xs
cana_NP _ uncons :: forall (y :: k) (ys :: [k]). c y => s (y : ys) -> (f y, s ys)
uncons = SList xs -> s xs -> NP f xs
forall (ys :: [k]). All c ys => SList ys -> s ys -> NP f ys
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: forall ys . (All c ys) => SList ys -> s ys -> NP f ys
    go :: SList ys -> s ys -> NP f ys
go SNil  _ = NP f ys
forall k (f :: k -> *). NP f '[]
Nil
    go SCons s :: s ys
s = case s (x : xs) -> (f x, s xs)
forall (y :: k) (ys :: [k]). c y => s (y : ys) -> (f y, s ys)
uncons s ys
s (x : xs)
s of
      (x :: f x
x, s' :: s xs
s') -> f x
x f x -> NP f xs -> NP f (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* SList xs -> s xs -> NP f xs
forall (ys :: [k]). All c ys => SList ys -> s ys -> NP f ys
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList s xs
s'

-- | Specialization of 'htrans'.
--
-- @since 0.3.1.0
--
trans_NP ::
     AllZip c xs ys
  => proxy c
  -> (forall x y . c x y => f x -> g y)
  -> NP f xs -> NP g ys
trans_NP :: proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP _ _t :: forall (x :: k) (y :: k). c x y => f x -> g y
_t Nil       = NP g ys
forall k (f :: k -> *). NP f '[]
Nil
trans_NP p :: proxy c
p  t :: forall (x :: k) (y :: k). c x y => f x -> g y
t (x :: f x
x :* xs :: NP f xs
xs) = f x -> g (Head ys)
forall (x :: k) (y :: k). c x y => f x -> g y
t f x
x g (Head ys) -> NP g (Tail ys) -> NP g (Head ys : Tail ys)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g (Tail ys)
forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP proxy c
p forall (x :: k) (y :: k). c x y => f x -> g y
t NP f xs
xs

-- | Specialization of 'htrans'.
--
-- @since 0.3.1.0
--
trans_POP ::
     AllZip2 c xss yss
  => proxy c
  -> (forall x y . c x y => f x -> g y)
  -> POP f xss -> POP g yss
trans_POP :: proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> POP f xss
-> POP g yss
trans_POP p :: proxy c
p t :: forall (x :: k) (y :: k). c x y => f x -> g y
t =
  NP (NP g) yss -> POP g yss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP (NP (NP g) yss -> POP g yss)
-> (POP f xss -> NP (NP g) yss) -> POP f xss -> POP g yss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (AllZip c)
-> (forall (x :: [k]) (y :: [k]). AllZip c x y => NP f x -> NP g y)
-> NP (NP f) xss
-> NP (NP g) yss
forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP (proxy c -> Proxy (AllZip c)
forall a b (proxy :: (a -> b -> Constraint) -> *)
       (c :: a -> b -> Constraint).
proxy c -> Proxy (AllZip c)
allZipP proxy c
p) (proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f x
-> NP g y
forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP proxy c
p forall (x :: k) (y :: k). c x y => f x -> g y
t) (NP (NP f) xss -> NP (NP g) yss)
-> (POP f xss -> NP (NP f) xss) -> POP f xss -> NP (NP g) yss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. POP f xss -> NP (NP f) xss
forall k (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
unPOP

allZipP :: proxy c -> Proxy (AllZip c)
allZipP :: proxy c -> Proxy (AllZip c)
allZipP _ = Proxy (AllZip c)
forall k (t :: k). Proxy t
Proxy

-- | Specialization of 'hcoerce'.
--
-- @since 0.3.1.0
--
coerce_NP ::
     forall f g xs ys .
     AllZip (LiftedCoercible f g) xs ys
  => NP f xs -> NP g ys
coerce_NP :: NP f xs -> NP g ys
coerce_NP =
  NP f xs -> NP g ys
forall a b. a -> b
unsafeCoerce

-- | Safe version of 'coerce_NP'.
--
-- For documentation purposes only; not exported.
--
_safe_coerce_NP ::
     forall f g xs ys .
     AllZip (LiftedCoercible f g) xs ys
  => NP f xs -> NP g ys
_safe_coerce_NP :: NP f xs -> NP g ys
_safe_coerce_NP =
  Proxy (LiftedCoercible f g)
-> (forall (x :: k) (y :: k).
    LiftedCoercible f g x y =>
    f x -> g y)
-> NP f xs
-> NP g ys
forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP (Proxy (LiftedCoercible f g)
forall k (t :: k). Proxy t
Proxy :: Proxy (LiftedCoercible f g)) forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y
forall a b. Coercible a b => a -> b
coerce

-- | Specialization of 'hcoerce'.
--
-- @since 0.3.1.0
--
coerce_POP ::
     forall f g xss yss .
     AllZip2 (LiftedCoercible f g) xss yss
  => POP f xss -> POP g yss
coerce_POP :: POP f xss -> POP g yss
coerce_POP =
  POP f xss -> POP g yss
forall a b. a -> b
unsafeCoerce

-- | Safe version of 'coerce_POP'.
--
-- For documentation purposes only; not exported.
--
_safe_coerce_POP ::
     forall f g xss yss .
     AllZip2 (LiftedCoercible f g) xss yss
  => POP f xss -> POP g yss
_safe_coerce_POP :: POP f xss -> POP g yss
_safe_coerce_POP =
  Proxy (LiftedCoercible f g)
-> (forall (x :: k) (y :: k).
    LiftedCoercible f g x y =>
    f x -> g y)
-> POP f xss
-> POP g yss
forall k k (c :: k -> k -> Constraint) (xss :: [[k]])
       (yss :: [[k]]) (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *)
       (g :: k -> *).
AllZip2 c xss yss =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> POP f xss
-> POP g yss
trans_POP (Proxy (LiftedCoercible f g)
forall k (t :: k). Proxy t
Proxy :: Proxy (LiftedCoercible f g)) forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y
forall a b. Coercible a b => a -> b
coerce

-- | Specialization of 'hfromI'.
--
-- @since 0.3.1.0
--
fromI_NP ::
     forall f xs ys .
     AllZip (LiftedCoercible I f) xs ys
  => NP I xs -> NP f ys
fromI_NP :: NP I xs -> NP f ys
fromI_NP = NP I xs -> NP f ys
forall l1 k2 l2 (h1 :: (* -> *) -> l1 -> *) (f :: k2 -> *)
       (xs :: l1) (ys :: l2) (h2 :: (k2 -> *) -> l2 -> *).
(AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2) =>
h1 I xs -> h2 f ys
hfromI

-- | Specialization of 'htoI'.
--
-- @since 0.3.1.0
--
toI_NP ::
     forall f xs ys .
     AllZip (LiftedCoercible f I) xs ys
  => NP f xs -> NP I ys
toI_NP :: NP f xs -> NP I ys
toI_NP = NP f xs -> NP I ys
forall k1 l1 l2 (h1 :: (k1 -> *) -> l1 -> *) (f :: k1 -> *)
       (xs :: l1) (ys :: l2) (h2 :: (* -> *) -> l2 -> *).
(AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2) =>
h1 f xs -> h2 I ys
htoI

-- | Specialization of 'hfromI'.
--
-- @since 0.3.1.0
--
fromI_POP ::
     forall f xss yss .
     AllZip2 (LiftedCoercible I f) xss yss
  => POP I xss -> POP f yss
fromI_POP :: POP I xss -> POP f yss
fromI_POP = POP I xss -> POP f yss
forall l1 k2 l2 (h1 :: (* -> *) -> l1 -> *) (f :: k2 -> *)
       (xs :: l1) (ys :: l2) (h2 :: (k2 -> *) -> l2 -> *).
(AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2) =>
h1 I xs -> h2 f ys
hfromI

-- | Specialization of 'htoI'.
--
-- @since 0.3.1.0
--
toI_POP ::
     forall f xss yss .
     AllZip2 (LiftedCoercible f I) xss yss
  => POP f xss -> POP I yss
toI_POP :: POP f xss -> POP I yss
toI_POP = POP f xss -> POP I yss
forall k1 l1 l2 (h1 :: (k1 -> *) -> l1 -> *) (f :: k1 -> *)
       (xs :: l1) (ys :: l2) (h2 :: (* -> *) -> l2 -> *).
(AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2) =>
h1 f xs -> h2 I ys
htoI

instance HTrans NP NP where
  htrans :: proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NP f xs
-> NP g ys
htrans  = proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NP f xs
-> NP g ys
forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP
  hcoerce :: NP f xs -> NP g ys
hcoerce = NP f xs -> NP g ys
forall k k (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
AllZip (LiftedCoercible f g) xs ys =>
NP f xs -> NP g ys
coerce_NP
instance HTrans POP POP where
  htrans :: proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> POP f xs
-> POP g ys
htrans  = proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> POP f xs
-> POP g ys
forall k k (c :: k -> k -> Constraint) (xss :: [[k]])
       (yss :: [[k]]) (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *)
       (g :: k -> *).
AllZip2 c xss yss =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> POP f xss
-> POP g yss
trans_POP
  hcoerce :: POP f xs -> POP g ys
hcoerce = POP f xs -> POP g ys
forall k k (f :: k -> *) (g :: k -> *) (xss :: [[k]])
       (yss :: [[k]]).
AllZip2 (LiftedCoercible f g) xss yss =>
POP f xss -> POP g yss
coerce_POP