{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# 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 qualified Data.List.NonEmpty.Singletons as NE
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 qualified Data.Text as T
import Data.Tuple.Singletons
import Data.Vinyl hiding ((:~:))
import Data.Vinyl.CoRec
import qualified Data.Vinyl.Functor as V
import qualified Data.Vinyl.TypeLevel as V
import GHC.Generics ((:*:) (..))
import Lens.Micro hiding ((%~))
import Lens.Micro.Extras
import Text.Show.Singletons
import Unsafe.Coerce
fmapIdent :: Fmap IdSym0 as :~: as
fmapIdent :: forall {f :: * -> *} {b} (as :: f b). Fmap IdSym0 as :~: as
fmapIdent = (Any :~: Any) -> Fmap IdSym0 as :~: as
forall a b. a -> b
unsafeCoerce Any :~: Any
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 (as :: f k). Fmap IdSym0 as :~: as
forall {f :: * -> *} {b} (as :: f b). Fmap IdSym0 as :~: as
fmapIdent @as of
Fmap IdSym0 as :~: as
Refl -> Sing IdSym0
-> (forall (a :: k). g a -> m (h (IdSym0 @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap IdSym0 as))
forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
(h :: k -> *) (as :: f a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
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
forall (a :: TyFun k 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 (a :: k). Elem f as a -> g a -> j a)
-> Prod f g as -> Prod f j as
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 -> g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x (Elem f as a -> Prod f h as -> h a
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 (a :: k). Proxy a) -> Prod f Proxy as
forall {k} (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
forall (g :: k -> *). (forall (a :: k). g a) -> Prod f g as
pureProd Proxy a
forall (a :: k). Proxy a
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 (a :: k). Elem f as a -> Proxy a -> Elem f as a)
-> Prod f Proxy as -> Prod f (Elem f as) as
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 -> Proxy a -> Elem f as a
forall (a :: k). Elem f as a -> Proxy a -> Elem f as a
forall a b. a -> b -> a
const Prod f Proxy as
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 (a :: k). Sing a -> Proxy a)
-> Prod f Sing as -> Prod f Proxy as
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 (Proxy a -> Sing a -> Proxy a
forall a b. a -> b -> a
const Proxy a
forall {k} (t :: k). Proxy t
Proxy) (Prod f Sing as -> Prod f Proxy as)
-> (Sing as -> Prod f Sing as) -> Sing as -> Prod f Proxy as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall {k} (as :: f k). Sing as -> Prod f Sing as
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 = Identity (Prod f h as) -> Prod f h as
forall a. Identity a -> a
runIdentity (Identity (Prod f h as) -> Prod f h as)
-> (Prod f g as -> Identity (Prod f h as))
-> Prod f g as
-> Prod f h as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). g a -> Identity (h a))
-> Prod f g as -> Identity (Prod f h as)
forall {k} (g :: k -> *) (h :: k -> *) (as :: f k) (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
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 (h a -> Identity (h a)
forall a. a -> Identity a
Identity (h a -> Identity (h a)) -> (g a -> h a) -> g a -> Identity (h a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> h a
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 (a :: k). g a -> h a -> (:*:) g h a)
-> Prod f g as -> Prod f h as -> Prod f (g :*: h) as
forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: f k).
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
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 g a -> h a -> (:*:) g h a
forall (a :: k). g a -> h a -> (:*:) g h a
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 = Identity (Prod f h (Fmap ff as)) -> Prod f h (Fmap ff as)
forall a. Identity a -> a
runIdentity (Identity (Prod f h (Fmap ff as)) -> Prod f h (Fmap ff as))
-> (Prod f g as -> Identity (Prod f h (Fmap ff as)))
-> Prod f g as
-> Prod f h (Fmap ff as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing ff
-> (forall (a :: a). g a -> Identity (h (ff @@ a)))
-> Prod f g as
-> Identity (Prod f h (Fmap ff as))
forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
(h :: k -> *) (as :: f a).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
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 (h (Apply ff a) -> Identity (h (Apply ff a))
forall a. a -> Identity a
Identity (h (Apply ff a) -> Identity (h (Apply ff a)))
-> (g a -> h (Apply ff a)) -> g a -> Identity (h (Apply ff a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> h (Apply ff a)
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 (a :: k). (:*:) (Elem f as) g a -> h a)
-> Prod f (Elem f as :*: g) as -> Prod f h as
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) -> Elem f as a -> g a -> h a
forall (a :: k). Elem f as a -> g a -> h a
f Elem f as a
i g a
x) (Prod f (Elem f as :*: g) as -> Prod f h as)
-> (Prod f g as -> Prod f (Elem f as :*: g) as)
-> Prod f g as
-> Prod f h as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prod f g as -> Prod f (Elem f as :*: g) as
forall {k} (g :: k -> *) (as :: f k).
Prod f g as -> Prod f (Elem f as :*: g) as
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 = Elem f as a -> Prod f Sing as -> Sing a
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 Sing as -> Sing a)
-> (Sing as -> Prod f Sing as) -> Sing as -> Sing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall {k} (as :: f k). Sing as -> Prod f Sing as
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 = Getting (g a) (Prod f g as) (g a) -> Prod f g as -> g a
forall a s. Getting a s a -> s -> a
view (Elem f as a -> Lens' (Prod f g as) (g a)
forall {k} (as :: f k) (a :: k) (g :: k -> *).
Elem f as a -> Lens' (Prod f g as) (g a)
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 (a :: k). (:*:) (Elem f as) g a -> m (h a))
-> Prod f (Elem f as :*: g) as -> m (Prod f h as)
forall {k} (g :: k -> *) (h :: k -> *) (as :: f k) (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
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) -> Elem f as a -> g a -> m (h a)
forall (a :: k). Elem f as a -> g a -> m (h a)
f Elem f as a
i g a
x) (Prod f (Elem f as :*: g) as -> m (Prod f h as))
-> (Prod f g as -> Prod f (Elem f as :*: g) as)
-> Prod f g as
-> m (Prod f h as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prod f g as -> Prod f (Elem f as :*: g) as
forall {k} (g :: k -> *) (as :: f k).
Prod f g as -> Prod f (Elem f as :*: g) as
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 = Const m (Prod f Any as) -> m
forall {k} a (b :: k). Const a b -> a
getConst (Const m (Prod f Any as) -> m)
-> (Prod f g as -> Const m (Prod f Any as)) -> Prod f g as -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). Elem f as a -> g a -> Const m (Any a))
-> Prod f g as -> Const m (Prod f Any as)
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 -> m -> Const m (Any a)
forall {k} a (b :: k). a -> Const a b
Const (m -> Const m (Any a)) -> (g a -> m) -> g a -> Const m (Any a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elem f as a -> g a -> m
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 (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
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 ((g a -> m) -> Elem f as a -> g a -> m
forall a b. a -> b -> a
const g a -> m
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 (a :: k). Elem f as a -> Sing a -> m)
-> Prod f Sing as -> m
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 Elem f as a -> Sing a -> m
forall (a :: k). Elem f as a -> Sing a -> m
f (Prod f Sing as -> m)
-> (Sing as -> Prod f Sing as) -> Sing as -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall {k} (as :: f k). Sing as -> Prod f Sing as
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 (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
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 ((Sing a -> m) -> Elem f as a -> Sing a -> m
forall a b. a -> b -> a
const Sing a -> m
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 (a :: k). Elem f as a -> g a)
-> Prod f (Elem f as) bs -> Prod f g bs
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 -> Prod f g as -> g a
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
(All -> Bool) -> (Prod f g as -> All) -> Prod f g as -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). Const All a -> All)
-> Prod f (Const All) as -> All
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 Const All a -> All
forall (a :: k). Const All a -> All
forall {k} a (b :: k). Const a b -> a
getConst
(Prod f (Const All) as -> All)
-> (Prod f g as -> Prod f (Const All) as) -> Prod f g as -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). (:.) (Dict Eq) g a -> g a -> Const All a)
-> Prod f (Dict Eq :. g) as -> Prod f g as -> Prod f (Const All) as
forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: f k).
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
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 -> All -> Const All a
forall {k} a (b :: k). a -> Const a b
Const (Bool -> All
All (g a
x g a -> g a -> Bool
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
forall (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 (a :: k). Const Ordering a -> Ordering)
-> Prod f (Const Ordering) as -> Ordering
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 Const Ordering a -> Ordering
forall (a :: k). Const Ordering a -> Ordering
forall {k} a (b :: k). Const a b -> a
getConst
(Prod f (Const Ordering) as -> Ordering)
-> (Prod f g as -> Prod f (Const Ordering) as)
-> Prod f g as
-> Ordering
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). (:.) (Dict Ord) g a -> g a -> Const Ordering a)
-> Prod f (Dict Ord :. g) as
-> Prod f g as
-> Prod f (Const Ordering) as
forall {k} (g :: k -> *) (h :: k -> *) (j :: k -> *) (as :: f k).
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
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 -> Ordering -> Const Ordering a
forall {k} a (b :: k). a -> Const a b
Const (g a -> g a -> Ordering
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
forall (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 (a :: k). Elem f as a -> g a)
-> Prod f (Elem f as) as -> Prod f g as
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 -> g a
forall (a :: k). Elem f as a -> g a
f Prod f (Elem f as) as
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 (a :: k). Elem f as a -> m (g a))
-> Prod f (Elem f as) as -> m (Prod f g as)
forall {k} (g :: k -> *) (h :: k -> *) (as :: f k) (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
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 -> m (g a)
forall (a :: k). Elem f as a -> m (g a)
f Prod f (Elem f as) as
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)
#if __GLASGOW_HASKELL__ >= 908
type instance forall as a. Sing = SIndex as a :: Index as a -> Type
#else
type instance Sing = SIndex as a :: Index as a -> Type
#endif
instance SingI 'IZ where
sing :: Sing 'IZ
sing = Sing 'IZ
SIndex (a : as) a 'IZ
forall {k} (a :: k) (a :: [k]). SIndex (a : a) a 'IZ
SIZ
instance SingI i => SingI ('IS i) where
sing :: Sing ('IS i)
sing = SIndex bs a i -> SIndex (b : bs) a ('IS i)
forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SIndex (b : a) a ('IS a)
SIS Sing i
SIndex bs a i
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 -> Demote (Index as a)
Index (a : as) a
forall {k} (a :: k) (a :: [k]). Index (a : a) a
IZ
SIS SIndex bs a i
j -> Index bs a -> Index (b : bs) a
forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) a
IS (Sing i -> Demote (Index bs a)
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Index bs a). Sing a -> Demote (Index bs a)
fromSing Sing i
SIndex bs a i
j)
toSing :: Demote (Index as a) -> SomeSing (Index as a)
toSing Demote (Index as a)
i = Index as a
-> (forall (i :: Index as a).
SIndex as a i -> SomeSing (Index as a))
-> SomeSing (Index as a)
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)
Index as a
i Sing i -> SomeSing (Index as a)
SIndex as a i -> SomeSing (Index as a)
forall k (a :: k). Sing a -> SomeSing k
forall (i :: Index as a). SIndex as a i -> SomeSing (Index as a)
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 -> ((SIndex bs b 'IZ -> r) -> SIndex bs b 'IZ -> r
forall a b. (a -> b) -> a -> b
$ SIndex bs b 'IZ
SIndex (b : as) b 'IZ
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 -> Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
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 (SIndex bs b ('IS i) -> r
forall (i :: Index bs b). SIndex bs b i -> r
f (SIndex bs b ('IS i) -> r)
-> (SIndex bs b i -> SIndex bs b ('IS i)) -> SIndex bs b i -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIndex bs b i -> SIndex bs b ('IS i)
SIndex bs b i -> SIndex (b : bs) b ('IS i)
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 -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
SIS SIndex bs a i
_ -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
SIS SIndex bs a i
i' -> \case
Sing b
SIndex (b : bs) a b
SIZ -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
SIS SIndex bs a i
j' -> case Sing i
SIndex bs a i
i' Sing i -> Sing i -> Decision (i :~: i)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
forall (a :: Index bs a) (b :: Index bs a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing i
SIndex bs a i
j' of
Proved i :~: i
Refl -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
Disproved Refuted (i :~: i)
v -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case a :~: b
Refl -> Refuted (i :~: i)
v i :~: i
i :~: i
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 -> Rec Sing '[]
Prod [] Sing as
forall {u} (a :: u -> *). Rec a '[]
RNil
Sing n1
x `SCons` Sing n2
xs -> Sing n1
x Sing n1 -> Rec Sing n2 -> Rec Sing (n1 : n2)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing n2 -> Prod [] Sing n2
forall {k} (as :: [k]). Sing as -> Prod [] Sing as
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 -> Sing as
SList '[]
forall a. SList '[]
SNil
Sing r
x :& Rec Sing rs
xs -> Sing r
x Sing r -> Sing rs -> SList (r : rs)
forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> SList (n1 : n2)
`SCons` Prod [] Sing rs -> Sing rs
forall {k} (as :: [k]). Prod [] Sing as -> Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing rs
Prod [] 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 = Prod [] g as -> m (Prod [] h as)
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 -> Rec h '[] -> m (Rec h '[])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec h '[]
forall {u} (a :: u -> *). Rec a '[]
RNil
g r
x :& Rec g rs
xs -> h r -> Rec h rs -> Rec h (r : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) (h r -> Rec h rs -> Rec h (r : rs))
-> m (h r) -> m (Rec h rs -> Rec h (r : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g r -> m (h r)
forall (a :: k). g a -> m (h a)
f g r
x m (Rec h rs -> Rec h (r : rs))
-> m (Rec h rs) -> m (Rec h (r : rs))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Prod [] g rs -> m (Prod [] h rs)
forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go Rec g rs
Prod [] 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 = Prod [] g as -> Prod [] h as -> Prod [] j as
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 -> Rec j '[]
Prod [] j bs
forall {u} (a :: u -> *). Rec a '[]
RNil
g r
x :& Rec g rs
xs -> \case
h r
y :& Rec h rs
ys -> g r -> h r -> j r
forall (a :: k). g a -> h a -> j a
f g r
x h r
h r
y j r -> Rec j rs -> Rec j (r : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Prod [] g rs -> Prod [] h rs -> Prod [] j rs
forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go Rec g rs
Prod [] g rs
xs Rec h rs
Prod [] 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 = Prod [] g as -> m (Prod [] h (Fmap ff as))
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 -> Rec h '[] -> m (Rec h '[])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec h '[]
forall {u} (a :: u -> *). Rec a '[]
RNil
g r
x :& Rec g rs
xs -> h (Apply ff r)
-> Rec h (Fmap_6989586621679431527 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621679431527 ff rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) (h (Apply ff r)
-> Rec h (Fmap_6989586621679431527 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621679431527 ff rs))
-> m (h (Apply ff r))
-> m (Rec h (Fmap_6989586621679431527 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621679431527 ff rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g r -> m (h (Apply ff r))
forall (a :: a). g a -> m (h (ff @@ a))
f g r
x m (Rec h (Fmap_6989586621679431527 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621679431527 ff rs))
-> m (Rec h (Fmap_6989586621679431527 ff rs))
-> m (Rec h (Apply ff r : Fmap_6989586621679431527 ff rs))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Prod [] g rs -> m (Prod [] h (Fmap ff rs))
forall (bs :: [a]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go Rec g rs
Prod [] 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 -> Rec (Index '[] :*: g) '[]
Prod [] (Elem [] as :*: g) as
forall {u} (a :: u -> *). Rec a '[]
RNil
g r
x :& Rec g rs
xs -> (Index (r : rs) r
forall {k} (a :: k) (a :: [k]). Index (a : a) a
IZ Index (r : rs) r -> g r -> (:*:) (Index (r : rs)) g r
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g r
x) (:*:) (Index (r : rs)) g r
-> Rec (Index (r : rs) :*: g) rs
-> Rec (Index (r : rs) :*: g) (r : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& (forall (a :: k).
(:*:) (Index rs) g a -> (:*:) (Index (r : rs)) g a)
-> Prod [] (Index rs :*: g) rs -> Prod [] (Index (r : rs) :*: g) 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) -> Index rs a -> Index (r : rs) a
forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> Index (a : a) a
IS Index rs a
i Index (r : rs) a -> g a -> (:*:) (Index (r : rs)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (Prod [] g rs -> Prod [] (Elem [] rs :*: g) rs
forall {k} (g :: k -> *) (as :: [k]).
Prod [] g as -> Prod [] (Elem [] as :*: g) as
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
Prod [] 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)) = Elem [] as a -> Prod [] g as -> f (Prod [] g as)
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 -> (g a -> Rec g rs -> Rec g (a : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g rs
xs) (g a -> Rec g (a : rs)) -> f (g a) -> f (Rec g (a : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g r
x
IS Index bs a
i -> \case
g r
x :& Rec g rs
xs -> (g r
x g r -> Rec g bs -> Rec g (r : bs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) (Rec g bs -> Rec g (r : bs)) -> f (Rec g bs) -> f (Rec g (r : bs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
forall (bs :: [k]).
Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go Index bs a
Elem [] bs a
i Rec g rs
Prod [] g bs
xs
toRec :: forall {a} (g :: a -> *) (as :: [a]).
Prod [] g as -> Rec g (ToList as)
toRec = Rec g as -> Rec g as
Prod [] g as -> Rec g (ToList as)
forall a. a -> a
id
withPureProd :: forall {k} (g :: k -> *) (as :: [k]) r.
Prod [] g as -> (PureProd [] as => r) -> r
withPureProd = Rec g as -> ((RecApplicative as, PureProd [] as) => r) -> r
Prod [] g as -> (PureProd [] as => r) -> r
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 -> r -> r
((RecApplicative as, PureProd [] as) => r) -> r
forall a. a -> a
id
f r
_ :& Rec f rs
xs -> Rec f rs -> ((RecApplicative rs, PureProd [] rs) => r) -> r
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 (x :: k). g x) -> Rec g as
(forall (x :: k). g x) -> Prod [] g as
forall {u} (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
forall (f :: k -> *). (forall (x :: k). f x) -> Rec f as
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
forall (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
forall (c :: * -> Constraint) (f :: k -> *) (rs :: [k]).
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)
#if __GLASGOW_HASKELL__ >= 908
type instance forall as a. Sing = SIJust as a :: IJust as a -> Type
#else
type instance Sing = SIJust as a :: IJust as a -> Type
#endif
instance SingI 'IJust where
sing :: Sing 'IJust
sing = Sing 'IJust
SIJust ('Just a) a 'IJust
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 = Demote (IJust as a)
IJust ('Just a) a
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 = Sing 'IJust -> SomeSing (IJust as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IJust
SIJust ('Just a) a 'IJust
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 = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
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
forall (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
Prod Maybe 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)) -> (Int -> f a -> ShowS) -> String -> Int -> f a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> f a -> ShowS
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
(==) = PMaybe f as -> PMaybe f as -> Bool
Prod Maybe f as -> Prod Maybe 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 = PMaybe f as -> PMaybe f as -> Ordering
Prod Maybe f as -> Prod Maybe f as -> Ordering
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 Elem Maybe = IJust
type Prod Maybe = PMaybe
singProd :: forall {k} (as :: Maybe k). Sing as -> Prod Maybe Sing as
singProd = \case
Sing as
SMaybe as
SNothing -> PMaybe Sing 'Nothing
Prod Maybe Sing as
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
SJust Sing n
x -> Sing n -> PMaybe Sing ('Just n)
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 -> Sing as
SMaybe 'Nothing
forall a. SMaybe 'Nothing
SNothing
PJust Sing a
x -> Sing a -> SMaybe ('Just a)
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 -> PMaybe (IJust 'Nothing :*: g) 'Nothing
Prod Maybe (Elem Maybe as :*: g) as
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust g a
x -> (:*:) (IJust ('Just a)) g a
-> PMaybe (IJust ('Just a) :*: g) ('Just a)
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (IJust ('Just a) a
forall {k} (a :: k). IJust ('Just a) a
IJust IJust ('Just a) a -> g a -> (:*:) (IJust ('Just a)) g a
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 -> PMaybe h 'Nothing -> m (PMaybe h 'Nothing)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PMaybe h 'Nothing
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust g a
x -> h a -> PMaybe h ('Just a)
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (h a -> PMaybe h ('Just a)) -> m (h a) -> m (PMaybe h ('Just a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
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 -> PMaybe j 'Nothing
Prod Maybe j as
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust g a
x -> \case
PJust h a
y -> j a -> PMaybe j ('Just a)
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
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 -> PMaybe h 'Nothing -> m (PMaybe h 'Nothing)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PMaybe h 'Nothing
forall {k} (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust g a
x -> h (Apply ff a) -> PMaybe h ('Just (Apply ff a))
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (h (Apply ff a) -> PMaybe h ('Just (Apply ff a)))
-> m (h (Apply ff a)) -> m (PMaybe h ('Just (Apply ff a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
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 -> g a -> PMaybe g ('Just a)
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (g a -> PMaybe g ('Just a)) -> f (g a) -> f (PMaybe g ('Just a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
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 -> Rec g '[]
Rec g (ToList as)
forall {u} (a :: u -> *). Rec a '[]
RNil
PJust g a
x -> g a
x g a -> Rec g '[] -> Rec g '[a]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
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 -> r -> r
(PureProd Maybe as => r) -> r
forall a. a -> a
id
PJust g a
_ -> r -> r
(PureProd Maybe as => r) -> r
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
_ = PMaybe g 'Nothing
Prod Maybe g 'Nothing
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 = g a -> PMaybe g ('Just a)
(forall (a :: k). g a) -> Prod Maybe g ('Just a)
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust
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
_ = PMaybe g 'Nothing
Prod Maybe g 'Nothing
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 = g a -> PMaybe g ('Just a)
(forall (a :: a). c a => g a) -> Prod Maybe g ('Just a)
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust
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 = PMaybe (Dict c :. g) 'Nothing
Prod Maybe (Dict c :. g) 'Nothing
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) = Compose (Dict c) g a -> PMaybe (Dict c :. g) ('Just a)
forall {k} (f :: k -> *) (a :: k). f a -> PMaybe f ('Just a)
PJust (Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
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)
#if __GLASGOW_HASKELL__ >= 908
type instance forall as a. Sing = SIRight as a :: IRight as a -> Type
#else
type instance Sing = SIRight as a :: IRight as a -> Type
#endif
instance SingI 'IRight where
sing :: Sing 'IRight
sing = Sing 'IRight
SIRight ('Right a) a 'IRight
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 = Demote (IRight as a)
IRight ('Right a) a
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 = Sing 'IRight -> SomeSing (IRight as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IRight
SIRight ('Right a) a 'IRight
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 = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
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
forall (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
Prod (Either j) f as
xs of
PLeft Sing e
e -> (Int -> Sing e -> ShowS) -> String -> Int -> Sing e -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> Sing e -> ShowS
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)) -> (Int -> f a -> ShowS) -> String -> Int -> f a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec String
"PRight" Int
d f a
x
where
go :: a -> Sing t2 -> ShowS
go (a -> Demote Natural
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 (Text -> String)
-> (Sing (ShowsPrec a t2 a) -> Text)
-> Sing (ShowsPrec a t2 a)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing (ShowsPrec a t2 a) -> Demote Symbol
Sing (ShowsPrec a t2 a) -> Text
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing (Sing (ShowsPrec a t2 a) -> String)
-> Sing (ShowsPrec a t2 a) -> String
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing t2
-> Sing a
-> Sing (Apply (Apply (Apply ShowsPrecSym0 a) t2) a)
forall (t1 :: Natural) (t2 :: a) (t3 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)
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 Elem (Either j) = IRight
type Prod (Either j) = PEither
singProd :: forall {k} (as :: Either j k). Sing as -> Prod (Either j) Sing as
singProd = \case
SLeft Sing n
e -> Sing n -> PEither Sing ('Left n)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing n
e
SRight Sing n
x -> Sing n -> PEither Sing ('Right n)
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 -> Sing e -> SEither ('Left e)
forall a b (n :: a). Sing n -> SEither ('Left n)
SLeft Sing e
e
PRight Sing a
x -> Sing a -> SEither ('Right a)
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 -> Sing e -> PEither (IRight ('Left e) :*: g) ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e
PRight g a
x -> (:*:) (IRight ('Right a)) g a
-> PEither (IRight ('Right a) :*: g) ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (IRight ('Right a) a
forall {k} {j} (a :: k). IRight ('Right a) a
IRight IRight ('Right a) a -> g a -> (:*:) (IRight ('Right a)) g a
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 -> PEither h ('Left e) -> m (PEither h ('Left e))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sing e -> PEither h ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e)
PRight g a
x -> h a -> PEither h ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (h a -> PEither h ('Right a))
-> m (h a) -> m (PEither h ('Right a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
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
_ -> Sing e -> PEither j ('Left 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 -> j a -> PEither j ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
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 -> PEither h ('Left e) -> m (PEither h ('Left e))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sing e -> PEither h ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
e)
PRight g a
x -> h (Apply ff a) -> PEither h ('Right (Apply ff a))
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (h (Apply ff a) -> PEither h ('Right (Apply ff a)))
-> m (h (Apply ff a)) -> m (PEither h ('Right (Apply ff a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
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 -> g a -> PEither g ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (g a -> PEither g ('Right a))
-> f (g a) -> f (PEither g ('Right a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
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
_ -> Rec g '[]
Rec g (ToList as)
forall {u} (a :: u -> *). Rec a '[]
RNil
PRight g a
x -> g a
x g a -> Rec g '[] -> Rec g '[a]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
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 -> r -> r
(PureProd (Either j) as => r) -> r
forall a. a -> a
id
PRight g a
_ -> r -> r
(PureProd (Either j) as => r) -> r
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
_ = Sing e -> PEither g ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
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 = g a -> PEither g ('Right a)
(forall (a :: k). g a) -> Prod (Either j) g ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight
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
_ = Sing e -> PEither g ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
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 = g a -> PEither g ('Right a)
(forall (a :: b). c a => g a) -> Prod (Either j) g ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight
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) = Sing e -> PEither (Dict c :. g) ('Left e)
forall {k} {k} (a :: k) (f :: k -> *).
Sing a -> PEither f ('Left a)
PLeft Sing e
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) = Compose (Dict c) g a -> PEither (Dict c :. g) ('Right a)
forall {k} {j} (f :: k -> *) (a :: k). f a -> PEither f ('Right a)
PRight (Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
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)
#if __GLASGOW_HASKELL__ >= 908
type instance forall as a. Sing = SNEIndex as a :: NEIndex as a -> Type
#else
type instance Sing = SNEIndex as a :: NEIndex as a -> Type
#endif
instance SingI 'NEHead where
sing :: Sing 'NEHead
sing = Sing 'NEHead
SNEIndex (a ':| as) a 'NEHead
forall {k} (a :: k) (a :: [k]). SNEIndex (a ':| a) a 'NEHead
SNEHead
instance SingI i => SingI ('NETail i) where
sing :: Sing ('NETail i)
sing = SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)
forall {k} (a :: [k]) (a :: k) (a :: Index a a) (b :: k).
SIndex a a a -> SNEIndex (b ':| a) a ('NETail a)
SNETail Sing i
SIndex as a i
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 -> Demote (NEIndex as a)
NEIndex (a ':| as) a
forall {k} (a :: k) (a :: [k]). NEIndex (a ':| a) a
NEHead
SNETail SIndex as a i
i -> Index as a -> NEIndex (b ':| as) a
forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> NEIndex (a ':| a) a
NETail (Index as a -> NEIndex (b ':| as) a)
-> Index as a -> NEIndex (b ':| as) a
forall a b. (a -> b) -> a -> b
$ Sing i -> Demote (Index as a)
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Index as a). Sing a -> Demote (Index as a)
fromSing Sing i
SIndex as a i
i
toSing :: Demote (NEIndex as a) -> SomeSing (NEIndex as a)
toSing = \case
Demote (NEIndex as a)
NEIndex as a
NEHead -> Sing 'NEHead -> SomeSing (NEIndex as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'NEHead
SNEIndex (a ':| as) a 'NEHead
forall {k} (a :: k) (a :: [k]). SNEIndex (a ':| a) a 'NEHead
SNEHead
NETail Index as a
i -> Demote (Index as a)
-> (forall {a :: Index as a}. Sing a -> SomeSing (NEIndex as a))
-> SomeSing (NEIndex as a)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote (Index as a)
Index as a
i ((forall {a :: Index as a}. Sing a -> SomeSing (NEIndex as a))
-> SomeSing (NEIndex as a))
-> (forall {a :: Index as a}. Sing a -> SomeSing (NEIndex as a))
-> SomeSing (NEIndex as a)
forall a b. (a -> b) -> a -> b
$ Sing ('NETail a) -> SomeSing (NEIndex as a)
SNEIndex (b ':| as) a ('NETail a) -> SomeSing (NEIndex as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SNEIndex (b ':| as) a ('NETail a) -> SomeSing (NEIndex as a))
-> (SIndex as a a -> SNEIndex (b ':| as) a ('NETail a))
-> SIndex as a a
-> SomeSing (NEIndex as a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIndex as a a -> SNEIndex (b ':| as) a ('NETail a)
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 -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
SNETail SIndex as a i
_ -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
SNETail SIndex as a i
i -> \case
Sing b
SNEIndex (b ':| as) a b
SNEHead -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
SNETail SIndex as a i
j -> case Sing i
SIndex as a i
i Sing i -> Sing i -> Decision (i :~: i)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
forall (a :: Index as a) (b :: Index as a).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing i
SIndex as a i
j of
Proved i :~: i
Refl -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
Disproved Refuted (i :~: i)
v -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case a :~: b
Refl -> Refuted (i :~: i)
v i :~: i
i :~: i
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 Elem NonEmpty = NEIndex
type 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 Sing n1 -> Rec Sing n2 -> NERec Sing (n1 ':| n2)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| Sing n2 -> Prod [] Sing n2
forall {k} (as :: [k]). Sing as -> Prod [] Sing as
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 Sing a -> Sing as -> SNonEmpty (a ':| as)
forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> SNonEmpty (n1 ':| n2)
NE.:%| Prod [] Sing as -> Sing as
forall {k} (as :: [k]). Prod [] Sing as -> Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing as
Prod [] 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) =
(NEIndex (a ':| as) a
forall {k} (a :: k) (a :: [k]). NEIndex (a ':| a) a
NEHead NEIndex (a ':| as) a -> g a -> (:*:) (NEIndex (a ':| as)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
(:*:) (NEIndex (a ':| as)) g a
-> Rec (NEIndex (a ':| as) :*: g) as
-> NERec (NEIndex (a ':| as) :*: g) (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| (forall (a :: k).
(:*:) (Index as) g a -> (:*:) (NEIndex (a ':| as)) g a)
-> Prod [] (Index as :*: g) as
-> Prod [] (NEIndex (a ':| as) :*: g) as
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) -> Index as a -> NEIndex (a ':| as) a
forall {k} (a :: [k]) (a :: k) (a :: k).
Index a a -> NEIndex (a ':| a) a
NETail Index as a
i NEIndex (a ':| as) a -> g a -> (:*:) (NEIndex (a ':| as)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (Prod [] g as -> Prod [] (Elem [] as :*: g) as
forall {k} (g :: k -> *) (as :: [k]).
Prod [] g as -> Prod [] (Elem [] as :*: g) as
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
Prod [] 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) =
h a -> Rec h as -> NERec h (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
(:&|) (h a -> Rec h as -> NERec h (a ':| as))
-> m (h a) -> m (Rec h as -> NERec h (a ':| as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x m (Rec h as -> NERec h (a ':| as))
-> m (Rec h as) -> m (NERec h (a ':| as))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (a :: k). g a -> m (h a))
-> Prod [] g as -> m (Prod [] h as)
forall {k} (g :: k -> *) (h :: k -> *) (as :: [k]) (m :: * -> *).
Applicative m =>
(forall (a :: k). g a -> m (h a))
-> Prod [] g as -> m (Prod [] h as)
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 g a -> m (h a)
forall (a :: k). g a -> m (h a)
f Rec g as
Prod [] 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) = g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y j a -> Rec j as -> NERec j (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| (forall (a :: k). g a -> h a -> j a)
-> Prod [] g as -> Prod [] h as -> Prod [] j as
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
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 g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f Rec g as
Prod [] g as
xs Rec h as
Prod [] 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) =
h (Apply ff a)
-> Rec h (Fmap_6989586621679431527 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621679431527 ff as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
(:&|) (h (Apply ff a)
-> Rec h (Fmap_6989586621679431527 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621679431527 ff as))
-> m (h (Apply ff a))
-> m (Rec h (Fmap_6989586621679431527 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621679431527 ff as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a). g a -> m (h (ff @@ a))
f g a
x m (Rec h (Fmap_6989586621679431527 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621679431527 ff as))
-> m (Rec h (Fmap_6989586621679431527 ff as))
-> m (NERec h (Apply ff a ':| Fmap_6989586621679431527 ff as))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
forall {a} {k} (m :: * -> *) (ff :: a ~> k) (g :: a -> *)
(h :: k -> *) (as :: [a]).
Applicative m =>
Sing ff
-> (forall (a :: a). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
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 g a -> m (h (ff @@ a))
forall (a :: a). g a -> m (h (ff @@ a))
f Rec g as
Prod [] 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 -> (g a -> Rec g as -> NERec g (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| Rec g as
xs) (g a -> NERec g (a ':| as)) -> f (g a) -> f (NERec g (a ':| as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
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 g a -> Rec g as -> NERec g (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&|) (Rec g as -> NERec g (a ':| as))
-> f (Rec g as) -> f (NERec g (a ':| as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elem [] as a -> Lens' (Prod [] g as) (g a)
forall {k} (as :: [k]) (a :: k) (g :: k -> *).
Elem [] as a -> Lens' (Prod [] g as) (g a)
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
Elem [] as a
i g a -> f (g a)
f Rec g as
Prod [] 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 g a -> Rec g as -> Rec g (a : as)
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) = g a
-> Rec g as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
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 -> ((RecApplicative as, PureProd [] as) => r) -> r
Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r) -> r
forall {k} (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList
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 = g a
forall (a :: k). g a
x g a -> Rec g as -> NERec g (a ':| as)
forall {u} (f :: u -> *) (a :: u) (a :: [u]).
f a -> Rec f a -> NERec f (a ':| a)
:&| (forall (a :: k). g a) -> Prod [] g as
forall {k} (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
forall (g :: k -> *). (forall (a :: k). g a) -> Prod [] g as
pureProd g a
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 = g a
forall (a :: a). c a => g a
x g a -> Rec g as -> NERec g (a ':| as)
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
forall (f :: * -> *) (c :: a -> Constraint) (as :: f a)
(g :: a -> *).
PureProdC f c as =>
(forall (a :: a). c a => g a) -> Prod f g as
pureProdC @_ @c g a
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) =
Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)
Compose (Dict c) g a
-> Rec (Dict c :. g) as -> NERec (Dict c :. g) (a ':| as)
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
forall (f :: * -> *) (c :: * -> Constraint) (g :: a -> *)
(as :: f a).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @c Rec g as
Prod [] 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 -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
IS Index bs b
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
IS Index bs a
i -> \case
Index as b
IZ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
IS Index bs b
j -> Index bs a -> Index bs b -> Maybe (a :~: b)
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
Index bs b
j Maybe (a :~: b) -> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case a :~: b
Refl -> a :~: a
a :~: b
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 -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
NETail Index as b
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
NETail Index as a
i -> \case
NEIndex as b
NEHead -> Maybe (a :~: b)
forall a. Maybe a
Nothing
NETail Index as b
j -> Index as a -> Index as b -> Maybe (a :~: b)
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
Index as b
j Maybe (a :~: b) -> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case a :~: b
Refl -> a :~: a
a :~: b
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)
#if __GLASGOW_HASKELL__ >= 908
type instance forall as a. Sing = SISnd as a :: ISnd as a -> Type
#else
type instance Sing = SISnd as a :: ISnd as a -> Type
#endif
instance SingI 'ISnd where
sing :: Sing 'ISnd
sing = Sing 'ISnd
SISnd '(a, b) b 'ISnd
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 = Demote (ISnd as a)
ISnd '(a, a) a
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 = Sing 'ISnd -> SomeSing (ISnd as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'ISnd
SISnd '(a, a) a 'ISnd
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 = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
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 Elem ((,) j) = ISnd
type Prod ((,) j) = PTup
singProd :: forall {k} (as :: (j, k)). Sing as -> Prod ((,) j) Sing as
singProd (STuple2 Sing n1
w Sing n2
x) = Sing n1 -> Sing n2 -> PTup Sing '(n1, n2)
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) = Sing w -> Sing a -> STuple2 '(w, a)
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) = Sing w
-> (:*:) (ISnd '(w, a)) g a -> PTup (ISnd '(w, a) :*: g) '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w (ISnd '(w, a) a
forall {j} {k} (a :: j) (b :: k). ISnd '(a, b) b
ISnd ISnd '(w, a) a -> g a -> (:*:) (ISnd '(w, a)) g a
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) = Sing w -> h a -> PTup h '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w (h a -> PTup h '(w, a)) -> m (h a) -> m (PTup h '(w, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
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) = Sing w -> j a -> PTup j '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
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) = Sing w -> h (Apply ff a) -> PTup h '(w, Apply ff a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
w (h (Apply ff a) -> PTup h '(w, Apply ff a))
-> m (h (Apply ff a)) -> m (PTup h '(w, Apply ff a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
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) = Sing a -> g a -> PTup g '(a, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing a
Sing w
w (g a -> PTup g '(a, a)) -> f (g a) -> f (PTup g '(a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
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 g a -> Rec g '[] -> Rec g '[a]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
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 = r
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 = Sing w -> g a -> PTup g '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
forall {k} (a :: k). SingI a => Sing a
sing
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 = Sing w -> g a -> PTup g '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
forall {k} (a :: k). SingI a => Sing a
sing
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) = Sing w -> Compose (Dict c) g a -> PTup (Dict c :. g) '(w, a)
forall {k} {k} (a :: k) (f :: k -> *) (a :: k).
Sing a -> f a -> PTup f '(a, a)
PTup Sing w
Sing w
w (Compose (Dict c) g a -> PTup (Dict c :. g) '(w, a))
-> Compose (Dict c) g a -> PTup (Dict c :. g) '(w, a)
forall a b. (a -> b) -> a -> b
$ Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
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)
#if __GLASGOW_HASKELL__ >= 908
type instance forall as a. Sing = SIIdentity as a :: IIdentity as a -> Type
#else
type instance Sing = SIIdentity as a :: IIdentity as a -> Type
#endif
instance SingI 'IId where
sing :: Sing 'IId
sing = Sing 'IId
SIIdentity ('Identity x) x 'IId
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 = Demote (IIdentity as a)
IIdentity ('Identity a) a
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 = Sing 'IId -> SomeSing (IIdentity as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IId
SIIdentity ('Identity a) a 'IId
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 = (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
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) = Sing n -> PIdentity Sing ('Identity n)
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) = Sing a -> SIdentity ('Identity a)
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) = (:*:) (IIdentity ('Identity a)) g a
-> PIdentity (IIdentity ('Identity a) :*: g) ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (IIdentity ('Identity a) a
forall {k} (x :: k). IIdentity ('Identity x) x
IId IIdentity ('Identity a) a
-> g a -> (:*:) (IIdentity ('Identity a)) g a
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) = h a -> PIdentity h ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (h a -> PIdentity h ('Identity a))
-> m (h a) -> m (PIdentity h ('Identity a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
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) = j a -> PIdentity j ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
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) = h (Apply ff a) -> PIdentity h ('Identity (Apply ff a))
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (h (Apply ff a) -> PIdentity h ('Identity (Apply ff a)))
-> m (h (Apply ff a)) -> m (PIdentity h ('Identity (Apply ff a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
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) = g a -> PIdentity g ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (g a -> PIdentity g ('Identity a))
-> f (g a) -> f (PIdentity g ('Identity a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
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 g a -> Rec g '[] -> Rec g '[a]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
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 = r
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 = g a -> PIdentity g ('Identity a)
(forall (a :: k). g a) -> Prod Identity g ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity
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 = g a -> PIdentity g ('Identity a)
(forall (a :: a). c a => g a) -> Prod Identity g ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity
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) = Compose (Dict c) g a -> PIdentity (Dict c :. g) ('Identity a)
forall {k} (f :: k -> *) (a :: k). f a -> PIdentity f ('Identity a)
PIdentity (Compose (Dict c) g a -> PIdentity (Dict c :. g) ('Identity a))
-> Compose (Dict c) g a -> PIdentity (Dict c :. g) ('Identity a)
forall a b. (a -> b) -> a -> b
$ Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
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 = Rec (Index rs) rs -> Index rs r
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
forall (f :: k -> *). (RecElemFCtx Rec f, r ~ r) => Rec f rs -> f r
rgetC Rec (Index rs) rs
Prod [] (Elem [] rs) rs
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 -> f a -> CoRec f as
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 -> Maybe (CoRec f as) -> CoRec f as
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (CoRec f as) -> CoRec f as)
-> (Rec (Maybe :. f) as -> Maybe (CoRec f as))
-> Rec (Maybe :. f) as
-> CoRec f as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Maybe :. f) as -> Maybe (CoRec f as)
forall {k} (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField (Rec (Maybe :. f) as -> CoRec f as)
-> Rec (Maybe :. f) as -> CoRec f as
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Index (b : bs) a -> (:.) Maybe f a)
-> Prod [] (Index (b : bs)) (b : bs)
-> Prod [] (Maybe :. f) (b : bs)
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 bs a -> f a -> Index (b : bs) a -> Compose Maybe f a
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) Prod [] (Index (b : bs)) (b : bs)
Prod [] (Elem [] (b : bs)) (b : bs)
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 Index (b : bs) a -> Index (b : bs) c -> Maybe (a :~: c)
forall {k} (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal (Index bs a -> Index (b : bs) a
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 -> Maybe (f c) -> Compose Maybe f c
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (f c -> Maybe (f c)
forall a. a -> Maybe a
Just f a
f c
x)
Maybe (a :~: c)
Nothing -> Maybe (f c) -> Compose Maybe f c
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose Maybe (f c)
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 Index as a -> Sing a -> CoRec Sing as
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 Sing a -> Sing a1 -> Decision (a :~: a1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a1
y of
Proved a :~: a1
Refl -> r -> r
(RElem a as (RIndex a as) => r) -> r
forall a. a -> a
id
Disproved Refuted (a :~: a1)
_ -> \RElem a as (RIndex a as) => r
_ -> String -> r
forall a. String -> a
errorWithoutStackTrace String
"why :|"
where
x :: Sing a
x = Sing a
forall {k} (a :: k). SingI a => Sing a
sing