functor-products (empty) → 0.1.0.0
raw patch · 7 files changed
+1349/−0 lines, 7 filesdep +basedep +microlensdep +singletonssetup-changed
Dependencies added: base, microlens, singletons, text, vinyl
Files
- CHANGELOG.md +11/−0
- LICENSE +30/−0
- README.md +7/−0
- Setup.hs +2/−0
- functor-products.cabal +48/−0
- src/Data/Type/Functor/Product.hs +1036/−0
- src/Data/Type/Functor/XProduct.hs +215/−0
+ CHANGELOG.md view
@@ -0,0 +1,11 @@+Changelog+=========++Version 0.1.0.0+---------------++*August 12, 2019*++<https://github.com/mstksg/functor-products/releases/tag/v0.1.0.0>++* Initial release
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Justin Le (c) 2019++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Justin Le nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,7 @@+# functor-products++Generalizes the `Rec` type in *[vinyl][]* to work over various different+`Foldable` instances, instead of just lists. Provides a unifying abstraction+for all of them, as well as data types to index into them.++[vinyl]: https://hackage.haskell.org/package/vinyl
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ functor-products.cabal view
@@ -0,0 +1,48 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 83a2a477a74fb1c07966f240f4ed4022f464195965fd7542022e0e4677e6a815++name: functor-products+version: 0.1.0.0+synopsis: General functor products for various Foldable instances+description: Generalizes the Rec type in vinyl to work over various different Foldable+ instances, instead of just lists. Provides a unifying abstraction for all+ of them, as well as data types to index into them.+category: Data+homepage: https://github.com/mstksg/functor-products#readme+bug-reports: https://github.com/mstksg/functor-products/issues+author: Justin Le+maintainer: justin@jle.im+copyright: (c) Justin Le 2019+license: BSD3+license-file: LICENSE+tested-with: GHC >= 8.6+build-type: Simple+extra-source-files:+ README.md+ CHANGELOG.md++source-repository head+ type: git+ location: https://github.com/mstksg/functor-products++library+ exposed-modules:+ Data.Type.Functor.Product+ Data.Type.Functor.XProduct+ other-modules:+ Paths_functor_products+ hs-source-dirs:+ src+ ghc-options: -Wall -Wcompat -Wredundant-constraints -Werror=incomplete-patterns+ build-depends:+ base >=4.7 && <5+ , microlens+ , singletons >=2.5+ , text+ , vinyl+ default-language: Haskell2010
+ src/Data/Type/Functor/Product.hs view
@@ -0,0 +1,1036 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module : Data.Type.Functor.Product+-- Copyright : (c) Justin Le 2018+-- License : BSD3+--+-- Maintainer : justin@jle.im+-- Stability : experimental+-- Portability : non-portable+--+-- Generalized functor products based on lifted 'Foldable's.+--+-- For example, @'Rec' f '[a,b,c]@ from /vinyl/ contains an @f a@, @f b@,+-- and @f c@.+--+-- @'PMaybe' f ('Just a)@ contains an @f a@ and @'PMaybe' f 'Nothing@+-- contains nothing.+--+-- Also provide data types for "indexing" into each foldable.++module Data.Type.Functor.Product (+ -- * Classes+ FProd(..), Shape+ , PureProd(..), pureShape+ , PureProdC(..), ReifyConstraintProd(..)+ , AllConstrainedProd+ -- ** Functions+ , indexProd, mapProd, foldMapProd, hmap, zipProd+ , imapProd, itraverseProd, ifoldMapProd+ , generateProd, generateProdA+ , selectProd, indices+ , eqProd, compareProd+ -- *** Over singletons+ , indexSing, singShape+ , foldMapSing, ifoldMapSing+ -- * Instances+ , Rec(..), Index(..), withPureProdList+ , PMaybe(..), IJust(..)+ , PEither(..), IRight(..)+ , NERec(..), NEIndex(..), withPureProdNE+ , PTup(..), ISnd(..)+ , PIdentity(..), IIdentity(..)+ , sameIndexVal, sameNEIndexVal+ -- ** Interfacing with vinyl+ , rElemIndex, indexRElem, toCoRec+ -- * Singletons+ , SIndex(..), SIJust(..), SIRight(..), SNEIndex(..), SISnd(..), SIIdentity(..)+ , Sing (SIndex', SIJust', SIRight', SNEIndex', SISnd', SIIdentity')+ -- * Defunctionalization symbols+ , ElemSym0, ElemSym1, ElemSym2+ , ProdSym0, ProdSym1, ProdSym2+ ) where++import Control.Applicative+import Data.Functor.Classes+import Data.Functor.Identity+import Data.Kind+import Data.List.NonEmpty (NonEmpty(..))+import Data.Maybe+import Data.Semigroup+import Data.Singletons+import Data.Singletons.Decide+import Data.Singletons.Prelude hiding (Elem, ElemSym0, ElemSym1, ElemSym2)+import Data.Singletons.Prelude.Foldable hiding (Elem, ElemSym0, ElemSym1, ElemSym2)+import Data.Singletons.Prelude.Identity+import Data.Vinyl hiding ((:~:))+import Data.Vinyl.CoRec+import GHC.Generics ((:*:)(..))+import Lens.Micro hiding ((%~))+import Lens.Micro.Extras+import Unsafe.Coerce+import qualified Data.Singletons.Prelude.List.NonEmpty as NE+import qualified Data.Text as T+import qualified Data.Vinyl.Functor as V+import qualified Data.Vinyl.TypeLevel as V++fmapIdent :: Fmap IdSym0 as :~: as+fmapIdent = unsafeCoerce Refl++-- | Simply witness the /shape/ of an argument (ie, @'Shape' [] as@+-- witnesses the length of @as@, and @'Shape' Maybe as@ witnesses whether+-- or not @as@ is 'Just' or 'Nothing').+type Shape f = (Prod f Proxy :: f k -> Type)++-- | Unify different functor products over a Foldable @f@.+class (PFunctor f, SFunctor f, PFoldable f, SFoldable f) => FProd (f :: Type -> Type) where+ type Elem f = (i :: f k -> k -> Type) | i -> f+ type Prod f = (p :: (k -> Type) -> f k -> Type) | p -> f++ -- | You can convert a singleton of a foldable value into a foldable product of+ -- singletons. This essentially "breaks up" the singleton into its+ -- individual items. Should be an inverse with 'prodSing'.+ singProd :: Sing as -> Prod f Sing as++ -- | Collect a collection of singletons back into a single singleton.+ -- Should be an inverse with 'singProd'.+ prodSing :: Prod f Sing as -> Sing as++ -- | Pair up each item in a foldable product with its index.+ withIndices+ :: Prod f g as+ -> Prod f (Elem f as :*: g) as++ -- | Traverse a foldable functor product with a RankN applicative function,+ -- mapping over each value and sequencing the effects.+ --+ -- This is the generalization of 'rtraverse'.+ traverseProd+ :: forall g h as m. Applicative m+ => (forall a. g a -> m (h a))+ -> Prod f g as+ -> m (Prod f h as)+ traverseProd = case fmapIdent @as of+ Refl -> htraverse (sing @IdSym0)++ -- | Zip together two foldable functor products with a Rank-N function.+ zipWithProd+ :: (forall a. g a -> h a -> j a)+ -> Prod f g as+ -> Prod f h as+ -> Prod f j as+ zipWithProd f xs ys = imapProd (\i x -> f x (indexProd i ys)) xs++ -- | Traverse a foldable functor product with a type-changing function.+ htraverse+ :: Applicative m+ => Sing ff+ -> (forall a. g a -> m (h (ff @@ a)))+ -> Prod f g as+ -> m (Prod f h (Fmap ff as))++ -- | A 'Lens' into an item in a foldable functor product, given its+ -- index.+ --+ -- This roughly generalizes 'rlens'.+ ixProd+ :: Elem f as a+ -> Lens' (Prod f g as) (g a)++ -- | Fold a functor product into a 'Rec'.+ toRec :: Prod f g as -> Rec g (ToList as)++ -- | Get a 'PureProd' instance from a foldable functor product+ -- providing its shape.+ withPureProd+ :: Prod f g as+ -> (PureProd f as => r)+ -> r++-- | Create @'Prod' f@ if you can give a @g a@ for every slot.+class PureProd (f :: Type -> Type) (as :: f k) where+ pureProd :: (forall a. g a) -> Prod f g as++-- | Create @'Prod' f@ if you can give a @g a@ for every slot, given some+-- constraint.+class PureProdC (f :: Type -> Type) c (as :: f k) where+ pureProdC :: (forall a. c a => g a) -> Prod f g as++-- | Pair up each item in a @'Prod' f@ with a witness that @f a@ satisfies+-- some constraint.+class ReifyConstraintProd (f :: Type -> Type) c (g :: k -> Type) (as :: f k) where+ reifyConstraintProd :: Prod f g as -> Prod f (Dict c V.:. g) as++data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type+data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type+type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a++type instance Apply (ElemSym0 f) as = ElemSym1 f as+type instance Apply (ElemSym1 f as) a = Elem f as a++data ProdSym0 (f :: Type -> Type) :: (k -> Type) ~> f k ~> Type+data ProdSym1 (f :: Type -> Type) :: (k -> Type) -> f k ~> Type+type ProdSym2 (f :: Type -> Type) (g :: k -> Type) (as :: f k) = Prod f g as++type instance Apply (ProdSym0 f) g = ProdSym1 f g+type instance Apply (ProdSym1 f g) as = Prod f g as++-- | A convenient wrapper over 'V.AllConstrained' that works for any+-- Foldable @f@.+type AllConstrainedProd c as = V.AllConstrained c (ToList as)++-- | Create a 'Shape' given an instance of 'PureProd'.+pureShape :: PureProd f as => Shape f as+pureShape = pureProd Proxy++-- | Generate a 'Prod' of indices for an @as@.+indices :: (FProd f, PureProd f as) => Prod f (Elem f as) as+indices = imapProd const pureShape++-- | Convert a @'Sing' as@ into a @'Shape' f as@, witnessing the shape of+-- of @as@ but dropping all of its values.+singShape+ :: FProd f+ => Sing as+ -> Shape f as+singShape = mapProd (const Proxy) . singProd++-- | Map a RankN function over a 'Prod'. The generalization of 'rmap'.+mapProd+ :: FProd f+ => (forall a. g a -> h a)+ -> Prod f g as+ -> Prod f h as+mapProd f = runIdentity . traverseProd (Identity . f)++-- | Zip together the values in two 'Prod's.+zipProd+ :: FProd f+ => Prod f g as+ -> Prod f h as+ -> Prod f (g :*: h) as+zipProd = zipWithProd (:*:)++-- | Map a type-changing function over every item in a 'Prod'.+hmap+ :: FProd f+ => Sing ff+ -> (forall a. g a -> h (ff @@ a))+ -> Prod f g as+ -> Prod f h (Fmap ff as)+hmap ff f = runIdentity . htraverse ff (Identity . f)++-- | 'mapProd', but with access to the index at each element.+imapProd+ :: FProd f+ => (forall a. Elem f as a -> g a -> h a)+ -> Prod f g as+ -> Prod f h as+imapProd f = mapProd (\(i :*: x) -> f i x) . withIndices++-- | Extract the item from the container witnessed by the 'Elem'+indexSing+ :: forall f as a. FProd f+ => Elem f as a -- ^ Witness+ -> Sing as -- ^ Collection+ -> Sing a+indexSing i = indexProd i . singProd++-- | Use an 'Elem' to index a value out of a 'Prod'.+indexProd+ :: FProd f+ => Elem f as a+ -> Prod f g as+ -> g a+indexProd i = view (ixProd i)++-- | 'traverseProd', but with access to the index at each element.+itraverseProd+ :: (FProd f, Applicative m)+ => (forall a. Elem f as a -> g a -> m (h a))+ -> Prod f g as+ -> m (Prod f h as)+itraverseProd f = traverseProd (\(i :*: x) -> f i x) . withIndices++-- | 'foldMapProd', but with access to the index at each element.+ifoldMapProd+ :: (FProd f, Monoid m)+ => (forall a. Elem f as a -> g a -> m)+ -> Prod f g as+ -> m+ifoldMapProd f = getConst . itraverseProd (\i -> Const . f i)++-- | Map a RankN function over a 'Prod' and collect the results as+-- a 'Monoid'.+foldMapProd+ :: (FProd f, Monoid m)+ => (forall a. g a -> m)+ -> Prod f g as+ -> m+foldMapProd f = ifoldMapProd (const f)++-- | 'foldMapSing' but with access to the index.+ifoldMapSing+ :: forall f k (as :: f k) m. (FProd f, Monoid m)+ => (forall a. Elem f as a -> Sing a -> m)+ -> Sing as+ -> m+ifoldMapSing f = ifoldMapProd f . singProd++-- | A 'foldMap' over all items in a collection.+foldMapSing+ :: forall f k (as :: f k) m. (FProd f, Monoid m)+ => (forall (a :: k). Sing a -> m)+ -> Sing as+ -> m+foldMapSing f = ifoldMapSing (const f)++-- | Rearrange or permute the items in a 'Prod' based on a 'Prod' of+-- indices.+--+-- @+-- 'selectProd' ('IS' 'IZ' ':&' IZ :& 'RNil') ("hi" :& "bye" :& "ok" :& RNil)+-- == "bye" :& "hi" :& RNil+-- @+selectProd+ :: FProd f+ => Prod f (Elem f as) bs+ -> Prod f g as+ -> Prod f g bs+selectProd is xs = mapProd (`indexProd` xs) is++-- | An implementation of equality testing for all 'FProd' instances, as+-- long as each of the items are instances of 'Eq'.+eqProd+ :: (FProd f, ReifyConstraintProd f Eq g as)+ => Prod f g as+ -> Prod f g as+ -> Bool+eqProd xs = getAll+ . foldMapProd getConst+ . zipWithProd (\(V.Compose (Dict x)) y -> Const (All (x == y)))+ (reifyConstraintProd @_ @Eq xs)++-- | An implementation of order comparison for all 'FProd' instances, as+-- long as each of the items are instances of 'Ord'.+compareProd+ :: (FProd f, ReifyConstraintProd f Ord g as)+ => Prod f g as+ -> Prod f g as+ -> Ordering+compareProd xs = foldMapProd getConst+ . zipWithProd (\(V.Compose (Dict x)) y -> Const (compare x y))+ (reifyConstraintProd @_ @Ord xs)++-- | Construct a 'Prod' purely by providing a generating function for each+-- index.+generateProd+ :: (FProd f, PureProd f as)+ => (forall a. Elem f as a -> g a)+ -> Prod f g as+generateProd f = mapProd f indices++-- | Construct a 'Prod' in an 'Applicative' context by providing+-- a generating function for each index.+generateProdA+ :: (FProd f, PureProd f as, Applicative m)+ => (forall a. Elem f as a -> m (g a))+ -> m (Prod f g as)+generateProdA f = traverseProd f indices+++-- | Witness an item in a type-level list by providing its index.+--+-- The number of 'IS's correspond to the item's position in the list.+--+-- @+-- 'IZ' :: 'Index' '[5,10,2] 5+-- 'IS' 'IZ' :: 'Index' '[5,10,2] 10+-- 'IS' ('IS' 'IZ') :: 'Index' '[5,10,2] 2+-- @+data Index :: [k] -> k -> Type where+ IZ :: Index (a ': as) a+ IS :: Index bs a -> Index (b ': bs) a++deriving instance Show (Index as a)+deriving instance Eq (Index as a)+deriving instance Ord (Index as a)++-- | Kind-indexed singleton for 'Index'. Provided as a separate data+-- declaration to allow you to use these at the type level. However, the+-- main interface is still provided through the newtype wrapper 'SIndex'',+-- which has an actual proper 'Sing' instance.+data SIndex as a :: Index as a -> Type where+ SIZ :: SIndex (a ': as) a 'IZ+ SIS :: SIndex bs a i -> SIndex (b ': bs) a ('IS i)++deriving instance Show (SIndex as a i)++newtype instance Sing (i :: Index as a) where+ SIndex' :: SIndex as a i -> Sing i++instance SingI 'IZ where+ sing = SIndex' SIZ++instance SingI i => SingI ('IS i) where+ sing = case sing of+ SIndex' i -> SIndex' (SIS i)++instance SingKind (Index as a) where+ type Demote (Index as a) = Index as a+ fromSing (SIndex' i) = go i+ where+ go :: SIndex bs b i -> Index bs b+ go = \case+ SIZ -> IZ+ SIS j -> IS (go j)+ toSing i = go i (SomeSing . SIndex')+ where+ go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r+ go = \case+ IZ -> ($ SIZ)+ IS j -> \f -> go j (f . SIS)++instance SDecide (Index as a) where+ SIndex' i %~ SIndex' j = go i j+ where+ go :: SIndex bs b i -> SIndex bs b j -> Decision (i :~: j)+ go = \case+ SIZ -> \case+ SIZ -> Proved Refl+ SIS _ -> Disproved $ \case {}+ SIS i' -> \case+ SIZ -> Disproved $ \case {}+ SIS j' -> case go i' j' of+ Proved Refl -> Proved Refl+ Disproved v -> Disproved $ \case Refl -> v Refl++instance FProd [] where+ type Elem [] = Index+ type Prod [] = Rec++ singProd = \case+ SNil -> RNil+ x `SCons` xs -> x :& singProd xs++ prodSing = \case+ RNil -> SNil+ x :& xs -> x `SCons` prodSing xs++ traverseProd+ :: forall g h m as. Applicative m+ => (forall a. g a -> m (h a))+ -> Prod [] g as+ -> m (Prod [] h as)+ traverseProd f = go+ where+ go :: Prod [] g bs -> m (Prod [] h bs)+ go = \case+ RNil -> pure RNil+ x :& xs -> (:&) <$> f x <*> go xs++ zipWithProd+ :: forall g h j as. ()+ => (forall a. g a -> h a -> j a)+ -> Prod [] g as+ -> Prod [] h as+ -> Prod [] j as+ zipWithProd f = go+ where+ go :: Prod [] g bs -> Prod [] h bs -> Prod [] j bs+ go = \case+ RNil -> \case+ RNil -> RNil+ x :& xs -> \case+ y :& ys -> f x y :& go xs ys++ htraverse+ :: forall ff g h as m. Applicative m+ => Sing ff+ -> (forall a. g a -> m (h (ff @@ a)))+ -> Prod [] g as+ -> m (Prod [] h (Fmap ff as))+ htraverse _ f = go+ where+ go :: Prod [] g bs -> m (Prod [] h (Fmap ff bs))+ go = \case+ RNil -> pure RNil+ x :& xs -> (:&) <$> f x <*> go xs++ withIndices = \case+ RNil -> RNil+ x :& xs -> (IZ :*: x) :& mapProd (\(i :*: y) -> IS i :*: y) (withIndices xs)++ ixProd+ :: forall g as a. ()+ => Elem [] as a+ -> Lens' (Prod [] g as) (g a)+ ixProd i0 (f :: g a -> h (g a)) = go i0+ where+ go :: Elem [] bs a -> Prod [] g bs -> h (Prod [] g bs)+ go = \case+ IZ -> \case+ x :& xs -> (:& xs) <$> f x+ IS i -> \case+ x :& xs -> (x :&) <$> go i xs++ toRec = id++ withPureProd = withPureProdList++-- | A stronger version of 'withPureProd' for 'Rec', providing+-- a 'RecApplicative' instance as well.+withPureProdList+ :: Rec f as+ -> ((RecApplicative as, PureProd [] as) => r)+ -> r+withPureProdList = \case+ RNil -> id+ _ :& xs -> withPureProdList xs++instance RecApplicative as => PureProd [] as where+ pureProd = rpure++instance RPureConstrained c as => PureProdC [] c as where+ pureProdC = rpureConstrained @c++instance ReifyConstraint c f as => ReifyConstraintProd [] c f as where+ reifyConstraintProd = reifyConstraint @c++-- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is+-- 'Just'.+data IJust :: Maybe k -> k -> Type where+ IJust :: IJust ('Just a) a++deriving instance Show (IJust as a)+deriving instance Read (IJust ('Just a) a)+deriving instance Eq (IJust as a)+deriving instance Ord (IJust as a)++-- | Kind-indexed singleton for 'IJust'. Provided as a separate data+-- declaration to allow you to use these at the type level. However, the+-- main interface is still provided through the newtype wrapper 'SIJust'',+-- which has an actual proper 'Sing' instance.+--+-- This distinction will be unnecessary once 'Sing' is a type family.+data SIJust as a :: IJust as a -> Type where+ SIJust :: SIJust ('Just a) a 'IJust++deriving instance Show (SIJust as a i)++newtype instance Sing (i :: IJust as a) where+ SIJust' :: SIJust as a i -> Sing i++instance SingI 'IJust where+ sing = SIJust' SIJust++instance SingKind (IJust as a) where+ type Demote (IJust as a) = IJust as a+ fromSing (SIJust' SIJust) = IJust+ toSing IJust = SomeSing (SIJust' SIJust)++instance SDecide (IJust as a) where+ SIJust' SIJust %~ SIJust' SIJust = Proved Refl++-- | A @'PMaybe' f 'Nothing@ contains nothing, and a @'PMaybe' f ('Just a)@+-- contains an @f a@.+--+-- In practice this can be useful to write polymorphic+-- functions/abstractions that contain an argument that can be "turned off"+-- for different instances.+data PMaybe :: (k -> Type) -> Maybe k -> Type where+ PNothing :: PMaybe f 'Nothing+ PJust :: f a -> PMaybe f ('Just a)++instance ReifyConstraintProd Maybe Show f as => Show (PMaybe f as) where+ showsPrec d xs = case reifyConstraintProd @_ @Show xs of+ PNothing -> showString "PNothing"+ PJust (V.Compose (Dict x)) -> showsUnaryWith showsPrec "PJust" d x+instance ReifyConstraintProd Maybe Eq f as => Eq (PMaybe f as) where+ (==) = eqProd+instance (ReifyConstraintProd Maybe Eq f as, ReifyConstraintProd Maybe Ord f as) => Ord (PMaybe f as) where+ compare = compareProd++instance FProd Maybe where+ type instance Elem Maybe = IJust+ type instance Prod Maybe = PMaybe++ singProd = \case+ SNothing -> PNothing+ SJust x -> PJust x+ prodSing = \case+ PNothing -> SNothing+ PJust x -> SJust x+ withIndices = \case+ PNothing -> PNothing+ PJust x -> PJust (IJust :*: x)+ traverseProd f = \case+ PNothing -> pure PNothing+ PJust x -> PJust <$> f x+ zipWithProd f = \case+ PNothing -> \case+ PNothing -> PNothing+ PJust x -> \case+ PJust y -> PJust (f x y)+ htraverse _ f = \case+ PNothing -> pure PNothing+ PJust x -> PJust <$> f x+ ixProd = \case+ IJust -> \f -> \case+ PJust x -> PJust <$> f x+ toRec = \case+ PNothing -> RNil+ PJust x -> x :& RNil+ withPureProd = \case+ PNothing -> id+ PJust _ -> id++instance PureProd Maybe 'Nothing where+ pureProd _ = PNothing+instance PureProd Maybe ('Just a) where+ pureProd x = PJust x++instance PureProdC Maybe c 'Nothing where+ pureProdC _ = PNothing+instance c a => PureProdC Maybe c ('Just a) where+ pureProdC x = PJust x++instance ReifyConstraintProd Maybe c g 'Nothing where+ reifyConstraintProd PNothing = PNothing+instance c (g a) => ReifyConstraintProd Maybe c g ('Just a) where+ reifyConstraintProd (PJust x) = PJust (V.Compose (Dict x))++-- | Witness an item in a type-level @'Either' j@ by proving the 'Either'+-- is 'Right'.+data IRight :: Either j k -> k -> Type where+ IRight :: IRight ('Right a) a++deriving instance Show (IRight as a)+deriving instance Read (IRight ('Right a) a)+deriving instance Eq (IRight as a)+deriving instance Ord (IRight as a)++-- | Kind-indexed singleton for 'IRight'. Provided as a separate data+-- declaration to allow you to use these at the type level. However, the+-- main interface is still provided through the newtype wrapper 'SIRight'',+-- which has an actual proper 'Sing' instance.+data SIRight as a :: IRight as a -> Type where+ SIRight :: SIRight ('Right a) a 'IRight++deriving instance Show (SIRight as a i)++newtype instance Sing (i :: IRight as a) where+ SIRight' :: SIRight as a i -> Sing i++instance SingI 'IRight where+ sing = SIRight' SIRight++instance SingKind (IRight as a) where+ type Demote (IRight as a) = IRight as a+ fromSing (SIRight' SIRight) = IRight+ toSing IRight = SomeSing (SIRight' SIRight)++instance SDecide (IRight as a) where+ SIRight' SIRight %~ SIRight' SIRight = Proved Refl++-- | A @'PEither' f ('Left e)@ contains @'Sing' e@, and a @'PMaybe' f ('Right a)@+-- contains an @f a@.+--+-- In practice this can be useful in the same situatinos that 'PMaybe' can,+-- but with an extra value in the case where value @f@ is "turned off" with+-- 'Left'.+data PEither :: (k -> Type) -> Either j k -> Type where+ PLeft :: Sing e -> PEither f ('Left e)+ PRight :: f a -> PEither f ('Right a)++instance (SShow j, ReifyConstraintProd (Either j) Show f as) => Show (PEither f as) where+ showsPrec d xs = case reifyConstraintProd @_ @Show xs of+ PLeft e -> showsUnaryWith go "PLeft" d e+ PRight (V.Compose (Dict x)) -> showsUnaryWith showsPrec "PRight" d x+ where+ go (fromIntegral->FromSing i) x (T.pack->FromSing str) = T.unpack . fromSing $ sShowsPrec i x str+ go _ _ _ = undefined++instance FProd (Either j) where+ type instance Elem (Either j) = IRight+ type instance Prod (Either j) = PEither++ singProd = \case+ SLeft e -> PLeft e+ SRight x -> PRight x+ prodSing = \case+ PLeft e -> SLeft e+ PRight x -> SRight x+ withIndices = \case+ PLeft e -> PLeft e+ PRight x -> PRight (IRight :*: x)+ traverseProd f = \case+ PLeft e -> pure (PLeft e)+ PRight x -> PRight <$> f x+ zipWithProd f = \case+ PLeft e -> \case+ PLeft _ -> PLeft e+ PRight x -> \case+ PRight y -> PRight (f x y)+ htraverse _ f = \case+ PLeft e -> pure (PLeft e)+ PRight x -> PRight <$> f x+ ixProd = \case+ IRight -> \f -> \case+ PRight x -> PRight <$> f x+ toRec = \case+ PLeft _ -> RNil+ PRight x -> x :& RNil+ withPureProd = \case+ PLeft Sing -> id+ PRight _ -> id++instance SingI e => PureProd (Either j) ('Left e) where+ pureProd _ = PLeft sing+instance PureProd (Either j) ('Right a) where+ pureProd x = PRight x++instance SingI e => PureProdC (Either j) c ('Left e) where+ pureProdC _ = (PLeft sing)+instance c a => PureProdC (Either j) c ('Right a) where+ pureProdC x = PRight x++instance ReifyConstraintProd (Either j) c g ('Left e) where+ reifyConstraintProd (PLeft e) = PLeft e+instance c (g a) => ReifyConstraintProd (Either j) c g ('Right a) where+ reifyConstraintProd (PRight x) = PRight (V.Compose (Dict x))++-- | Witness an item in a type-level 'NonEmpty' by either indicating that+-- it is the "head", or by providing an index in the "tail".+data NEIndex :: NonEmpty k -> k -> Type where+ NEHead :: NEIndex (a ':| as) a+ NETail :: Index as a -> NEIndex (b ':| as) a++deriving instance Show (NEIndex as a)+deriving instance Eq (NEIndex as a)+deriving instance Ord (NEIndex as a)++-- | Kind-indexed singleton for 'NEIndex'. Provided as a separate data+-- declaration to allow you to use these at the type level. However, the+-- main interface is still provided through the newtype wrapper+-- 'SNEIndex'', which has an actual proper 'Sing' instance.+data SNEIndex as a :: NEIndex as a -> Type where+ SNEHead :: SNEIndex (a ':| as) a 'NEHead+ SNETail :: SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)++deriving instance Show (SNEIndex as a i)++newtype instance Sing (i :: NEIndex as a) where+ SNEIndex' :: SNEIndex as a i -> Sing i++instance SingI 'NEHead where+ sing = SNEIndex' SNEHead++instance SingI i => SingI ('NETail i) where+ sing = case sing of+ SIndex' i -> SNEIndex' (SNETail i)++instance SingKind (NEIndex as a) where+ type Demote (NEIndex as a) = NEIndex as a+ fromSing = \case+ SNEIndex' SNEHead -> NEHead+ SNEIndex' (SNETail i) -> NETail $ fromSing (SIndex' i)+ toSing = \case+ NEHead -> SomeSing (SNEIndex' SNEHead)+ NETail i -> withSomeSing i $ \case+ SIndex' j -> SomeSing (SNEIndex' (SNETail j))++instance SDecide (NEIndex as a) where+ (%~) = \case+ SNEIndex' SNEHead -> \case+ SNEIndex' SNEHead -> Proved Refl+ SNEIndex' (SNETail _) -> Disproved $ \case {}+ SNEIndex' (SNETail i) -> \case+ SNEIndex' SNEHead -> Disproved $ \case {}+ SNEIndex' (SNETail j) -> case SIndex' i %~ SIndex' j of+ Proved Refl -> Proved Refl+ Disproved v -> Disproved $ \case Refl -> v Refl++-- | A non-empty version of 'Rec'.+data NERec :: (k -> Type) -> NonEmpty k -> Type where+ (:&|) :: f a -> Rec f as -> NERec f (a ':| as)+infixr 5 :&|++deriving instance (Show (f a), RMap as, ReifyConstraint Show f as, RecordToList as) => Show (NERec f (a ':| as))+deriving instance (Eq (f a), Eq (Rec f as)) => Eq (NERec f (a ':| as))+deriving instance (Ord (f a), Ord (Rec f as)) => Ord (NERec f (a ':| as))++instance FProd NonEmpty where+ type instance Elem NonEmpty = NEIndex+ type instance Prod NonEmpty = NERec++ singProd (x NE.:%| xs) = x :&| singProd xs+ prodSing (x :&| xs) = x NE.:%| prodSing xs+ withIndices (x :&| xs) =+ (NEHead :*: x)+ :&| mapProd (\(i :*: y) -> NETail i :*: y) (withIndices xs)+ traverseProd f (x :&| xs) =+ (:&|) <$> f x <*> traverseProd f xs+ zipWithProd f (x :&| xs) (y :&| ys) = f x y :&| zipWithProd f xs ys+ htraverse ff f (x :&| xs) =+ (:&|) <$> f x <*> htraverse ff f xs+ ixProd = \case+ NEHead -> \f -> \case+ x :&| xs -> (:&| xs) <$> f x+ NETail i -> \f -> \case+ x :&| xs -> (x :&|) <$> ixProd i f xs+ toRec (x :&| xs) = x :& xs+ withPureProd (x :&| xs) = withPureProdNE x xs++-- | A stronger version of 'withPureProd' for 'NERec', providing+-- a 'RecApplicative' instance as well.+withPureProdNE+ :: f a+ -> Rec f as+ -> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)+ -> r+withPureProdNE _ xs = withPureProdList xs++instance RecApplicative as => PureProd NonEmpty (a ':| as) where+ pureProd x = x :&| pureProd x++instance (c a, RPureConstrained c as) => PureProdC NonEmpty c (a ':| as) where+ pureProdC x = x :&| pureProdC @_ @c x++instance (c (g a), ReifyConstraint c g as) => ReifyConstraintProd NonEmpty c g (a ':| as) where+ reifyConstraintProd (x :&| xs) = V.Compose (Dict x)+ :&| reifyConstraintProd @_ @c xs++-- | Test if two indices point to the same item in a list.+--+-- We have to return a 'Maybe' here instead of a 'Decision', because it+-- might be the case that the same item might be duplicated in a list.+-- Therefore, even if two indices are different, we cannot prove that the+-- values they point to are different.+sameIndexVal+ :: Index as a+ -> Index as b+ -> Maybe (a :~: b)+sameIndexVal = \case+ IZ -> \case+ IZ -> Just Refl+ IS _ -> Nothing+ IS i -> \case+ IZ -> Nothing+ IS j -> sameIndexVal i j <&> \case Refl -> Refl+++-- | Test if two indices point to the same item in a non-empty list.+--+-- We have to return a 'Maybe' here instead of a 'Decision', because it+-- might be the case that the same item might be duplicated in a list.+-- Therefore, even if two indices are different, we cannot prove that the+-- values they point to are different.+sameNEIndexVal+ :: NEIndex as a+ -> NEIndex as b+ -> Maybe (a :~: b)+sameNEIndexVal = \case+ NEHead -> \case+ NEHead -> Just Refl+ NETail _ -> Nothing+ NETail i -> \case+ NEHead -> Nothing+ NETail j -> sameIndexVal i j <&> \case Refl -> Refl++-- | Trivially witness an item in the second field of a type-level tuple.+data ISnd :: (j, k) -> k -> Type where+ ISnd :: ISnd '(a, b) b++deriving instance Show (ISnd as a)+deriving instance Read (ISnd '(a, b) b)+deriving instance Eq (ISnd as a)+deriving instance Ord (ISnd as a)++-- | Kind-indexed singleton for 'ISnd'. Provided as a separate data+-- declaration to allow you to use these at the type level. However, the+-- main interface is still provided through the newtype wrapper 'SISnd'',+-- which has an actual proper 'Sing' instance.+data SISnd as a :: ISnd as a -> Type where+ SISnd :: SISnd '(a, b) b 'ISnd++deriving instance Show (SISnd as a i)++newtype instance Sing (i :: ISnd as a) where+ SISnd' :: SISnd as a i -> Sing i++instance SingI 'ISnd where+ sing = SISnd' SISnd++instance SingKind (ISnd as a) where+ type Demote (ISnd as a) = ISnd as a+ fromSing (SISnd' SISnd) = ISnd+ toSing ISnd = SomeSing (SISnd' SISnd)++instance SDecide (ISnd as a) where+ SISnd' SISnd %~ SISnd' SISnd = Proved Refl++-- | A 'PTup' tuples up some singleton with some value; a @'PTup' f '(w,+-- a)@ contains a @'Sing' w@ and an @f a@.+--+-- This can be useful for carrying along some witness aside a functor+-- value.+data PTup :: (k -> Type) -> (j, k) -> Type where+ PTup :: Sing w -> f a -> PTup f '(w, a)++deriving instance (Show (Sing w), Show (f a)) => Show (PTup f '(w, a))+deriving instance (Read (Sing w), Read (f a)) => Read (PTup f '(w, a))+deriving instance (Eq (Sing w), Eq (f a)) => Eq (PTup f '(w, a))+deriving instance (Ord (Sing w), Ord (f a)) => Ord (PTup f '(w, a))++instance FProd ((,) j) where+ type instance Elem ((,) j) = ISnd+ type instance Prod ((,) j) = PTup++ singProd (STuple2 w x) = PTup w x+ prodSing (PTup w x) = STuple2 w x+ withIndices (PTup w x) = PTup w (ISnd :*: x)+ traverseProd f (PTup w x) = PTup w <$> f x+ zipWithProd f (PTup w x) (PTup _ y) = PTup w (f x y)+ htraverse _ f (PTup w x) = PTup w <$> f x+ ixProd ISnd f (PTup w x) = PTup w <$> f x+ toRec (PTup _ x) = x :& RNil+ withPureProd (PTup Sing _) x = x++instance SingI w => PureProd ((,) j) '(w, a) where+ pureProd x = PTup sing x++instance (SingI w, c a) => PureProdC ((,) j) c '(w, a) where+ pureProdC x = PTup sing x++instance c (g a) => ReifyConstraintProd ((,) j) c g '(w, a) where+ reifyConstraintProd (PTup w x) = PTup w $ V.Compose (Dict x)++-- | Trivially witness the item held in an 'Identity'.+--+-- @since 0.1.3.0+data IIdentity :: Identity k -> k -> Type where+ IId :: IIdentity ('Identity x) x++deriving instance Show (IIdentity as a)+deriving instance Read (IIdentity ('Identity a) a)+deriving instance Eq (IIdentity as a)+deriving instance Ord (IIdentity as a)++-- | Kind-indexed singleton for 'IIdentity'. Provided as a separate data+-- declaration to allow you to use these at the type level. However, the+-- main interface is still provided through the newtype wrapper 'SIIdentity'',+-- which has an actual proper 'Sing' instance.+--+-- @since 0.1.5.0+data SIIdentity as a :: IIdentity as a -> Type where+ SIId :: SIIdentity ('Identity a) a 'IId++deriving instance Show (SIIdentity as a i)++newtype instance Sing (i :: IIdentity as a) where+ SIIdentity' :: SIIdentity as a i -> Sing i++instance SingI 'IId where+ sing = SIIdentity' SIId++instance SingKind (IIdentity as a) where+ type Demote (IIdentity as a) = IIdentity as a+ fromSing (SIIdentity' SIId) = IId+ toSing IId = SomeSing (SIIdentity' SIId)++instance SDecide (IIdentity as a) where+ SIIdentity' SIId %~ SIIdentity' SIId = Proved Refl++-- | A 'PIdentity' is a trivial functor product; it is simply the functor,+-- itself, alone. @'PIdentity' f ('Identity' a)@ is simply @f a@. This+-- may be useful in conjunction with other combinators.+data PIdentity :: (k -> Type) -> Identity k -> Type where+ PIdentity :: f a -> PIdentity f ('Identity a)++deriving instance Show (f a) => Show (PIdentity f ('Identity a))+deriving instance Read (f a) => Read (PIdentity f ('Identity a))+deriving instance Eq (f a) => Eq (PIdentity f ('Identity a))+deriving instance Ord (f a) => Ord (PIdentity f ('Identity a))++instance FProd Identity where+ type Elem Identity = IIdentity+ type Prod Identity = PIdentity++ singProd (SIdentity x) = PIdentity x+ prodSing (PIdentity x) = SIdentity x+ withIndices (PIdentity x) = PIdentity (IId :*: x)+ traverseProd f (PIdentity x) = PIdentity <$> f x+ zipWithProd f (PIdentity x) (PIdentity y) = PIdentity (f x y)+ htraverse _ f (PIdentity x) = PIdentity <$> f x+ ixProd IId f (PIdentity x) = PIdentity <$> f x+ toRec (PIdentity x) = x :& RNil+ withPureProd (PIdentity _) x = x++instance PureProd Identity ('Identity a) where+ pureProd x = PIdentity x++instance c a => PureProdC Identity c ('Identity a) where+ pureProdC x = PIdentity x++instance c (g a) => ReifyConstraintProd Identity c g ('Identity a) where+ reifyConstraintProd (PIdentity x) = PIdentity $ V.Compose (Dict x)++-- | Produce an 'Index' from an 'RElem' constraint.+rElemIndex+ :: forall r rs i. (RElem r rs i, PureProd [] rs)+ => Index rs r+rElemIndex = rgetC indices++-- | Use an 'Index' to inject an @f a@ into a 'CoRec'.+toCoRec+ :: forall as a f. (RecApplicative as, FoldRec as as)+ => Index as a+ -> f a+ -> CoRec f as+toCoRec = \case+ IZ -> CoRec+ IS i -> \x -> fromJust . firstField $ mapProd (go i x) indices+ where+ go :: Index bs a -> f a -> Index (b ': bs) c -> V.Compose Maybe f c+ go i x j = case sameIndexVal (IS i) j of+ Just Refl -> V.Compose (Just x)+ Nothing -> V.Compose Nothing++-- | If we have @'Index' as a@, we should also be able to create an item+-- that would require @'RElem' a as ('V.RIndex' as a)@. Along with+-- 'rElemIndex', this essentially converts between the indexing system in+-- this library and the indexing system of /vinyl/.+indexRElem+ :: (SDecide k, SingI (a :: k), RecApplicative as, FoldRec as as)+ => Index as a+ -> (RElem a as (V.RIndex a as) => r)+ -> r+indexRElem i = case toCoRec i x of+ CoRec y -> case x %~ y of+ Proved Refl -> id+ Disproved _ -> errorWithoutStackTrace "why :|"+ where+ x = sing
+ src/Data/Type/Functor/XProduct.hs view
@@ -0,0 +1,215 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}++-- |+-- Module : Data.Type.Functor.XProduct+-- Copyright : (c) Justin Le 2018+-- License : BSD3+--+-- Maintainer : justin@jle.im+-- Stability : experimental+-- Portability : non-portable+--+-- Generalize "Data.Vinyl.XRec": provides a version of products in+-- "Data.Type.Functor.Product" that "erases" newtype wrappers and other+-- syntactical noise.+--+-- "Data.Type.Functor.Product" is the "main functionality", but this module+-- provides an alternative interface that may be more convenient in some+-- situations, in the same way that 'XRec' can be more convenient than+-- 'Rec' in some situations.+--+module Data.Type.Functor.XProduct (+ XProd+ , fromXProd+ , toXProd+ -- * Functions+ , mapProdX, mapProdXEndo+ , imapProdX, zipWithProdX+ , ixProdX, traverseProdX, traverseProdXEndo, itraverseProdX+ , foldMapProdX, ifoldMapProdX+ -- * Instances+ , XRec, pattern (::&), pattern XRNil+ , XMaybe, pattern XNothing, pattern XJust+ , XEither, pattern XLeft, pattern XRight+ , XNERec, pattern (::&|)+ , XTup, pattern XTup+ , XIdentity, pattern XIdentity+ ) where++import Data.Functor.Identity+import Data.Kind+import Data.List.NonEmpty (NonEmpty(..))+import Data.Type.Functor.Product+import Data.Vinyl+import Data.Vinyl.XRec+import Lens.Micro+import qualified Data.Vinyl.Functor as V++-- | Generalize 'XRec' to work over any foldable @f@ that implements+-- 'FProd'. See 'Prod' and 'FProd' for more information.+type XProd f g = (Prod f (XData g) :: f k -> Type)++-- | Convert an 'XProd' back into a regular ol' 'Prod'.+fromXProd :: forall f g as. (FProd f, PureProdC f (IsoHKD g) as) => XProd f g as -> Prod f g as+fromXProd = zipWithProd (\(V.Lift u) x -> u x)+ (pureProdC @_ @(IsoHKD g) (V.Lift (unHKD . unX)))++-- | Convert a 'Prod' into a fancy 'XProd'.+toXProd :: forall f g as. (FProd f, PureProdC f (IsoHKD g) as) => Prod f g as -> XProd f g as+toXProd = zipWithProd (\(V.Lift u) x -> u x)+ (pureProdC @_ @(IsoHKD g) (V.Lift (XData . toHKD)))++-- | Convenient wrapper over 'mapProd' that lets you deal with the+-- "simplified" inner types. Generalizes 'rmapX'.+mapProdX+ :: forall f g h as. FProd f+ => (forall a. HKD g a -> HKD h a)+ -> XProd f g as+ -> XProd f h as+mapProdX f = mapProd $ \(XData x :: XData g a) -> XData (f @a x)++-- | A version of 'mapProdX' that doesn't change the context @g@; this can+-- be easier for type inference in some situations. Generalizes+-- 'rmapXEndo'.+mapProdXEndo+ :: forall f g as. FProd f+ => (forall a. HKD g a -> HKD g a)+ -> XProd f g as+ -> XProd f g as+mapProdXEndo f = mapProd $ \(XData x :: XData g a) -> XData (f @a x)++-- | A version of 'mapProdX' that passes along the index 'Elem' with each+-- value. This can help with type inference in some situations.+imapProdX+ :: forall f g h as. FProd f+ => (forall a. Elem f as a -> HKD g a -> HKD h a)+ -> XProd f g as+ -> XProd f h as+imapProdX f = imapProd $ \i -> XData . f i . unX++-- | Zip two 'XProd's together by supplying a function that works on their+-- simplified 'HKD' values.+zipWithProdX+ :: forall f g h j as. FProd f+ => (forall a. HKD g a -> HKD h a -> HKD j a)+ -> XProd f g as+ -> XProd f h as+ -> XProd f j as+zipWithProdX f = zipWithProd $ \(XData x :: XData g a) (XData y) -> XData (f @a x y)++-- | Given an index into an 'XProd', provides a lens into the simplified+-- item that that index points to.+ixProdX+ :: FProd f+ => Elem f as a+ -> Lens' (XProd f g as) (HKD g a)+ixProdX i = ixProd i . (\f (XData x) -> XData <$> f x)++-- | Convenient wrapper over 'traverseProd' that lets you deal with the+-- "simplified" inner types.+traverseProdX+ :: forall f g h m as. (FProd f, Applicative m)+ => (forall a. HKD g a -> m (HKD h a))+ -> XProd f g as+ -> m (XProd f h as)+traverseProdX f = traverseProd $ \(XData x :: XData g a) -> XData <$> f @a x++-- | A version of 'traverseProdX' that doesn't change the context @g@; this can+-- be easier for type inference in some situations.+traverseProdXEndo+ :: forall f g m as. (FProd f, Applicative m)+ => (forall a. HKD g a -> m (HKD g a))+ -> XProd f g as+ -> m (XProd f g as)+traverseProdXEndo f = traverseProd $ \(XData x :: XData g a) -> XData <$> f @a x++-- | A version of 'traverseProdX' that passes along the index 'Elem' with+-- each value. This can help with type inference in some situations.+itraverseProdX+ :: forall f g h m as. (FProd f, Applicative m)+ => (forall a. Elem f as a -> HKD g a -> m (HKD h a))+ -> XProd f g as+ -> m (XProd f h as)+itraverseProdX f = itraverseProd $ \i -> fmap XData . f i . unX++-- | Convenient wrapper over 'foldMapProd' that lets you deal with the+-- "simplified" inner types.+foldMapProdX+ :: forall f g m as. (FProd f, Monoid m)+ => (forall a. HKD g a -> m)+ -> XProd f g as+ -> m+foldMapProdX f = foldMapProd $ \(XData x :: XData g a) -> f @a x++-- | A version of 'foldMapProdX' that passes along the index 'Elem' with+-- each value. This can help with type inference in some situations.+ifoldMapProdX+ :: forall f g m as. (FProd f, Monoid m)+ => (forall a. Elem f as a -> HKD g a -> m)+ -> XProd f g as+ -> m+ifoldMapProdX f = ifoldMapProd $ \i -> f i . unX++-- | 'PMaybe' over 'HKD'-d types.+type XMaybe f = PMaybe (XData f)++-- | 'PEither' over 'HKD'-d types.+type XEither f = PEither (XData f)++-- | 'NERec' over 'HKD'-d types.+type XNERec f = NERec (XData f)++-- | 'PTup' over 'HKD'-d types.+type XTup f = PTup (XData f)++-- | 'PIdentity' over 'HKD'-d types.+type XIdentity f = PIdentity (XData f)++-- | 'PNothing' for 'XMaybe'.+pattern XNothing :: XMaybe f 'Nothing+pattern XNothing = PNothing++-- | 'PJust' for 'XMaybe': allows you to provide the simplified type.+pattern XJust :: HKD f a -> XMaybe f ('Just a)+pattern XJust x = PJust (XData x)++-- | 'PLeft' for 'XEither'.+pattern XLeft :: Sing e -> XEither f ('Left e)+pattern XLeft e = PLeft e++-- | 'PRight' for 'XEither': allows you to provide the simplified type.+pattern XRight :: HKD f a -> XEither f ('Right a)+pattern XRight x = PRight (XData x)++-- | A version of ':&|' that allows you to provide the simplified type, for+-- 'XNERec'.+pattern (::&|) :: HKD f a -> XRec f as -> XNERec f (a ':| as)+pattern x ::&| xs = XData x :&| xs++-- | A version of 'PTup' that allows you to provide the simplified type,+-- for 'XTup'.+pattern XTup :: Sing w -> HKD f a -> XTup f '(w, a)+pattern XTup w x = PTup w (XData x)++-- | A version of 'PIdentity' that allows you to provide the simplified+-- type, for 'XIdentity'.+pattern XIdentity :: HKD f a -> XIdentity f ('Identity a)+pattern XIdentity x = PIdentity (XData x)++{-# COMPLETE (::&|) #-}+{-# COMPLETE XIdentity #-}+{-# COMPLETE XJust #-}+{-# COMPLETE XLeft #-}+{-# COMPLETE XNothing #-}+{-# COMPLETE XRight #-}+{-# COMPLETE XTup #-}+