{-# 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 (
FProd(..), Shape
, PureProd(..), pureShape
, PureProdC(..), ReifyConstraintProd(..)
, AllConstrainedProd
, indexProd, mapProd, foldMapProd, hmap, zipProd
, imapProd, itraverseProd, ifoldMapProd
, generateProd, generateProdA
, selectProd, indices
, eqProd, compareProd
, indexSing, singShape
, foldMapSing, ifoldMapSing
, Rec(..), Index(..), withPureProdList
, PMaybe(..), IJust(..)
, PEither(..), IRight(..)
, NERec(..), NEIndex(..), withPureProdNE
, PTup(..), ISnd(..)
, PIdentity(..), IIdentity(..)
, sameIndexVal, sameNEIndexVal
, rElemIndex, indexRElem, toCoRec
, SIndex(..), SIJust(..), SIRight(..), SNEIndex(..), SISnd(..), SIIdentity(..)
, ElemSym0, ElemSym1, ElemSym2
, ProdSym0, ProdSym1, ProdSym2
) where
import Control.Applicative
import Data.Either.Singletons
import Data.Foldable.Singletons hiding (Elem, ElemSym0, ElemSym1, ElemSym2)
import Data.Function.Singletons
import Data.Functor.Classes
import Data.Functor.Identity
import Data.Functor.Identity.Singletons
import Data.Functor.Singletons
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
import Data.List.Singletons hiding (Elem, ElemSym0, ElemSym1, ElemSym2)
import Data.Maybe
import Data.Maybe.Singletons
import Data.Semigroup
import Data.Singletons
import Data.Singletons.Decide
import Data.Tuple.Singletons
import Data.Vinyl hiding ((:~:))
import Data.Vinyl.CoRec
import GHC.Generics ((:*:)(..))
import Lens.Micro hiding ((%~))
import Lens.Micro.Extras
import Text.Show.Singletons
import Unsafe.Coerce
import qualified Data.List.NonEmpty.Singletons 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 :: forall {f :: * -> *} {b} (as :: f b). Fmap IdSym0 as :~: as
fmapIdent = forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl
type Shape f = (Prod f Proxy :: f k -> Type)
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
singProd :: Sing as -> Prod f Sing as
prodSing :: Prod f Sing as -> Sing as
withIndices
:: Prod f g as
-> Prod f (Elem f as :*: g) as
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 forall {f :: * -> *} {b} (as :: f b). Fmap IdSym0 as :~: as
fmapIdent @as of
Fmap IdSym0 as :~: as
Refl -> forall (f :: * -> *) {a} {k} (m :: * -> *) (ff :: a ~> k)
(g :: a -> *) (h :: k -> *) (as :: f a).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse (forall {k} (a :: k). SingI a => Sing a
sing @IdSym0)
zipWithProd
:: (forall a. g a -> h a -> j a)
-> Prod f g as
-> Prod f h as
-> Prod f j as
zipWithProd forall (a :: k). g a -> h a -> j a
f Prod f g as
xs Prod f h as
ys = forall {k} (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd (\Elem f as a
i g a
x -> forall (a :: k). g a -> h a -> j a
f g a
x (forall {k} (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
indexProd Elem f as a
i Prod f h as
ys)) Prod f g as
xs
htraverse
:: Applicative m
=> Sing ff
-> (forall a. g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
ixProd
:: Elem f as a
-> Lens' (Prod f g as) (g a)
toRec :: Prod f g as -> Rec g (ToList as)
withPureProd
:: Prod f g as
-> (PureProd f as => r)
-> r
class PureProd f as where
pureProd :: (forall a. g a) -> Prod f g as
class PureProdC f c as where
pureProdC :: (forall a. c a => g a) -> Prod f g as
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
type AllConstrainedProd c as = V.AllConstrained c (ToList as)
pureShape :: PureProd f as => Shape f as
pureShape :: forall {k} (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape = forall {k} (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
pureProd forall {k} (t :: k). Proxy t
Proxy
indices :: (FProd f, PureProd f as) => Prod f (Elem f as) as
indices :: forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices = forall {k} (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd forall a b. a -> b -> a
const forall {k} (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape
singShape
:: FProd f
=> Sing as
-> Shape f as
singShape :: forall {k} (f :: * -> *) (as :: f k).
FProd f =>
Sing as -> Shape f as
singShape = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall a b. a -> b -> a
const forall {k} (t :: k). Proxy t
Proxy) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
mapProd
:: FProd f
=> (forall a. g a -> h a)
-> Prod f g as
-> Prod f h as
mapProd :: forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). g a -> h a
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
(m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). g a -> h a
f)
zipProd
:: FProd f
=> Prod f g as
-> Prod f h as
-> Prod f (g :*: h) as
zipProd :: forall {k} (f :: * -> *) (g :: k -> *) (as :: f k) (h :: k -> *).
FProd f =>
Prod f g as -> Prod f h as -> Prod f (g :*: h) as
zipProd = forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)
hmap
:: FProd f
=> Sing ff
-> (forall a. g a -> h (ff @@ a))
-> Prod f g as
-> Prod f h (Fmap ff as)
hmap :: forall {a} {k} (f :: * -> *) (ff :: a ~> k) (g :: a -> *)
(h :: k -> *) (as :: f a).
FProd f =>
Sing ff
-> (forall (a :: a). g a -> h (ff @@ a))
-> Prod f g as
-> Prod f h (Fmap ff as)
hmap Sing ff
ff forall (a :: a). g a -> h (ff @@ a)
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {a} {k} (m :: * -> *) (ff :: a ~> k)
(g :: a -> *) (h :: k -> *) (as :: f a).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse Sing ff
ff (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: a). g a -> h (ff @@ a)
f)
imapProd
:: FProd f
=> (forall a. Elem f as a -> g a -> h a)
-> Prod f g as
-> Prod f h as
imapProd :: forall {k} (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd forall (a :: k). Elem f as a -> g a -> h a
f = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (\(Elem f as a
i :*: g a
x) -> forall (a :: k). Elem f as a -> g a -> h a
f Elem f as a
i g a
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices
indexSing
:: forall f as a. FProd f
=> Elem f as a
-> Sing as
-> Sing a
indexSing :: forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f as a
i = forall {k} (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
indexProd Elem f as a
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
indexProd
:: FProd f
=> Elem f as a
-> Prod f g as
-> g a
indexProd :: forall {k} (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
indexProd Elem f as a
i = forall a s. Getting a s a -> s -> a
view (forall (f :: * -> *) {k} (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Lens' (Prod f g as) (g a)
ixProd Elem f as a
i)
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 :: forall {k} (f :: * -> *) (m :: * -> *) (as :: f k) (g :: k -> *)
(h :: k -> *).
(FProd f, Applicative m) =>
(forall (a :: k). Elem f as a -> g a -> m (h a))
-> Prod f g as -> m (Prod f h as)
itraverseProd forall (a :: k). Elem f as a -> g a -> m (h a)
f = forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
(m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd (\(Elem f as a
i :*: g a
x) -> forall (a :: k). Elem f as a -> g a -> m (h a)
f Elem f as a
i g a
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices
ifoldMapProd
:: (FProd f, Monoid m)
=> (forall a. Elem f as a -> g a -> m)
-> Prod f g as
-> m
ifoldMapProd :: forall {k} (f :: * -> *) m (as :: f k) (g :: k -> *).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd forall (a :: k). Elem f as a -> g a -> m
f = forall {k} a (b :: k). Const a b -> a
getConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: * -> *) (m :: * -> *) (as :: f k) (g :: k -> *)
(h :: k -> *).
(FProd f, Applicative m) =>
(forall (a :: k). Elem f as a -> g a -> m (h a))
-> Prod f g as -> m (Prod f h as)
itraverseProd (\Elem f as a
i -> forall {k} a (b :: k). a -> Const a b
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). Elem f as a -> g a -> m
f Elem f as a
i)
foldMapProd
:: (FProd f, Monoid m)
=> (forall a. g a -> m)
-> Prod f g as
-> m
foldMapProd :: forall {k} (f :: * -> *) m (g :: k -> *) (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd forall (a :: k). g a -> m
f = forall {k} (f :: * -> *) m (as :: f k) (g :: k -> *).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd (forall a b. a -> b -> a
const forall (a :: k). g a -> m
f)
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 :: forall (f :: * -> *) k (as :: f k) m.
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
ifoldMapSing forall (a :: k). Elem f as a -> Sing a -> m
f = forall {k} (f :: * -> *) m (as :: f k) (g :: k -> *).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd forall (a :: k). Elem f as a -> Sing a -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
foldMapSing
:: forall f k (as :: f k) m. (FProd f, Monoid m)
=> (forall (a :: k). Sing a -> m)
-> Sing as
-> m
foldMapSing :: forall (f :: * -> *) k (as :: f k) m.
(FProd f, Monoid m) =>
(forall (a :: k). Sing a -> m) -> Sing as -> m
foldMapSing forall (a :: k). Sing a -> m
f = forall (f :: * -> *) k (as :: f k) m.
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
ifoldMapSing (forall a b. a -> b -> a
const forall (a :: k). Sing a -> m
f)
selectProd
:: FProd f
=> Prod f (Elem f as) bs
-> Prod f g as
-> Prod f g bs
selectProd :: forall {k} (f :: * -> *) (as :: f k) (bs :: f k) (g :: k -> *).
FProd f =>
Prod f (Elem f as) bs -> Prod f g as -> Prod f g bs
selectProd Prod f (Elem f as) bs
is Prod f g as
xs = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall {k} (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
`indexProd` Prod f g as
xs) Prod f (Elem f as) bs
is
eqProd
:: (FProd f, ReifyConstraintProd f Eq g as)
=> Prod f g as
-> Prod f g as
-> Bool
eqProd :: forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Eq g as) =>
Prod f g as -> Prod f g as -> Bool
eqProd Prod f g as
xs = All -> Bool
getAll
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: * -> *) m (g :: k -> *) (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd forall {k} a (b :: k). Const a b -> a
getConst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd (\(V.Compose (Dict g a
x)) g a
y -> forall {k} a (b :: k). a -> Const a b
Const (Bool -> All
All (g a
x forall a. Eq a => a -> a -> Bool
== g a
y)))
(forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Eq Prod f g as
xs)
compareProd
:: (FProd f, ReifyConstraintProd f Ord g as)
=> Prod f g as
-> Prod f g as
-> Ordering
compareProd :: forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Ord g as) =>
Prod f g as -> Prod f g as -> Ordering
compareProd Prod f g as
xs = forall {k} (f :: * -> *) m (g :: k -> *) (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd forall {k} a (b :: k). Const a b -> a
getConst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd (\(V.Compose (Dict g a
x)) g a
y -> forall {k} a (b :: k). a -> Const a b
Const (forall a. Ord a => a -> a -> Ordering
compare g a
x g a
y))
(forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Ord Prod f g as
xs)
generateProd
:: (FProd f, PureProd f as)
=> (forall a. Elem f as a -> g a)
-> Prod f g as
generateProd :: forall {k} (f :: * -> *) (as :: f k) (g :: k -> *).
(FProd f, PureProd f as) =>
(forall (a :: k). Elem f as a -> g a) -> Prod f g as
generateProd forall (a :: k). Elem f as a -> g a
f = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). Elem f as a -> g a
f forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices
generateProdA
:: (FProd f, PureProd f as, Applicative m)
=> (forall a. Elem f as a -> m (g a))
-> m (Prod f g as)
generateProdA :: forall {k} (f :: * -> *) (as :: f k) (m :: * -> *) (g :: k -> *).
(FProd f, PureProd f as, Applicative m) =>
(forall (a :: k). Elem f as a -> m (g a)) -> m (Prod f g as)
generateProdA forall (a :: k). Elem f as a -> m (g a)
f = forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
(m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd forall (a :: k). Elem f as a -> m (g a)
f forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices
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)
data SIndex (as :: [k]) (a :: k) :: 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 :: Sing 'IZ
sing = forall {k} (a :: k) (a :: [k]). SIndex (a : a) a 'IZ
SIZ
instance SingI i => SingI ('IS i) where
sing :: Sing ('IS i)
sing = forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SIndex (b : a) a ('IS a)
SIS forall {k} (a :: k). SingI a => Sing a
sing
instance SingKind (Index as a) where
type Demote (Index as a) = Index as a
fromSing :: forall (a :: Index as a). Sing a -> Demote (Index as a)
fromSing = \case
Sing a
SIndex as a a
SIZ -> forall {k} (a :: k) (a :: [k]). Index (a : a) a
IZ
SIS SIndex bs a i
j -> forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) a
IS (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing SIndex bs a i
j)
toSing :: Demote (Index as a) -> SomeSing (Index as a)
toSing Demote (Index as a)
i = forall {k} (bs :: [k]) (b :: k) r.
Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
go Demote (Index as a)
i forall k (a :: k). Sing a -> SomeSing k
SomeSing
where
go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r
go :: forall {k} (bs :: [k]) (b :: k) r.
Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
go = \case
Index bs b
IZ -> (forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k) (a :: [k]). SIndex (a : a) a 'IZ
SIZ)
IS Index bs b
j -> \forall (i :: Index bs b). SIndex bs b i -> r
f -> forall {k} (bs :: [k]) (b :: k) r.
Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
go Index bs b
j (forall (i :: Index bs b). SIndex bs b i -> r
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SIndex (b : a) a ('IS a)
SIS)
instance SDecide (Index as a) where
%~ :: forall (a :: Index as a) (b :: Index as a).
Sing a -> Sing b -> Decision (a :~: b)
(%~) = \case
Sing a
SIndex as a a
SIZ -> \case
Sing b
SIndex (a : as) a b
SIZ -> forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
SIS SIndex bs a i
_ -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
SIS SIndex bs a i
i' -> \case
Sing b
SIndex (b : bs) a b
SIZ -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
SIS SIndex bs a i
j' -> case SIndex bs a i
i' forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SIndex bs a i
j' of
Proved i :~: i
Refl -> forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
Disproved Refuted (i :~: i)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case a :~: b
Refl -> Refuted (i :~: i)
v forall {k} (a :: k). a :~: a
Refl
instance FProd [] where
type Elem [] = Index
type Prod [] = Rec
singProd :: forall {k} (as :: [k]). Sing as -> Prod [] Sing as
singProd = \case
Sing as
SList as
SNil -> forall {u} (a :: u -> *). Rec a '[]
RNil
Sing n1
x `SCons` Sing n2
xs -> Sing n1
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd Sing n2
xs
prodSing :: forall {k} (as :: [k]). Prod [] Sing as -> Sing as
prodSing = \case
Rec Sing as
Prod [] Sing as
RNil -> forall a. SList '[]
SNil
Sing r
x :& Rec Sing rs
xs -> Sing r
x forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> SList (n1 : n2)
`SCons` forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing rs
xs
traverseProd
:: forall g h m as. Applicative m
=> (forall a. g a -> m (h a))
-> Prod [] g as
-> m (Prod [] h as)
traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (m :: * -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod [] g as -> m (Prod [] h as)
traverseProd forall (a :: k). g a -> m (h a)
f = forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go
where
go :: Prod [] g bs -> m (Prod [] h bs)
go :: forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go = \case
Rec g bs
Prod [] g bs
RNil -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {u} (a :: u -> *). Rec a '[]
RNil
g r
x :& Rec g rs
xs -> forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g r
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go Rec g rs
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 :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: [k]).
(forall (a :: k). g a -> h a -> j a)
-> Prod [] g as -> Prod [] h as -> Prod [] j as
zipWithProd forall (a :: k). g a -> h a -> j a
f = forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go
where
go :: Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go :: forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go = \case
Rec g bs
Prod [] g bs
RNil -> \case
Rec h '[]
Prod [] h bs
RNil -> forall {u} (a :: u -> *). Rec a '[]
RNil
g r
x :& Rec g rs
xs -> \case
h r
y :& Rec h rs
ys -> forall (a :: k). g a -> h a -> j a
f g r
x h r
y forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go Rec g rs
xs Rec h rs
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 :: forall {a} {k} (ff :: a ~> k) (g :: a -> *) (h :: k -> *)
(as :: [a]) (m :: * -> *).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f = forall (bs :: [a]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go
where
go :: Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go :: forall (bs :: [a]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go = \case
Rec g bs
Prod [] g bs
RNil -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {u} (a :: u -> *). Rec a '[]
RNil
g r
x :& Rec g rs
xs -> forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g r
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (bs :: [a]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go Rec g rs
xs
withIndices :: forall {k} (g :: k -> *) (as :: [k]).
Prod [] g as -> Prod [] (Elem [] as :*: g) as
withIndices = \case
Rec g as
Prod [] g as
RNil -> forall {u} (a :: u -> *). Rec a '[]
RNil
g r
x :& Rec g rs
xs -> (forall {k} (a :: k) (a :: [k]). Index (a : a) a
IZ forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g r
x) forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (\(Index rs a
i :*: g a
y) -> forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) a
IS Index rs a
i forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (forall (f :: * -> *) {k} (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices Rec g rs
xs)
ixProd
:: forall g as a. ()
=> Elem [] as a
-> Lens' (Prod [] g as) (g a)
ixProd :: forall {k} (g :: k -> *) (as :: [k]) (a :: k).
Elem [] as a -> Lens' (Prod [] g as) (g a)
ixProd Elem [] as a
i0 (g a -> f (g a)
f :: g a -> h (g a)) = forall (bs :: [k]).
Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go Elem [] as a
i0
where
go :: Elem [] bs a -> Prod [] g bs -> h (Prod [] g bs)
go :: forall (bs :: [k]).
Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go = \case
Index bs a
Elem [] bs a
IZ -> \case
g r
x :& Rec g rs
xs -> (forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g rs
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g r
x
IS Index bs a
i -> \case
g r
x :& Rec g rs
xs -> (g r
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (bs :: [k]).
Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go Index bs a
i Rec g rs
xs
toRec :: forall {a} (g :: a -> *) (as :: [a]).
Prod [] g as -> Rec g (ToList as)
toRec = forall a. a -> a
id
withPureProd :: forall {k} (g :: k -> *) (as :: [k]) r.
Prod [] g as -> (PureProd [] as => r) -> r
withPureProd = forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList
withPureProdList
:: Rec f as
-> ((RecApplicative as, PureProd [] as) => r)
-> r
withPureProdList :: forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList = \case
Rec f as
RNil -> forall a. a -> a
id
f r
_ :& Rec f rs
xs -> forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList Rec f rs
xs
instance RecApplicative as => PureProd [] as where
pureProd :: forall (g :: k -> *). (forall (a :: k). g a) -> Prod [] g as
pureProd = forall {u} (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure
instance RPureConstrained c as => PureProdC [] c as where
pureProdC :: forall (g :: k -> *). (forall (a :: k). c a => g a) -> Prod [] g as
pureProdC = forall {k} (c :: k -> Constraint) (ts :: [k]) (f :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). c a => f a) -> Rec f ts
rpureConstrained @c
instance ReifyConstraint c f as => ReifyConstraintProd [] c f as where
reifyConstraintProd :: Prod [] f as -> Prod [] (Dict c :. f) as
reifyConstraintProd = forall {u} (c :: * -> Constraint) (f :: u -> *) (rs :: [u]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
reifyConstraint @c
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)
data SIJust (as :: Maybe k) (a :: k) :: 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 :: Sing 'IJust
sing = forall {k} (a :: k). SIJust ('Just a) a 'IJust
SIJust
instance SingKind (IJust as a) where
type Demote (IJust as a) = IJust as a
fromSing :: forall (a :: IJust as a). Sing a -> Demote (IJust as a)
fromSing Sing a
SIJust as a a
SIJust = forall {k} (a :: k). IJust ('Just a) a
IJust
toSing :: Demote (IJust as a) -> SomeSing (IJust as a)
toSing Demote (IJust as a)
IJust as a
IJust = forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {k} (a :: k). SIJust ('Just a) a 'IJust
SIJust
instance SDecide (IJust as a) where
Sing a
SIJust as a a
SIJust %~ :: forall (a :: IJust as a) (b :: IJust as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
SIJust ('Just a) a b
SIJust = forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
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 :: Int -> PMaybe f as -> ShowS
showsPrec Int
d PMaybe f as
xs = case forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Show PMaybe f as
xs of
PMaybe (Dict Show :. f) as
Prod Maybe (Dict Show :. f) as
PNothing -> String -> ShowS
showString String
"PNothing"
PJust (V.Compose (Dict f a
x)) -> forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith forall a. Show a => Int -> a -> ShowS
showsPrec String
"PJust" Int
d f a
x
instance ReifyConstraintProd Maybe Eq f as => Eq (PMaybe f as) where
== :: PMaybe f as -> PMaybe f as -> Bool
(==) = forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Eq g as) =>
Prod f g as -> Prod f g as -> Bool
eqProd
instance (ReifyConstraintProd Maybe Eq f as, ReifyConstraintProd Maybe Ord f as) => Ord (PMaybe f as) where
compare :: PMaybe f as -> PMaybe f as -> Ordering
compare = forall {k} (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Ord g as) =>
Prod f g as -> Prod f g as -> Ordering
compareProd
instance FProd Maybe where
type instance Elem Maybe = IJust
type instance Prod Maybe = PMaybe
singProd :: forall {k} (as :: Maybe k). Sing as -> Prod Maybe Sing as
singProd = \case
Sing as
SMaybe as
SNothing -> forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
SJust Sing n
x -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust Sing n
x
prodSing :: forall {k} (as :: Maybe k). Prod Maybe Sing as -> Sing as
prodSing = \case
PMaybe Sing as
Prod Maybe Sing as
PNothing -> forall a. SMaybe 'Nothing
SNothing
PJust Sing a
x -> forall a (n :: a). Sing n -> SMaybe ('Just n)
SJust Sing a
x
withIndices :: forall {k} (g :: k -> *) (as :: Maybe k).
Prod Maybe g as -> Prod Maybe (Elem Maybe as :*: g) as
withIndices = \case
PMaybe g as
Prod Maybe g as
PNothing -> forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust g a
x -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (forall {k} (a :: k). IJust ('Just a) a
IJust forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: Maybe k)
(m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod Maybe g as -> m (Prod Maybe h as)
traverseProd forall (a :: k). g a -> m (h a)
f = \case
PMaybe g as
Prod Maybe g as
PNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust g a
x -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x
zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: Maybe k).
(forall (a :: k). g a -> h a -> j a)
-> Prod Maybe g as -> Prod Maybe h as -> Prod Maybe j as
zipWithProd forall (a :: k). g a -> h a -> j a
f = \case
PMaybe g as
Prod Maybe g as
PNothing -> \case
PMaybe h 'Nothing
Prod Maybe h as
PNothing -> forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust g a
x -> \case
PJust h a
y -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (forall (a :: k). g a -> h a -> j a
f g a
x h a
y)
htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
(h :: k -> *) (as :: Maybe a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod Maybe g as
-> m (Prod Maybe h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f = \case
PMaybe g as
Prod Maybe g as
PNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust g a
x -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x
ixProd :: forall {k} (as :: Maybe k) (a :: k) (g :: k -> *).
Elem Maybe as a -> Lens' (Prod Maybe g as) (g a)
ixProd = \case
IJust as a
Elem Maybe as a
IJust -> \g a -> f (g a)
f -> \case
PJust g a
x -> forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
toRec :: forall {a} (g :: a -> *) (as :: Maybe a).
Prod Maybe g as -> Rec g (ToList as)
toRec = \case
PMaybe g as
Prod Maybe g as
PNothing -> forall {u} (a :: u -> *). Rec a '[]
RNil
PJust g a
x -> g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {u} (a :: u -> *). Rec a '[]
RNil
withPureProd :: forall {k} (g :: k -> *) (as :: Maybe k) r.
Prod Maybe g as -> (PureProd Maybe as => r) -> r
withPureProd = \case
PMaybe g as
Prod Maybe g as
PNothing -> forall a. a -> a
id
PJust g a
_ -> forall a. a -> a
id
instance PureProd Maybe 'Nothing where
pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod Maybe g 'Nothing
pureProd forall (a :: k). g a
_ = forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
instance PureProd Maybe ('Just a) where
pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod Maybe g ('Just a)
pureProd forall (a :: k). g a
x = forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (a :: k). g a
x
instance PureProdC Maybe c 'Nothing where
pureProdC :: forall (g :: k -> *).
(forall (a :: k). c a => g a) -> Prod Maybe g 'Nothing
pureProdC forall (a :: k). c a => g a
_ = forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
instance c a => PureProdC Maybe c ('Just a) where
pureProdC :: forall (g :: a -> *).
(forall (a :: a). c a => g a) -> Prod Maybe g ('Just a)
pureProdC forall (a :: a). c a => g a
x = forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust forall (a :: a). c a => g a
x
instance ReifyConstraintProd Maybe c g 'Nothing where
reifyConstraintProd :: Prod Maybe g 'Nothing -> Prod Maybe (Dict c :. g) 'Nothing
reifyConstraintProd PMaybe g 'Nothing
Prod Maybe g 'Nothing
PNothing = forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
instance c (g a) => ReifyConstraintProd Maybe c g ('Just a) where
reifyConstraintProd :: Prod Maybe g ('Just a) -> Prod Maybe (Dict c :. g) ('Just a)
reifyConstraintProd (PJust g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x))
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)
data SIRight (as :: Either j k) (a :: k) :: 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 :: Sing 'IRight
sing = forall {k} {j} (a :: k). SIRight ('Right a) a 'IRight
SIRight
instance SingKind (IRight as a) where
type Demote (IRight as a) = IRight as a
fromSing :: forall (a :: IRight as a). Sing a -> Demote (IRight as a)
fromSing Sing a
SIRight as a a
SIRight = forall {k} {j} (a :: k). IRight ('Right a) a
IRight
toSing :: Demote (IRight as a) -> SomeSing (IRight as a)
toSing Demote (IRight as a)
IRight as a
IRight = forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {k} {j} (a :: k). SIRight ('Right a) a 'IRight
SIRight
instance SDecide (IRight as a) where
Sing a
SIRight as a a
SIRight %~ :: forall (a :: IRight as a) (b :: IRight as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
SIRight ('Right a) a b
SIRight = forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
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 :: Int -> PEither f as -> ShowS
showsPrec Int
d PEither f as
xs = case forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Show PEither f as
xs of
PLeft Sing e
e -> forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith forall {a} {a} {t2 :: a}.
(Integral a, SShow a) =>
a -> Sing t2 -> ShowS
go String
"PLeft" Int
d Sing e
e
PRight (V.Compose (Dict f a
x)) -> forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith forall a. Show a => Int -> a -> ShowS
showsPrec String
"PRight" Int
d f a
x
where
go :: a -> Sing t2 -> ShowS
go (forall a b. (Integral a, Num b) => a -> b
fromIntegral->FromSing Sing a
i) Sing t2
x (String -> Text
T.pack->FromSing Sing a
str) = Text -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing forall a b. (a -> b) -> a -> b
$ forall a (t1 :: Natural) (t2 :: a) (t3 :: Symbol).
SShow a =>
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)
sShowsPrec Sing a
i Sing t2
x Sing a
str
instance FProd (Either j) where
type instance Elem (Either j) = IRight
type instance Prod (Either j) = PEither
singProd :: forall {k} (as :: Either j k). Sing as -> Prod (Either j) Sing as
singProd = \case
SLeft Sing n
e -> forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing n
e
SRight Sing n
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight Sing n
x
prodSing :: forall {k} (as :: Either j k). Prod (Either j) Sing as -> Sing as
prodSing = \case
PLeft Sing e
e -> forall a b (n :: a). Sing n -> SEither ('Left n)
SLeft Sing e
e
PRight Sing a
x -> forall a b (n :: b). Sing n -> SEither ('Right n)
SRight Sing a
x
withIndices :: forall {k} (g :: k -> *) (as :: Either j k).
Prod (Either j) g as
-> Prod (Either j) (Elem (Either j) as :*: g) as
withIndices = \case
PLeft Sing e
e -> forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e
PRight g a
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (forall {k} {j} (a :: k). IRight ('Right a) a
IRight forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: Either j k)
(m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod (Either j) g as -> m (Prod (Either j) h as)
traverseProd forall (a :: k). g a -> m (h a)
f = \case
PLeft Sing e
e -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e)
PRight g a
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x
zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: Either j k).
(forall (a :: k). g a -> h a -> j a)
-> Prod (Either j) g as
-> Prod (Either j) h as
-> Prod (Either j) j as
zipWithProd forall (a :: k). g a -> h a -> j a
f = \case
PLeft Sing e
e -> \case
PLeft Sing e
_ -> forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e
PRight g a
x -> \case
PRight h a
y -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (forall (a :: k). g a -> h a -> j a
f g a
x h a
y)
htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
(h :: k -> *) (as :: Either j a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod (Either j) g as
-> m (Prod (Either j) h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f = \case
PLeft Sing e
e -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e)
PRight g a
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x
ixProd :: forall {k} (as :: Either j k) (a :: k) (g :: k -> *).
Elem (Either j) as a -> Lens' (Prod (Either j) g as) (g a)
ixProd = \case
IRight as a
Elem (Either j) as a
IRight -> \g a -> f (g a)
f -> \case
PRight g a
x -> forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
toRec :: forall {a} (g :: a -> *) (as :: Either j a).
Prod (Either j) g as -> Rec g (ToList as)
toRec = \case
PLeft Sing e
_ -> forall {u} (a :: u -> *). Rec a '[]
RNil
PRight g a
x -> g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {u} (a :: u -> *). Rec a '[]
RNil
withPureProd :: forall {k} (g :: k -> *) (as :: Either j k) r.
Prod (Either j) g as -> (PureProd (Either j) as => r) -> r
withPureProd = \case
PLeft Sing e
Sing -> forall a. a -> a
id
PRight g a
_ -> forall a. a -> a
id
instance SingI e => PureProd (Either j) ('Left e) where
pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod (Either j) g ('Left e)
pureProd forall (a :: k). g a
_ = forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft forall {k} (a :: k). SingI a => Sing a
sing
instance PureProd (Either j) ('Right a) where
pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod (Either j) g ('Right a)
pureProd forall (a :: k). g a
x = forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (a :: k). g a
x
instance SingI e => PureProdC (Either j) c ('Left e) where
pureProdC :: forall (g :: k -> *).
(forall (a :: k). c a => g a) -> Prod (Either j) g ('Left e)
pureProdC forall (a :: k). c a => g a
_ = (forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft forall {k} (a :: k). SingI a => Sing a
sing)
instance c a => PureProdC (Either j) c ('Right a) where
pureProdC :: forall (g :: b -> *).
(forall (a :: b). c a => g a) -> Prod (Either j) g ('Right a)
pureProdC forall (a :: b). c a => g a
x = forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight forall (a :: b). c a => g a
x
instance ReifyConstraintProd (Either j) c g ('Left e) where
reifyConstraintProd :: Prod (Either j) g ('Left e)
-> Prod (Either j) (Dict c :. g) ('Left e)
reifyConstraintProd (PLeft Sing e
e) = forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e
instance c (g a) => ReifyConstraintProd (Either j) c g ('Right a) where
reifyConstraintProd :: Prod (Either j) g ('Right a)
-> Prod (Either j) (Dict c :. g) ('Right a)
reifyConstraintProd (PRight g a
x) = forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x))
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)
data SNEIndex (as :: NonEmpty k) (a :: k) :: 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 :: Sing 'NEHead
sing = forall {k} (a :: k) (a :: [k]). SNEIndex (a ':| a) a 'NEHead
SNEHead
instance SingI i => SingI ('NETail i) where
sing :: Sing ('NETail i)
sing = forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SNEIndex (b ':| a) a ('NETail a)
SNETail forall {k} (a :: k). SingI a => Sing a
sing
instance SingKind (NEIndex as a) where
type Demote (NEIndex as a) = NEIndex as a
fromSing :: forall (a :: NEIndex as a). Sing a -> Demote (NEIndex as a)
fromSing = \case
Sing a
SNEIndex as a a
SNEHead -> forall {k} (a :: k) (a :: [k]). NEIndex (a ':| a) a
NEHead
SNETail SIndex as a i
i -> forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> NEIndex (a ':| a) a
NETail forall a b. (a -> b) -> a -> b
$ forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing SIndex as a i
i
toSing :: Demote (NEIndex as a) -> SomeSing (NEIndex as a)
toSing = \case
Demote (NEIndex as a)
NEIndex as a
NEHead -> forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {k} (a :: k) (a :: [k]). SNEIndex (a ':| a) a 'NEHead
SNEHead
NETail Index as a
i -> forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Index as a
i forall a b. (a -> b) -> a -> b
$ forall k (a :: k). Sing a -> SomeSing k
SomeSing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SNEIndex (b ':| a) a ('NETail a)
SNETail
instance SDecide (NEIndex as a) where
%~ :: forall (a :: NEIndex as a) (b :: NEIndex as a).
Sing a -> Sing b -> Decision (a :~: b)
(%~) = \case
Sing a
SNEIndex as a a
SNEHead -> \case
Sing b
SNEIndex (a ':| as) a b
SNEHead -> forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
SNETail SIndex as a i
_ -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
SNETail SIndex as a i
i -> \case
Sing b
SNEIndex (b ':| as) a b
SNEHead -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
SNETail SIndex as a i
j -> case SIndex as a i
i forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SIndex as a i
j of
Proved i :~: i
Refl -> forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
Disproved Refuted (i :~: i)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case a :~: b
Refl -> Refuted (i :~: i)
v forall {k} (a :: k). a :~: a
Refl
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 :: forall {k} (as :: NonEmpty k). Sing as -> Prod NonEmpty Sing as
singProd (Sing n1
x NE.:%| Sing n2
xs) = Sing n1
x forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd Sing n2
xs
prodSing :: forall {k} (as :: NonEmpty k). Prod NonEmpty Sing as -> Sing as
prodSing (Sing a
x :&| Rec Sing as
xs) = Sing a
x forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> SNonEmpty (n1 ':| n2)
NE.:%| forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing as
xs
withIndices :: forall {k} (g :: k -> *) (as :: NonEmpty k).
Prod NonEmpty g as -> Prod NonEmpty (Elem NonEmpty as :*: g) as
withIndices (g a
x :&| Rec g as
xs) =
(forall {k} (a :: k) (a :: [k]). NEIndex (a ':| a) a
NEHead forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (\(Index as a
i :*: g a
y) -> forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> NEIndex (a ':| a) a
NETail Index as a
i forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (forall (f :: * -> *) {k} (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices Rec g as
xs)
traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: NonEmpty k)
(m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod NonEmpty g as -> m (Prod NonEmpty h as)
traverseProd forall (a :: k). g a -> m (h a)
f (g a
x :&| Rec g as
xs) =
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
(:&|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (as :: f k)
(m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd forall (a :: k). g a -> m (h a)
f Rec g as
xs
zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: NonEmpty k).
(forall (a :: k). g a -> h a -> j a)
-> Prod NonEmpty g as -> Prod NonEmpty h as -> Prod NonEmpty j as
zipWithProd forall (a :: k). g a -> h a -> j a
f (g a
x :&| Rec g as
xs) (h a
y :&| Rec h as
ys) = forall (a :: k). g a -> h a -> j a
f g a
x h a
y forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall (f :: * -> *) {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd forall (a :: k). g a -> h a -> j a
f Rec g as
xs Rec h as
ys
htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
(h :: k -> *) (as :: NonEmpty a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod NonEmpty g as
-> m (Prod NonEmpty h (Fmap ff as))
htraverse Sing ff
ff forall (a :: a). g a -> m (h (ff @@ a))
f (g a
x :&| Rec g as
xs) =
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
(:&|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) {a} {k} (m :: * -> *) (ff :: a ~> k)
(g :: a -> *) (h :: k -> *) (as :: f a).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse Sing ff
ff forall (a :: a). g a -> m (h (ff @@ a))
f Rec g as
xs
ixProd :: forall {k} (as :: NonEmpty k) (a :: k) (g :: k -> *).
Elem NonEmpty as a -> Lens' (Prod NonEmpty g as) (g a)
ixProd = \case
NEIndex as a
Elem NonEmpty as a
NEHead -> \g a -> f (g a)
f -> \case
g a
x :&| Rec g as
xs -> (forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| Rec g as
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
NETail Index as a
i -> \g a -> f (g a)
f -> \case
g a
x :&| Rec g as
xs -> (g a
x forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) {k} (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Lens' (Prod f g as) (g a)
ixProd Index as a
i g a -> f (g a)
f Rec g as
xs
toRec :: forall {a} (g :: a -> *) (as :: NonEmpty a).
Prod NonEmpty g as -> Rec g (ToList as)
toRec (g a
x :&| Rec g as
xs) = g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g as
xs
withPureProd :: forall {k} (g :: k -> *) (as :: NonEmpty k) r.
Prod NonEmpty g as -> (PureProd NonEmpty as => r) -> r
withPureProd (g a
x :&| Rec g as
xs) = forall {k} (f :: k -> *) (a :: k) (as :: [k]) r.
f a
-> Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
withPureProdNE g a
x Rec g as
xs
withPureProdNE
:: f a
-> Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
withPureProdNE :: forall {k} (f :: k -> *) (a :: k) (as :: [k]) r.
f a
-> Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
withPureProdNE f a
_ Rec f as
xs = forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList Rec f as
xs
instance RecApplicative as => PureProd NonEmpty (a ':| as) where
pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod NonEmpty g (a ':| as)
pureProd forall (a :: k). g a
x = forall (a :: k). g a
x forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall {k} (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
pureProd forall (a :: k). g a
x
instance (c a, RPureConstrained c as) => PureProdC NonEmpty c (a ':| as) where
pureProdC :: forall (g :: a -> *).
(forall (a :: a). c a => g a) -> Prod NonEmpty g (a ':| as)
pureProdC forall (a :: a). c a => g a
x = forall (a :: a). c a => g a
x forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall {k} (f :: * -> *) (c :: k -> Constraint) (as :: f k)
(g :: k -> *).
PureProdC f c as =>
(forall (a :: k). c a => g a) -> Prod f g as
pureProdC @_ @c forall (a :: a). c a => g a
x
instance (c (g a), ReifyConstraint c g as) => ReifyConstraintProd NonEmpty c g (a ':| as) where
reifyConstraintProd :: Prod NonEmpty g (a ':| as)
-> Prod NonEmpty (Dict c :. g) (a ':| as)
reifyConstraintProd (g a
x :&| Rec g as
xs) = forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| forall {k} (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @c Rec g as
xs
sameIndexVal
:: Index as a
-> Index as b
-> Maybe (a :~: b)
sameIndexVal :: forall {k} (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal = \case
Index as a
IZ -> \case
Index as b
IZ -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
IS Index bs b
_ -> forall a. Maybe a
Nothing
IS Index bs a
i -> \case
Index as b
IZ -> forall a. Maybe a
Nothing
IS Index bs b
j -> forall {k} (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal Index bs a
i Index bs b
j forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case a :~: b
Refl -> forall {k} (a :: k). a :~: a
Refl
sameNEIndexVal
:: NEIndex as a
-> NEIndex as b
-> Maybe (a :~: b)
sameNEIndexVal :: forall {k} (as :: NonEmpty k) (a :: k) (b :: k).
NEIndex as a -> NEIndex as b -> Maybe (a :~: b)
sameNEIndexVal = \case
NEIndex as a
NEHead -> \case
NEIndex as b
NEHead -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
NETail Index as b
_ -> forall a. Maybe a
Nothing
NETail Index as a
i -> \case
NEIndex as b
NEHead -> forall a. Maybe a
Nothing
NETail Index as b
j -> forall {k} (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal Index as a
i Index as b
j forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case a :~: b
Refl -> forall {k} (a :: k). a :~: a
Refl
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)
data SISnd (as :: (j, k)) (a :: k) :: 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 :: Sing 'ISnd
sing = forall {j} {k} (a :: j) (b :: k). SISnd '(a, b) b 'ISnd
SISnd
instance SingKind (ISnd as a) where
type Demote (ISnd as a) = ISnd as a
fromSing :: forall (a :: ISnd as a). Sing a -> Demote (ISnd as a)
fromSing Sing a
SISnd as a a
SISnd = forall {j} {k} (a :: j) (b :: k). ISnd '(a, b) b
ISnd
toSing :: Demote (ISnd as a) -> SomeSing (ISnd as a)
toSing Demote (ISnd as a)
ISnd as a
ISnd = forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {j} {k} (a :: j) (b :: k). SISnd '(a, b) b 'ISnd
SISnd
instance SDecide (ISnd as a) where
Sing a
SISnd as a a
SISnd %~ :: forall (a :: ISnd as a) (b :: ISnd as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
SISnd '(a, a) a b
SISnd = forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
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 :: forall {k} (as :: (j, k)). Sing as -> Prod ((,) j) Sing as
singProd (STuple2 Sing n1
w Sing n2
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing n1
w Sing n2
x
prodSing :: forall {k} (as :: (j, k)). Prod ((,) j) Sing as -> Sing as
prodSing (PTup Sing w
w Sing a
x) = forall a b (n1 :: a) (n2 :: b).
Sing n1 -> Sing n2 -> STuple2 '(n1, n2)
STuple2 Sing w
w Sing a
x
withIndices :: forall {k} (g :: k -> *) (as :: (j, k)).
Prod ((,) j) g as -> Prod ((,) j) (Elem ((,) j) as :*: g) as
withIndices (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w (forall {j} {k} (a :: j) (b :: k). ISnd '(a, b) b
ISnd forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: (j, k))
(m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod ((,) j) g as -> m (Prod ((,) j) h as)
traverseProd forall (a :: k). g a -> m (h a)
f (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x
zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: (j, k)).
(forall (a :: k). g a -> h a -> j a)
-> Prod ((,) j) g as -> Prod ((,) j) h as -> Prod ((,) j) j as
zipWithProd forall (a :: k). g a -> h a -> j a
f (PTup Sing w
w g a
x) (PTup Sing w
_ h a
y) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w (forall (a :: k). g a -> h a -> j a
f g a
x h a
y)
htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
(h :: k -> *) (as :: (j, a)).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod ((,) j) g as
-> m (Prod ((,) j) h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x
ixProd :: forall {k} (as :: (j, k)) (a :: k) (g :: k -> *).
Elem ((,) j) as a -> Lens' (Prod ((,) j) g as) (g a)
ixProd ISnd as a
Elem ((,) j) as a
ISnd g a -> f (g a)
f (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
toRec :: forall {a} (g :: a -> *) (as :: (j, a)).
Prod ((,) j) g as -> Rec g (ToList as)
toRec (PTup Sing w
_ g a
x) = g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {u} (a :: u -> *). Rec a '[]
RNil
withPureProd :: forall {k} (g :: k -> *) (as :: (j, k)) r.
Prod ((,) j) g as -> (PureProd ((,) j) as => r) -> r
withPureProd (PTup Sing w
Sing g a
_) PureProd ((,) j) as => r
x = PureProd ((,) j) as => r
x
instance SingI w => PureProd ((,) j) '(w, a) where
pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod ((,) j) g '(w, a)
pureProd forall (a :: k). g a
x = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup forall {k} (a :: k). SingI a => Sing a
sing forall (a :: k). g a
x
instance (SingI w, c a) => PureProdC ((,) j) c '(w, a) where
pureProdC :: forall (g :: k -> *).
(forall (a :: k). c a => g a) -> Prod ((,) j) g '(w, a)
pureProdC forall (a :: k). c a => g a
x = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup forall {k} (a :: k). SingI a => Sing a
sing forall (a :: k). c a => g a
x
instance c (g a) => ReifyConstraintProd ((,) j) c g '(w, a) where
reifyConstraintProd :: Prod ((,) j) g '(w, a) -> Prod ((,) j) (Dict c :. g) '(w, a)
reifyConstraintProd (PTup Sing w
w g a
x) = forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w forall a b. (a -> b) -> a -> b
$ forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)
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)
data SIIdentity (as :: Identity k) (a :: k) :: 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 :: Sing 'IId
sing = forall {k} (a :: k). SIIdentity ('Identity a) a 'IId
SIId
instance SingKind (IIdentity as a) where
type Demote (IIdentity as a) = IIdentity as a
fromSing :: forall (a :: IIdentity as a). Sing a -> Demote (IIdentity as a)
fromSing Sing a
SIIdentity as a a
SIId = forall {k} (x :: k). IIdentity ('Identity x) x
IId
toSing :: Demote (IIdentity as a) -> SomeSing (IIdentity as a)
toSing Demote (IIdentity as a)
IIdentity as a
IId = forall k (a :: k). Sing a -> SomeSing k
SomeSing forall {k} (a :: k). SIIdentity ('Identity a) a 'IId
SIId
instance SDecide (IIdentity as a) where
Sing a
SIIdentity as a a
SIId %~ :: forall (a :: IIdentity as a) (b :: IIdentity as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
SIIdentity ('Identity a) a b
SIId = forall a. a -> Decision a
Proved forall {k} (a :: k). a :~: a
Refl
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 :: forall {k} (as :: Identity k). Sing as -> Prod Identity Sing as
singProd (SIdentity Sing n
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity Sing n
x
prodSing :: forall {k} (as :: Identity k). Prod Identity Sing as -> Sing as
prodSing (PIdentity Sing a
x) = forall a (n :: a). Sing n -> SIdentity ('Identity n)
SIdentity Sing a
x
withIndices :: forall {k} (g :: k -> *) (as :: Identity k).
Prod Identity g as -> Prod Identity (Elem Identity as :*: g) as
withIndices (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (forall {k} (x :: k). IIdentity ('Identity x) x
IId forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
traverseProd :: forall {k} (g :: k -> *) (h :: k -> *) (as :: Identity k)
(m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod Identity g as -> m (Prod Identity h as)
traverseProd forall (a :: k). g a -> m (h a)
f (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). g a -> m (h a)
f g a
x
zipWithProd :: forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: Identity k).
(forall (a :: k). g a -> h a -> j a)
-> Prod Identity g as -> Prod Identity h as -> Prod Identity j as
zipWithProd forall (a :: k). g a -> h a -> j a
f (PIdentity g a
x) (PIdentity h a
y) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (forall (a :: k). g a -> h a -> j a
f g a
x h a
y)
htraverse :: forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
(h :: k -> *) (as :: Identity a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod Identity g as
-> m (Prod Identity h (Fmap ff as))
htraverse Sing ff
_ forall (a :: a). g a -> m (h (ff @@ a))
f (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: a). g a -> m (h (ff @@ a))
f g a
x
ixProd :: forall {k} (as :: Identity k) (a :: k) (g :: k -> *).
Elem Identity as a -> Lens' (Prod Identity g as) (g a)
ixProd IIdentity as a
Elem Identity as a
IId g a -> f (g a)
f (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
x
toRec :: forall {a} (g :: a -> *) (as :: Identity a).
Prod Identity g as -> Rec g (ToList as)
toRec (PIdentity g a
x) = g a
x forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {u} (a :: u -> *). Rec a '[]
RNil
withPureProd :: forall {k} (g :: k -> *) (as :: Identity k) r.
Prod Identity g as -> (PureProd Identity as => r) -> r
withPureProd (PIdentity g a
_) PureProd Identity as => r
x = PureProd Identity as => r
x
instance PureProd Identity ('Identity a) where
pureProd :: forall (g :: k -> *).
(forall (a :: k). g a) -> Prod Identity g ('Identity a)
pureProd forall (a :: k). g a
x = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (a :: k). g a
x
instance c a => PureProdC Identity c ('Identity a) where
pureProdC :: forall (g :: a -> *).
(forall (a :: a). c a => g a) -> Prod Identity g ('Identity a)
pureProdC forall (a :: a). c a => g a
x = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall (a :: a). c a => g a
x
instance c (g a) => ReifyConstraintProd Identity c g ('Identity a) where
reifyConstraintProd :: Prod Identity g ('Identity a)
-> Prod Identity (Dict c :. g) ('Identity a)
reifyConstraintProd (PIdentity g a
x) = forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity forall a b. (a -> b) -> a -> b
$ forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)
rElemIndex
:: forall r rs i. (RElem r rs i, PureProd [] rs)
=> Index rs r
rElemIndex :: forall {k} (r :: k) (rs :: [k]) (i :: Nat).
(RElem r rs i, PureProd [] rs) =>
Index rs r
rElemIndex = forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
(rs :: [k]) (rs' :: [k]) (i :: Nat) (f :: k -> *).
(RecElem record r r' rs rs' i, RecElemFCtx record f, r ~ r') =>
record f rs -> f r
rgetC forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices
toCoRec
:: forall k (as :: [k]) a f. (RecApplicative as, FoldRec as as)
=> Index as a
-> f a
-> CoRec f as
toCoRec :: forall k (as :: [k]) (a :: k) (f :: k -> *).
(RecApplicative as, FoldRec as as) =>
Index as a -> f a -> CoRec f as
toCoRec = \case
Index as a
IZ -> forall {k} (a1 :: k) (b :: [k]) (a :: k -> *).
RElem a1 b (RIndex a1 b) =>
a a1 -> CoRec a b
CoRec
IS Index bs a
i -> \f a
x -> forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField forall a b. (a -> b) -> a -> b
$ forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall (bs :: [k]) (b :: k) (c :: k).
Index bs a -> f a -> Index (b : bs) c -> Compose Maybe f c
go Index bs a
i f a
x) forall {k} (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices
where
go :: Index bs a -> f a -> Index (b ': bs) c -> V.Compose Maybe f c
go :: forall (bs :: [k]) (b :: k) (c :: k).
Index bs a -> f a -> Index (b : bs) c -> Compose Maybe f c
go Index bs a
i f a
x Index (b : bs) c
j = case forall {k} (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal (forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) a
IS Index bs a
i) Index (b : bs) c
j of
Just a :~: c
Refl -> forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (forall a. a -> Maybe a
Just f a
x)
Maybe (a :~: c)
Nothing -> forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose forall a. Maybe a
Nothing
indexRElem
:: (SDecide k, SingI (a :: k), RecApplicative as, FoldRec as as)
=> Index as a
-> (RElem a as (V.RIndex a as) => r)
-> r
indexRElem :: forall k (a :: k) (as :: [k]) r.
(SDecide k, SingI a, RecApplicative as, FoldRec as as) =>
Index as a -> (RElem a as (RIndex a as) => r) -> r
indexRElem Index as a
i = case forall k (as :: [k]) (a :: k) (f :: k -> *).
(RecApplicative as, FoldRec as as) =>
Index as a -> f a -> CoRec f as
toCoRec Index as a
i Sing a
x of
CoRec Sing a1
y -> case Sing a
x forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a1
y of
Proved a :~: a1
Refl -> forall a. a -> a
id
Disproved Refuted (a :~: a1)
_ -> \RElem a as (RIndex a as) => r
_ -> forall a. String -> a
errorWithoutStackTrace String
"why :|"
where
x :: Sing a
x = forall {k} (a :: k). SingI a => Sing a
sing