{-# 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