{-# LANGUAGE BangPatterns #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-deprecations #-} -- | n-ary sums (and sums of products) module Data.SOP.NS ( -- * Datatypes NS(..) , SOP(..) , unSOP -- * Constructing sums , Injection , injections , shift , shiftInjection , apInjs_NP , apInjs'_NP , apInjs_POP , apInjs'_POP -- * Destructing sums , unZ , index_NS , index_SOP , Ejection , ejections , shiftEjection -- * Application , ap_NS , ap_SOP -- * Lifting / mapping , liftA_NS , liftA_SOP , liftA2_NS , liftA2_SOP , cliftA_NS , cliftA_SOP , cliftA2_NS , cliftA2_SOP , map_NS , map_SOP , cmap_NS , cmap_SOP -- * Dealing with @'All' c@ , cliftA2'_NS -- * Comparison , compare_NS , ccompare_NS , compare_SOP , ccompare_SOP -- * Collapsing , collapse_NS , collapse_SOP -- * Folding and sequencing , ctraverse__NS , ctraverse__SOP , traverse__NS , traverse__SOP , cfoldMap_NS , cfoldMap_SOP , sequence'_NS , sequence'_SOP , sequence_NS , sequence_SOP , ctraverse'_NS , ctraverse'_SOP , traverse'_NS , traverse'_SOP , ctraverse_NS , ctraverse_SOP -- * Catamorphism and anamorphism , cata_NS , ccata_NS , ana_NS , cana_NS -- * Expanding sums to products , expand_NS , cexpand_NS , expand_SOP , cexpand_SOP -- * Transformation of index lists and coercions , trans_NS , trans_SOP , coerce_NS , coerce_SOP , fromI_NS , fromI_SOP , toI_NS , toI_SOP ) where import Data.Coerce import Data.Kind (Type) import Data.Proxy (Proxy (..)) import Unsafe.Coerce import Control.DeepSeq (NFData(..)) import Data.SOP.BasicFunctors import Data.SOP.Classes import Data.SOP.Constraint import Data.SOP.NP import Data.SOP.Sing -- * Datatypes -- | An n-ary sum. -- -- The sum is parameterized by a type constructor @f@ and -- indexed by a type-level list @xs@. The length of the list -- determines the number of choices in the sum and if the -- @i@-th element of the list is of type @x@, then the @i@-th -- choice of the sum is of type @f x@. -- -- The constructor names are chosen to resemble Peano-style -- natural numbers, i.e., 'Z' is for "zero", and 'S' is for -- "successor". Chaining 'S' and 'Z' chooses the corresponding -- component of the sum. -- -- /Examples:/ -- -- > Z :: f x -> NS f (x ': xs) -- > S . Z :: f y -> NS f (x ': y ': xs) -- > S . S . Z :: f z -> NS f (x ': y ': z ': xs) -- > ... -- -- Note that empty sums (indexed by an empty list) have no -- non-bottom elements. -- -- Two common instantiations of @f@ are the identity functor 'I' -- and the constant functor 'K'. For 'I', the sum becomes a -- direct generalization of the 'Either' type to arbitrarily many -- choices. For @'K' a@, the result is a homogeneous choice type, -- where the contents of the type-level list are ignored, but its -- length specifies the number of options. -- -- In the context of the SOP approach to generic programming, an -- n-ary sum describes the top-level structure of a datatype, -- which is a choice between all of its constructors. -- -- /Examples:/ -- -- > Z (I 'x') :: NS I '[ Char, Bool ] -- > S (Z (I True)) :: NS I '[ Char, Bool ] -- > S (Z (K 1)) :: NS (K Int) '[ Char, Bool ] -- data NS :: (k -> Type) -> [k] -> Type where Z :: f x -> NS f (x ': xs) S :: NS f xs -> NS f (x ': xs) deriving instance All (Show `Compose` f) xs => Show (NS f xs) deriving instance All (Eq `Compose` f) xs => Eq (NS f xs) deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs) -- | @since 0.2.5.0 instance All (NFData `Compose` f) xs => NFData (NS f xs) where rnf :: NS f xs -> () rnf (Z x :: f x x) = f x -> () forall a. NFData a => a -> () rnf f x x rnf (S xs :: NS f xs xs) = NS f xs -> () forall a. NFData a => a -> () rnf NS f xs xs -- | The type of ejections from an n-ary sum. -- -- An ejection is the pattern matching function for one part of the n-ary sum. -- -- It is the opposite of an 'Injection'. -- -- @since 0.5.0.0 -- type Ejection (f :: k -> Type) (xs :: [k]) = K (NS f xs) -.-> Maybe :.: f -- | Compute all ejections from an n-ary sum. -- -- Each element of the resulting product contains one of the ejections. -- -- @since 0.5.0.0 -- ejections :: forall xs f . SListI xs => NP (Ejection f xs) xs ejections :: NP (Ejection f xs) xs ejections = case SList xs forall k (xs :: [k]). SListI xs => SList xs sList :: SList xs of SNil -> NP (Ejection f xs) xs forall k (f :: k -> *). NP f '[] Nil SCons -> (K (NS f xs) x -> (:.:) Maybe f x) -> (-.->) (K (NS f xs)) (Maybe :.: f) x forall k (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn (Maybe (f x) -> (:.:) Maybe f x forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp (Maybe (f x) -> (:.:) Maybe f x) -> (K (NS f xs) x -> Maybe (f x)) -> K (NS f xs) x -> (:.:) Maybe f x forall b c a. (b -> c) -> (a -> b) -> a -> c . (\ns :: NS f xs ns -> case NS f xs ns of Z fx :: f x fx -> f x -> Maybe (f x) forall a. a -> Maybe a Just f x fx; S _ -> Maybe (f x) forall a. Maybe a Nothing) (NS f xs -> Maybe (f x)) -> (K (NS f xs) x -> NS f xs) -> K (NS f xs) x -> Maybe (f x) forall b c a. (b -> c) -> (a -> b) -> a -> c . K (NS f xs) x -> NS f xs forall k a (b :: k). K a b -> a unK) (-.->) (K (NS f xs)) (Maybe :.: f) x -> NP (Ejection f xs) xs -> NP (Ejection f xs) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* (forall (a :: k). Ejection f xs a -> (-.->) (K (NS f xs)) (Maybe :.: f) a) -> NP (Ejection f xs) xs -> NP (Ejection f xs) 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). Ejection f xs a -> (-.->) (K (NS f xs)) (Maybe :.: f) a forall a (f :: a -> *) (x :: a) (xs :: [a]) (a :: a). Ejection f xs a -> Ejection f (x : xs) a shiftEjection NP (Ejection f xs) xs forall k (xs :: [k]) (f :: k -> *). SListI xs => NP (Ejection f xs) xs ejections -- | -- @since 0.5.0.0 -- shiftEjection :: forall f x xs a . Ejection f xs a -> Ejection f (x ': xs) a shiftEjection :: Ejection f xs a -> Ejection f (x : xs) a shiftEjection (Fn f :: K (NS f xs) a -> (:.:) Maybe f a f) = (K (NS f (x : xs)) a -> (:.:) Maybe f a) -> Ejection f (x : xs) a forall k (f :: k -> *) (g :: k -> *) (a :: k). (f a -> g a) -> (-.->) f g a Fn ((K (NS f (x : xs)) a -> (:.:) Maybe f a) -> Ejection f (x : xs) a) -> (K (NS f (x : xs)) a -> (:.:) Maybe f a) -> Ejection f (x : xs) a forall a b. (a -> b) -> a -> b $ (\ns :: NS f (x : xs) ns -> case NS f (x : xs) ns of Z _ -> Maybe (f a) -> (:.:) Maybe f a forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp Maybe (f a) forall a. Maybe a Nothing; S s :: NS f xs s -> K (NS f xs) a -> (:.:) Maybe f a f (NS f xs -> K (NS f xs) a forall k a (b :: k). a -> K a b K NS f xs s)) (NS f (x : xs) -> (:.:) Maybe f a) -> (K (NS f (x : xs)) a -> NS f (x : xs)) -> K (NS f (x : xs)) a -> (:.:) Maybe f a forall b c a. (b -> c) -> (a -> b) -> a -> c . K (NS f (x : xs)) a -> NS f (x : xs) forall k a (b :: k). K a b -> a unK -- | Extract the payload from a unary sum. -- -- For larger sums, this function would be partial, so it is only -- provided with a rather restrictive type. -- -- /Example:/ -- -- >>> unZ (Z (I 'x')) -- I 'x' -- -- @since 0.2.2.0 -- unZ :: NS f '[x] -> f x unZ :: NS f '[x] -> f x unZ (Z x :: f x x) = f x f x x unZ (S x :: NS f xs x) = case NS f xs x of {} -- | Obtain the index from an n-ary sum. -- -- An n-nary sum represents a choice between n different options. -- This function returns an integer between 0 and n - 1 indicating -- the option chosen by the given value. -- -- /Examples:/ -- -- >>> index_NS (S (S (Z (I False)))) -- 2 -- >>> index_NS (Z (K ())) -- 0 -- -- @since 0.2.4.0 -- index_NS :: forall f xs . NS f xs -> Int index_NS :: NS f xs -> Int index_NS = Int -> NS f xs -> Int forall (ys :: [k]). Int -> NS f ys -> Int go 0 where go :: forall ys . Int -> NS f ys -> Int go :: Int -> NS f ys -> Int go !Int acc (Z _) = Int acc go !Int acc (S x :: NS f xs x) = Int -> NS f xs -> Int forall (ys :: [k]). Int -> NS f ys -> Int go (Int acc Int -> Int -> Int forall a. Num a => a -> a -> a + 1) NS f xs x instance HIndex NS where hindex :: NS f xs -> Int hindex = NS f xs -> Int forall k (f :: k -> *) (xs :: [k]). NS f xs -> Int index_NS -- | A sum of products. -- -- This is a 'newtype' for an 'NS' of an 'NP'. The elements of the -- (inner) products are applications of the parameter @f@. The type -- 'SOP' is indexed by the list of lists that determines the sizes -- of both the (outer) sum and all the (inner) products, as well as -- the types of all the elements of the inner products. -- -- A @'SOP' 'I'@ reflects the structure of a normal Haskell datatype. -- The sum structure represents the choice between the different -- constructors, the product structure represents the arguments of -- each constructor. -- newtype SOP (f :: (k -> Type)) (xss :: [[k]]) = SOP (NS (NP f) xss) deriving instance (Show (NS (NP f) xss)) => Show (SOP f xss) deriving instance (Eq (NS (NP f) xss)) => Eq (SOP f xss) deriving instance (Ord (NS (NP f) xss)) => Ord (SOP f xss) -- | @since 0.2.5.0 instance (NFData (NS (NP f) xss)) => NFData (SOP f xss) where rnf :: SOP f xss -> () rnf (SOP xss :: NS (NP f) xss xss) = NS (NP f) xss -> () forall a. NFData a => a -> () rnf NS (NP f) xss xss -- | Unwrap a sum of products. unSOP :: SOP f xss -> NS (NP f) xss unSOP :: SOP f xss -> NS (NP f) xss unSOP (SOP xss :: NS (NP f) xss xss) = NS (NP f) xss xss type instance AllN NS c = All c type instance AllN SOP c = All2 c -- | Obtain the index from an n-ary sum of products. -- -- An n-nary sum represents a choice between n different options. -- This function returns an integer between 0 and n - 1 indicating -- the option chosen by the given value. -- -- /Specification:/ -- -- @ -- 'index_SOP' = 'index_NS' '.' 'unSOP' -- @ -- -- /Example:/ -- -- >>> index_SOP (SOP (S (Z (I True :* I 'x' :* Nil)))) -- 1 -- -- @since 0.2.4.0 -- index_SOP :: SOP f xs -> Int index_SOP :: SOP f xs -> Int index_SOP = NS (NP f) xs -> Int forall k (f :: k -> *) (xs :: [k]). NS f xs -> Int index_NS (NS (NP f) xs -> Int) -> (SOP f xs -> NS (NP f) xs) -> SOP f xs -> Int forall b c a. (b -> c) -> (a -> b) -> a -> c . SOP f xs -> NS (NP f) xs forall k (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss unSOP instance HIndex SOP where hindex :: SOP f xs -> Int hindex = SOP f xs -> Int forall k (f :: k -> *) (xs :: [[k]]). SOP f xs -> Int index_SOP -- * Constructing sums -- | The type of injections into an n-ary sum. -- -- If you expand the type synonyms and newtypes involved, you get -- -- > Injection f xs a = (f -.-> K (NS f xs)) a ~= f a -> K (NS f xs) a ~= f a -> NS f xs -- -- If we pick @a@ to be an element of @xs@, this indeed corresponds to an -- injection into the sum. -- type Injection (f :: k -> Type) (xs :: [k]) = f -.-> K (NS f xs) -- | Compute all injections into an n-ary sum. -- -- Each element of the resulting product contains one of the injections. -- injections :: forall xs f. SListI xs => NP (Injection f xs) xs injections :: NP (Injection f xs) xs injections = case SList xs forall k (xs :: [k]). SListI xs => SList xs sList :: SList xs of SNil -> NP (Injection f xs) xs forall k (f :: k -> *). NP f '[] Nil SCons -> (f x -> K (NS f (x : xs)) x) -> (-.->) f (K (NS f (x : xs))) x forall k (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn (NS f (x : xs) -> K (NS f (x : xs)) x forall k a (b :: k). a -> K a b K (NS f (x : xs) -> K (NS f (x : xs)) x) -> (f x -> NS f (x : xs)) -> f x -> K (NS f (x : xs)) x forall b c a. (b -> c) -> (a -> b) -> a -> c . f x -> NS f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z) (-.->) f (K (NS f (x : xs))) x -> NP (f -.-> K (NS f (x : xs))) xs -> NP (f -.-> K (NS f (x : xs))) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* (forall (a :: k). Injection f xs a -> (-.->) f (K (NS f (x : xs))) a) -> NP (Injection f xs) xs -> NP (f -.-> K (NS f (x : xs))) 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). Injection f xs a -> (-.->) f (K (NS f (x : xs))) a forall a (f :: a -> *) (xs :: [a]) (a :: a) (x :: a). Injection f xs a -> Injection f (x : xs) a shiftInjection NP (Injection f xs) xs forall k (xs :: [k]) (f :: k -> *). SListI xs => NP (Injection f xs) xs injections -- | Shift an injection. -- -- Given an injection, return an injection into a sum that is one component larger. -- shiftInjection :: Injection f xs a -> Injection f (x ': xs) a shiftInjection :: Injection f xs a -> Injection f (x : xs) a shiftInjection (Fn f :: f a -> K (NS f xs) a f) = (f a -> K (NS f (x : xs)) a) -> Injection f (x : xs) a forall k (f :: k -> *) (g :: k -> *) (a :: k). (f a -> g a) -> (-.->) f g a Fn ((f a -> K (NS f (x : xs)) a) -> Injection f (x : xs) a) -> (f a -> K (NS f (x : xs)) a) -> Injection f (x : xs) a forall a b. (a -> b) -> a -> b $ NS f (x : xs) -> K (NS f (x : xs)) a forall k a (b :: k). a -> K a b K (NS f (x : xs) -> K (NS f (x : xs)) a) -> (f a -> NS f (x : xs)) -> f a -> K (NS f (x : xs)) a forall b c a. (b -> c) -> (a -> b) -> a -> c . NS f xs -> NS f (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NS f xs -> NS f (x : xs)) -> (f a -> NS f xs) -> f a -> NS f (x : xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . K (NS f xs) a -> NS f xs forall k a (b :: k). K a b -> a unK (K (NS f xs) a -> NS f xs) -> (f a -> K (NS f xs) a) -> f a -> NS f xs forall b c a. (b -> c) -> (a -> b) -> a -> c . f a -> K (NS f xs) a f {-# DEPRECATED shift "Use 'shiftInjection' instead." #-} -- | Shift an injection. -- -- Given an injection, return an injection into a sum that is one component larger. -- shift :: Injection f xs a -> Injection f (x ': xs) a shift :: Injection f xs a -> Injection f (x : xs) a shift = Injection f xs a -> Injection f (x : xs) a forall a (f :: a -> *) (xs :: [a]) (a :: a) (x :: a). Injection f xs a -> Injection f (x : xs) a shiftInjection -- | Apply injections to a product. -- -- Given a product containing all possible choices, produce a -- list of sums by applying each injection to the appropriate -- element. -- -- /Example:/ -- -- >>> apInjs_NP (I 'x' :* I True :* I 2 :* Nil) -- [Z (I 'x'),S (Z (I True)),S (S (Z (I 2)))] -- apInjs_NP :: SListI xs => NP f xs -> [NS f xs] apInjs_NP :: NP f xs -> [NS f xs] apInjs_NP = NP (K (NS f xs)) xs -> [NS f xs] forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NP (K (NS f xs)) xs -> [NS f xs]) -> (NP f xs -> NP (K (NS f xs)) xs) -> NP f xs -> [NS f xs] forall b c a. (b -> c) -> (a -> b) -> a -> c . NP f xs -> NP (K (NS f xs)) xs forall k (xs :: [k]) (f :: k -> *). SListI xs => NP f xs -> NP (K (NS f xs)) xs apInjs'_NP -- | `apInjs_NP` without `hcollapse`. -- -- >>> apInjs'_NP (I 'x' :* I True :* I 2 :* Nil) -- K (Z (I 'x')) :* K (S (Z (I True))) :* K (S (S (Z (I 2)))) :* Nil -- -- @since 0.2.5.0 -- apInjs'_NP :: SListI xs => NP f xs -> NP (K (NS f xs)) xs apInjs'_NP :: NP f xs -> NP (K (NS f xs)) xs apInjs'_NP = Prod NP (f -.-> K (NS f xs)) xs -> NP f xs -> NP (K (NS f xs)) xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs hap Prod NP (f -.-> K (NS f xs)) xs forall k (xs :: [k]) (f :: k -> *). SListI xs => NP (Injection f xs) xs injections -- | Apply injections to a product of product. -- -- This operates on the outer product only. Given a product -- containing all possible choices (that are products), -- produce a list of sums (of products) by applying each -- injection to the appropriate element. -- -- /Example:/ -- -- >>> apInjs_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil)) -- [SOP (Z (I 'x' :* Nil)),SOP (S (Z (I True :* I 2 :* Nil)))] -- apInjs_POP :: SListI xss => POP f xss -> [SOP f xss] apInjs_POP :: POP f xss -> [SOP f xss] apInjs_POP = (NS (NP f) xss -> SOP f xss) -> [NS (NP f) xss] -> [SOP f xss] forall a b. (a -> b) -> [a] -> [b] map NS (NP f) xss -> SOP f xss forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss SOP ([NS (NP f) xss] -> [SOP f xss]) -> (POP f xss -> [NS (NP f) xss]) -> POP f xss -> [SOP f xss] forall b c a. (b -> c) -> (a -> b) -> a -> c . NP (NP f) xss -> [NS (NP f) xss] forall k (xs :: [k]) (f :: k -> *). SListI xs => NP f xs -> [NS f xs] apInjs_NP (NP (NP f) xss -> [NS (NP f) xss]) -> (POP f xss -> NP (NP f) xss) -> POP f xss -> [NS (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 -- | `apInjs_POP` without `hcollapse`. -- -- /Example:/ -- -- >>> apInjs'_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil)) -- K (SOP (Z (I 'x' :* Nil))) :* K (SOP (S (Z (I True :* I 2 :* Nil)))) :* Nil -- -- @since 0.2.5.0 -- apInjs'_POP :: SListI xss => POP f xss -> NP (K (SOP f xss)) xss apInjs'_POP :: POP f xss -> NP (K (SOP f xss)) xss apInjs'_POP = (forall (a :: [k]). K (NS (NP f) xss) a -> K (SOP f xss) a) -> NP (K (NS (NP f) xss)) xss -> NP (K (SOP f xss)) 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 (SOP f xss -> K (SOP f xss) a forall k a (b :: k). a -> K a b K (SOP f xss -> K (SOP f xss) a) -> (K (NS (NP f) xss) a -> SOP f xss) -> K (NS (NP f) xss) a -> K (SOP f xss) a forall b c a. (b -> c) -> (a -> b) -> a -> c . NS (NP f) xss -> SOP f xss forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss SOP (NS (NP f) xss -> SOP f xss) -> (K (NS (NP f) xss) a -> NS (NP f) xss) -> K (NS (NP f) xss) a -> SOP f xss forall b c a. (b -> c) -> (a -> b) -> a -> c . K (NS (NP f) xss) a -> NS (NP f) xss forall k a (b :: k). K a b -> a unK) (NP (K (NS (NP f) xss)) xss -> NP (K (SOP f xss)) xss) -> (POP f xss -> NP (K (NS (NP f) xss)) xss) -> POP f xss -> NP (K (SOP f xss)) xss forall b c a. (b -> c) -> (a -> b) -> a -> c . Prod NP (NP f -.-> K (NS (NP f) xss)) xss -> NP (NP f) xss -> NP (K (NS (NP f) xss)) xss forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs hap Prod NP (NP f -.-> K (NS (NP f) xss)) xss forall k (xs :: [k]) (f :: k -> *). SListI xs => NP (Injection f xs) xs injections (NP (NP f) xss -> NP (K (NS (NP f) xss)) xss) -> (POP f xss -> NP (NP f) xss) -> POP f xss -> NP (K (NS (NP f) xss)) 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 type instance UnProd NP = NS type instance UnProd POP = SOP instance HApInjs NS where hapInjs :: Prod NS f xs -> [NS f xs] hapInjs = Prod NS f xs -> [NS f xs] forall k (xs :: [k]) (f :: k -> *). SListI xs => NP f xs -> [NS f xs] apInjs_NP instance HApInjs SOP where hapInjs :: Prod SOP f xs -> [SOP f xs] hapInjs = Prod SOP f xs -> [SOP f xs] forall k (xss :: [[k]]) (f :: k -> *). SListI xss => POP f xss -> [SOP f xss] apInjs_POP -- * Application -- | Specialization of 'hap'. ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs ap_NS (Fn f :: f x -> g x f :* _) (Z x :: f x x) = g x -> NS g (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (f x -> g x f f x f x x) ap_NS (_ :* fs :: NP (f -.-> g) xs fs) (S xs :: NS f xs xs) = NS g xs -> NS g (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NP (f -.-> g) xs -> NS f xs -> NS g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). NP (f -.-> g) xs -> NS f xs -> NS g xs ap_NS NP (f -.-> g) xs fs NS f xs NS f xs xs) ap_NS Nil x :: NS f xs x = case NS f xs x of {} -- | Specialization of 'hap'. ap_SOP :: POP (f -.-> g) xss -> SOP f xss -> SOP g xss ap_SOP :: POP (f -.-> g) xss -> SOP f xss -> SOP g xss ap_SOP (POP fss' :: NP (NP (f -.-> g)) xss fss') (SOP xss' :: NS (NP f) xss xss') = NS (NP g) xss -> SOP g xss forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss SOP (NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss forall k (f :: k -> *) (g :: k -> *) (xss :: [[k]]). NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss go NP (NP (f -.-> g)) xss fss' NS (NP f) xss xss') where go :: NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss go :: NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss go (fs :: NP (f -.-> g) x fs :* _ ) (Z xs :: NP f x xs ) = NP g x -> NS (NP g) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (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 ) go (_ :* fss :: NP (NP (f -.-> g)) xs fss) (S xss :: NS (NP f) xs xss) = NS (NP g) xs -> NS (NP g) (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NP (NP (f -.-> g)) xs -> NS (NP f) xs -> NS (NP g) xs forall k (f :: k -> *) (g :: k -> *) (xss :: [[k]]). NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss go NP (NP (f -.-> g)) xs fss NS (NP f) xs NS (NP f) xs xss) go Nil x :: NS (NP f) xss x = case NS (NP f) xss x of {} -- The definition of 'ap_SOP' is a more direct variant of -- '_ap_SOP_spec'. The direct definition has the advantage -- that it avoids the 'SListI' constraint. _ap_SOP_spec :: SListI xss => POP (t -.-> f) xss -> SOP t xss -> SOP f xss _ap_SOP_spec :: POP (t -.-> f) xss -> SOP t xss -> SOP f xss _ap_SOP_spec (POP fs :: NP (NP (t -.-> f)) xss fs) (SOP xs :: NS (NP t) xss xs) = NS (NP f) xss -> SOP f xss forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss SOP ((forall (a :: [k]). NP (t -.-> f) a -> NP t a -> NP f a) -> NP (NP (t -.-> f)) xss -> NS (NP t) xss -> NS (NP f) 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 -> NS g xs -> NS h xs liftA2_NS forall (a :: [k]). NP (t -.-> f) a -> NP t a -> NP f a forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). NP (f -.-> g) xs -> NP f xs -> NP g xs ap_NP NP (NP (t -.-> f)) xss fs NS (NP t) xss xs) type instance Same NS = NS type instance Same SOP = SOP type instance Prod NS = NP type instance Prod SOP = POP type instance SListIN NS = SListI type instance SListIN SOP = SListI2 instance HAp NS where hap :: Prod NS (f -.-> g) xs -> NS f xs -> NS g xs hap = Prod NS (f -.-> g) xs -> NS f xs -> NS g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). NP (f -.-> g) xs -> NS f xs -> NS g xs ap_NS instance HAp SOP where hap :: Prod SOP (f -.-> g) xs -> SOP f xs -> SOP g xs hap = Prod SOP (f -.-> g) xs -> SOP f xs -> SOP g xs forall k (f :: k -> *) (g :: k -> *) (xss :: [[k]]). POP (f -.-> g) xss -> SOP f xss -> SOP g xss ap_SOP -- * Lifting / mapping -- | Specialization of 'hliftA'. liftA_NS :: SListI xs => (forall a. f a -> g a) -> NS f xs -> NS g xs -- | Specialization of 'hliftA'. liftA_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss liftA_NS :: (forall (a :: k). f a -> g a) -> NS f xs -> NS g xs liftA_NS = (forall (a :: k). f a -> g a) -> NS f xs -> NS 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_SOP :: (forall (a :: k). f a -> g a) -> SOP f xss -> SOP g xss liftA_SOP = (forall (a :: k). f a -> g a) -> SOP f xss -> SOP 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_NS :: SListI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs -- | Specialization of 'hliftA2'. liftA2_SOP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss liftA2_NS :: (forall (a :: k). f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs liftA2_NS = (forall (a :: k). f a -> g a -> h a) -> NP f xs -> NS g xs -> NS 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_SOP :: (forall (a :: k). f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss liftA2_SOP = (forall (a :: k). f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP 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 'hmap', which is equivalent to 'hliftA'. map_NS :: SListI xs => (forall a. f a -> g a) -> NS f xs -> NS g xs -- | Specialization of 'hmap', which is equivalent to 'hliftA'. map_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss map_NS :: (forall (a :: k). f a -> g a) -> NS f xs -> NS g xs map_NS = (forall (a :: k). f a -> g a) -> NS f xs -> NS 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_SOP :: (forall (a :: k). f a -> g a) -> SOP f xss -> SOP g xss map_SOP = (forall (a :: k). f a -> g a) -> SOP f xss -> SOP 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 'hcliftA'. cliftA_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NS f xs -> NS g xs -- | Specialization of 'hcliftA'. cliftA_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP f xss -> SOP g xss cliftA_NS :: proxy c -> (forall (a :: k). c a => f a -> g a) -> NS f xs -> NS g xs cliftA_NS = proxy c -> (forall (a :: k). c a => f a -> g a) -> NS f xs -> NS 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_SOP :: proxy c -> (forall (a :: k). c a => f a -> g a) -> SOP f xss -> SOP g xss cliftA_SOP = proxy c -> (forall (a :: k). c a => f a -> g a) -> SOP f xss -> SOP 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_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs -- | Specialization of 'hcliftA2'. cliftA2_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss cliftA2_NS :: proxy c -> (forall (a :: k). c a => f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs cliftA2_NS = proxy c -> (forall (a :: k). c a => f a -> g a -> h a) -> NP f xs -> NS g xs -> NS 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_SOP :: proxy c -> (forall (a :: k). c a => f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss cliftA2_SOP = proxy c -> (forall (a :: k). c a => f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP 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 'hcmap', which is equivalent to 'hcliftA'. cmap_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NS f xs -> NS g xs -- | Specialization of 'hcmap', which is equivalent to 'hcliftA'. cmap_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP f xss -> SOP g xss cmap_NS :: proxy c -> (forall (a :: k). c a => f a -> g a) -> NS f xs -> NS g xs cmap_NS = proxy c -> (forall (a :: k). c a => f a -> g a) -> NS f xs -> NS 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_SOP :: proxy c -> (forall (a :: k). c a => f a -> g a) -> SOP f xss -> SOP g xss cmap_SOP = proxy c -> (forall (a :: k). c a => f a -> g a) -> SOP f xss -> SOP 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 -- * Dealing with @'All' c@ -- | Specialization of 'hcliftA2''. {-# DEPRECATED cliftA2'_NS "Use 'cliftA2_NS' instead." #-} cliftA2'_NS :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NS g xss -> NS h xss cliftA2'_NS :: proxy c -> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs) -> NP f xss -> NS g xss -> NS h xss cliftA2'_NS = proxy c -> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs) -> NP f xss -> NS g xss -> NS 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' -- * Comparison -- | Compare two sums with respect to the choice they -- are making. -- -- A value that chooses the first option -- is considered smaller than one that chooses the second -- option. -- -- If the choices are different, then either the first -- (if the first is smaller than the second) -- or the third (if the first is larger than the second) -- argument are called. If both choices are equal, then the -- second argument is called, which has access to the -- elements contained in the sums. -- -- @since 0.3.2.0 -- compare_NS :: forall r f g xs . r -- ^ what to do if first is smaller -> (forall x . f x -> g x -> r) -- ^ what to do if both are equal -> r -- ^ what to do if first is larger -> NS f xs -> NS g xs -> r compare_NS :: r -> (forall (x :: k). f x -> g x -> r) -> r -> NS f xs -> NS g xs -> r compare_NS lt :: r lt eq :: forall (x :: k). f x -> g x -> r eq gt :: r gt = NS f xs -> NS g xs -> r forall (ys :: [k]). NS f ys -> NS g ys -> r go where go :: forall ys . NS f ys -> NS g ys -> r go :: NS f ys -> NS g ys -> r go (Z x :: f x x) (Z y :: g x y) = f x -> g x -> r forall (x :: k). f x -> g x -> r eq f x x g x g x y go (Z _) (S _) = r lt go (S _) (Z _) = r gt go (S xs :: NS f xs xs) (S ys :: NS g xs ys) = NS f xs -> NS g xs -> r forall (ys :: [k]). NS f ys -> NS g ys -> r go NS f xs xs NS g xs NS g xs ys -- -- NOTE: The above could be written in terms of -- ccompare_NS, but the direct definition avoids the -- SListI constraint. We may change this in the future. -- | Constrained version of 'compare_NS'. -- -- @since 0.3.2.0 -- ccompare_NS :: forall c proxy r f g xs . (All c xs) => proxy c -> r -- ^ what to do if first is smaller -> (forall x . c x => f x -> g x -> r) -- ^ what to do if both are equal -> r -- ^ what to do if first is larger -> NS f xs -> NS g xs -> r ccompare_NS :: proxy c -> r -> (forall (x :: k). c x => f x -> g x -> r) -> r -> NS f xs -> NS g xs -> r ccompare_NS _ lt :: r lt eq :: forall (x :: k). c x => f x -> g x -> r eq gt :: r gt = NS f xs -> NS g xs -> r forall (ys :: [k]). All c ys => NS f ys -> NS g ys -> r go where go :: forall ys . (All c ys) => NS f ys -> NS g ys -> r go :: NS f ys -> NS g ys -> r go (Z x :: f x x) (Z y :: g x y) = f x -> g x -> r forall (x :: k). c x => f x -> g x -> r eq f x x g x g x y go (Z _) (S _) = r lt go (S _) (Z _) = r gt go (S xs :: NS f xs xs) (S ys :: NS g xs ys) = NS f xs -> NS g xs -> r forall (ys :: [k]). All c ys => NS f ys -> NS g ys -> r go NS f xs xs NS g xs NS g xs ys -- | Compare two sums of products with respect to the -- choice in the sum they are making. -- -- Only the sum structure is used for comparison. -- This is a small wrapper around 'ccompare_NS' for -- a common special case. -- -- @since 0.3.2.0 -- compare_SOP :: forall r f g xss . r -- ^ what to do if first is smaller -> (forall xs . NP f xs -> NP g xs -> r) -- ^ what to do if both are equal -> r -- ^ what to do if first is larger -> SOP f xss -> SOP g xss -> r compare_SOP :: r -> (forall (xs :: [k]). NP f xs -> NP g xs -> r) -> r -> SOP f xss -> SOP g xss -> r compare_SOP lt :: r lt eq :: forall (xs :: [k]). NP f xs -> NP g xs -> r eq gt :: r gt (SOP xs :: NS (NP f) xss xs) (SOP ys :: NS (NP g) xss ys) = r -> (forall (xs :: [k]). NP f xs -> NP g xs -> r) -> r -> NS (NP f) xss -> NS (NP g) xss -> r forall k r (f :: k -> *) (g :: k -> *) (xs :: [k]). r -> (forall (x :: k). f x -> g x -> r) -> r -> NS f xs -> NS g xs -> r compare_NS r lt forall (xs :: [k]). NP f xs -> NP g xs -> r eq r gt NS (NP f) xss xs NS (NP g) xss ys -- | Constrained version of 'compare_SOP'. -- -- @since 0.3.2.0 -- ccompare_SOP :: forall c proxy r f g xss . (All2 c xss) => proxy c -> r -- ^ what to do if first is smaller -> (forall xs . All c xs => NP f xs -> NP g xs -> r) -- ^ what to do if both are equal -> r -- ^ what to do if first is larger -> SOP f xss -> SOP g xss -> r ccompare_SOP :: proxy c -> r -> (forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r) -> r -> SOP f xss -> SOP g xss -> r ccompare_SOP p :: proxy c p lt :: r lt eq :: forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r eq gt :: r gt (SOP xs :: NS (NP f) xss xs) (SOP ys :: NS (NP g) xss ys) = Proxy (All c) -> r -> (forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r) -> r -> NS (NP f) xss -> NS (NP g) xss -> r forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) r (f :: k -> *) (g :: k -> *) (xs :: [k]). All c xs => proxy c -> r -> (forall (x :: k). c x => f x -> g x -> r) -> r -> NS f xs -> NS g xs -> r ccompare_NS (proxy c -> Proxy (All c) forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint). proxy c -> Proxy (All c) allP proxy c p) r lt forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r eq r gt NS (NP f) xss xs NS (NP g) xss ys -- * Collapsing -- | Specialization of 'hcollapse'. collapse_NS :: NS (K a) xs -> a -- | Specialization of 'hcollapse'. collapse_SOP :: SListI xss => SOP (K a) xss -> [a] collapse_NS :: NS (K a) xs -> a collapse_NS (Z (K x :: a x)) = a x collapse_NS (S xs :: NS (K a) xs xs) = NS (K a) xs -> a forall k a (xs :: [k]). NS (K a) xs -> a collapse_NS NS (K a) xs xs collapse_SOP :: SOP (K a) xss -> [a] collapse_SOP = NS (K [a]) xss -> [a] forall k a (xs :: [k]). NS (K a) xs -> a collapse_NS (NS (K [a]) xss -> [a]) -> (SOP (K a) xss -> NS (K [a]) xss) -> SOP (K a) xss -> [a] forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (a :: [k]). NP (K a) a -> K [a] a) -> NS (NP (K a)) xss -> NS (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) (NS (NP (K a)) xss -> NS (K [a]) xss) -> (SOP (K a) xss -> NS (NP (K a)) xss) -> SOP (K a) xss -> NS (K [a]) xss forall b c a. (b -> c) -> (a -> b) -> a -> c . SOP (K a) xss -> NS (NP (K a)) xss forall k (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss unSOP type instance CollapseTo NS a = a type instance CollapseTo SOP a = [a] instance HCollapse NS where hcollapse :: NS (K a) xs -> CollapseTo NS a hcollapse = NS (K a) xs -> CollapseTo NS a forall k a (xs :: [k]). NS (K a) xs -> a collapse_NS instance HCollapse SOP where hcollapse :: SOP (K a) xs -> CollapseTo SOP a hcollapse = SOP (K a) xs -> CollapseTo SOP a forall k (xss :: [[k]]) a. SListI xss => SOP (K a) xss -> [a] collapse_SOP -- * Folding -- | Specialization of 'hctraverse_'. -- -- /Note:/ we don't need 'Applicative' constraint. -- -- @since 0.3.2.0 -- ctraverse__NS :: forall c proxy xs f g. (All c xs) => proxy c -> (forall a. c a => f a -> g ()) -> NS f xs -> g () ctraverse__NS :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g () ctraverse__NS _ f :: forall (a :: k). c a => f a -> g () f = NS f xs -> g () forall (ys :: [k]). All c ys => NS f ys -> g () go where go :: All c ys => NS f ys -> g () go :: NS f ys -> g () go (Z x :: f x x) = f x -> g () forall (a :: k). c a => f a -> g () f f x x go (S xs :: NS f xs xs) = NS f xs -> g () forall (ys :: [k]). All c ys => NS f ys -> g () go NS f xs xs -- | Specialization of 'htraverse_'. -- -- /Note:/ we don't need 'Applicative' constraint. -- -- @since 0.3.2.0 -- traverse__NS :: forall xs f g. (SListI xs) => (forall a. f a -> g ()) -> NS f xs -> g () traverse__NS :: (forall (a :: k). f a -> g ()) -> NS f xs -> g () traverse__NS f :: forall (a :: k). f a -> g () f = NS f xs -> g () forall (ys :: [k]). NS f ys -> g () go where go :: NS f ys -> g () go :: NS f ys -> g () go (Z x :: f x x) = f x -> g () forall (a :: k). f a -> g () f f x x go (S xs :: NS f xs xs) = NS f xs -> g () forall (ys :: [k]). NS f ys -> g () go NS f xs xs -- | Specialization of 'hctraverse_'. -- -- @since 0.3.2.0 -- ctraverse__SOP :: forall c proxy xss f g. (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g ()) -> SOP f xss -> g () ctraverse__SOP :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> SOP f xss -> g () ctraverse__SOP 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 ()) -> NS (NP f) xss -> g () forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (xs :: [k]) (f :: k -> *) (g :: * -> *). All c xs => proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g () ctraverse__NS (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) (NS (NP f) xss -> g ()) -> (SOP f xss -> NS (NP f) xss) -> SOP f xss -> g () forall b c a. (b -> c) -> (a -> b) -> a -> c . SOP f xss -> NS (NP f) xss forall k (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss unSOP -- | Specialization of 'htraverse_'. -- -- @since 0.3.2.0 -- traverse__SOP :: forall xss f g. (SListI2 xss, Applicative g) => (forall a. f a -> g ()) -> SOP f xss -> g () traverse__SOP :: (forall (a :: k). f a -> g ()) -> SOP f xss -> g () traverse__SOP f :: forall (a :: k). f a -> g () f = Proxy Top -> (forall (a :: k). Top a => f a -> g ()) -> SOP 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 ()) -> SOP f xss -> g () ctraverse__SOP Proxy Top forall k. Proxy Top topP forall (a :: k). f a -> g () forall (a :: k). Top a => f a -> g () f {-# INLINE traverse__SOP #-} topP :: Proxy Top topP :: Proxy Top topP = Proxy Top forall k (t :: k). Proxy t Proxy instance HTraverse_ NS where hctraverse_ :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g () hctraverse_ = proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g () forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (xs :: [k]) (f :: k -> *) (g :: * -> *). All c xs => proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g () ctraverse__NS htraverse_ :: (forall (a :: k). f a -> g ()) -> NS f xs -> g () htraverse_ = (forall (a :: k). f a -> g ()) -> NS f xs -> g () forall k (xs :: [k]) (f :: k -> *) (g :: * -> *). SListI xs => (forall (a :: k). f a -> g ()) -> NS f xs -> g () traverse__NS instance HTraverse_ SOP where hctraverse_ :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> SOP f xs -> g () hctraverse_ = proxy c -> (forall (a :: k). c a => f a -> g ()) -> SOP 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 ()) -> SOP f xss -> g () ctraverse__SOP htraverse_ :: (forall (a :: k). f a -> g ()) -> SOP f xs -> g () htraverse_ = (forall (a :: k). f a -> g ()) -> SOP f xs -> g () forall k (xss :: [[k]]) (f :: k -> *) (g :: * -> *). (SListI2 xss, Applicative g) => (forall (a :: k). f a -> g ()) -> SOP f xss -> g () traverse__SOP -- | Specialization of 'hcfoldMap'. -- -- /Note:/ We don't need 'Monoid' instance. -- -- @since 0.3.2.0 -- cfoldMap_NS :: forall c proxy f xs m. (All c xs) => proxy c -> (forall a. c a => f a -> m) -> NS f xs -> m cfoldMap_NS :: proxy c -> (forall (a :: k). c a => f a -> m) -> NS f xs -> m cfoldMap_NS _ f :: forall (a :: k). c a => f a -> m f = NS f xs -> m forall (ys :: [k]). All c ys => NS f ys -> m go where go :: All c ys => NS f ys -> m go :: NS f ys -> m go (Z x :: f x x) = f x -> m forall (a :: k). c a => f a -> m f f x x go (S xs :: NS f xs xs) = NS f xs -> m forall (ys :: [k]). All c ys => NS f ys -> m go NS f xs xs -- | Specialization of 'hcfoldMap'. -- -- @since 0.3.2.0 -- cfoldMap_SOP :: (All2 c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> SOP f xs -> m cfoldMap_SOP :: proxy c -> (forall (a :: k). c a => f a -> m) -> SOP f xs -> m cfoldMap_SOP = proxy c -> (forall (a :: k). c a => f a -> m) -> SOP 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'_NS :: Applicative f => NS (f :.: g) xs -> f (NS g xs) sequence'_NS :: NS (f :.: g) xs -> f (NS g xs) sequence'_NS (Z mx :: (:.:) f g x mx) = g x -> NS g (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (g x -> NS g (x : xs)) -> f (g x) -> f (NS 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 sequence'_NS (S mxs :: NS (f :.: g) xs mxs) = NS g xs -> NS g (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NS g xs -> NS g (x : xs)) -> f (NS g xs) -> f (NS g (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> NS (f :.: g) xs -> f (NS g xs) forall k (f :: * -> *) (g :: k -> *) (xs :: [k]). Applicative f => NS (f :.: g) xs -> f (NS g xs) sequence'_NS NS (f :.: g) xs mxs -- | Specialization of 'hsequence''. sequence'_SOP :: (SListI xss, Applicative f) => SOP (f :.: g) xss -> f (SOP g xss) sequence'_SOP :: SOP (f :.: g) xss -> f (SOP g xss) sequence'_SOP = (NS (NP g) xss -> SOP g xss) -> f (NS (NP g) xss) -> f (SOP g xss) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap NS (NP g) xss -> SOP g xss forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss SOP (f (NS (NP g) xss) -> f (SOP g xss)) -> (SOP (f :.: g) xss -> f (NS (NP g) xss)) -> SOP (f :.: g) xss -> f (SOP g xss) forall b c a. (b -> c) -> (a -> b) -> a -> c . NS (f :.: NP g) xss -> f (NS (NP g) xss) forall k (f :: * -> *) (g :: k -> *) (xs :: [k]). Applicative f => NS (f :.: g) xs -> f (NS g xs) sequence'_NS (NS (f :.: NP g) xss -> f (NS (NP g) xss)) -> (SOP (f :.: g) xss -> NS (f :.: NP g) xss) -> SOP (f :.: g) xss -> f (NS (NP g) xss) forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (a :: [k]). NP (f :.: g) a -> (:.:) f (NP g) a) -> NS (NP (f :.: g)) xss -> NS (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) (NS (NP (f :.: g)) xss -> NS (f :.: NP g) xss) -> (SOP (f :.: g) xss -> NS (NP (f :.: g)) xss) -> SOP (f :.: g) xss -> NS (f :.: NP g) xss forall b c a. (b -> c) -> (a -> b) -> a -> c . SOP (f :.: g) xss -> NS (NP (f :.: g)) xss forall k (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss unSOP -- | Specialization of 'hctraverse''. -- -- /Note:/ as 'NS' has exactly one element, the 'Functor' constraint is enough. -- -- @since 0.3.2.0 -- ctraverse'_NS :: forall c proxy xs f f' g. (All c xs, Functor g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) ctraverse'_NS :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) ctraverse'_NS _ f :: forall (a :: k). c a => f a -> g (f' a) f = NS f xs -> g (NS f' xs) forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys) go where go :: All c ys => NS f ys -> g (NS f' ys) go :: NS f ys -> g (NS f' ys) go (Z x :: f x x) = f' x -> NS f' (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (f' x -> NS f' (x : xs)) -> g (f' x) -> g (NS 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 go (S xs :: NS f xs xs) = NS f' xs -> NS f' (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NS f' xs -> NS f' (x : xs)) -> g (NS f' xs) -> g (NS f' (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> NS f xs -> g (NS f' xs) forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys) go NS f xs xs -- | Specialization of 'htraverse''. -- -- /Note:/ as 'NS' has exactly one element, the 'Functor' constraint is enough. -- -- @since 0.3.2.0 -- traverse'_NS :: forall xs f f' g. (SListI xs, Functor g) => (forall a. f a -> g (f' a)) -> NS f xs -> g (NS f' xs) traverse'_NS :: (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs) traverse'_NS f :: forall (a :: k). f a -> g (f' a) f = Proxy Top -> (forall (a :: k). Top a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *). (All c xs, Functor g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) ctraverse'_NS 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'_NS #-} -- | Specialization of 'hctraverse''. -- -- @since 0.3.2.0 -- ctraverse'_SOP :: (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss) ctraverse'_SOP :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss) ctraverse'_SOP p :: proxy c p f :: forall (a :: k). c a => f a -> g (f' a) f = (NS (NP f') xss -> SOP f' xss) -> g (NS (NP f') xss) -> g (SOP f' xss) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap NS (NP f') xss -> SOP f' xss forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss SOP (g (NS (NP f') xss) -> g (SOP f' xss)) -> (SOP f xss -> g (NS (NP f') xss)) -> SOP f xss -> g (SOP 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)) -> NS (NP f) xss -> g (NS (NP f') xss) forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *). (All c xs, Functor g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) ctraverse'_NS (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) (NS (NP f) xss -> g (NS (NP f') xss)) -> (SOP f xss -> NS (NP f) xss) -> SOP f xss -> g (NS (NP f') xss) forall b c a. (b -> c) -> (a -> b) -> a -> c . SOP f xss -> NS (NP f) xss forall k (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss unSOP -- | Specialization of 'htraverse''. -- -- @since 0.3.2.0 -- traverse'_SOP :: (SListI2 xss, Applicative g) => (forall a. f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss) traverse'_SOP :: (forall (a :: k). f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss) traverse'_SOP f :: forall (a :: k). f a -> g (f' a) f = Proxy Top -> (forall (a :: k). Top a => f a -> g (f' a)) -> SOP f xss -> g (SOP 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)) -> SOP f xss -> g (SOP f' xss) ctraverse'_SOP 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'_SOP #-} instance HSequence NS where hsequence' :: NS (f :.: g) xs -> f (NS g xs) hsequence' = NS (f :.: g) xs -> f (NS g xs) forall k (f :: * -> *) (g :: k -> *) (xs :: [k]). Applicative f => NS (f :.: g) xs -> f (NS g xs) sequence'_NS hctraverse' :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) hctraverse' = proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *). (All c xs, Functor g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) ctraverse'_NS htraverse' :: (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs) htraverse' = (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs) forall k (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *). (SListI xs, Functor g) => (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs) traverse'_NS instance HSequence SOP where hsequence' :: SOP (f :.: g) xs -> f (SOP g xs) hsequence' = SOP (f :.: g) xs -> f (SOP g xs) forall k (xss :: [[k]]) (f :: * -> *) (g :: k -> *). (SListI xss, Applicative f) => SOP (f :.: g) xss -> f (SOP g xss) sequence'_SOP hctraverse' :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> SOP f xs -> g (SOP f' xs) hctraverse' = proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> SOP f xs -> g (SOP 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)) -> SOP f xss -> g (SOP f' xss) ctraverse'_SOP htraverse' :: (forall (a :: k). f a -> g (f' a)) -> SOP f xs -> g (SOP f' xs) htraverse' = (forall (a :: k). f a -> g (f' a)) -> SOP f xs -> g (SOP f' xs) forall k (xss :: [[k]]) (g :: * -> *) (f :: k -> *) (f' :: k -> *). (SListI2 xss, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss) traverse'_SOP -- | Specialization of 'hsequence'. sequence_NS :: (SListI xs, Applicative f) => NS f xs -> f (NS I xs) -- | Specialization of 'hsequence'. sequence_SOP :: (All SListI xss, Applicative f) => SOP f xss -> f (SOP I xss) sequence_NS :: NS f xs -> f (NS I xs) sequence_NS = NS f xs -> f (NS 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_SOP :: SOP f xss -> f (SOP I xss) sequence_SOP = SOP f xss -> f (SOP 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_NS :: (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_SOP :: (All2 c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs) ctraverse_NS :: proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs) ctraverse_NS = 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_SOP :: proxy c -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs) ctraverse_SOP = 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 'NS'. -- -- Takes arguments determining what to do for 'Z' -- and what to do for 'S'. The result type is still -- indexed over the type-level lit. -- -- @since 0.2.3.0 -- cata_NS :: forall r f xs . (forall y ys . f y -> r (y ': ys)) -> (forall y ys . r ys -> r (y ': ys)) -> NS f xs -> r xs cata_NS :: (forall (y :: k) (ys :: [k]). f y -> r (y : ys)) -> (forall (y :: k) (ys :: [k]). r ys -> r (y : ys)) -> NS f xs -> r xs cata_NS z :: forall (y :: k) (ys :: [k]). f y -> r (y : ys) z s :: forall (y :: k) (ys :: [k]). r ys -> r (y : ys) s = NS f xs -> r xs forall (ys :: [k]). NS f ys -> r ys go where go :: forall ys . NS f ys -> r ys go :: NS f ys -> r ys go (Z x :: f x x) = f x -> r (x : xs) forall (y :: k) (ys :: [k]). f y -> r (y : ys) z f x x go (S i :: NS f xs i) = r xs -> r (x : xs) forall (y :: k) (ys :: [k]). r ys -> r (y : ys) s (NS f xs -> r xs forall (ys :: [k]). NS f ys -> r ys go NS f xs i) -- | Constrained catamorphism for 'NS'. -- -- @since 0.2.3.0 -- ccata_NS :: forall c proxy r f xs . (All c xs) => proxy c -> (forall y ys . c y => f y -> r (y ': ys)) -> (forall y ys . c y => r ys -> r (y ': ys)) -> NS f xs -> r xs ccata_NS :: proxy c -> (forall (y :: k) (ys :: [k]). c y => f y -> r (y : ys)) -> (forall (y :: k) (ys :: [k]). c y => r ys -> r (y : ys)) -> NS f xs -> r xs ccata_NS _ z :: forall (y :: k) (ys :: [k]). c y => f y -> r (y : ys) z s :: forall (y :: k) (ys :: [k]). c y => r ys -> r (y : ys) s = NS f xs -> r xs forall (ys :: [k]). All c ys => NS f ys -> r ys go where go :: forall ys . (All c ys) => NS f ys -> r ys go :: NS f ys -> r ys go (Z x :: f x x) = f x -> r (x : xs) forall (y :: k) (ys :: [k]). c y => f y -> r (y : ys) z f x x go (S i :: NS f xs i) = r xs -> r (x : xs) forall (y :: k) (ys :: [k]). c y => r ys -> r (y : ys) s (NS f xs -> r xs forall (ys :: [k]). All c ys => NS f ys -> r ys go NS f xs i) -- | Anamorphism for 'NS'. -- -- @since 0.2.3.0 -- ana_NS :: forall s f xs . (SListI xs) => (forall r . s '[] -> r) -> (forall y ys . s (y ': ys) -> Either (f y) (s ys)) -> s xs -> NS f xs ana_NS :: (forall r. s '[] -> r) -> (forall (y :: k) (ys :: [k]). s (y : ys) -> Either (f y) (s ys)) -> s xs -> NS f xs ana_NS refute :: forall r. s '[] -> r refute decide :: forall (y :: k) (ys :: [k]). s (y : ys) -> Either (f y) (s ys) decide = Proxy Top -> (forall r. s '[] -> r) -> (forall (y :: k) (ys :: [k]). Top y => s (y : ys) -> Either (f y) (s ys)) -> s xs -> NS f xs forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (s :: [k] -> *) (f :: k -> *) (xs :: [k]). All c xs => proxy c -> (forall r. s '[] -> r) -> (forall (y :: k) (ys :: [k]). c y => s (y : ys) -> Either (f y) (s ys)) -> s xs -> NS f xs cana_NS Proxy Top forall k. Proxy Top topP forall r. s '[] -> r refute forall (y :: k) (ys :: [k]). s (y : ys) -> Either (f y) (s ys) forall (y :: k) (ys :: [k]). Top y => s (y : ys) -> Either (f y) (s ys) decide {-# INLINE ana_NS #-} -- | Constrained anamorphism for 'NS'. -- -- @since 0.2.3.0 -- cana_NS :: forall c proxy s f xs . (All c xs) => proxy c -> (forall r . s '[] -> r) -> (forall y ys . c y => s (y ': ys) -> Either (f y) (s ys)) -> s xs -> NS f xs cana_NS :: proxy c -> (forall r. s '[] -> r) -> (forall (y :: k) (ys :: [k]). c y => s (y : ys) -> Either (f y) (s ys)) -> s xs -> NS f xs cana_NS _ refute :: forall r. s '[] -> r refute decide :: forall (y :: k) (ys :: [k]). c y => s (y : ys) -> Either (f y) (s ys) decide = SList xs -> s xs -> NS f xs forall (ys :: [k]). All c ys => SList ys -> s ys -> NS 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 -> NS f ys go :: SList ys -> s ys -> NS f ys go SNil s :: s ys s = s '[] -> NS f ys forall r. s '[] -> r refute s ys s '[] s go SCons s :: s ys s = case s (x : xs) -> Either (f x) (s xs) forall (y :: k) (ys :: [k]). c y => s (y : ys) -> Either (f y) (s ys) decide s ys s (x : xs) s of Left x :: f x x -> f x -> NS f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z f x x Right s' :: s xs s' -> NS f xs -> NS f (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (SList xs -> s xs -> NS f xs forall (ys :: [k]). All c ys => SList ys -> s ys -> NS f ys go SList xs forall k (xs :: [k]). SListI xs => SList xs sList s xs s') -- * Expanding sums to products -- | Specialization of 'hexpand'. -- -- @since 0.2.5.0 -- expand_NS :: forall f xs . (SListI xs) => (forall x . f x) -> NS f xs -> NP f xs expand_NS :: (forall (x :: k). f x) -> NS f xs -> NP f xs expand_NS d :: forall (x :: k). f x d = Proxy Top -> (forall (x :: k). Top x => f x) -> NS f xs -> NP f xs forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (xs :: [k]). All c xs => proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs cexpand_NS Proxy Top forall k. Proxy Top topP forall (x :: k). f x forall (x :: k). Top x => f x d {-# INLINE expand_NS #-} -- | Specialization of 'hcexpand'. -- -- @since 0.2.5.0 -- cexpand_NS :: forall c proxy f xs . (All c xs) => proxy c -> (forall x . c x => f x) -> NS f xs -> NP f xs cexpand_NS :: proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs cexpand_NS p :: proxy c p d :: forall (x :: k). c x => f x d = NS f xs -> NP f xs forall (ys :: [k]). All c ys => NS f ys -> NP f ys go where go :: forall ys . All c ys => NS f ys -> NP f ys go :: NS f ys -> NP f ys go (Z x :: f x x) = 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) :* proxy c -> (forall (x :: k). c x => f x) -> NP f xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs hcpure proxy c p forall (x :: k). c x => f x d go (S i :: NS f xs i) = f x forall (x :: k). c x => f x d 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) :* NS f xs -> NP f xs forall (ys :: [k]). All c ys => NS f ys -> NP f ys go NS f xs i -- | Specialization of 'hexpand'. -- -- @since 0.2.5.0 -- expand_SOP :: forall f xss . (All SListI xss) => (forall x . f x) -> SOP f xss -> POP f xss expand_SOP :: (forall (x :: k). f x) -> SOP f xss -> POP f xss expand_SOP d :: forall (x :: k). f x d = Proxy Top -> (forall (x :: k). Top x => f x) -> SOP f xss -> POP f xss forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (xss :: [[k]]). All2 c xss => proxy c -> (forall (x :: k). c x => f x) -> SOP f xss -> POP f xss cexpand_SOP Proxy Top forall k. Proxy Top topP forall (x :: k). f x forall (x :: k). Top x => f x d {-# INLINE cexpand_SOP #-} -- | Specialization of 'hcexpand'. -- -- @since 0.2.5.0 -- cexpand_SOP :: forall c proxy f xss . (All2 c xss) => proxy c -> (forall x . c x => f x) -> SOP f xss -> POP f xss cexpand_SOP :: proxy c -> (forall (x :: k). c x => f x) -> SOP f xss -> POP f xss cexpand_SOP p :: proxy c p d :: forall (x :: k). c x => f x d = 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 -> POP f xss) -> (SOP f xss -> NP (NP f) xss) -> SOP f xss -> POP f xss forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy (All c) -> (forall (x :: [k]). All c x => NP f x) -> NS (NP f) xss -> NP (NP f) xss forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (xs :: [k]). All c xs => proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs cexpand_NS (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 (x :: k). c x => f x) -> NP f x forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs hcpure proxy c p forall (x :: k). c x => f x d) (NS (NP f) xss -> NP (NP f) xss) -> (SOP f xss -> NS (NP f) xss) -> SOP f xss -> NP (NP f) xss forall b c a. (b -> c) -> (a -> b) -> a -> c . SOP f xss -> NS (NP f) xss forall k (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss unSOP allP :: proxy c -> Proxy (All c) allP :: proxy c -> Proxy (All c) allP _ = Proxy (All c) forall k (t :: k). Proxy t Proxy instance HExpand NS where hexpand :: (forall (x :: k). f x) -> NS f xs -> Prod NS f xs hexpand = (forall (x :: k). f x) -> NS f xs -> Prod NS f xs forall k (f :: k -> *) (xs :: [k]). SListI xs => (forall (x :: k). f x) -> NS f xs -> NP f xs expand_NS hcexpand :: proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs hcexpand = proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (xs :: [k]). All c xs => proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs cexpand_NS instance HExpand SOP where hexpand :: (forall (x :: k). f x) -> SOP f xs -> Prod SOP f xs hexpand = (forall (x :: k). f x) -> SOP f xs -> Prod SOP f xs forall k (f :: k -> *) (xss :: [[k]]). All SListI xss => (forall (x :: k). f x) -> SOP f xss -> POP f xss expand_SOP hcexpand :: proxy c -> (forall (x :: k). c x => f x) -> SOP f xs -> Prod SOP f xs hcexpand = proxy c -> (forall (x :: k). c x => f x) -> SOP f xs -> Prod SOP f xs forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (xss :: [[k]]). All2 c xss => proxy c -> (forall (x :: k). c x => f x) -> SOP f xss -> POP f xss cexpand_SOP -- | Specialization of 'htrans'. -- -- @since 0.3.1.0 -- trans_NS :: AllZip c xs ys => proxy c -> (forall x y . c x y => f x -> g y) -> NS f xs -> NS g ys trans_NS :: proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NS f xs -> NS g ys trans_NS _ t :: forall (x :: k) (y :: k). c x y => f x -> g y t (Z x :: f x x) = g (Head ys) -> NS g (Head ys : Tail ys) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (f x -> g (Head ys) forall (x :: k) (y :: k). c x y => f x -> g y t f x x) trans_NS p :: proxy c p t :: forall (x :: k) (y :: k). c x y => f x -> g y t (S x :: NS f xs x) = NS g (Tail ys) -> NS g (Head ys : Tail ys) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NS f xs -> NS 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) -> NS f xs -> NS g ys trans_NS proxy c p forall (x :: k) (y :: k). c x y => f x -> g y t NS f xs x) -- | Specialization of 'htrans'. -- -- @since 0.3.1.0 -- trans_SOP :: AllZip2 c xss yss => proxy c -> (forall x y . c x y => f x -> g y) -> SOP f xss -> SOP g yss trans_SOP :: proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> SOP f xss -> SOP g yss trans_SOP p :: proxy c p t :: forall (x :: k) (y :: k). c x y => f x -> g y t = NS (NP g) yss -> SOP g yss forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss SOP (NS (NP g) yss -> SOP g yss) -> (SOP f xss -> NS (NP g) yss) -> SOP f xss -> SOP 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) -> NS (NP f) xss -> NS (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) -> NS f xs -> NS g ys trans_NS (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 k1 k2 (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2]) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). AllZip c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NP f xs -> NP g ys trans_NP proxy c p forall (x :: k) (y :: k). c x y => f x -> g y t) (NS (NP f) xss -> NS (NP g) yss) -> (SOP f xss -> NS (NP f) xss) -> SOP f xss -> NS (NP g) yss forall b c a. (b -> c) -> (a -> b) -> a -> c . SOP f xss -> NS (NP f) xss forall k (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss unSOP 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_NS :: forall f g xs ys . AllZip (LiftedCoercible f g) xs ys => NS f xs -> NS g ys coerce_NS :: NS f xs -> NS g ys coerce_NS = NS f xs -> NS g ys forall a b. a -> b unsafeCoerce -- | Safe version of 'coerce_NS'. -- -- For documentation purposes only; not exported. -- _safe_coerce_NS :: forall f g xs ys . AllZip (LiftedCoercible f g) xs ys => NS f xs -> NS g ys _safe_coerce_NS :: NS f xs -> NS g ys _safe_coerce_NS = Proxy (LiftedCoercible f g) -> (forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y) -> NS f xs -> NS 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) -> NS f xs -> NS g ys trans_NS (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_SOP :: forall f g xss yss . AllZip2 (LiftedCoercible f g) xss yss => SOP f xss -> SOP g yss coerce_SOP :: SOP f xss -> SOP g yss coerce_SOP = SOP f xss -> SOP g yss forall a b. a -> b unsafeCoerce -- | Safe version of 'coerce_SOP'. -- -- For documentation purposes only; not exported. -- _safe_coerce_SOP :: forall f g xss yss . AllZip2 (LiftedCoercible f g) xss yss => SOP f xss -> SOP g yss _safe_coerce_SOP :: SOP f xss -> SOP g yss _safe_coerce_SOP = Proxy (LiftedCoercible f g) -> (forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y) -> SOP f xss -> SOP 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) -> SOP f xss -> SOP g yss trans_SOP (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_NS :: forall f xs ys . AllZip (LiftedCoercible I f) xs ys => NS I xs -> NS f ys fromI_NS :: NS I xs -> NS f ys fromI_NS = NS I xs -> NS 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_NS :: forall f xs ys . AllZip (LiftedCoercible f I) xs ys => NS f xs -> NS I ys toI_NS :: NS f xs -> NS I ys toI_NS = NS f xs -> NS 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_SOP :: forall f xss yss . AllZip2 (LiftedCoercible I f) xss yss => SOP I xss -> SOP f yss fromI_SOP :: SOP I xss -> SOP f yss fromI_SOP = SOP I xss -> SOP 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_SOP :: forall f xss yss . AllZip2 (LiftedCoercible f I) xss yss => SOP f xss -> SOP I yss toI_SOP :: SOP f xss -> SOP I yss toI_SOP = SOP f xss -> SOP 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 NS NS where htrans :: proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NS f xs -> NS g ys htrans = proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NS f xs -> NS 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) -> NS f xs -> NS g ys trans_NS hcoerce :: NS f xs -> NS g ys hcoerce = NS f xs -> NS g ys forall k k (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]). AllZip (LiftedCoercible f g) xs ys => NS f xs -> NS g ys coerce_NS instance HTrans SOP SOP where htrans :: proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> SOP f xs -> SOP g ys htrans = proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> SOP f xs -> SOP 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) -> SOP f xss -> SOP g yss trans_SOP hcoerce :: SOP f xs -> SOP g ys hcoerce = SOP f xs -> SOP g ys forall k k (f :: k -> *) (g :: k -> *) (xss :: [[k]]) (yss :: [[k]]). AllZip2 (LiftedCoercible f g) xss yss => SOP f xss -> SOP g yss coerce_SOP