{-# 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 f x
x)  = f x -> ()
forall a. NFData a => a -> ()
rnf f x
x
    rnf (S 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
  SList xs
SNil  -> NP (Ejection f xs) xs
forall k (f :: k -> *). NP f '[]
Nil
  SList xs
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 f xs
ns -> case NS f xs
ns of Z f x
fx -> f x -> Maybe (f x)
forall a. a -> Maybe a
Just f x
fx; S NS f xs
_ -> 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 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 f (x : xs)
ns -> case NS f (x : xs)
ns of Z f x
_ -> 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 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 f x
x) = f x
f x
x
unZ (S 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 Int
0
  where
    go :: forall ys . Int -> NS f ys -> Int
    go :: Int -> NS f ys -> Int
go !Int
acc (Z f x
_) = Int
acc
    go !Int
acc (S 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
+ Int
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 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 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
  SList xs
SNil   -> NP (Injection f xs) xs
forall k (f :: k -> *). NP f '[]
Nil
  SList xs
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 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 x -> g x
f  :* NP (f -.-> g) xs
_)   (Z 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 ((-.->) f g x
_     :* NP (f -.-> g) xs
fs)  (S 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 NP (f -.-> g) xs
Nil            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 NP (NP (f -.-> g)) xss
fss') (SOP 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 (NP (f -.-> g) x
fs :* NP (NP (f -.-> g)) xs
_  ) (Z 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 (NP (f -.-> g) x
_  :* NP (NP (f -.-> g)) xs
fss) (S 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 NP (NP (f -.-> g)) xss
Nil         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 NP (NP (t -.-> f)) xss
fs) (SOP 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 r
lt forall (x :: k). f x -> g x -> r
eq 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 f x
x)  (Z 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 f x
_)  (S NS g xs
_)  = r
lt
    go (S NS f xs
_)  (Z g x
_)  = r
gt
    go (S NS f xs
xs) (S 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 proxy c
_ r
lt forall (x :: k). c x => f x -> g x -> r
eq 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 f x
x)  (Z 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 f x
_)  (S NS g xs
_)  = r
lt
    go (S NS f xs
_)  (Z g x
_)  = r
gt
    go (S NS f xs
xs) (S 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 r
lt forall (xs :: [k]). NP f xs -> NP g xs -> r
eq r
gt (SOP NS (NP f) xss
xs) (SOP 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 proxy c
p r
lt forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r
eq r
gt (SOP NS (NP f) xss
xs) (SOP 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 a
x)) = a
x
collapse_NS (S 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 proxy c
_ 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 f x
x)  = f x -> g ()
forall (a :: k). c a => f a -> g ()
f f x
x
    go (S 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 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 f x
x)  = f x -> g ()
forall (a :: k). f a -> g ()
f f x
x
    go (S 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 proxy c
p 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 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 proxy c
_ 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 f x
x)  = f x -> m
forall (a :: k). c a => f a -> m
f f x
x
    go (S 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 (:.:) 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 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 proxy c
_ 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 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 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 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 proxy c
p 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 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 forall (y :: k) (ys :: [k]). f y -> r (y : ys)
z 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 f x
x) = f x -> r (x : xs)
forall (y :: k) (ys :: [k]). f y -> r (y : ys)
z f x
x
    go (S 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 proxy c
_ forall (y :: k) (ys :: [k]). c y => f y -> r (y : ys)
z 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 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 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 forall r. s '[] -> r
refute 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 proxy c
_ forall r. s '[] -> r
refute 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 SList ys
SNil  s ys
s = s '[] -> NS f ys
forall r. s '[] -> r
refute s ys
s '[]
s
    go SList ys
SCons 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 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 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 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 proxy c
p 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 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 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 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 proxy c
p 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 c
_ = 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 proxy c
_ forall (x :: k) (y :: k). c x y => f x -> g y
t (Z 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 proxy c
p forall (x :: k) (y :: k). c x y => f x -> g y
t (S 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 proxy c
p 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 c
_ = 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
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
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