{-# LANGUAGE UndecidableInstances #-}
module Data.Hefty.Extensible where
import Control.Effect.Class (Signature)
import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)
import Data.Extensible (Forall, Match (Match), htabulateFor, leadership, match)
import Data.Extensible.Sum (exhaust, strikeAt, (<:|), type (:/) (EmbedAt))
import Data.Free.Extensible (TypeIndex, findFirstMembership)
import Data.Hefty.Union (
UnionH (
HasMembershipH,
absurdUnionH,
inject0H,
injectH,
projectH,
weakenH,
(|+:)
),
)
import Data.Proxy (Proxy (Proxy))
import GHC.TypeNats (KnownNat)
import Type.Membership (nextMembership)
newtype ExtensibleUnionH hs f a = ExtensibleUnionH {forall (hs :: [Signature]) (f :: * -> *) a.
ExtensibleUnionH hs f a -> hs :/ FieldAppH f a
unExtensibleUnionH :: hs :/ FieldAppH f a}
newtype FieldAppH f a (h :: Signature) = FieldAppH {forall (f :: * -> *) a (h :: Signature). FieldAppH f a h -> h f a
unFieldAppH :: h f a}
instance Forall HFunctor hs => HFunctor (ExtensibleUnionH hs) where
hfmap :: forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> ExtensibleUnionH hs f :-> ExtensibleUnionH hs g
hfmap f :-> g
f =
forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (xs :: [k]) (h :: k -> *) a.
(xs :& Match h a) -> (xs :/ h) -> a
match
( forall {k} (c :: k -> Constraint) (xs :: [k])
(proxy :: (k -> Constraint) -> *) (h :: k -> *).
Forall c xs =>
proxy c
-> (forall (x :: k). c x => Membership xs x -> h x) -> xs :& h
htabulateFor @HFunctor forall {k} (t :: k). Proxy t
Proxy \Membership hs x
w ->
forall {k} (h :: k -> *) r (x :: k). (h x -> r) -> Match h r x
Match forall a b. (a -> b) -> a -> b
$ forall {k} (xs :: [k]) (x :: k) (h :: k -> *).
Membership xs x -> h x -> xs :/ h
EmbedAt Membership hs x
w forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). h f a -> FieldAppH f a h
FieldAppH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: Signature) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap f :-> g
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). FieldAppH f a h -> h f a
unFieldAppH
)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (hs :: [Signature]) (f :: * -> *) a.
ExtensibleUnionH hs f a -> hs :/ FieldAppH f a
unExtensibleUnionH
{-# INLINE hfmap #-}
instance UnionH ExtensibleUnionH where
type HasMembershipH _ h hs = KnownNat (TypeIndex hs h)
injectH :: forall (h :: Signature) (hs :: [Signature]) (f :: * -> *).
HasMembershipH ExtensibleUnionH h hs =>
h f ~> ExtensibleUnionH hs f
injectH = forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (xs :: [k]) (x :: k) (h :: k -> *).
Membership xs x -> h x -> xs :/ h
EmbedAt forall {k} (xs :: [k]) (x :: k).
KnownNat (TypeIndex xs x) =>
Membership xs x
findFirstMembership forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). h f a -> FieldAppH f a h
FieldAppH
{-# INLINE injectH #-}
projectH :: forall (h :: Signature) (hs :: [Signature]) (f :: * -> *) a.
HasMembershipH ExtensibleUnionH h hs =>
ExtensibleUnionH hs f a -> Maybe (h f a)
projectH (ExtensibleUnionH hs :/ FieldAppH f a
u) = forall (f :: * -> *) a (h :: Signature). FieldAppH f a h -> h f a
unFieldAppH forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (h :: k -> *) (x :: k) (xs :: [k]).
Membership xs x -> (xs :/ h) -> Maybe (h x)
strikeAt forall {k} (xs :: [k]) (x :: k).
KnownNat (TypeIndex xs x) =>
Membership xs x
findFirstMembership hs :/ FieldAppH f a
u
{-# INLINE projectH #-}
absurdUnionH :: forall (f :: * -> *) a x. ExtensibleUnionH '[] f a -> x
absurdUnionH = forall {k} (h :: k -> *) r. ('[] :/ h) -> r
exhaust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (hs :: [Signature]) (f :: * -> *) a.
ExtensibleUnionH hs f a -> hs :/ FieldAppH f a
unExtensibleUnionH
{-# INLINE absurdUnionH #-}
inject0H :: forall (h :: Signature) (f :: * -> *) (hs :: [Signature]).
h f ~> ExtensibleUnionH (h : hs) f
inject0H = forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (xs :: [k]) (x :: k) (h :: k -> *).
Membership xs x -> h x -> xs :/ h
EmbedAt forall {k} (x :: k) (xs :: [k]). Membership (x : xs) x
leadership forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). h f a -> FieldAppH f a h
FieldAppH
{-# INLINE inject0H #-}
weakenH :: forall (hs :: [Signature]) (f :: * -> *) (h :: Signature).
ExtensibleUnionH hs f ~> ExtensibleUnionH (h : hs) f
weakenH (ExtensibleUnionH (EmbedAt Membership hs x
w FieldAppH f x x
e)) =
forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH forall a b. (a -> b) -> a -> b
$ forall {k} (xs :: [k]) (x :: k) (h :: k -> *).
Membership xs x -> h x -> xs :/ h
EmbedAt (forall {k} (xs :: [k]) (y :: k) (x :: k).
Membership xs y -> Membership (x : xs) y
nextMembership Membership hs x
w) FieldAppH f x x
e
{-# INLINE weakenH #-}
h f a -> r
f |+: :: forall (h :: Signature) (f :: * -> *) a r (hs :: [Signature]).
(h f a -> r)
-> (ExtensibleUnionH hs f a -> r)
-> ExtensibleUnionH (h : hs) f a
-> r
|+: ExtensibleUnionH hs f a -> r
g = (h f a -> r
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (h :: Signature). FieldAppH f a h -> h f a
unFieldAppH forall {k} (h :: k -> *) (x :: k) r (xs :: [k]).
(h x -> r) -> ((xs :/ h) -> r) -> ((x : xs) :/ h) -> r
<:| ExtensibleUnionH hs f a -> r
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (hs :: [Signature]) (f :: * -> *) a.
(hs :/ FieldAppH f a) -> ExtensibleUnionH hs f a
ExtensibleUnionH) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (hs :: [Signature]) (f :: * -> *) a.
ExtensibleUnionH hs f a -> hs :/ FieldAppH f a
unExtensibleUnionH
{-# INLINE (|+:) #-}