{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Functor.XProduct (
XProd
, fromXProd
, toXProd
, mapProdX, mapProdXEndo
, imapProdX, zipWithProdX
, ixProdX, traverseProdX, traverseProdXEndo, itraverseProdX
, foldMapProdX, ifoldMapProdX
, XRec, pattern (::&), pattern XRNil
, XMaybe, pattern XNothing, pattern XJust
, XEither, pattern XLeft, pattern XRight
, XNERec, pattern (::&|)
, XTup, pattern XTup
, XIdentity, pattern XIdentity
) where
import Data.Functor.Identity
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
import Data.Singletons
import Data.Type.Functor.Product
import Data.Vinyl
import Data.Vinyl.XRec
import Lens.Micro
import qualified Data.Vinyl.Functor as V
type XProd f g = (Prod f (XData g) :: f k -> Type)
fromXProd :: forall f g as. (FProd f, PureProdC f (IsoHKD g) as) => XProd f g as -> Prod f g as
fromXProd :: XProd f g as -> Prod f g as
fromXProd = (forall (a :: k). Lift (->) (XData g) g a -> XData g a -> g a)
-> Prod f (Lift (->) (XData g) g) as -> XProd f g as -> Prod f g 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.Lift u) x :: XData g a
x -> XData g a -> g a
u XData g a
x)
((forall (a :: k). IsoHKD g a => Lift (->) (XData g) g a)
-> Prod f (Lift (->) (XData g) g) as
forall k (f :: * -> *) (c :: k -> Constraint) (as :: f k)
(g :: k -> *).
PureProdC f c as =>
(forall (a :: k). c a => g a) -> Prod f g as
pureProdC @_ @(IsoHKD g) ((XData g a -> g a) -> Lift (->) (XData g) g a
forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l')
(x :: k).
op (f x) (g x) -> Lift op f g x
V.Lift (HKD g a -> g a
forall k (f :: k -> *) (a :: k). IsoHKD f a => HKD f a -> f a
unHKD (HKD g a -> g a) -> (XData g a -> HKD g a) -> XData g a -> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData g a -> HKD g a
forall k (t :: k -> *) (a :: k). XData t a -> HKD t a
unX)))
toXProd :: forall f g as. (FProd f, PureProdC f (IsoHKD g) as) => Prod f g as -> XProd f g as
toXProd :: Prod f g as -> XProd f g as
toXProd = (forall (a :: k). Lift (->) g (XData g) a -> g a -> XData g a)
-> Prod f (Lift (->) g (XData g)) as -> Prod f g as -> XProd f g 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.Lift u) x :: g a
x -> g a -> XData g a
u g a
x)
((forall (a :: k). IsoHKD g a => Lift (->) g (XData g) a)
-> Prod f (Lift (->) g (XData g)) as
forall k (f :: * -> *) (c :: k -> Constraint) (as :: f k)
(g :: k -> *).
PureProdC f c as =>
(forall (a :: k). c a => g a) -> Prod f g as
pureProdC @_ @(IsoHKD g) ((g a -> XData g a) -> Lift (->) g (XData g) a
forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l')
(x :: k).
op (f x) (g x) -> Lift op f g x
V.Lift (HKD g a -> XData g a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> XData g a) -> (g a -> HKD g a) -> g a -> XData g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> HKD g a
forall k (f :: k -> *) (a :: k). IsoHKD f a => f a -> HKD f a
toHKD)))
mapProdX
:: forall f g h as. FProd f
=> (forall a. HKD g a -> HKD h a)
-> XProd f g as
-> XProd f h as
mapProdX :: (forall (a :: k). HKD g a -> HKD h a)
-> XProd f g as -> XProd f h as
mapProdX f :: forall (a :: k). HKD g a -> HKD h a
f = (forall (a :: k). XData g a -> XData h a)
-> XProd f g as -> XProd 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 ((forall (a :: k). XData g a -> XData h a)
-> XProd f g as -> XProd f h as)
-> (forall (a :: k). XData g a -> XData h a)
-> XProd f g as
-> XProd f h as
forall a b. (a -> b) -> a -> b
$ \(XData x :: XData g a) -> HKD h a -> XData h a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> HKD h a
forall (a :: k). HKD g a -> HKD h a
f @a HKD g a
x)
mapProdXEndo
:: forall f g as. FProd f
=> (forall a. HKD g a -> HKD g a)
-> XProd f g as
-> XProd f g as
mapProdXEndo :: (forall (a :: k). HKD g a -> HKD g a)
-> XProd f g as -> XProd f g as
mapProdXEndo f :: forall (a :: k). HKD g a -> HKD g a
f = (forall (a :: k). XData g a -> XData g a)
-> XProd f g as -> XProd 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 ((forall (a :: k). XData g a -> XData g a)
-> XProd f g as -> XProd f g as)
-> (forall (a :: k). XData g a -> XData g a)
-> XProd f g as
-> XProd f g as
forall a b. (a -> b) -> a -> b
$ \(XData x :: XData g a) -> HKD g a -> XData g a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> HKD g a
forall (a :: k). HKD g a -> HKD g a
f @a HKD g a
x)
imapProdX
:: forall f g h as. FProd f
=> (forall a. Elem f as a -> HKD g a -> HKD h a)
-> XProd f g as
-> XProd f h as
imapProdX :: (forall (a :: k). Elem f as a -> HKD g a -> HKD h a)
-> XProd f g as -> XProd f h as
imapProdX f :: forall (a :: k). Elem f as a -> HKD g a -> HKD h a
f = (forall (a :: k). Elem f as a -> XData g a -> XData h a)
-> XProd f g as -> XProd f h 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 ((forall (a :: k). Elem f as a -> XData g a -> XData h a)
-> XProd f g as -> XProd f h as)
-> (forall (a :: k). Elem f as a -> XData g a -> XData h a)
-> XProd f g as
-> XProd f h as
forall a b. (a -> b) -> a -> b
$ \i :: Elem f as a
i -> HKD h a -> XData h a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD h a -> XData h a)
-> (XData g a -> HKD h a) -> XData g a -> XData h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elem f as a -> HKD g a -> HKD h a
forall (a :: k). Elem f as a -> HKD g a -> HKD h a
f Elem f as a
i (HKD g a -> HKD h a)
-> (XData g a -> HKD g a) -> XData g a -> HKD h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData g a -> HKD g a
forall k (t :: k -> *) (a :: k). XData t a -> HKD t a
unX
zipWithProdX
:: forall f g h j as. FProd f
=> (forall a. HKD g a -> HKD h a -> HKD j a)
-> XProd f g as
-> XProd f h as
-> XProd f j as
zipWithProdX :: (forall (a :: k). HKD g a -> HKD h a -> HKD j a)
-> XProd f g as -> XProd f h as -> XProd f j as
zipWithProdX f :: forall (a :: k). HKD g a -> HKD h a -> HKD j a
f = (forall (a :: k). XData g a -> XData h a -> XData j a)
-> XProd f g as -> XProd f h as -> XProd 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 ((forall (a :: k). XData g a -> XData h a -> XData j a)
-> XProd f g as -> XProd f h as -> XProd f j as)
-> (forall (a :: k). XData g a -> XData h a -> XData j a)
-> XProd f g as
-> XProd f h as
-> XProd f j as
forall a b. (a -> b) -> a -> b
$ \(XData x :: XData g a) (XData y) -> HKD j a -> XData j a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> HKD h a -> HKD j a
forall (a :: k). HKD g a -> HKD h a -> HKD j a
f @a HKD g a
x HKD h a
y)
ixProdX
:: FProd f
=> Elem f as a
-> Lens' (XProd f g as) (HKD g a)
ixProdX :: Elem f as a -> Lens' (XProd f g as) (HKD g a)
ixProdX i :: Elem f as a
i = Elem f as a -> Lens' (XProd f g as) (XData 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 ((XData g a -> f (XData g a)) -> XProd f g as -> f (XProd f g as))
-> ((HKD g a -> f (HKD g a)) -> XData g a -> f (XData g a))
-> (HKD g a -> f (HKD g a))
-> XProd f g as
-> f (XProd f g as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\f :: HKD g a -> f (HKD g a)
f (XData x :: HKD g a
x) -> HKD g a -> XData g a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> XData g a) -> f (HKD g a) -> f (XData g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HKD g a -> f (HKD g a)
f HKD g a
x)
traverseProdX
:: forall f g h m as. (FProd f, Applicative m)
=> (forall a. HKD g a -> m (HKD h a))
-> XProd f g as
-> m (XProd f h as)
traverseProdX :: (forall (a :: k). HKD g a -> m (HKD h a))
-> XProd f g as -> m (XProd f h as)
traverseProdX f :: forall (a :: k). HKD g a -> m (HKD h a)
f = (forall (a :: k). XData g a -> m (XData h a))
-> XProd f g as -> m (XProd 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 ((forall (a :: k). XData g a -> m (XData h a))
-> XProd f g as -> m (XProd f h as))
-> (forall (a :: k). XData g a -> m (XData h a))
-> XProd f g as
-> m (XProd f h as)
forall a b. (a -> b) -> a -> b
$ \(XData x :: XData g a) -> HKD h a -> XData h a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD h a -> XData h a) -> m (HKD h a) -> m (XData h a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HKD g a -> m (HKD h a)
forall (a :: k). HKD g a -> m (HKD h a)
f @a HKD g a
x
traverseProdXEndo
:: forall f g m as. (FProd f, Applicative m)
=> (forall a. HKD g a -> m (HKD g a))
-> XProd f g as
-> m (XProd f g as)
traverseProdXEndo :: (forall (a :: k). HKD g a -> m (HKD g a))
-> XProd f g as -> m (XProd f g as)
traverseProdXEndo f :: forall (a :: k). HKD g a -> m (HKD g a)
f = (forall (a :: k). XData g a -> m (XData g a))
-> XProd f g as -> m (XProd f g 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 ((forall (a :: k). XData g a -> m (XData g a))
-> XProd f g as -> m (XProd f g as))
-> (forall (a :: k). XData g a -> m (XData g a))
-> XProd f g as
-> m (XProd f g as)
forall a b. (a -> b) -> a -> b
$ \(XData x :: XData g a) -> HKD g a -> XData g a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (HKD g a -> XData g a) -> m (HKD g a) -> m (XData g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HKD g a -> m (HKD g a)
forall (a :: k). HKD g a -> m (HKD g a)
f @a HKD g a
x
itraverseProdX
:: forall f g h m as. (FProd f, Applicative m)
=> (forall a. Elem f as a -> HKD g a -> m (HKD h a))
-> XProd f g as
-> m (XProd f h as)
itraverseProdX :: (forall (a :: k). Elem f as a -> HKD g a -> m (HKD h a))
-> XProd f g as -> m (XProd f h as)
itraverseProdX f :: forall (a :: k). Elem f as a -> HKD g a -> m (HKD h a)
f = (forall (a :: k). Elem f as a -> XData g a -> m (XData h a))
-> XProd f g as -> m (XProd f h 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 ((forall (a :: k). Elem f as a -> XData g a -> m (XData h a))
-> XProd f g as -> m (XProd f h as))
-> (forall (a :: k). Elem f as a -> XData g a -> m (XData h a))
-> XProd f g as
-> m (XProd f h as)
forall a b. (a -> b) -> a -> b
$ \i :: Elem f as a
i -> (HKD h a -> XData h a) -> m (HKD h a) -> m (XData h a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HKD h a -> XData h a
forall k (t :: k -> *) (a :: k). HKD t a -> XData t a
XData (m (HKD h a) -> m (XData h a))
-> (XData g a -> m (HKD h a)) -> XData g a -> m (XData h a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elem f as a -> HKD g a -> m (HKD h a)
forall (a :: k). Elem f as a -> HKD g a -> m (HKD h a)
f Elem f as a
i (HKD g a -> m (HKD h a))
-> (XData g a -> HKD g a) -> XData g a -> m (HKD h a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData g a -> HKD g a
forall k (t :: k -> *) (a :: k). XData t a -> HKD t a
unX
foldMapProdX
:: forall f g m as. (FProd f, Monoid m)
=> (forall a. HKD g a -> m)
-> XProd f g as
-> m
foldMapProdX :: (forall (a :: k). HKD g a -> m) -> XProd f g as -> m
foldMapProdX f :: forall (a :: k). HKD g a -> m
f = (forall (a :: k). XData g a -> m) -> XProd f g as -> m
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). XData g a -> m) -> XProd f g as -> m)
-> (forall (a :: k). XData g a -> m) -> XProd f g as -> m
forall a b. (a -> b) -> a -> b
$ \(XData x :: XData g a) -> HKD g a -> m
forall (a :: k). HKD g a -> m
f @a HKD g a
x
ifoldMapProdX
:: forall f g m as. (FProd f, Monoid m)
=> (forall a. Elem f as a -> HKD g a -> m)
-> XProd f g as
-> m
ifoldMapProdX :: (forall (a :: k). Elem f as a -> HKD g a -> m) -> XProd f g as -> m
ifoldMapProdX f :: forall (a :: k). Elem f as a -> HKD g a -> m
f = (forall (a :: k). Elem f as a -> XData g a -> m)
-> XProd 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 ((forall (a :: k). Elem f as a -> XData g a -> m)
-> XProd f g as -> m)
-> (forall (a :: k). Elem f as a -> XData g a -> m)
-> XProd f g as
-> m
forall a b. (a -> b) -> a -> b
$ \i :: Elem f as a
i -> Elem f as a -> HKD g a -> m
forall (a :: k). Elem f as a -> HKD g a -> m
f Elem f as a
i (HKD g a -> m) -> (XData g a -> HKD g a) -> XData g a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XData g a -> HKD g a
forall k (t :: k -> *) (a :: k). XData t a -> HKD t a
unX
type XMaybe f = PMaybe (XData f)
type XEither f = PEither (XData f)
type XNERec f = NERec (XData f)
type XTup f = PTup (XData f)
type XIdentity f = PIdentity (XData f)
pattern XNothing :: XMaybe f 'Nothing
pattern $bXNothing :: XMaybe f 'Nothing
$mXNothing :: forall r k (f :: k -> *).
XMaybe f 'Nothing -> (Void# -> r) -> (Void# -> r) -> r
XNothing = PNothing
pattern XJust :: HKD f a -> XMaybe f ('Just a)
pattern $bXJust :: HKD f a1 -> XMaybe f ('Just a1)
$mXJust :: forall r a (f :: a -> *) (a1 :: a).
XMaybe f ('Just a1) -> (HKD f a1 -> r) -> (Void# -> r) -> r
XJust x = PJust (XData x)
pattern XLeft :: Sing e -> XEither f ('Left e)
pattern $bXLeft :: Sing e -> XEither f ('Left e)
$mXLeft :: forall r j k (e :: j) (f :: k -> *).
XEither f ('Left e) -> (Sing e -> r) -> (Void# -> r) -> r
XLeft e = PLeft e
pattern XRight :: HKD f a -> XEither f ('Right a)
pattern $bXRight :: HKD f a -> XEither f ('Right a)
$mXRight :: forall r b j (f :: b -> *) (a :: b).
XEither f ('Right a) -> (HKD f a -> r) -> (Void# -> r) -> r
XRight x = PRight (XData x)
pattern (::&|) :: HKD f a -> XRec f as -> XNERec f (a ':| as)
pattern x $b::&| :: HKD f a1 -> XRec f as -> XNERec f (a1 ':| as)
$m::&| :: forall r a (f :: a -> *) (a1 :: a) (as :: [a]).
XNERec f (a1 ':| as)
-> (HKD f a1 -> XRec f as -> r) -> (Void# -> r) -> r
::&| xs = XData x :&| xs
pattern XTup :: Sing w -> HKD f a -> XTup f '(w, a)
pattern $bXTup :: Sing w -> HKD f a -> XTup f '(w, a)
$mXTup :: forall r j k (w :: j) (f :: k -> *) (a :: k).
XTup f '(w, a) -> (Sing w -> HKD f a -> r) -> (Void# -> r) -> r
XTup w x = PTup w (XData x)
pattern XIdentity :: HKD f a -> XIdentity f ('Identity a)
pattern $bXIdentity :: HKD f a1 -> XIdentity f ('Identity a1)
$mXIdentity :: forall r a (f :: a -> *) (a1 :: a).
XIdentity f ('Identity a1) -> (HKD f a1 -> r) -> (Void# -> r) -> r
XIdentity x = PIdentity (XData x)
{-# COMPLETE (::&|) #-}
{-# COMPLETE XIdentity #-}
{-# COMPLETE XJust #-}
{-# COMPLETE XLeft #-}
{-# COMPLETE XNothing #-}
{-# COMPLETE XRight #-}
{-# COMPLETE XTup #-}