diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,11 @@ +Changelog +========= + +Version 0.1.0.0 +--------------- + +*August 12, 2019* + + + +* Initial release diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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 diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/functor-products.cabal b/functor-products.cabal new file mode 100644 --- /dev/null +++ b/functor-products.cabal @@ -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 diff --git a/src/Data/Type/Functor/Product.hs b/src/Data/Type/Functor/Product.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Functor/Product.hs @@ -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 diff --git a/src/Data/Type/Functor/XProduct.hs b/src/Data/Type/Functor/XProduct.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Functor/XProduct.hs @@ -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 #-} +