{-# 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(..)
-- * 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 as 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 c as 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 c g as 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'.
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)
type instance Sing = SIndex as a :: Index as a -> Type
instance SingI 'IZ where
sing = SIZ
instance SingI i => SingI ('IS i) where
sing = SIS sing
instance SingKind (Index as a) where
type Demote (Index as a) = Index as a
fromSing = \case
SIZ -> IZ
SIS j -> IS (fromSing j)
toSing i = go i SomeSing
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
(%~) = \case
SIZ -> \case
SIZ -> Proved Refl
SIS _ -> Disproved $ \case {}
SIS i' -> \case
SIZ -> Disproved $ \case {}
SIS j' -> case 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'.
data SIJust as a :: IJust as a -> Type where
SIJust :: SIJust ('Just a) a 'IJust
deriving instance Show (SIJust as a i)
type instance Sing = SIJust as a :: IJust as a -> Type
instance SingI 'IJust where
sing = SIJust
instance SingKind (IJust as a) where
type Demote (IJust as a) = IJust as a
fromSing SIJust = IJust
toSing IJust = SomeSing SIJust
instance SDecide (IJust as a) where
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'.
data SIRight as a :: IRight as a -> Type where
SIRight :: SIRight ('Right a) a 'IRight
deriving instance Show (SIRight as a i)
type instance Sing = SIRight as a :: IRight as a -> Type
instance SingI 'IRight where
sing = SIRight
instance SingKind (IRight as a) where
type Demote (IRight as a) = IRight as a
fromSing SIRight = IRight
toSing IRight = SomeSing SIRight
instance SDecide (IRight as a) where
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'.
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)
type instance Sing = SNEIndex as a :: NEIndex as a -> Type
instance SingI 'NEHead where
sing = SNEHead
instance SingI i => SingI ('NETail i) where
sing = SNETail sing
instance SingKind (NEIndex as a) where
type Demote (NEIndex as a) = NEIndex as a
fromSing = \case
SNEHead -> NEHead
SNETail i -> NETail $ fromSing i
toSing = \case
NEHead -> SomeSing SNEHead
NETail i -> withSomeSing i $ SomeSing . SNETail
instance SDecide (NEIndex as a) where
(%~) = \case
SNEHead -> \case
SNEHead -> Proved Refl
SNETail _ -> Disproved $ \case {}
SNETail i -> \case
SNEHead -> Disproved $ \case {}
SNETail j -> case i %~ 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'.
data SISnd as a :: ISnd as a -> Type where
SISnd :: SISnd '(a, b) b 'ISnd
deriving instance Show (SISnd as a i)
type instance Sing = SISnd as a :: ISnd as a -> Type
instance SingI 'ISnd where
sing = SISnd
instance SingKind (ISnd as a) where
type Demote (ISnd as a) = ISnd as a
fromSing SISnd = ISnd
toSing ISnd = SomeSing SISnd
instance SDecide (ISnd as a) where
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'.
--
-- @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)
type instance Sing = SIIdentity as a :: IIdentity as a -> Type
instance SingI 'IId where
sing = SIId
instance SingKind (IIdentity as a) where
type Demote (IIdentity as a) = IIdentity as a
fromSing SIId = IId
toSing IId = SomeSing SIId
instance SDecide (IIdentity as a) where
SIId %~ 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