[fix] SIGSEGV bug in 'transform' and unsound type signature in 'decomp'.

[add] SemanticsZoo and Continuation2 examples.

heftia-effects/Example/Continuation2/Main.hs

@@ -5,20 +5,19 @@
 module Main where
 
 import Control.Arrow ((>>>))
-import Control.Effect.ExtensibleChurch (runEff, type (!!))
-import Control.Effect.Hefty (send1, unkeyEff, type ($))
 import Control.Effect.Interpreter.Heftia.Reader (runAsk, runLocal)
 import Control.Effect.Interpreter.Heftia.ShiftReset (evalShift, runShift_)
 import Control.Effect.Interpreter.Heftia.State (evalState)
 import Control.Effect.Key (key)
 import Control.Monad.Extra (whenM)
+import Control.Monad.Hefty.Interpret (runEff)
+import Control.Monad.Hefty.Transform (raise, unkey)
+import Control.Monad.Hefty.Types (Eff, send, send0)
 import Control.Monad.IO.Class (liftIO)
-import Data.Effect.HFunctor ((:+:))
 import Data.Effect.Key (type (#>))
 import Data.Effect.Reader (Ask, Local, ask, local)
 import Data.Effect.ShiftReset (Shift, Shift_, getCC, getCC_)
 import Data.Effect.State (State, get'', modify)
-import Data.Free.Sum (type (+))
 import Data.Function ((&))
 import Data.Functor ((<&>))
 
@@ -68,20 +67,20 @@ handleReaderThenShift =
         & runAsk 1
         & runEff
         & evalShift
-        & (unkeyEff >>> evalState 0)
+        & (unkey >>> evalState 0)
         & runEff
   where
-    prog :: Local Int !! Ask Int + Shift () !! "counter" #> State Int + IO $ ()
+    prog :: Eff '[Local Int] '[Ask Int, Eff '[Shift ()] '["counter" #> State Int, IO]] ()
     prog = do
-        k <- send1 getCC
+        k <- raise $ send0 getCC
         env <- ask @Int
-        send1 $ liftIO $ putStrLn $ "[local scope outer] env = " ++ show env
+        raise $ send0 $ liftIO $ putStrLn $ "[local scope outer] env = " ++ show env
         local @Int (* 2) do
-            whenM (send1 (get'' @"counter") <&> (< 5)) do
-                send1 $ modify (+ 1) & key @"counter"
+            whenM (raise $ send0 (get'' @"counter") <&> (< 5)) do
+                raise $ send0 $ modify (+ 1) & key @"counter"
                 env' <- ask @Int
-                send1 $ liftIO $ putStrLn $ "[local scope inner] env = " ++ show env'
-                send1 k
+                raise $ send0 $ liftIO $ putStrLn $ "[local scope inner] env = " ++ show env'
+                send k
 
 handleShiftThenReader :: IO ()
 handleShiftThenReader = do
@@ -89,10 +88,10 @@ handleShiftThenReader = do
         & runShift_
         & runLocal
         & runAsk 1
-        & (unkeyEff >>> evalState 0)
+        & (unkey >>> evalState 0)
         & runEff
   where
-    prog :: Shift_ :+: Local Int !! Ask Int + "counter" #> State Int + IO $ ()
+    prog :: Eff '[Shift_, Local Int] '[Ask Int, "counter" #> State Int, IO] ()
     prog = do
         k <- getCC_
         env <- ask @Int

heftia-effects/Example/SemanticsZoo/Main.hs

@@ -14,19 +14,25 @@ module Main where
 
 import Control.Applicative ((<|>))
 import Control.Effect (type (~>))
-import Control.Effect.ExtensibleChurch ((:!!))
-import Control.Effect.Hefty (interpretRec, runPure, type ($))
 import Control.Effect.Interpreter.Heftia.Except (runCatch, runThrow)
 import Control.Effect.Interpreter.Heftia.NonDet (runChooseH, runNonDet)
 import Control.Effect.Interpreter.Heftia.State (evalState)
-import Control.Effect.Interpreter.Heftia.Writer (elaborateWriterPre, runTell)
+import Control.Effect.Interpreter.Heftia.Writer (runTell, runWriterHPre)
+import Control.Monad.Hefty (
+    HFunctors,
+    interpretRec,
+    runPure,
+    type ($),
+    type (:!!),
+    type (<<|),
+    type (<|),
+ )
 import Data.Effect.Except (Catch, Throw, catch, throw)
 import Data.Effect.NonDet (ChooseH, Empty)
 import Data.Effect.State (State, get, put)
 import Data.Effect.TH (makeEffectF)
 import Data.Effect.Writer (Tell, WriterH, listen, tell)
 import Data.Functor (($>))
-import Data.Hefty.Extensible (ForallHFunctor, type (<<|), type (<|))
 import Data.Monoid (Sum (Sum))
 
 statePlusExcept :: IO ()
@@ -44,46 +50,50 @@ statePlusExcept = do
 nonDetPlusExcept :: IO ()
 nonDetPlusExcept = do
     let action1
-            , action2 ::
-                (Empty <| ef, ChooseH <<| eh, Throw () <| ef, Catch () <<| eh) => eh :!! ef $ Bool
+            , action2
+                :: (Empty <| ef, ChooseH <<| eh, Throw () <| ef, Catch () <<| eh) => eh :!! ef $ Bool
         action1 = (pure True <|> throw ()) `catch` \() -> pure False
         action2 = (throw () <|> pure True) `catch` \() -> pure False
 
-        testAllPattern ::
-            ( forall eh ef.
-              (Empty <| ef, ChooseH <<| eh, Throw () <| ef, Catch () <<| eh) =>
-              (eh :!! ef) Bool
-            ) ->
-            String ->
-            IO ()
+        testAllPattern
+            :: ( forall eh ef
+                  . (Empty <| ef, ChooseH <<| eh, Throw () <| ef, Catch () <<| eh)
+                 => (eh :!! ef) Bool
+               )
+            -> String
+            -> IO ()
         testAllPattern action name = do
             putStr $ "( runNonDet . runThrow . runCatch . runChooseH $ " <> name <> " ) = "
             print . runPure $
-                runNonDet @[] . runThrow @() . runCatch @() . runChooseH $ action
+                runNonDet @[] . runThrow @() . runCatch @() . runChooseH $
+                    action
 
             putStr $ "( runThrow . runNonDet . runCatch . runChooseH $ " <> name <> " ) = "
             print . runPure $
-                runThrow @() . runNonDet @[] . runCatch @() . runChooseH $ action
+                runThrow @() . runNonDet @[] . runCatch @() . runChooseH $
+                    action
 
     testAllPattern action1 "action1"
     testAllPattern action2 "action2"
 
 nonDetPlusWriter :: IO ()
 nonDetPlusWriter = do
-    let action ::
-            (Empty <| ef, ChooseH <<| eh, Tell (Sum Int) <| ef, WriterH (Sum Int) <<| eh) =>
-            eh :!! ef $ (Sum Int, Bool)
+    let action
+            :: (Empty <| ef, ChooseH <<| eh, Tell (Sum Int) <| ef, WriterH (Sum Int) <<| eh)
+            => eh :!! ef $ (Sum Int, Bool)
         action = listen $ add 1 *> (add 2 $> True <|> add 3 $> False)
           where
             add = tell . Sum @Int
 
     putStr "( runNonDet . runTell . elaborateWriter . runChooseH $ action ) = "
     print . map (\(Sum m, (Sum n, b)) -> (m, (n, b))) . runPure $
-        runNonDet @[] . runTell @(Sum Int) . elaborateWriterPre @(Sum Int) . runChooseH $ action
+        runNonDet @[] . runTell @(Sum Int) . runWriterHPre @(Sum Int) . runChooseH $
+            action
 
     putStr "( runTell . runNonDet . elaborateWriter . runChooseH $ action ) = "
     print . (\(Sum m, xs) -> (m, map (\(Sum n, b) -> (n, b)) xs)) . runPure $
-        runTell @(Sum Int) . runNonDet @[] . elaborateWriterPre @(Sum Int) . runChooseH $ action
+        runTell @(Sum Int) . runNonDet @[] . runWriterHPre @(Sum Int) . runChooseH $
+            action
 
 data SomeEff a where
     SomeAction :: SomeEff String
@@ -94,7 +104,7 @@ theIssue12 = do
     let action :: (Catch String <<| eh, Throw String <| ef, SomeEff <| ef) => eh :!! ef $ String
         action = someAction `catch` \(_ :: String) -> pure "caught"
 
-        runSomeEff :: (ForallHFunctor eh, Throw String <| ef) => eh :!! LSomeEff ': ef ~> eh :!! ef
+        runSomeEff :: (HFunctors eh, Throw String <| ef) => eh :!! SomeEff ': ef ~> eh :!! ef
         runSomeEff = interpretRec (\SomeAction -> throw "not caught")
 
     putStr "interpret SomeEff then runCatch : ( runThrow . runCatch . runSomeEff $ action ) = "

heftia-effects/src/Control/Effect/Interpreter/Heftia/Resource.hs

@@ -16,11 +16,10 @@ An elaborator for the t'Control.Effect.Class.Resource.Resource' effect class.
 module Control.Effect.Interpreter.Heftia.Resource where
 
 import Control.Effect (type (~>))
-import Control.Monad.Hefty (HFunctors)
 import Control.Monad.Hefty.Interpret (interpretRecH)
 import Control.Monad.Hefty.Types (Eff, Elab)
 import Data.Effect.OpenUnion.Internal.FO (type (<|))
-import Data.Effect.OpenUnion.Internal.HO (type (<<|))
+import Data.Effect.OpenUnion.Internal.HO (HFunctors, type (<<|))
 import Data.Effect.Resource (Resource (Bracket, BracketOnExcept))
 import Data.Effect.Unlift (UnliftIO)
 import UnliftIO (MonadUnliftIO, bracket, bracketOnError)

heftia-effects/src/Control/Effect/Interpreter/Heftia/ShiftReset.hs

@@ -5,8 +5,7 @@
 module Control.Effect.Interpreter.Heftia.ShiftReset where
 
 import Control.Effect (type (~>))
-import Control.Monad.Hefty (runEff)
-import Control.Monad.Hefty.Interpret (interpretHBy_, interpretRecH, iterAllEffHFBy)
+import Control.Monad.Hefty.Interpret (interpretHBy_, interpretRecH, iterAllEffHFBy, runEff)
 import Control.Monad.Hefty.Transform (raiseH)
 import Control.Monad.Hefty.Types (Eff, sendUnionBy, sendUnionHBy)
 import Data.Effect.Key (KeyH (KeyH))

heftia-effects/src/Control/Effect/Interpreter/Heftia/State.hs

@@ -14,7 +14,6 @@ Interpreter for the t'Data.Effect.State.State' effect.
 module Control.Effect.Interpreter.Heftia.State where
 
 import Control.Effect (type (~>))
-import Control.Monad.Hefty (HFunctors)
 import Control.Monad.Hefty.Interpret (interpretRec)
 import Control.Monad.Hefty.Interpret.State (
     StateInterpreter,
@@ -24,6 +23,7 @@ import Control.Monad.Hefty.Interpret.State (
  )
 import Control.Monad.Hefty.Types (Eff)
 import Data.Effect.OpenUnion.Internal.FO (type (<|))
+import Data.Effect.OpenUnion.Internal.HO (HFunctors)
 import Data.Effect.State (State (Get, Put), get, put)
 import Data.Function ((&))
 import Data.Functor ((<&>))

heftia/src/Control/Monad/Hefty.hs

@@ -83,6 +83,10 @@ import Control.Monad.Hefty.Transform (
     raises,
     raisesH,
     raisesUnder,
+    rekey,
+    rekeyH,
+    retag,
+    retagH,
     rewrite,
     rewriteH,
     subsume,
@@ -110,6 +114,10 @@ import Control.Monad.Hefty.Transform (
     unbundleN,
     unbundleUnder,
     unbundleUnderH,
+    unkey,
+    unkeyH,
+    untag,
+    untagH,
  )
 import Control.Monad.Hefty.Types (
     Eff (Op, Val),

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

@@ -8,6 +8,7 @@ import Control.Effect (type (~>))
 import Control.Monad.Hefty.Interpret (iterAllEffHFBy)
 import Control.Monad.Hefty.Types (Eff, sendUnionBy, sendUnionHBy)
 import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Key
 import Data.Effect.OpenUnion.Internal (
     BundleUnder,
     Drop,
@@ -74,6 +75,7 @@ import Data.Effect.OpenUnion.Internal.HO (
     weakensH,
     type (<<|),
  )
+import Data.Effect.Tag
 import GHC.TypeNats (KnownNat)
 
 transform
@@ -81,7 +83,7 @@ transform
      . (HFunctors eh)
     => (e ~> e')
     -> Eff eh (e ': ef) ~> Eff eh (e' ': ef)
-transform f = transEff (either id (inj . f) . decomp)
+transform f = transEff (either weaken (inj . f) . decomp)
 {-# INLINE transform #-}
 
 transformH
@@ -354,6 +356,62 @@ unbundleAllH :: (HFunctors eh) => Eff '[UnionH eh] ef ~> Eff eh ef
 unbundleAllH = transEffH unbundleAllUnionH
 {-# INLINE unbundleAllH #-}
 
+untag
+    :: forall tag e ef eh
+     . (HFunctors eh)
+    => Eff eh (e # tag ': ef) ~> Eff eh (e ': ef)
+untag = transform unTag
+{-# INLINE untag #-}
+
+retag
+    :: forall tag' tag e ef eh
+     . (HFunctors eh)
+    => Eff eh (e # tag ': ef) ~> Eff eh (e # tag' ': ef)
+retag = transform $ Tag . unTag
+{-# INLINE retag #-}
+
+untagH
+    :: forall tag e eh ef
+     . (HFunctor e, HFunctors (e ## tag ': eh))
+    => Eff (e ## tag ': eh) ef ~> Eff (e ': eh) ef
+untagH = transformH unTagH
+{-# INLINE untagH #-}
+
+retagH
+    :: forall tag' tag e eh ef
+     . (HFunctor e, HFunctors (e ## tag ': eh))
+    => Eff (e ## tag ': eh) ef ~> Eff (e ## tag' ': eh) ef
+retagH = transformH $ TagH . unTagH
+{-# INLINE retagH #-}
+
+unkey
+    :: forall key e ef eh
+     . (HFunctors eh)
+    => Eff eh (key #> e ': ef) ~> Eff eh (e ': ef)
+unkey = transform unKey
+{-# INLINE unkey #-}
+
+rekey
+    :: forall key' key e ef eh
+     . (HFunctors eh)
+    => Eff eh (key #> e ': ef) ~> Eff eh (key' #> e ': ef)
+rekey = transform $ Key . unKey
+{-# INLINE rekey #-}
+
+unkeyH
+    :: forall key e eh ef
+     . (HFunctor e, HFunctors (key ##> e ': eh))
+    => Eff (key ##> e ': eh) ef ~> Eff (e ': eh) ef
+unkeyH = transformH unKeyH
+{-# INLINE unkeyH #-}
+
+rekeyH
+    :: forall key' key e eh ef
+     . (HFunctor e, HFunctors (key ##> e ': eh))
+    => Eff (key ##> e ': eh) ef ~> Eff (key' ##> e ': eh) ef
+rekeyH = transformH $ KeyH . unKeyH
+{-# INLINE rekeyH #-}
+
 transEff
     :: forall ef ef' eh
      . (HFunctors eh)

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

@@ -19,6 +19,7 @@ import Data.Effect.Fail (Fail)
 import Data.Effect.Fail qualified as E
 import Data.Effect.Fix (Fix)
 import Data.Effect.Fix qualified as E
+import Data.Effect.Key (Key (Key), KeyH (KeyH), type (##>), type (#>))
 import Data.Effect.NonDet (ChooseH, Empty, chooseH)
 import Data.Effect.NonDet qualified as E
 import Data.Effect.OpenUnion.Internal.FO (Lookup, MemberBy, Union, inj, type (<|))
@@ -82,12 +83,12 @@ instance (e <<| eh) => SendSig e (Eff eh ef) where
     sendSig = sendH
     {-# INLINE sendSig #-}
 
-instance (MemberBy key ef, e ~ Lookup key ef) => SendInsBy key e (Eff eh ef) where
-    sendInsBy = send
+instance (MemberBy key ef, key #> e ~ Lookup key ef) => SendInsBy key e (Eff eh ef) where
+    sendInsBy = send . Key @key
     {-# INLINE sendInsBy #-}
 
-instance (MemberHBy key eh, e ~ LookupH key eh) => SendSigBy key e (Eff eh ef) where
-    sendSigBy = sendH
+instance (MemberHBy key eh, key ##> e ~ LookupH key eh) => SendSigBy key e (Eff eh ef) where
+    sendSigBy = sendH . KeyH @key
     {-# INLINE sendSigBy #-}
 
 instance

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

@@ -204,7 +204,7 @@ is returned if the @'Union' (e ': es) :: 'EffectF'@ contains @e :: 'EffectF'@, a
 
 /O(1)/
 -}
-decomp :: Union (e ': es) a -> Either (Union r a) (e a)
+decomp :: Union (e ': es) a -> Either (Union es a) (e a)
 decomp (Union 0 a) = Right $ unsafeCoerce a
 decomp (Union n a) = Left $ Union (n - 1) a
 {-# INLINE [2] decomp #-}