[WIP] union manipulation.

heftia/heftia.cabal

@@ -60,12 +60,17 @@ source-repository head
 library
     exposed-modules:
         Control.Monad.Hefty
+        Control.Monad.Hefty.Types
+        Control.Monad.Hefty.Interpret
+        Control.Monad.Hefty.Interpret.State
+        Control.Monad.Hefty.Transform
         Data.Effect.OpenUnion
         Data.Effect.OpenUnion.Internal
         Data.Effect.OpenUnion.Internal.FO
         Data.Effect.OpenUnion.Internal.HO
         Data.Effect.OpenUnion.Internal.Weaken
         Data.Effect.OpenUnion.Internal.Strengthen
+        Data.Effect.OpenUnion.Internal.Bundle
 
     reexported-modules:
         Data.Effect,

heftia/src/Control/Monad/Hefty/Interpret.hs

@@ -0,0 +1,465 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+-- SPDX-License-Identifier: MPL-2.0
+
+module Control.Monad.Hefty.Interpret where
+
+import Control.Arrow ((>>>))
+import Control.Effect (type (~>))
+import Control.Monad.Hefty.Types (
+    Eff (Op, Val),
+    Elab,
+    Elaborator,
+    Interpreter,
+    sendUnionBy,
+    sendUnionHBy,
+ )
+import Data.Effect.HFunctor (HFunctor, hfmap)
+import Data.Effect.OpenUnion.Internal.FO (
+    Member (prj),
+    Union,
+    extract,
+    nil,
+    weakenN,
+    weakens,
+    (!+),
+    type (<!),
+ )
+import Data.Effect.OpenUnion.Internal.HO (
+    MemberH (prjH),
+    UnionH,
+    extractH,
+    hfmapUnion,
+    nilH,
+    weakenNH,
+    weakensH,
+    (!!+),
+    type (<!!),
+ )
+import Data.Effect.OpenUnion.Internal.Weaken (IsSuffixOf, Weaken)
+import Data.FTCQueue (FTCQueue, ViewL (TOne, (:|)), tviewl, (><))
+
+{- | Iteratively interprets all effects in an 'Eff' computation.
+The function takes interpreters for higher-order effects and first-order effects, and applies them.
+-}
+iterAllEffHFBy
+    :: forall eh ef m ans a
+     . (Monad m)
+    => (a -> m ans)
+    -> Interpreter (UnionH eh (Eff eh ef)) m ans
+    -> Interpreter (Union ef) m ans
+    -> Eff eh ef a
+    -> m ans
+iterAllEffHFBy ret fh ff = loop
+  where
+    loop = \case
+        Val x -> ret x
+        Op u q -> either fh ff u k
+          where
+            k = loop . qApp q
+{-# INLINE iterAllEffHFBy #-}
+
+qApp :: FTCQueue (Eff eh ef) a b -> a -> Eff eh ef b
+qApp q' x = case tviewl q' of
+    TOne k -> k x
+    k :| t -> case k x of
+        Val y -> qApp t y
+        Op u q -> Op u (q >< t)
+
+-- | Lifts a natural transformation into an interpreter.
+plain :: forall e m ans. (Monad m) => (e ~> m) -> Interpreter e m ans
+plain i e k = i e >>= k
+{-# INLINE plain #-}
+
+iterEffBy :: forall e m ans a. (Monad m) => (a -> m ans) -> Interpreter e m ans -> Eff '[] '[e] a -> m ans
+iterEffBy ret hdl = iterAllEffHFBy ret nilH (hdl . extract)
+{-# INLINE iterEffBy #-}
+
+iterEffHBy :: forall e m ans a. (Monad m, HFunctor e) => (a -> m ans) -> Interpreter (e (Eff '[e] '[])) m ans -> Eff '[e] '[] a -> m ans
+iterEffHBy ret elb = iterAllEffHFBy ret (elb . extractH) nil
+{-# INLINE iterEffHBy #-}
+
+iterEffRecHWith :: forall e m. (Monad m, HFunctor e) => (forall ans. Elaborator e m ans) -> Eff '[e] '[] ~> m
+iterEffRecHWith elb = loop
+  where
+    loop :: Eff '[e] '[] ~> m
+    loop = iterEffHBy pure (elb . hfmap loop)
+{-# INLINE iterEffRecHWith #-}
+
+iterEffRecH :: forall e m. (Monad m, HFunctor e) => Elab e m -> Eff '[e] '[] ~> m
+iterEffRecH elb = iterEffRecHWith $ plain elb
+{-# INLINE iterEffRecH #-}
+
+iterEffHFBy
+    :: forall eh ef m ans a
+     . (Monad m, HFunctor eh)
+    => (a -> m ans)
+    -> Interpreter (eh (Eff '[eh] '[ef])) m ans
+    -> Interpreter ef m ans
+    -> Eff '[eh] '[ef] a
+    -> m ans
+iterEffHFBy ret elb hdl = iterAllEffHFBy ret (elb . extractH) (hdl . extract)
+{-# INLINE iterEffHFBy #-}
+
+iterEffRecHFWith
+    :: forall eh ef m
+     . (Monad m, HFunctor eh)
+    => (forall ans. Elaborator eh m ans)
+    -> (forall ans. Interpreter ef m ans)
+    -> Eff '[eh] '[ef] ~> m
+iterEffRecHFWith fh ff = loop
+  where
+    loop :: Eff '[eh] '[ef] ~> m
+    loop = iterEffHFBy pure (fh . hfmap loop) ff
+{-# INLINE iterEffRecHFWith #-}
+
+runEff :: (Monad m) => Eff '[] '[m] ~> m
+runEff = iterEffBy pure $ plain id
+{-# INLINE runEff #-}
+
+runPure :: Eff '[] '[] a -> a
+runPure = loop
+  where
+    loop = \case
+        Val x -> x
+        Op u _ -> case u of
+            Left u' -> nilH u'
+            Right u' -> nil u'
+{-# INLINE runPure #-}
+
+interpretBy
+    :: forall e ef ans a
+     . (a -> Eff '[] ef ans)
+    -> Interpreter e (Eff '[] ef) ans
+    -> Eff '[] (e ': ef) a
+    -> Eff '[] ef ans
+interpretBy = reinterpretBy
+{-# INLINE interpretBy #-}
+
+interpretWith
+    :: forall e ef a
+     . Interpreter e (Eff '[] ef) a
+    -> Eff '[] (e ': ef) a
+    -> Eff '[] ef a
+interpretWith = reinterpretWith
+{-# INLINE interpretWith #-}
+
+interpret
+    :: forall e ef
+     . (e ~> Eff '[] ef)
+    -> Eff '[] (e ': ef) ~> Eff '[] ef
+interpret = reinterpret
+{-# INLINE interpret #-}
+
+interpretRecWith
+    :: forall e ef eh a
+     . (forall ans. Interpreter e (Eff eh ef) ans)
+    -> Eff eh (e ': ef) a
+    -> Eff eh ef a
+interpretRecWith = reinterpretRecWith
+{-# INLINE interpretRecWith #-}
+
+interpretRec
+    :: forall e ef eh
+     . (e ~> Eff eh ef)
+    -> Eff eh (e ': ef) ~> Eff eh ef
+interpretRec = reinterpretRec
+{-# INLINE interpretRec #-}
+
+interpretHBy
+    :: forall e eh ef ans a
+     . (HFunctor e)
+    => (a -> Eff eh ef ans)
+    -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
+    -> Eff '[e] ef a
+    -> Eff eh ef ans
+interpretHBy = reinterpretHBy
+{-# INLINE interpretHBy #-}
+
+interpretHWith
+    :: forall e eh ef a
+     . (HFunctor e)
+    => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
+    -> Eff '[e] ef a
+    -> Eff eh ef a
+interpretHWith = reinterpretHWith
+{-# INLINE interpretHWith #-}
+
+interpretH
+    :: forall e eh ef
+     . (HFunctor e)
+    => (e (Eff '[e] ef) ~> Eff eh ef)
+    -> Eff '[e] ef ~> Eff eh ef
+interpretH = reinterpretH
+{-# INLINE interpretH #-}
+
+interpretRecHWith
+    :: forall e eh ef a
+     . (HFunctor e)
+    => (forall ans. Elaborator e (Eff eh ef) ans)
+    -> Eff (e ': eh) ef a
+    -> Eff eh ef a
+interpretRecHWith = reinterpretRecHWith
+{-# INLINE interpretRecHWith #-}
+
+interpretRecH
+    :: forall e eh ef
+     . (HFunctor e)
+    => Elab e (Eff eh ef)
+    -> Eff (e ': eh) ef ~> Eff eh ef
+interpretRecH = reinterpretRecH
+{-# INLINE interpretRecH #-}
+
+reinterpretBy
+    :: forall e ef' ef ans a
+     . (ef `IsSuffixOf` ef')
+    => (a -> Eff '[] ef' ans)
+    -> Interpreter e (Eff '[] ef') ans
+    -> Eff '[] (e ': ef) a
+    -> Eff '[] ef' ans
+reinterpretBy ret hdl = iterAllEffHFBy ret nilH (hdl !+ flip sendUnionBy . weakens)
+{-# INLINE reinterpretBy #-}
+
+reinterpretNBy
+    :: forall n e ef' ef ans a
+     . (Weaken n ef ef')
+    => (a -> Eff '[] ef' ans)
+    -> Interpreter e (Eff '[] ef') ans
+    -> Eff '[] (e ': ef) a
+    -> Eff '[] ef' ans
+reinterpretNBy ret hdl = iterAllEffHFBy ret nilH (hdl !+ flip sendUnionBy . weakenN @n)
+{-# INLINE reinterpretNBy #-}
+
+reinterpretWith
+    :: forall e ef' ef a
+     . (ef `IsSuffixOf` ef')
+    => Interpreter e (Eff '[] ef') a
+    -> Eff '[] (e ': ef) a
+    -> Eff '[] ef' a
+reinterpretWith = reinterpretBy pure
+{-# INLINE reinterpretWith #-}
+
+reinterpretNWith
+    :: forall n e ef' ef a
+     . (Weaken n ef ef')
+    => Interpreter e (Eff '[] ef') a
+    -> Eff '[] (e ': ef) a
+    -> Eff '[] ef' a
+reinterpretNWith = reinterpretNBy @n pure
+{-# INLINE reinterpretNWith #-}
+
+reinterpret :: forall e ef' ef. (ef `IsSuffixOf` ef') => (e ~> Eff '[] ef') -> Eff '[] (e ': ef) ~> Eff '[] ef'
+reinterpret f = reinterpretWith (plain f)
+{-# INLINE reinterpret #-}
+
+reinterpretN :: forall n e ef' ef. (Weaken n ef ef') => (e ~> Eff '[] ef') -> Eff '[] (e ': ef) ~> Eff '[] ef'
+reinterpretN f = reinterpretNWith @n (plain f)
+{-# INLINE reinterpretN #-}
+
+reinterpretRecWith
+    :: forall e ef' ef eh a
+     . (ef `IsSuffixOf` ef')
+    => (forall ans. Interpreter e (Eff eh ef') ans)
+    -> Eff eh (e ': ef) a
+    -> Eff eh ef' a
+reinterpretRecWith hdl = loop
+  where
+    loop :: Eff eh (e ': ef) ~> Eff eh ef'
+    loop = iterAllEffHFBy pure (flip sendUnionHBy . hfmap loop) (hdl !+ flip sendUnionBy . weakens)
+{-# INLINE reinterpretRecWith #-}
+
+reinterpretRecNWith
+    :: forall n e ef' ef eh a
+     . (Weaken n ef ef')
+    => (forall ans. Interpreter e (Eff eh ef') ans)
+    -> Eff eh (e ': ef) a
+    -> Eff eh ef' a
+reinterpretRecNWith hdl = loop
+  where
+    loop :: Eff eh (e ': ef) ~> Eff eh ef'
+    loop = iterAllEffHFBy pure (flip sendUnionHBy . hfmap loop) (hdl !+ flip sendUnionBy . weakenN @n)
+{-# INLINE reinterpretRecNWith #-}
+
+reinterpretRec :: forall e ef' ef eh. (ef `IsSuffixOf` ef') => (e ~> Eff eh ef') -> Eff eh (e ': ef) ~> Eff eh ef'
+reinterpretRec f = reinterpretRecWith (plain f)
+{-# INLINE reinterpretRec #-}
+
+reinterpretRecN :: forall n e ef' ef eh. (Weaken n ef ef') => (e ~> Eff eh ef') -> Eff eh (e ': ef) ~> Eff eh ef'
+reinterpretRecN f = reinterpretRecNWith @n (plain f)
+{-# INLINE reinterpretRecN #-}
+
+reinterpretHBy
+    :: forall e eh ef ans a
+     . (HFunctor e)
+    => (a -> Eff eh ef ans)
+    -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
+    -> Eff '[e] ef a
+    -> Eff eh ef ans
+reinterpretHBy ret elb = iterAllEffHFBy ret (elb !!+ nilH) (flip sendUnionBy)
+{-# INLINE reinterpretHBy #-}
+
+reinterpretNHBy
+    :: forall n e eh ef ans a
+     . (HFunctor e, Weaken n '[] eh)
+    => (a -> Eff eh ef ans)
+    -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
+    -> Eff '[e] ef a
+    -> Eff eh ef ans
+reinterpretNHBy = reinterpretHBy
+{-# INLINE reinterpretNHBy #-}
+
+reinterpretHWith
+    :: forall e eh ef a
+     . (HFunctor e)
+    => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
+    -> Eff '[e] ef a
+    -> Eff eh ef a
+reinterpretHWith = reinterpretHBy pure
+{-# INLINE reinterpretHWith #-}
+
+reinterpretNHWith
+    :: forall n e eh ef a
+     . (HFunctor e, Weaken n '[] eh)
+    => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
+    -> Eff '[e] ef a
+    -> Eff eh ef a
+reinterpretNHWith = reinterpretHWith
+{-# INLINE reinterpretNHWith #-}
+
+reinterpretH
+    :: forall e eh ef
+     . (HFunctor e)
+    => (e (Eff '[e] ef) ~> Eff eh ef)
+    -> Eff '[e] ef ~> Eff eh ef
+reinterpretH elb = reinterpretHWith (plain elb)
+{-# INLINE reinterpretH #-}
+
+reinterpretNH
+    :: forall n e eh ef
+     . (HFunctor e, Weaken n '[] eh)
+    => (e (Eff '[e] ef) ~> Eff eh ef)
+    -> Eff '[e] ef ~> Eff eh ef
+reinterpretNH = reinterpretH
+{-# INLINE reinterpretNH #-}
+
+reinterpretRecHWith
+    :: forall e eh eh' ef a
+     . (HFunctor e, eh `IsSuffixOf` eh')
+    => (forall ans. Elaborator e (Eff eh' ef) ans)
+    -> Eff (e ': eh) ef a
+    -> Eff eh' ef a
+reinterpretRecHWith elb = loop
+  where
+    loop :: Eff (e ': eh) ef ~> Eff eh' ef
+    loop =
+        iterAllEffHFBy
+            pure
+            (elb . hfmap loop !!+ flip sendUnionHBy . weakensH . hfmapUnion loop)
+            (flip sendUnionBy)
+{-# INLINE reinterpretRecHWith #-}
+
+reinterpretRecNHWith
+    :: forall n e eh eh' ef a
+     . (HFunctor e, Weaken n eh eh')
+    => (forall ans. Elaborator e (Eff eh' ef) ans)
+    -> Eff (e ': eh) ef a
+    -> Eff eh' ef a
+reinterpretRecNHWith elb = loop
+  where
+    loop :: Eff (e ': eh) ef ~> Eff eh' ef
+    loop =
+        iterAllEffHFBy
+            pure
+            (elb . hfmap loop !!+ flip sendUnionHBy . weakenNH @n . hfmapUnion loop)
+            (flip sendUnionBy)
+{-# INLINE reinterpretRecNHWith #-}
+
+reinterpretRecH
+    :: forall e eh eh' ef
+     . (HFunctor e, eh `IsSuffixOf` eh')
+    => Elab e (Eff eh' ef)
+    -> Eff (e ': eh) ef ~> Eff eh' ef
+reinterpretRecH elb = reinterpretRecHWith (plain elb)
+{-# INLINE reinterpretRecH #-}
+
+reinterpretRecNH
+    :: forall n e eh eh' ef
+     . (HFunctor e, Weaken n eh eh')
+    => Elab e (Eff eh' ef)
+    -> Eff (e ': eh) ef ~> Eff eh' ef
+reinterpretRecNH elb = reinterpretRecNHWith @n (plain elb)
+{-# INLINE reinterpretRecNH #-}
+
+interposeBy
+    :: forall e ef ans a
+     . (e <! ef)
+    => (a -> Eff '[] ef ans)
+    -> Interpreter e (Eff '[] ef) ans
+    -> Eff '[] ef a
+    -> Eff '[] ef ans
+interposeBy ret f = iterAllEffHFBy ret nilH \u -> maybe (`sendUnionBy` u) f (prj @e u)
+{-# INLINE interposeBy #-}
+
+interposeWith
+    :: forall e ef a
+     . (e <! ef)
+    => Interpreter e (Eff '[] ef) a
+    -> Eff '[] ef a
+    -> Eff '[] ef a
+interposeWith = interposeBy pure
+{-# INLINE interposeWith #-}
+
+interpose
+    :: forall e ef
+     . (e <! ef)
+    => (e ~> Eff '[] ef)
+    -> Eff '[] ef ~> Eff '[] ef
+interpose f = interposeWith (plain f)
+{-# INLINE interpose #-}
+
+interposeRecWith
+    :: forall e ef eh a
+     . (e <! ef)
+    => (forall ans. Interpreter e (Eff eh ef) ans)
+    -> Eff eh ef a
+    -> Eff eh ef a
+interposeRecWith f = loop
+  where
+    loop :: Eff eh ef ~> Eff eh ef
+    loop = iterAllEffHFBy
+        pure
+        (flip sendUnionHBy . hfmapUnion loop)
+        \u -> maybe (`sendUnionBy` u) f (prj @e u)
+{-# INLINE interposeRecWith #-}
+
+interposeRec
+    :: forall e ef eh
+     . (e <! ef)
+    => (e ~> Eff eh ef)
+    -> Eff eh ef ~> Eff eh ef
+interposeRec f = interposeRecWith (plain f)
+{-# INLINE interposeRec #-}
+
+interposeRecHWith
+    :: forall e eh ef a
+     . (e <!! eh, HFunctor e)
+    => (forall ans. Elaborator e (Eff eh ef) ans)
+    -> Eff eh ef a
+    -> Eff eh ef a
+interposeRecHWith f = loop
+  where
+    loop :: Eff eh ef ~> Eff eh ef
+    loop =
+        iterAllEffHFBy
+            pure
+            (hfmapUnion loop >>> \u -> maybe (`sendUnionHBy` u) f (prjH @e u))
+            (flip sendUnionBy)
+{-# INLINE interposeRecHWith #-}
+
+interposeRecH
+    :: forall e eh ef
+     . (e <!! eh, HFunctor e)
+    => Elab e (Eff eh ef)
+    -> Eff eh ef ~> Eff eh ef
+interposeRecH f = interposeRecHWith (plain f)
+{-# INLINE interposeRecH #-}

heftia/src/Control/Monad/Hefty/Interpret/State.hs

@@ -0,0 +1,3 @@
+-- SPDX-License-Identifier: MPL-2.0
+
+module Control.Monad.Hefty.Interpret.State where

heftia/src/Control/Monad/Hefty/Transform.hs

@@ -0,0 +1,230 @@
+-- SPDX-License-Identifier: MPL-2.0
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Control.Monad.Hefty.Transform where
+
+import Control.Effect (type (~>))
+import Control.Monad.Hefty.Interpret (interpret, iterAllEffHFBy, runPure)
+import Control.Monad.Hefty.Types (Eff, sendUnionBy, sendUnionHBy)
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.OpenUnion.Internal.Bundle (Bundle, BundleUnder)
+import Data.Effect.OpenUnion.Internal.FO (
+    Union,
+    bundleAllUnion,
+    bundleUnion,
+    bundleUnionUnder,
+    decomp,
+    inj,
+    prj,
+    strengthenN,
+    strengthenNUnderM,
+    unbundleAllUnion,
+    unbundleUnion,
+    unbundleUnionUnder,
+    weakenN,
+    weakenNUnderM,
+    weakens,
+    type (<!),
+ )
+import Data.Effect.OpenUnion.Internal.HO (
+    UnionH,
+    bundleAllUnionH,
+    bundleUnionH,
+    bundleUnionUnderH,
+    decompH,
+    hfmapUnion,
+    injH,
+    prjH,
+    strengthenNH,
+    strengthenNUnderMH,
+    unbundleAllUnionH,
+    unbundleUnionH,
+    unbundleUnionUnderH,
+    weakenH,
+    weakenNH,
+    weakenNUnderMH,
+    weakensH,
+    type (<!!),
+ )
+import Data.Effect.OpenUnion.Internal.Strengthen (Strengthen, StrengthenUnder)
+import Data.Effect.OpenUnion.Internal.Weaken (IsSuffixOf, Weaken, WeakenUnder)
+import Data.Effect.State (State)
+
+transform :: forall e e' ef eh. (e ~> e') -> Eff eh (e ': ef) ~> Eff eh (e' ': ef)
+transform f = transEffHF id (either id (inj . f) . decomp)
+{-# INLINE transform #-}
+
+transformH
+    :: forall e e' eh ef
+     . (HFunctor e)
+    => (e (Eff (e' ': eh) ef) ~> e' (Eff (e' ': eh) ef))
+    -> Eff (e ': eh) ef ~> Eff (e' ': eh) ef
+transformH f = transEffHF (either weakenH (injH . f) . decompH) id
+{-# INLINE transformH #-}
+
+translate :: forall e e' ef eh. (e' <! ef) => (e ~> e') -> Eff eh (e ': ef) ~> Eff eh ef
+translate f = transEffHF id (either id (inj . f) . decomp)
+{-# INLINE translate #-}
+
+translateH
+    :: forall e e' eh ef
+     . (e' <!! eh, HFunctor e)
+    => (e (Eff eh ef) ~> e' (Eff eh ef))
+    -> Eff (e ': eh) ef ~> Eff eh ef
+translateH f = transEffHF (either id (injH . f) . decompH) id
+{-# INLINE translateH #-}
+
+rewrite :: forall e ef eh. (e <! ef) => (e ~> e) -> Eff eh ef ~> Eff eh ef
+rewrite f = transEffHF id \u -> maybe u (inj . f) $ prj @e u
+{-# INLINE rewrite #-}
+
+rewriteH
+    :: forall e eh ef
+     . (e <!! eh, HFunctor e)
+    => (e (Eff eh ef) ~> e (Eff eh ef))
+    -> Eff eh ef ~> Eff eh ef
+rewriteH f = transEffHF (\u -> maybe u (injH . f) $ prjH @e u) id
+{-# INLINE rewriteH #-}
+
+raise :: (ef `IsSuffixOf` ef') => Eff eh ef ~> Eff eh ef'
+raise = transEffHF id weakens
+{-# INLINE raise #-}
+
+raiseN :: forall len ef ef' eh. (Weaken len ef ef') => Eff eh ef ~> Eff eh ef'
+raiseN = transEffHF id (weakenN @len)
+{-# INLINE raiseN #-}
+
+raiseNUnder
+    :: forall len offset ef ef' eh
+     . (WeakenUnder len offset ef ef')
+    => Eff eh ef ~> Eff eh ef'
+raiseNUnder = transEffHF id (weakenNUnderM @len @offset)
+{-# INLINE raiseNUnder #-}
+
+raiseH :: (eh `IsSuffixOf` eh') => Eff eh ef ~> Eff eh' ef
+raiseH = transEffHF weakensH id
+{-# INLINE raiseH #-}
+
+raiseNH :: forall len eh eh' ef. (Weaken len eh eh') => Eff eh ef ~> Eff eh' ef
+raiseNH = transEffHF (weakenNH @len) id
+{-# INLINE raiseNH #-}
+
+raiseNUnderH
+    :: forall len offset eh eh' ef
+     . (WeakenUnder len offset eh eh')
+    => Eff eh ef ~> Eff eh' ef
+raiseNUnderH = transEffHF (weakenNUnderMH @len @offset) id
+{-# INLINE raiseNUnderH #-}
+
+subsumeN :: forall len ef ef' eh. (Strengthen len ef ef') => Eff eh ef ~> Eff eh ef'
+subsumeN = transEffHF id (strengthenN @len)
+{-# INLINE subsumeN #-}
+
+subsumeNUnder
+    :: forall len offset ef ef' eh
+     . (StrengthenUnder len offset ef ef')
+    => Eff eh ef ~> Eff eh ef'
+subsumeNUnder = transEffHF id (strengthenNUnderM @len @offset)
+{-# INLINE subsumeNUnder #-}
+
+subsumeNH :: forall len eh eh' ef. (Strengthen len eh eh') => Eff eh ef ~> Eff eh' ef
+subsumeNH = transEffHF (strengthenNH @len) id
+{-# INLINE subsumeNH #-}
+
+subsumeNUnderH
+    :: forall len offset eh eh' ef
+     . (StrengthenUnder len offset eh eh')
+    => Eff eh ef ~> Eff eh' ef
+subsumeNUnderH = transEffHF (strengthenNUnderMH @len @offset) id
+{-# INLINE subsumeNUnderH #-}
+
+-- todo: add raiseUnder(H), subsume(H), subsumeUnder(H)
+
+bundle
+    :: forall ef bundle rest eh
+     . (Bundle ef bundle rest)
+    => Eff eh ef ~> Eff eh (Union bundle ': rest)
+bundle = transEffHF id bundleUnion
+{-# INLINE bundle #-}
+
+unbundle
+    :: forall ef bundle rest eh
+     . (Bundle ef bundle rest)
+    => Eff eh (Union bundle ': rest) ~> Eff eh ef
+unbundle = transEffHF id unbundleUnion
+{-# INLINE unbundle #-}
+
+bundleUnder
+    :: forall offset bundle ef ef' eh
+     . (BundleUnder Union offset ef ef' bundle)
+    => Eff eh ef ~> Eff eh ef'
+bundleUnder = transEffHF id (bundleUnionUnder @offset)
+{-# INLINE bundleUnder #-}
+
+unbundleUnder
+    :: forall offset bundle ef ef' eh
+     . (BundleUnder Union offset ef ef' bundle)
+    => Eff eh ef' ~> Eff eh ef
+unbundleUnder = transEffHF id (unbundleUnionUnder @offset)
+{-# INLINE unbundleUnder #-}
+
+bundleAll :: Eff eh ef ~> Eff eh '[Union ef]
+bundleAll = transEffHF id bundleAllUnion
+{-# INLINE bundleAll #-}
+
+unbundleAll :: Eff eh '[Union ef] ~> Eff eh ef
+unbundleAll = transEffHF id unbundleAllUnion
+{-# INLINE unbundleAll #-}
+
+bundleH
+    :: forall eh bundle rest ef
+     . (Bundle eh bundle rest)
+    => Eff eh ef ~> Eff (UnionH bundle ': rest) ef
+bundleH = transEffHF bundleUnionH id
+{-# INLINE bundleH #-}
+
+unbundleH
+    :: forall eh bundle rest ef
+     . (Bundle eh bundle rest)
+    => Eff (UnionH bundle ': rest) ef ~> Eff eh ef
+unbundleH = transEffHF unbundleUnionH id
+{-# INLINE unbundleH #-}
+
+bundleUnderH
+    :: forall offset bundle eh eh' ef
+     . (BundleUnder UnionH offset eh eh' bundle)
+    => Eff eh ef ~> Eff eh' ef
+bundleUnderH = transEffHF (bundleUnionUnderH @offset) id
+{-# INLINE bundleUnderH #-}
+
+unbundleUnderH
+    :: forall offset bundle eh eh' ef
+     . (BundleUnder UnionH offset eh eh' bundle)
+    => Eff eh' ef ~> Eff eh ef
+unbundleUnderH = transEffHF (unbundleUnionUnderH @offset) id
+{-# INLINE unbundleUnderH #-}
+
+bundleAllH :: Eff eh ef ~> Eff '[UnionH eh] ef
+bundleAllH = transEffHF bundleAllUnionH id
+{-# INLINE bundleAllH #-}
+
+unbundleAllH :: Eff '[UnionH eh] ef ~> Eff eh ef
+unbundleAllH = transEffHF unbundleAllUnionH id
+{-# INLINE unbundleAllH #-}
+
+transEffHF
+    :: forall eh eh' ef ef'
+     . (UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef'))
+    -> (Union ef ~> Union ef')
+    -> Eff eh ef ~> Eff eh' ef'
+transEffHF fh ff = loop
+  where
+    loop :: Eff eh ef ~> Eff eh' ef'
+    loop =
+        iterAllEffHFBy
+            pure
+            (flip sendUnionHBy . fh . hfmapUnion loop)
+            (flip sendUnionBy . ff)
+{-# INLINE transEffHF #-}
+
+a = runPure $ interpret undefined $ interpret @(Union '[State Int, State Char]) undefined $ bundle $ pure @(Eff '[] '[State Int, State Char, State ()]) ()

heftia/src/Control/Monad/Hefty/Types.hs

@@ -0,0 +1,105 @@
+-- SPDX-License-Identifier: MPL-2.0
+
+module Control.Monad.Hefty.Types where
+
+import Control.Effect (type (~>))
+import Data.Effect.OpenUnion.Internal.FO (Union, inj, type (<!))
+import Data.Effect.OpenUnion.Internal.HO (UnionH, injH, type (<!!))
+import Data.FTCQueue (FTCQueue, tsingleton, (|>))
+import Data.Kind (Type)
+
+{- | The 'Eff' monad represents computations with effects.
+It supports higher-order effects @eh@ and first-order effects @ef@.
+-}
+data Eff eh ef a
+    = -- | A pure value.
+      Val a
+    | -- | An effectful operation, which can be either a higher-order effect or a first-order effect.
+      forall x. Op
+        (Either (UnionH eh (Eff eh ef) x) (Union ef x))
+        (FTCQueue (Eff eh ef) x a)
+        -- ^ the continuation of the operation.
+
+infixr 4 :!!
+
+{- | Type-level infix operator for 'Eff'.
+Allows writing @eh :!! ef@ instead of @Eff eh ef@.
+-}
+type (:!!) = Eff
+
+instance Functor (Eff eh ef) where
+    fmap f = \case
+        Val x -> Val (f x)
+        Op u q -> Op u (q |> (Val . f))
+    {-# INLINE fmap #-}
+
+instance Applicative (Eff eh ef) where
+    pure = Val
+    {-# INLINE pure #-}
+
+    Val f <*> Val x = Val $ f x
+    Val f <*> Op u q = Op u (q |> (Val . f))
+    Op u q <*> m = Op u (q |> (<$> m))
+    {-# INLINE (<*>) #-}
+
+instance Monad (Eff eh ef) where
+    m >>= k = case m of
+        Val x -> k x
+        Op e q -> Op e (q |> k)
+    {-# INLINE (>>=) #-}
+
+infixr 3 $
+infixr 4 $$
+
+-- | Type-level infix applcation for functors.
+type (f :: Type -> Type) $ a = f a
+
+-- | Type-level infix applcation for higher-order functors.
+type (h :: (Type -> Type) -> Type -> Type) $$ f = h f
+
+{- | Type synonym for an interpreter function.
+@Interpreter e m ans@ transforms an effect @e@ into a computation in @m@ where the result has the type (answer type) @ans@.
+-}
+type Interpreter e m (ans :: Type) = forall x. e x -> (x -> m ans) -> m ans
+
+{- | Type alias for an elaborator function.
+An 'Elaborator' is an interpreter for higher-order effects.
+-}
+type Elaborator e m ans = Interpreter (e m) m ans
+
+{- | Type alias for an elaborator transformation.
+An 'Elab' transforms an higher-order effect @e f@ into @f@.
+-}
+type Elab e f = e f ~> f
+
+sendUnion :: Union ef a -> Eff eh ef a
+sendUnion = sendUnionBy pure
+{-# INLINE sendUnion #-}
+
+sendUnionBy :: (a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
+sendUnionBy k u = Op (Right u) (tsingleton k)
+{-# INLINE sendUnionBy #-}
+
+sendUnionH :: UnionH eh (Eff eh ef) a -> Eff eh ef a
+sendUnionH = sendUnionHBy pure
+{-# INLINE sendUnionH #-}
+
+sendUnionHBy :: (a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans
+sendUnionHBy k u = Op (Left u) (tsingleton k)
+{-# INLINE sendUnionHBy #-}
+
+send :: (e <! ef) => e ~> Eff eh ef
+send = sendUnion . inj
+{-# INLINE send #-}
+
+sendH :: (e <!! eh) => e (Eff eh ef) ~> Eff eh ef
+sendH = sendUnionH . injH
+{-# INLINE sendH #-}
+
+send0 :: e ~> Eff eh (e ': ef)
+send0 = send
+{-# INLINE send0 #-}
+
+send0H :: e (Eff (e ': eh) ef) ~> Eff (e ': eh) ef
+send0H = sendH
+{-# INLINE send0H #-}

heftia/src/Data/Effect/OpenUnion.hs

@@ -8,47 +8,84 @@ Stability   :  experimental
 -}
 module Data.Effect.OpenUnion (
     module Data.Effect.OpenUnion.Internal,
-    module Data.Effect.OpenUnion.Internal.FO,
     module Data.Effect.OpenUnion.Internal.HO,
+    module Data.Effect.OpenUnion.Internal.FO,
     module Data.Effect.OpenUnion.Internal.Strengthen,
     module Data.Effect.OpenUnion.Internal.Weaken,
 ) where
 
-import Data.Effect.OpenUnion.Internal (IsSuffixOf, KnownLen, type (++))
+import Data.Effect.OpenUnion.Internal (
+    Drop,
+    KnownLength,
+    Length,
+    Reverse,
+    Take,
+    type (++),
+ )
 import Data.Effect.OpenUnion.Internal.FO (
     EffectF,
-    MemberF,
-    UnionF,
-    decomp0F,
-    decompF,
-    exhaustF,
-    extractF,
-    prefixF,
-    strengthenNF,
-    strengthenNUnderMF,
-    suffixF,
-    weakenF,
-    weakenNF,
-    weakenNUnderMF,
-    weakensF,
+    Member,
+    Union,
+    bundleAllUnion,
+    bundleUnion,
+    bundleUnionUnder,
+    decomp,
+    decomp0,
+    extract,
+    flipAllUnion,
+    flipUnion,
+    flipUnionUnder,
+    inj,
+    nil,
+    prefixUnion,
+    prefixUnionUnder,
+    prj,
+    strengthenN,
+    strengthenNUnderM,
+    suffixUnion,
+    suffixUnionOverN,
+    unbundleAllUnion,
+    unbundleUnion,
+    unbundleUnionUnder,
+    weaken,
+    weakenN,
+    weakenNUnderM,
+    weakens,
+    (!+),
+    type (<!),
  )
 import Data.Effect.OpenUnion.Internal.HO (
     EffectH,
     MemberH,
     UnionH,
+    bundleAllUnionH,
+    bundleUnionH,
+    bundleUnionUnderH,
     decomp0H,
     decompH,
-    exhaustH,
     extractH,
+    flipAllUnionH,
+    flipUnionH,
+    flipUnionUnderH,
     hfmapUnion,
-    prefixH,
+    injH,
+    nilH,
+    prefixUnionH,
+    prefixUnionUnderH,
+    prjH,
     strengthenNH,
     strengthenNUnderMH,
-    suffixH,
+    suffixUnionH,
+    suffixUnionOverNH,
+    unbundleAllUnionH,
+    unbundleUnionH,
+    unbundleUnionUnderH,
     weakenH,
     weakenNH,
     weakenNUnderMH,
     weakensH,
+    (!!+),
+    type (<!!),
  )
 import Data.Effect.OpenUnion.Internal.Strengthen (Strengthen, StrengthenUnder)
-import Data.Effect.OpenUnion.Internal.Weaken (Weaken, WeakenUnder)
+import Data.Effect.OpenUnion.Internal.Weaken (IsSuffixOf, Weaken, WeakenUnder)

heftia/src/Data/Effect/OpenUnion/Internal.hs

@@ -1,5 +1,7 @@
--- SPDX-License-Identifier: MPL-2.0 AND BSD-3-Clause
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- SPDX-License-Identifier: MPL-2.0 AND BSD-3-Clause
 
 -- This Source Code Form is subject to the terms of the Mozilla Public
 -- License, v. 2.0. If a copy of the MPL was not distributed with this
@@ -43,11 +45,15 @@ Copyright   :  (c) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis K
 License     :  MPL-2.0 (see the LICENSE file) AND BSD-3-Clause
 Maintainer  :  ymdfield@outlook.jp
 Stability   :  experimental
-Description :  Open unions (type-indexed co-products) for extensible first-order effects.
+Description :  Open unions (type-indexed co-products) for extensible effects.
 -}
 module Data.Effect.OpenUnion.Internal where
 
+import Data.Kind (Constraint)
+import Data.Proxy (Proxy (Proxy))
+import Data.Type.Equality (type (==))
 import GHC.TypeError (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), TypeError)
+import GHC.TypeNats (KnownNat, natVal, type (+), type (-))
 
 {- |
 Represents position of element @e :: k@ in a type list @es :: [k]@.
@@ -109,26 +115,97 @@ lexi-lambda/freer-simple#3, which describes the motivation in more detail.
 -}
 instance {-# INCOHERENT #-} IfNotFound e r w
 
-class IsSuffixOf es es' where
-    prefixLen :: Word
-
-instance IsSuffixOf es es where
-    prefixLen = 0
-
-instance {-# OVERLAPPABLE #-} (IsSuffixOf es es') => IsSuffixOf es (e ': es') where
-    prefixLen = 1 + prefixLen @es @es'
-
-class KnownLen (es :: [k]) where
-    -- | Get the length of the list.
-    reifyLen :: Word
-
-instance KnownLen '[] where
-    reifyLen = 0
-
-instance (KnownLen es) => KnownLen (e ': es) where
-    reifyLen = 1 + reifyLen @_ @es
-
 infixr 5 ++
 type family xs ++ ys where
     '[] ++ ys = ys
     (x ': xs) ++ ys = x ': (xs ++ ys)
+
+wordVal :: forall n. (KnownNat n) => Word
+wordVal = fromIntegral $ natVal @n Proxy
+{-# INLINE wordVal #-}
+
+type family Length es where
+    Length '[] = 0
+    Length (e ': es) = 1 + Length es
+
+class (KnownNat (Length es)) => KnownLength es
+instance (KnownNat (Length es)) => KnownLength es
+
+reifyLength :: forall es. (KnownLength es) => Word
+reifyLength = wordVal @(Length es)
+{-# INLINE reifyLength #-}
+
+type family PrefixLength es es' where
+    PrefixLength es es = 0
+    PrefixLength es (e ': es') = 1 + PrefixLength es es'
+
+type IsSuffixOf_ es es' = KnownNat (PrefixLength es es')
+class (IsSuffixOf_ es es') => IsSuffixOf es es'
+instance (IsSuffixOf_ es es') => IsSuffixOf es es'
+
+prefixLen :: forall es es'. (es `IsSuffixOf` es') => Word
+prefixLen = wordVal @(PrefixLength es es')
+{-# INLINE prefixLen #-}
+
+type WeakenN len es es' = (es ~ Drop len es', KnownNat len)
+
+type WeakenNUnderM len offset es es' =
+    (WeakenN len (Drop offset es) (Drop offset es'), KnownNat offset)
+
+type Strengthen es es' =
+    (StrengthenMap (PrefixLength es' es) es es', KnownNat (PrefixLength es es'))
+
+type StrengthenN len es es' = (StrengthenMap len es es', KnownNat len)
+
+type StrengthenUnderM offset es es' =
+    (StrengthenNUnderM (PrefixLength es' es) offset es es')
+
+type StrengthenNUnderM len offset es es' =
+    (StrengthenMap len (Drop offset es) (Drop offset es'), KnownNat len)
+
+type StrengthenMap len es es' = (StrengthenMap_ (len == 0) len es es')
+
+class
+    (isLenZero ~ (len == 0)) =>
+    StrengthenMap_ isLenZero len (es :: [k]) (es' :: [k])
+    where
+    strengthenMap :: Word -> Word
+
+instance StrengthenMap_ 'True 0 es es where
+    strengthenMap = id
+    {-# INLINE strengthenMap #-}
+
+instance
+    (StrengthenMap (len - 1) es es', FindElem e es, (len == 0) ~ 'False)
+    => StrengthenMap_ 'False len (e ': es) es'
+    where
+    strengthenMap = \case
+        0 -> unP $ elemNo @_ @e @es
+        n -> strengthenMap @_ @_ @(len - 1) @es @es' $ n - 1
+    {-# INLINE strengthenMap #-}
+
+type BundleUnderM u offset es es' bundle =
+    ( es' ~ Take offset es ++ (u bundle ': Drop (Length bundle) (Drop offset es))
+    , es ~ Take offset es' ++ bundle ++ Drop 1 (Drop offset es')
+    , bundle ~ Take (PrefixLength (Drop offset es) (Drop 1 (Drop offset es'))) (Drop offset es)
+    )
+
+type Split es init tail =
+    ( es ~ init ++ tail
+    , init ~ Take (PrefixLength es tail) es
+    , tail ~ Drop (Length init) tail
+    )
+
+type family Take n es where
+    Take 0 es = '[]
+    Take n (e ': es) = e ': Take n es
+
+type family Drop n es where
+    Drop 0 es = es
+    Drop n (e ': es) = Drop n es
+
+type Reverse es = Reverse_ '[] es
+
+type family Reverse_ acc es where
+    Reverse_ acc '[] = acc
+    Reverse_ acc (e ': es) = Reverse_ (e ': acc) es

heftia/src/Data/Effect/OpenUnion/Internal/Bundle.hs

@@ -0,0 +1,41 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- SPDX-License-Identifier: MPL-2.0
+
+{- |
+Copyright   :  (c) 2024 Sayo Koyoneda
+License     :  MPL-2.0 (see the LICENSE file)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+-}
+module Data.Effect.OpenUnion.Internal.Bundle where
+
+import Data.Effect.OpenUnion.Internal (KnownLength)
+import GHC.TypeLits (KnownNat, Natural, type (-))
+
+class
+    (KnownLength bundle) =>
+    Bundle (es :: [k]) (bundle :: [k]) (rest :: [k])
+        | bundle es -> rest
+        , bundle rest -> es
+
+instance Bundle es '[] es
+
+instance
+    (Bundle es bundle rest, KnownLength (e ': bundle))
+    => Bundle (e ': es) (e ': bundle) rest
+
+class
+    (KnownNat offset, KnownLength bundle) =>
+    BundleUnder (u :: [k] -> k) (offset :: Natural) (es :: [k]) (es' :: [k]) bundle
+        | offset es es' -> bundle
+        , u offset es bundle -> es'
+
+instance (Bundle es bundle rest) => BundleUnder u 0 es (u bundle ': rest) bundle
+
+instance
+    {-# OVERLAPPABLE #-}
+    (BundleUnder u (offset - 1) es es' bundle, KnownNat offset, KnownLength bundle)
+    => BundleUnder u offset (e ': es) (e ': es') bundle

heftia/src/Data/Effect/OpenUnion/Internal/FO.hs

@@ -49,12 +49,8 @@ Description :  Open unions (type-indexed co-products) for extensible first-order
 
 Implementation of an open union for first-order effects.
 
-Note that since this module is internal, the API may not be preserved when the minor version
-changes. In other words, this module does not follow the Haskell Package Versioning Policy
-specification.
-
-Importing this module allows unsafe access to the data structure of the open union, so it should not
-usually be imported.
+Importing this module allows unsafe access to the data structure of the open
+union, so it should not usually be imported directly.
 
 Based on [the open union in freer-simple](https://hackage.haskell.org/package/freer-simple-1.2.1.2/docs/Data-OpenUnion-Internal.html).
 -}
@@ -62,45 +58,47 @@ module Data.Effect.OpenUnion.Internal.FO where
 
 import Data.Coerce (coerce)
 import Data.Effect.OpenUnion.Internal (
+    Drop,
     FindElem (elemNo),
     IfNotFound,
     IsSuffixOf,
-    KnownLen,
+    KnownLength,
+    Length,
     P (unP),
+    Reverse,
+    Take,
     prefixLen,
-    reifyLen,
+    reifyLength,
+    wordVal,
     type (++),
  )
+import Data.Effect.OpenUnion.Internal.Bundle (Bundle, BundleUnder)
 import Data.Effect.OpenUnion.Internal.Strengthen (
     Strengthen,
     StrengthenUnder,
-    strengthenMap,
     strengthenUnderMap,
-    strengthenUnderOffset,
  )
 import Data.Effect.OpenUnion.Internal.Weaken (
     Weaken,
     WeakenUnder,
-    weakenLen,
-    weakenUnderLen,
-    weakenUnderOffset,
  )
 import Data.Kind (Type)
+import GHC.TypeNats (KnownNat, type (-))
 import Unsafe.Coerce (unsafeCoerce)
 
 -- | Kind of first-order effects.
 type EffectF = Type -> Type
 
 -- | Open union for first-order effects.
-data UnionF (es :: [EffectF]) (a :: Type) where
-    UnionF
+data Union (es :: [EffectF]) (a :: Type) where
+    Union
         :: {-# UNPACK #-} !Word
         -- ^ A natural number tag to identify the element of the union.
         -> e a
         -- ^ The data of the higher-order effect that is an element of the union.
-        -> UnionF es a
+        -> Union es a
 
-{- | Takes a request of type @e :: 'EffectF'@, and injects it into the 'UnionF'.
+{- | Takes a request of type @e :: 'EffectF'@, and injects it into the 'Union'.
 
 Summand is assigning a specified 'Word' value, which is a position in the
 type-list @(e ': es) :: 'EffectF'@.
@@ -109,26 +107,26 @@ __This function is unsafe.__
 
 /O(1)/
 -}
-unsafeInjF :: Word -> e a -> UnionF es a
-unsafeInjF = UnionF
-{-# INLINE unsafeInjF #-}
+unsafeInj :: Word -> e a -> Union es a
+unsafeInj = Union
+{-# INLINE unsafeInj #-}
 
-{- | Project a value of type @'UnionF' (e ': es) :: 'EffectF'@ into a possible
+{- | Project a value of type @'Union' (e ': es) :: 'EffectF'@ into a possible
 summand of the type @e :: 'EffectF'@. 'Nothing' means that @e :: 'EffectF'@ is not
-the value stored in the @'UnionF' (e ': es) :: 'EffectF'@.
+the value stored in the @'Union' (e ': es) :: 'EffectF'@.
 
 It is assumed that summand is stored in the 'Union' when the 'Word' value is
-the same value as is stored in the 'UnionF'.
+the same value as is stored in the 'Union'.
 
 __This function is unsafe.__
 
 /O(1)/
 -}
-unsafePrjF :: Word -> UnionF es a -> Maybe (e a)
-unsafePrjF n (UnionF n' e)
+unsafePrj :: Word -> Union es a -> Maybe (e a)
+unsafePrj n (Union n' e)
     | n == n' = Just (unsafeCoerce e)
     | otherwise = Nothing
-{-# INLINE unsafePrjF #-}
+{-# INLINE unsafePrj #-}
 
 {- | A constraint that requires that a particular effect, @e@, is a member of
 the type-level list @es@. This is used to parameterize an
@@ -139,10 +137,10 @@ For example, a computation that only needs access to a cell of mutable state
 containing an 'Integer' would likely use the following type:
 
 @
-'MemberF' ('Data.Effect.State.State' 'Integer') ef => 'Control.Monad.Hefty.Eff' eh ef ()
+'Member' ('Data.Effect.State.State' 'Integer') ef => 'Control.Monad.Hefty.Eff' eh ef ()
 @
 -}
-class (FindElem e es) => MemberF (e :: EffectF) es where
+class (FindElem e es) => Member (e :: EffectF) es where
     -- This type class is used for two following purposes:
     --
 
@@ -151,7 +149,7 @@ class (FindElem e es) => MemberF (e :: EffectF) es where
     --   type-list @es :: ['EffectF']@.
     --
 
-    -- * Provides a way how to inject\/project @e :: 'EffectF'@ into\/from a 'UnionF',
+    -- * Provides a way how to inject\/project @e :: 'EffectF'@ into\/from a 'Union',
 
     --   respectively.
     --
@@ -162,36 +160,39 @@ class (FindElem e es) => MemberF (e :: EffectF) es where
     -- @
 
     -- | Takes a request of type @e :: 'EffectF'@, and injects it into the
-    -- 'UnionF'.
+    -- 'Union'.
     --
     -- /O(1)/
-    injF :: e a -> UnionF es a
+    inj :: e a -> Union es a
 
-    -- | Project a value of type @'UnionF' (e ': es) :: 'EffectF'@ into a possible
+    -- | Project a value of type @'Union' (e ': es) :: 'EffectF'@ into a possible
     -- summand of the type @e :: 'EffectF'@. 'Nothing' means that @e :: 'EffectF'@ is
-    -- not the value stored in the @'UnionF' (e ': es) :: 'EffectF'@.
+    -- not the value stored in the @'Union' (e ': es) :: 'EffectF'@.
     --
     -- /O(1)/
-    prjF :: UnionF es a -> Maybe (e a)
+    prj :: Union es a -> Maybe (e a)
 
-instance (FindElem e es, IfNotFound e es es) => MemberF e es where
-    injF = unsafeInjF $ unP (elemNo :: P e es)
-    {-# INLINE injF #-}
+instance (FindElem e es, IfNotFound e es es) => Member e es where
+    inj = unsafeInj $ unP (elemNo :: P e es)
+    {-# INLINE inj #-}
 
-    prjF = unsafePrjF $ unP (elemNo :: P e es)
-    {-# INLINE prjF #-}
+    prj = unsafePrj $ unP (elemNo :: P e es)
+    {-# INLINE prj #-}
 
-{- | Orthogonal decomposition of a @'UnionF' (e ': es) :: 'EffectF'@. 'Right' value
-is returned if the @'UnionF' (e ': es) :: 'EffectF'@ contains @e :: 'EffectF'@, and
+infix 3 <!
+type (<!) = Member
+
+{- | Orthogonal decomposition of a @'Union' (e ': es) :: 'EffectF'@. 'Right' value
+is returned if the @'Union' (e ': es) :: 'EffectF'@ contains @e :: 'EffectF'@, and
 'Left' when it doesn't. Notice that 'Left' value contains
-@U'nionF' es :: 'EffectF'@, i.e. it can not contain @e :: 'EffectF'@.
+@'Union' es :: 'EffectF'@, i.e. it can not contain @e :: 'EffectF'@.
 
 /O(1)/
 -}
-decompF :: UnionF (e ': es) a -> Either (UnionF r a) (t a)
-decompF (UnionF 0 a) = Right $ unsafeCoerce a
-decompF (UnionF n a) = Left $ UnionF (n - 1) a
-{-# INLINE [2] decompF #-}
+decomp :: Union (e ': es) a -> Either (Union r a) (e a)
+decomp (Union 0 a) = Right $ unsafeCoerce a
+decomp (Union n a) = Left $ Union (n - 1) a
+{-# INLINE [2] decomp #-}
 
 {- | Specialized version of 'decomp' for efficiency.
 
@@ -199,73 +200,191 @@ decompF (UnionF n a) = Left $ UnionF (n - 1) a
 
 TODO: Check that it actually adds on efficiency.
 -}
-decomp0F :: UnionF '[t] a -> Either (UnionF '[] a) (t a)
-decomp0F (UnionF _ a) = Right $ unsafeCoerce a
-{-# INLINE decomp0F #-}
+decomp0 :: Union '[e] a -> Either (Union '[] a) (e a)
+decomp0 (Union _ a) = Right $ unsafeCoerce a
+{-# INLINE decomp0 #-}
 
-{-# RULES "decomp/singleton" decompF = decomp0F #-}
+{-# RULES "decomp/singleton" decomp = decomp0 #-}
+
+infixr 5 !+
+(!+) :: (e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
+(f !+ g) u = case decomp u of
+    Left x -> g x
+    Right x -> f x
+{-# INLINE (!+) #-}
 
 {- | Specialised version of 'prj'\/'decomp' that works on an
-@'UnionF' '[e] :: 'EffectF'@ which contains only one specific summand. Hence the
+@'Union' '[e] :: 'EffectF'@ which contains only one specific summand. Hence the
 absence of 'Maybe', and 'Either'.
 
 /O(1)/
 -}
-extractF :: UnionF '[e] a -> e a
-extractF (UnionF _ a) = unsafeCoerce a
-{-# INLINE extractF #-}
+extract :: Union '[e] a -> e a
+extract (Union _ a) = unsafeCoerce a
+{-# INLINE extract #-}
 
-{- | Inject whole @'UnionF' es@ into a weaker @'UnionF' (any ': es)@ that has one
+{- | Inject whole @'Union' es@ into a weaker @'Union' (any ': es)@ that has one
 more summand.
 
 /O(1)/
 -}
-weakenF :: UnionF es a -> UnionF (any ': es) a
-weakenF (UnionF n a) = UnionF (n + 1) a
-{-# INLINE weakenF #-}
+weaken :: Union es a -> Union (any ': es) a
+weaken (Union n a) = Union (n + 1) a
+{-# INLINE weaken #-}
 
-weakensF :: forall es es' a. (es `IsSuffixOf` es') => UnionF es a -> UnionF es' a
-weakensF (UnionF n a) = UnionF (n + prefixLen @es @es') a
-{-# INLINE weakensF #-}
+weakens :: forall es es' a. (es `IsSuffixOf` es') => Union es a -> Union es' a
+weakens (Union n a) = Union (n + prefixLen @es @es') a
+{-# INLINE weakens #-}
 
-weakenNF :: forall len es es' a. (Weaken len es es') => UnionF es a -> UnionF es' a
-weakenNF (UnionF n a) = UnionF (n + weakenLen @len @es @es') a
-{-# INLINE weakenNF #-}
+weakenN :: forall len es es' a. (Weaken len es es') => Union es a -> Union es' a
+weakenN (Union n a) = Union (n + wordVal @len) a
+{-# INLINE weakenN #-}
 
-weakenNUnderMF
+weakenNUnderM
     :: forall len offset es es' a
      . (WeakenUnder len offset es es')
-    => UnionF es a
-    -> UnionF es' a
-weakenNUnderMF u@(UnionF n a)
-    | n < weakenUnderOffset @len @offset @es @es' = coerce u
-    | otherwise = UnionF (n + weakenUnderLen @len @offset @es @es') a
-{-# INLINE weakenNUnderMF #-}
+    => Union es a
+    -> Union es' a
+weakenNUnderM u@(Union n a)
+    | n < wordVal @offset = coerce u
+    | otherwise = Union (n + wordVal @len) a
+{-# INLINE weakenNUnderM #-}
 
-strengthenNF :: forall len es es' a. (Strengthen len es es') => UnionF es a -> UnionF es' a
-strengthenNF (UnionF n a) = UnionF (strengthenMap @len @es @es' n) a
-{-# INLINE strengthenNF #-}
+strengthenN :: forall len es es' a. (Strengthen len es es') => Union es a -> Union es' a
+strengthenN (Union n a) = Union (strengthenUnderMap @len @0 @es @es' n) a
+{-# INLINE strengthenN #-}
 
-strengthenNUnderMF
+strengthenNUnderM
     :: forall len offset es es' a
      . (StrengthenUnder len offset es es')
-    => UnionF es a
-    -> UnionF es' a
-strengthenNUnderMF u@(UnionF n a)
+    => Union es a
+    -> Union es' a
+strengthenNUnderM u@(Union n a)
     | n < off = coerce u
-    | otherwise = UnionF (off + strengthenUnderMap @len @offset @es @es' (n - off)) a
+    | otherwise = Union (off + strengthenUnderMap @len @offset @es @es' (n - off)) a
   where
-    off = strengthenUnderOffset @len @offset @es @es'
-{-# INLINE strengthenNUnderMF #-}
+    off = wordVal @offset
+{-# INLINE strengthenNUnderM #-}
 
-prefixF :: forall any es a. (KnownLen any) => UnionF es a -> UnionF (any ++ es) a
-prefixF (UnionF n a) = UnionF (n + reifyLen @_ @any) a
-{-# INLINE prefixF #-}
+bundleUnion
+    :: forall bundle es rest a
+     . (Bundle es bundle rest)
+    => Union es a
+    -> Union (Union bundle ': rest) a
+bundleUnion (Union n a)
+    | n < len = Union 0 $ Union n a
+    | otherwise = Union (n - len + 1) a
+  where
+    len = reifyLength @bundle
+{-# INLINE bundleUnion #-}
 
-suffixF :: forall any es a. UnionF es a -> UnionF (es ++ any) a
-suffixF = coerce
-{-# INLINE suffixF #-}
+unbundleUnion
+    :: forall bundle es rest a
+     . (Bundle es bundle rest)
+    => Union (Union bundle ': rest) a
+    -> Union es a
+unbundleUnion (Union n a)
+    | n == 0 = unsafeCoerce a
+    | otherwise = Union (n - 1 + reifyLength @bundle) a
+{-# INLINE unbundleUnion #-}
 
-exhaustF :: UnionF '[] a -> r
-exhaustF _ = error "Effect system internal error: exhaustF - An empty effect union, which should not be possible to create, has been created."
-{-# INLINE exhaustF #-}
+bundleUnionUnder
+    :: forall offset bundle es es' a
+     . (BundleUnder Union offset es es' bundle)
+    => Union es a
+    -> Union es' a
+bundleUnionUnder u@(Union n a)
+    | n < off = coerce u
+    | n' < len = Union 0 $ Union n' a
+    | otherwise = Union (n - len + 1) a
+  where
+    off = wordVal @offset
+    len = reifyLength @bundle
+    n' = n - off
+{-# INLINE bundleUnionUnder #-}
+
+unbundleUnionUnder
+    :: forall offset bundle es es' a
+     . (BundleUnder Union offset es es' bundle)
+    => Union es' a
+    -> Union es a
+unbundleUnionUnder u@(Union n a)
+    | n < off = coerce u
+    | n == off =
+        case unsafeCoerce a of
+            Union n' a' -> Union (off + n') a'
+    | otherwise = Union (n - 1 + len) a
+  where
+    off = wordVal @offset
+    len = reifyLength @bundle
+{-# INLINE unbundleUnionUnder #-}
+
+bundleAllUnion :: Union es a -> Union '[Union es] a
+bundleAllUnion = Union 0
+{-# INLINE bundleAllUnion #-}
+
+unbundleAllUnion :: Union '[Union es] a -> Union es a
+unbundleAllUnion = extract
+{-# INLINE unbundleAllUnion #-}
+
+prefixUnion :: forall any es a. (KnownLength any) => Union es a -> Union (any ++ es) a
+prefixUnion (Union n a) = Union (n + reifyLength @any) a
+{-# INLINE prefixUnion #-}
+
+prefixUnionUnder
+    :: forall any offset es a
+     . (KnownLength any, KnownNat offset)
+    => Union es a
+    -> Union (Take offset es ++ any ++ Drop offset es) a
+prefixUnionUnder u@(Union n a)
+    | n < wordVal @offset = coerce u
+    | otherwise = Union (n + reifyLength @any) a
+{-# INLINE prefixUnionUnder #-}
+
+suffixUnion :: forall any es a. Union es a -> Union (es ++ any) a
+suffixUnion = coerce
+{-# INLINE suffixUnion #-}
+
+suffixUnionOverN
+    :: forall any offset es a
+     . (KnownLength any, KnownNat offset, KnownLength es)
+    => Union es a
+    -> Union (Take (Length es - offset) es ++ any ++ Drop (Length es - offset) es) a
+suffixUnionOverN u@(Union n a)
+    | n < reifyLength @es - wordVal @offset = coerce u
+    | otherwise = Union (n + reifyLength @any) a
+{-# INLINE suffixUnionOverN #-}
+
+flipAllUnion :: forall es a. (KnownLength es) => Union es a -> Union (Reverse es) a
+flipAllUnion (Union n a) = Union (reifyLength @es - n) a
+{-# INLINE flipAllUnion #-}
+
+flipUnion
+    :: forall len es a
+     . (KnownNat len)
+    => Union es a
+    -> Union (Reverse (Take len es) ++ Drop len es) a
+flipUnion u@(Union n a)
+    | n < len = Union (len - n) a
+    | otherwise = coerce u
+  where
+    len = wordVal @len
+{-# INLINE flipUnion #-}
+
+flipUnionUnder
+    :: forall len offset es a
+     . (KnownNat len, KnownNat offset)
+    => Union es a
+    -> Union (Take offset es ++ Reverse (Take len (Drop offset es)) ++ Drop len (Drop offset es)) a
+flipUnionUnder u@(Union n a)
+    | n >= off && n' < len = Union (off + len - n') a
+    | otherwise = coerce u
+  where
+    off = wordVal @offset
+    len = wordVal @len
+    n' = n - off
+{-# INLINE flipUnionUnder #-}
+
+nil :: Union '[] a -> r
+nil _ = error "Effect system internal error: nil - An empty effect union, which should not be possible to create, has been created."
+{-# INLINE nil #-}

heftia/src/Data/Effect/OpenUnion/Internal/HO.hs

@@ -52,9 +52,8 @@ Description :  Open unions (type-indexed co-products) for extensible higher-orde
 
 Implementation of an open union for higher-order effects.
 
-Note that since this module is internal, the API may not be preserved when the minor version changes. In other words, this module does not follow the Haskell Package Versioning Policy specification.
-
-Importing this module allows unsafe access to the data structure of the open union, so it should not usually be imported.
+Importing this module allows unsafe access to the data structure of the open
+union, so it should not usually be imported directly.
 
 Based on [the open union in freer-simple](https://hackage.haskell.org/package/freer-simple-1.2.1.2/docs/Data-OpenUnion-Internal.html).
 -}
@@ -64,30 +63,32 @@ import Control.Effect (type (~>))
 import Data.Coerce (coerce)
 import Data.Effect.HFunctor (HFunctor, hfmap)
 import Data.Effect.OpenUnion.Internal (
+    Drop,
     FindElem (elemNo),
     IfNotFound,
     IsSuffixOf,
-    KnownLen,
+    KnownLength,
+    Length,
     P (unP),
+    Reverse,
+    Take,
     prefixLen,
-    reifyLen,
+    reifyLength,
+    wordVal,
     type (++),
  )
+import Data.Effect.OpenUnion.Internal.Bundle (Bundle, BundleUnder)
 import Data.Effect.OpenUnion.Internal.Strengthen (
     Strengthen,
     StrengthenUnder,
-    strengthenMap,
     strengthenUnderMap,
-    strengthenUnderOffset,
  )
 import Data.Effect.OpenUnion.Internal.Weaken (
     Weaken,
     WeakenUnder,
-    weakenLen,
-    weakenUnderLen,
-    weakenUnderOffset,
  )
 import Data.Kind (Type)
+import GHC.TypeNats (KnownNat, type (-))
 import Unsafe.Coerce (unsafeCoerce)
 
 -- | Kind of higher-order effects.
@@ -98,7 +99,7 @@ data UnionH (es :: [EffectH]) (f :: Type -> Type) (a :: Type) where
     UnionH
         :: {-# UNPACK #-} !Word
         -- ^ A natural number tag to identify the element of the union.
-        -> e n a
+        -> e g a
         -- ^ The data of the higher-order effect that is an element of the union.
         -> (g ~> f)
         -- ^ Continuation of interpretation. Due to this component, this open union becomes a free 'HFunctor', which contributes to performance improvement.
@@ -123,7 +124,7 @@ unsafePrjH n (UnionH n' e koi)
 {-# INLINE unsafePrjH #-}
 
 class (FindElem e es) => MemberH (e :: EffectH) es where
-    injH :: (HFunctor e) => e f a -> UnionH es f a
+    injH :: e f a -> UnionH es f a
     prjH :: (HFunctor e) => UnionH es f a -> Maybe (e f a)
 
 instance (FindElem e es, IfNotFound e es es) => MemberH e es where
@@ -133,6 +134,9 @@ instance (FindElem e es, IfNotFound e es es) => MemberH e es where
     prjH = unsafePrjH $ unP (elemNo :: P e es)
     {-# INLINE prjH #-}
 
+infix 3 <!!
+type (<!!) = MemberH
+
 decompH :: (HFunctor e) => UnionH (e ': es) f a -> Either (UnionH es f a) (e f a)
 decompH (UnionH 0 a koi) = Right $ hfmap koi $ unsafeCoerce a
 decompH (UnionH n a koi) = Left $ UnionH (n - 1) a koi
@@ -143,6 +147,13 @@ decomp0H (UnionH _ a koi) = Right $ hfmap koi $ unsafeCoerce a
 {-# INLINE decomp0H #-}
 {-# RULES "decomp/singleton" decompH = decomp0H #-}
 
+infixr 5 !!+
+(!!+) :: (HFunctor e) => (e f a -> r) -> (UnionH es f a -> r) -> UnionH (e : es) f a -> r
+(f !!+ g) u = case decompH u of
+    Left x -> g x
+    Right x -> f x
+{-# INLINE (!!+) #-}
+
 extractH :: (HFunctor e) => UnionH '[e] f a -> e f a
 extractH (UnionH _ a koi) = hfmap koi $ unsafeCoerce a
 {-# INLINE extractH #-}
@@ -156,7 +167,7 @@ weakensH (UnionH n a koi) = UnionH (n + prefixLen @es @es') a koi
 {-# INLINE weakensH #-}
 
 weakenNH :: forall len es es' f a. (Weaken len es es') => UnionH es f a -> UnionH es' f a
-weakenNH (UnionH n a koi) = UnionH (n + weakenLen @len @es @es') a koi
+weakenNH (UnionH n a koi) = UnionH (n + wordVal @len) a koi
 {-# INLINE weakenNH #-}
 
 weakenNUnderMH
@@ -165,12 +176,12 @@ weakenNUnderMH
     => UnionH es f a
     -> UnionH es' f a
 weakenNUnderMH u@(UnionH n a koi)
-    | n < weakenUnderOffset @len @offset @es @es' = coerce u
-    | otherwise = UnionH (n + weakenUnderLen @len @offset @es @es') a koi
+    | n < wordVal @offset = coerce u
+    | otherwise = UnionH (n + wordVal @len) a koi
 {-# INLINE weakenNUnderMH #-}
 
 strengthenNH :: forall len es es' f a. (Strengthen len es es') => UnionH es f a -> UnionH es' f a
-strengthenNH (UnionH n a koi) = UnionH (strengthenMap @len @es @es' n) a koi
+strengthenNH (UnionH n a koi) = UnionH (strengthenUnderMap @len @0 @es @es' n) a koi
 {-# INLINE strengthenNH #-}
 
 strengthenNUnderMH
@@ -182,17 +193,129 @@ strengthenNUnderMH u@(UnionH n a koi)
     | n < off = coerce u
     | otherwise = UnionH (off + strengthenUnderMap @len @offset @es @es' (n - off)) a koi
   where
-    off = strengthenUnderOffset @len @offset @es @es'
+    off = wordVal @offset
 {-# INLINE strengthenNUnderMH #-}
 
-prefixH :: forall any es f a. (KnownLen any) => UnionH es f a -> UnionH (any ++ es) f a
-prefixH (UnionH n a koi) = UnionH (n + reifyLen @_ @any) a koi
-{-# INLINE prefixH #-}
+bundleUnionH
+    :: forall bundle es rest f a
+     . (Bundle es bundle rest)
+    => UnionH es f a
+    -> UnionH (UnionH bundle ': rest) f a
+bundleUnionH (UnionH n a koi)
+    | n < len = UnionH 0 (UnionH n a koi) id
+    | otherwise = UnionH (n - len + 1) a koi
+  where
+    len = reifyLength @bundle
+{-# INLINE bundleUnionH #-}
 
-suffixH :: forall any es f a. UnionH es f a -> UnionH (es ++ any) f a
-suffixH = coerce
-{-# INLINE suffixH #-}
+unbundleUnionH
+    :: forall bundle es rest f a
+     . (Bundle es bundle rest)
+    => UnionH (UnionH bundle ': rest) f a
+    -> UnionH es f a
+unbundleUnionH (UnionH n a koi)
+    | n == 0 = case unsafeCoerce a of
+        UnionH n' a' koi' -> UnionH n' a' (koi . koi')
+    | otherwise = UnionH (n - 1 + reifyLength @bundle) a koi
+{-# INLINE unbundleUnionH #-}
 
-exhaustH :: UnionH '[] f a -> r
-exhaustH _ = error "Effect system internal error: exhaustH - An empty effect union, which should not be possible to create, has been created."
-{-# INLINE exhaustH #-}
+bundleUnionUnderH
+    :: forall offset bundle es es' f a
+     . (BundleUnder UnionH offset es es' bundle)
+    => UnionH es f a
+    -> UnionH es' f a
+bundleUnionUnderH u@(UnionH n a koi)
+    | n < off = coerce u
+    | n' < len = UnionH 0 (UnionH n' a koi) id
+    | otherwise = UnionH (n - len + 1) a koi
+  where
+    off = wordVal @offset
+    len = reifyLength @bundle
+    n' = n - off
+{-# INLINE bundleUnionUnderH #-}
+
+unbundleUnionUnderH
+    :: forall offset bundle es es' f a
+     . (BundleUnder UnionH offset es es' bundle)
+    => UnionH es' f a
+    -> UnionH es f a
+unbundleUnionUnderH u@(UnionH n a koi)
+    | n < off = coerce u
+    | n == off =
+        case unsafeCoerce a of
+            UnionH n' a' koi' -> UnionH (off + n') a' (koi . koi')
+    | otherwise = UnionH (n - 1 + len) a koi
+  where
+    off = wordVal @offset
+    len = reifyLength @bundle
+{-# INLINE unbundleUnionUnderH #-}
+
+bundleAllUnionH :: UnionH es f a -> UnionH '[UnionH es] f a
+bundleAllUnionH u = UnionH 0 u id
+{-# INLINE bundleAllUnionH #-}
+
+unbundleAllUnionH :: UnionH '[UnionH es] f a -> UnionH es f a
+unbundleAllUnionH = extractH
+{-# INLINE unbundleAllUnionH #-}
+
+prefixUnionH :: forall any es f a. (KnownLength any) => UnionH es f a -> UnionH (any ++ es) f a
+prefixUnionH (UnionH n a koi) = UnionH (n + reifyLength @any) a koi
+{-# INLINE prefixUnionH #-}
+
+prefixUnionUnderH
+    :: forall any offset es f a
+     . (KnownLength any, KnownNat offset)
+    => UnionH es f a
+    -> UnionH (Take offset es ++ any ++ Drop offset es) f a
+prefixUnionUnderH u@(UnionH n a koi)
+    | n < wordVal @offset = coerce u
+    | otherwise = UnionH (n + reifyLength @any) a koi
+{-# INLINE prefixUnionUnderH #-}
+
+suffixUnionH :: forall any es f a. UnionH es f a -> UnionH (es ++ any) f a
+suffixUnionH = coerce
+{-# INLINE suffixUnionH #-}
+
+suffixUnionOverNH
+    :: forall any offset es f a
+     . (KnownLength any, KnownNat offset, KnownLength es)
+    => UnionH es f a
+    -> UnionH (Take (Length es - offset) es ++ any ++ Drop (Length es - offset) es) f a
+suffixUnionOverNH u@(UnionH n a koi)
+    | n < reifyLength @es - wordVal @offset = coerce u
+    | otherwise = UnionH (n + reifyLength @any) a koi
+{-# INLINE suffixUnionOverNH #-}
+
+flipAllUnionH :: forall es f a. (KnownLength es) => UnionH es f a -> UnionH (Reverse es) f a
+flipAllUnionH (UnionH n a koi) = UnionH (reifyLength @es - n) a koi
+{-# INLINE flipAllUnionH #-}
+
+flipUnionH
+    :: forall len es f a
+     . (KnownNat len)
+    => UnionH es f a
+    -> UnionH (Reverse (Take len es) ++ Drop len es) f a
+flipUnionH u@(UnionH n a koi)
+    | n < len = UnionH (len - n) a koi
+    | otherwise = coerce u
+  where
+    len = wordVal @len
+{-# INLINE flipUnionH #-}
+
+flipUnionUnderH
+    :: forall len offset es f a
+     . (KnownNat len, KnownNat offset)
+    => UnionH es f a
+    -> UnionH (Take offset es ++ Reverse (Take len (Drop offset es)) ++ Drop len (Drop offset es)) f a
+flipUnionUnderH u@(UnionH n a koi)
+    | n >= off && n' < len = UnionH (off + len - n') a koi
+    | otherwise = coerce u
+  where
+    off = wordVal @offset
+    len = wordVal @len
+    n' = n - off
+{-# INLINE flipUnionUnderH #-}
+
+nilH :: UnionH '[] f a -> r
+nilH _ = error "Effect system internal error: nilH - An empty effect union, which should not be possible to create, has been created."
+{-# INLINE nilH #-}

heftia/src/Data/Effect/OpenUnion/Internal/Strengthen.hs

@@ -13,30 +13,46 @@ Portability :  portable
 module Data.Effect.OpenUnion.Internal.Strengthen where
 
 import Data.Effect.OpenUnion.Internal (FindElem (elemNo), P (unP))
-import Data.Proxy (Proxy (Proxy))
-import GHC.TypeLits (KnownNat, natVal, type (-))
+import Data.Type.Equality (type (==))
+import GHC.TypeLits (KnownNat, Natural, type (-))
 
-class Strengthen len es es' where
-    strengthenMap :: Word -> Word
+type Strengthen len = StrengthenUnder_ 'True 0 (len == 0) len
+type StrengthenUnder len offset = StrengthenUnder_ (offset == 0) offset (len == 0) len
 
-instance Strengthen 0 es es where
-    strengthenMap = id
-    {-# INLINE strengthenMap #-}
+strengthenUnderMap :: forall len offset es es'. (StrengthenUnder len offset es es') => Word -> Word
+strengthenUnderMap = strengthenUnderMap_ @_ @(offset == 0) @offset @(len == 0) @len @es @es'
 
-instance {-# OVERLAPPABLE #-} (Strengthen (len - 1) es es', FindElem e es) => Strengthen len (e ': es) es' where
-    strengthenMap = \case
+class
+    ( isOffsetZero ~ (offset == 0)
+    , isLenZero ~ (len == 0)
+    , KnownNat offset
+    , KnownNat len
+    ) =>
+    StrengthenUnder_ (isOffsetZero :: Bool) (offset :: Natural) (isLenZero :: Bool) (len :: Natural) (es :: [k]) (es' :: [k])
+        | offset len es -> es'
+    where
+    strengthenUnderMap_ :: Word -> Word
+
+instance
+    ( StrengthenUnder len (offset - 1) es es'
+    , (offset == 0) ~ 'False
+    , isLenZero ~ (len == 0)
+    , KnownNat offset
+    , KnownNat len
+    )
+    => StrengthenUnder_ 'False offset isLenZero len (e ': es) (e ': es')
+    where
+    strengthenUnderMap_ = strengthenUnderMap @len @(offset - 1) @es @es'
+
+instance
+    (Strengthen (len - 1) es es', FindElem e es, (len == 0) ~ 'False, KnownNat len)
+    => StrengthenUnder_ 'True 0 'False len (e ': es) es'
+    where
+    strengthenUnderMap_ = \case
         0 -> unP $ elemNo @_ @e @es
-        n -> strengthenMap @(len - 1) @es @es' $ n - 1
-    {-# INLINE strengthenMap #-}
+        n -> strengthenUnderMap @(len - 1) @0 @es @es' $ n - 1
+    {-# INLINE strengthenUnderMap_ #-}
 
-class StrengthenUnder len offset es es' where
-    strengthenUnderMap :: Word -> Word
-    strengthenUnderOffset :: Word
-
-instance (Strengthen len es es') => StrengthenUnder len 0 es es' where
-    strengthenUnderMap = strengthenMap @len @es @es'
-    strengthenUnderOffset = 0
-
-instance {-# OVERLAPPABLE #-} (StrengthenUnder len (offset - 1) es es', KnownNat offset) => StrengthenUnder len offset es (e ': es') where
-    strengthenUnderMap = strengthenUnderMap @len @(offset - 1) @es @es'
-    strengthenUnderOffset = fromIntegral $ natVal @offset Proxy
+instance StrengthenUnder_ 'True 0 'True 0 es es where
+    strengthenUnderMap_ = id
+    {-# INLINE strengthenUnderMap_ #-}

heftia/src/Data/Effect/OpenUnion/Internal/Weaken.hs

@@ -12,26 +12,28 @@ Portability :  portable
 -}
 module Data.Effect.OpenUnion.Internal.Weaken where
 
-import Data.Proxy (Proxy (Proxy))
-import GHC.TypeLits (KnownNat, natVal, type (-))
+import Data.Type.Equality (type (==))
+import GHC.TypeNats (KnownNat, Natural, type (-))
 
-class Weaken len es es' where
-    weakenLen :: Word
+type Weaken len = WeakenUnder_ 'True 0 (len == 0) len
+type WeakenUnder len offset = WeakenUnder_ (offset == 0) offset (len == 0) len
 
-instance Weaken 0 es es where
-    weakenLen = 0
+class
+    (isOffsetZero ~ (offset == 0), isLenZero ~ (len == 0), KnownNat offset, KnownNat len) =>
+    WeakenUnder_ (isOffsetZero :: Bool) (offset :: Natural) (isLenZero :: Bool) (len :: Natural) es es'
+        | es' -> es
 
-instance {-# OVERLAPPABLE #-} (Weaken (len - 1) es es', KnownNat len) => Weaken len es (e ': es') where
-    weakenLen = fromIntegral $ natVal @len Proxy
+instance
+    ( WeakenUnder n (offset - 1) es es'
+    , (offset == 0) ~ 'False
+    , isLenZero ~ (len == 0)
+    , KnownNat offset
+    , KnownNat len
+    )
+    => WeakenUnder_ 'False offset isLenZero len (e ': es) (e ': es')
 
-class WeakenUnder len offset es es' where
-    weakenUnderLen :: Word
-    weakenUnderOffset :: Word
+instance
+    (Weaken (len - 1) es es', (len == 0) ~ 'False, KnownNat len)
+    => WeakenUnder_ 'True 0 'False len es (e ': es')
 
-instance (Weaken len es es') => WeakenUnder len 0 es es' where
-    weakenUnderLen = weakenLen @len @es @es'
-    weakenUnderOffset = 0
-
-instance {-# OVERLAPPABLE #-} (WeakenUnder len (offset - 1) es es', KnownNat offset) => WeakenUnder len offset es (e ': es') where
-    weakenUnderLen = weakenUnderLen @len @(offset - 1) @es @es'
-    weakenUnderOffset = fromIntegral $ natVal @offset Proxy
+instance WeakenUnder_ 'True 0 'True 0 es es