Reverse Indexed Union

examples/src/Capitalize.hs

@@ -6,13 +6,13 @@ module Capitalize
 
 import Data.Char (toUpper)
 
-import Control.Monad.Freer (Eff, Member, interpret, send)
+import Control.Monad.Freer (Eff, Member, HasLen, interpret, send)
 
 data Capitalize v where
   Capitalize :: String -> Capitalize String
 
 capitalize :: Member Capitalize r => String -> Eff r String
 capitalize = send . Capitalize
 
-runCapitalize :: Eff (Capitalize ': r) w -> Eff r w
+runCapitalize :: HasLen r => Eff (Capitalize ': r) w -> Eff r w
 runCapitalize = interpret $ \(Capitalize s) -> pure (map toUpper s)

examples/src/Console.hs

@@ -12,7 +12,7 @@ module Console
 import Data.Function ((&))
 import System.Exit (exitSuccess)
 
-import Control.Monad.Freer (Eff, LastMember, Member, interpretM, reinterpret3, run, runM, send)
+import Control.Monad.Freer (Eff, LastMember, Member, HasLen, interpretM, reinterpret3, run, runM, send)
 import Control.Monad.Freer.Error (Error, runError, throwError)
 import Control.Monad.Freer.State (State, get, put, runState)
 import Control.Monad.Freer.Writer (Writer, runWriter, tell)
@@ -61,7 +61,7 @@ runConsolePure inputs req = snd . fst $
 -------------------------------------------------------------------------------
                      -- Effectful Interpreter for Deeper Stack --
 -------------------------------------------------------------------------------
-runConsoleM :: forall effs a. LastMember IO effs
+runConsoleM :: forall effs a. (LastMember IO effs, HasLen effs)
             => Eff (Console ': effs) a -> Eff effs a
 runConsoleM = interpretM $ \case
   PutStrLn msg -> putStrLn msg
@@ -73,7 +73,8 @@ runConsoleM = interpretM $ \case
 -------------------------------------------------------------------------------
 runConsolePureM
   :: forall effs w
-   . [String]
+   . HasLen effs
+  => [String]
   -> Eff (Console ': effs) w
   -> Eff effs (Maybe w, [String], [String])
 runConsolePureM inputs req = do

package.yaml

@@ -57,6 +57,7 @@ library:
   dependencies:
   - natural-transformation >= 0.2
   - transformers-base
+  - ghc-prim
 
 executables:
   freer-examples:

src/Control/Monad/Freer.hs

@@ -215,6 +215,7 @@ module Control.Monad.Freer
 
     -- ** Building Effect Handlers
     -- *** Basic effect handlers
+  , HasLen
   , interpret
   , interpose
   , subsume
@@ -242,6 +243,7 @@ import Control.Monad.Freer.Internal
   ( Eff
   , LastMember
   , Member
+  , HasLen
   , Members
   , Weakens
   , (:++:)
@@ -259,7 +261,7 @@ import Control.Monad.Freer.Internal
 -- transformation from some effect @eff@ to some effectful computation with
 -- effects @effs@, produces a natural transformation from @'Eff' (eff ': effs)@
 -- to @'Eff' effs@.
-interpret :: forall eff effs. (eff ~> Eff effs) -> Eff (eff ': effs) ~> Eff effs
+interpret :: forall eff effs. HasLen effs => (eff ~> Eff effs) -> Eff (eff ': effs) ~> Eff effs
 interpret f = interpretWith (\e -> (f e >>=))
 {-# INLINE interpret #-}
 
@@ -271,29 +273,31 @@ interpose f = interposeWith (\e -> (f e >>=))
 
 -- | Interprets an effect in terms of another identical effect. This can be used
 -- to eliminate duplicate effects.
-subsume :: forall eff effs. Member eff effs => Eff (eff ': effs) ~> Eff effs
+subsume :: forall eff effs. (Member eff effs, HasLen effs) => Eff (eff ': effs) ~> Eff effs
 subsume = interpret send
 {-# INLINE subsume #-}
 
 -- | Like 'interpret', but instead of removing the interpreted effect @f@,
 -- reencodes it in some new effect @g@.
-reinterpret :: forall f g effs. (f ~> Eff (g ': effs)) -> Eff (f ': effs) ~> Eff (g ': effs)
+reinterpret :: forall f g effs. HasLen effs => (f ~> Eff (g ': effs)) -> Eff (f ': effs) ~> Eff (g ': effs)
 reinterpret f = replaceRelay pure (\e -> (f e >>=))
 {-# INLINE reinterpret #-}
 
 -- | Like 'reinterpret', but encodes the @f@ effect in /two/ new effects instead
 -- of just one.
 reinterpret2
   :: forall f g h effs
-   . (f ~> Eff (g ': h ': effs)) -> Eff (f ': effs) ~> Eff (g ': h ': effs)
+   . HasLen effs
+   => (f ~> Eff (g ': h ': effs)) -> Eff (f ': effs) ~> Eff (g ': h ': effs)
 reinterpret2 = reinterpretN @[g, h]
 {-# INLINE reinterpret2 #-}
 
 -- | Like 'reinterpret', but encodes the @f@ effect in /three/ new effects
 -- instead of just one.
 reinterpret3
   :: forall f g h i effs
-   . (f ~> Eff (g ': h ': i ': effs))
+   . HasLen effs
+  => (f ~> Eff (g ': h ': i ': effs))
   -> Eff (f ': effs) ~> Eff (g ': h ': i ': effs)
 reinterpret3 = reinterpretN @[g, h, i]
 {-# INLINE reinterpret3 #-}
@@ -304,7 +308,7 @@ reinterpret3 = reinterpretN @[g, h, i]
 -- have to explicitly pick @gs@ using @TypeApplications@. Prefer 'interpret',
 -- 'reinterpret', 'reinterpret2', or 'reinterpret3' where possible.
 reinterpretN
-  :: forall gs f effs. Weakens gs
+  :: forall gs f effs. (Weakens gs, HasLen effs)
   => (f ~> Eff (gs :++: effs)) -> Eff (f ': effs) ~> Eff (gs :++: effs)
 reinterpretN f = replaceRelayN @gs pure (\e -> (f e >>=))
 {-# INLINE reinterpretN #-}
@@ -322,7 +326,7 @@ reinterpretN f = replaceRelayN @gs pure (\e -> (f e >>=))
 -- @
 -- 'translate' f = 'reinterpret' ('send' . f)
 -- @
-translate :: forall f g effs. (f ~> g) -> Eff (f ': effs) ~> Eff (g ': effs)
+translate :: forall f g effs. HasLen effs => (f ~> g) -> Eff (f ': effs) ~> Eff (g ': effs)
 translate f = reinterpret (send . f)
 {-# INLINE translate #-}
 
@@ -337,7 +341,7 @@ translate f = reinterpret (send . f)
 -- @
 interpretM
   :: forall eff m effs
-   . (Monad m, LastMember m effs)
+   . (Monad m, LastMember m effs, HasLen effs)
   => (eff ~> m) -> Eff (eff ': effs) ~> Eff effs
 interpretM f = interpret (sendM . f)
 {-# INLINE interpretM #-}
@@ -355,7 +359,8 @@ interpretM f = interpret (sendM . f)
 -- @
 interpretWith
   :: forall eff effs b
-   . (forall v. eff v -> (v -> Eff effs b) -> Eff effs b)
+   . HasLen effs
+  => (forall v. eff v -> (v -> Eff effs b) -> Eff effs b)
   -> Eff (eff ': effs) b
   -> Eff effs b
 interpretWith = handleRelay pure

src/Control/Monad/Freer/Coroutine.hs

@@ -22,7 +22,7 @@ module Control.Monad.Freer.Coroutine
   , replyC
   ) where
 
-import Control.Monad.Freer.Internal (Eff, Member, handleRelay, interpose, send)
+import Control.Monad.Freer.Internal (Eff, Member, HasLen, handleRelay, interpose, send)
 
 -- | A type representing a yielding of control.
 --
@@ -59,7 +59,7 @@ replyC
 replyC (Yield a k) arr = pure $ Continue a (arr . k)
 
 -- | Launch a coroutine and report its status.
-runC :: Eff (Yield a b ': effs) r -> Eff effs (Status effs a b r)
+runC :: HasLen effs => Eff (Yield a b ': effs) r -> Eff effs (Status effs a b r)
 runC = handleRelay (pure . Done) replyC
 
 -- | Launch a coroutine and report its status, without handling (removing)

src/Control/Monad/Freer/Error.hs

@@ -19,7 +19,7 @@ module Control.Monad.Freer.Error
   , handleError
   ) where
 
-import Control.Monad.Freer (Eff, Member, interposeWith, interpretWith, send)
+import Control.Monad.Freer (Eff, Member, HasLen, interposeWith, interpretWith, send)
 import Control.Monad.Freer.Internal (handleRelay)
 
 -- | Exceptions of the type @e :: *@ with no resumption.
@@ -33,7 +33,7 @@ throwError e = send (Error e)
 -- | Handler for exception effects. If there are no exceptions thrown, returns
 -- 'Right'. If exceptions are thrown and not handled, returns 'Left', while
 -- interrupting the execution of any other effect handlers.
-runError :: forall e effs a. Eff (Error e ': effs) a -> Eff effs (Either e a)
+runError :: forall e effs a. HasLen effs => Eff (Error e ': effs) a -> Eff effs (Either e a)
 runError = handleRelay (pure . Right) (\(Error e) _ -> pure (Left e))
 
 -- | A catcher for Exceptions. Handlers are allowed to rethrow exceptions.
@@ -48,7 +48,8 @@ catchError m handle = interposeWith (\(Error e) _ -> handle e) m
 -- | A catcher for Exceptions. Handlers are /not/ allowed to rethrow exceptions.
 handleError
   :: forall e effs a
-   . Eff (Error e ': effs) a
+   . HasLen effs
+  => Eff (Error e ': effs) a
   -> (e -> Eff effs a)
   -> Eff effs a
 handleError m handle = interpretWith (\(Error e) _ -> handle e) m

src/Control/Monad/Freer/Fresh.hs

@@ -19,7 +19,7 @@ module Control.Monad.Freer.Fresh
   , evalFresh
   ) where
 
-import Control.Monad.Freer.Internal (Eff, Member, handleRelayS, send)
+import Control.Monad.Freer.Internal (Eff, Member, HasLen, handleRelayS, send)
 
 -- | Fresh effect model.
 data Fresh r where
@@ -31,11 +31,11 @@ fresh = send Fresh
 
 -- | Handler for 'Fresh' effects, with an 'Int' for a starting value. The
 -- return value includes the next fresh value.
-runFresh :: Int -> Eff (Fresh ': effs) a -> Eff effs (a, Int)
+runFresh :: HasLen effs => Int -> Eff (Fresh ': effs) a -> Eff effs (a, Int)
 runFresh s =
   handleRelayS s (\s' a -> pure (a, s')) (\s' Fresh k -> (k $! s' + 1) s')
 
 -- | Handler for 'Fresh' effects, with an 'Int' for a starting value. Discards
 -- the next fresh value.
-evalFresh :: Int -> Eff (Fresh ': effs) a -> Eff effs a
+evalFresh :: HasLen effs => Int -> Eff (Fresh ': effs) a -> Eff effs a
 evalFresh s = fmap fst . runFresh s

src/Control/Monad/Freer/Internal.hs

@@ -213,7 +213,8 @@ runM (E u q) = case extract u of
 -- | Like 'replaceRelay', but with support for an explicit state to help
 -- implement the interpreter.
 replaceRelayS
-  :: s
+  :: HasLen effs
+  => s
   -> (s -> a -> Eff (v ': effs) w)
   -> (forall x. s -> t x -> (s -> Arr (v ': effs) x w) -> Eff (v ': effs) w)
   -> Eff (t ': effs) a
@@ -233,7 +234,8 @@ replaceRelayS s' pure' bind = loop s'
 -- defined in terms of other ones without leaking intermediary implementation
 -- details through the type signature.
 replaceRelay
-  :: (a -> Eff (v ': effs) w)
+  :: HasLen effs
+  => (a -> Eff (v ': effs) w)
   -> (forall x. t x -> Arr (v ': effs) x w -> Eff (v ': effs) w)
   -> Eff (t ': effs) a
   -> Eff (v ': effs) w
@@ -249,7 +251,7 @@ replaceRelay pure' bind = loop
 
 replaceRelayN
   :: forall gs t a effs w
-   . Weakens gs
+   . (Weakens gs, HasLen effs)
   => (a -> Eff (gs :++: effs) w)
   -> (forall x. t x -> Arr (gs :++: effs) x w -> Eff (gs :++: effs) w)
   -> Eff (t ': effs) a
@@ -268,7 +270,8 @@ replaceRelayN pure' bind = loop
 
 -- | Given a request, either handle it or relay it.
 handleRelay
-  :: (a -> Eff effs b)
+  :: HasLen effs
+  => (a -> Eff effs b)
   -- ^ Handle a pure value.
   -> (forall v. eff v -> Arr effs v b -> Eff effs b)
   -- ^ Handle a request for effect of type @eff :: * -> *@.
@@ -289,7 +292,8 @@ handleRelay ret h = loop
 -- @s :: *@ to be handled for the target effect, or relayed to a handler that
 -- can- handle the target effect.
 handleRelayS
-  :: s
+  :: HasLen effs
+  => s
   -> (s -> a -> Eff effs b)
   -- ^ Handle a pure value.
   -> (forall v. s -> eff v -> (s -> Arr effs v b) -> Eff effs b)

src/Control/Monad/Freer/NonDet.hs

@@ -20,6 +20,7 @@ import Control.Monad (msum)
 import Control.Monad.Freer.Internal
   ( Eff(..)
   , Member
+  , HasLen
   , NonDet(..)
   , handleRelay
   , prj
@@ -30,7 +31,7 @@ import Control.Monad.Freer.Internal
 
 -- | A handler for nondeterminstic effects.
 makeChoiceA
-  :: Alternative f
+  :: (Alternative f, HasLen effs)
   => Eff (NonDet ': effs) a
   -> Eff effs (f a)
 makeChoiceA = handleRelay (pure . pure) $ \m k ->

src/Control/Monad/Freer/Reader.hs

@@ -30,7 +30,7 @@ module Control.Monad.Freer.Reader
     -- $localExample
   ) where
 
-import Control.Monad.Freer (Eff, Member, interpose, interpret, send)
+import Control.Monad.Freer (Eff, Member, HasLen, interpose, interpret, send)
 
 -- | Represents shared immutable environment of type @(e :: *)@ which is made
 -- available to effectful computation.
@@ -52,7 +52,7 @@ asks
 asks f = f <$> ask
 
 -- | Handler for 'Reader' effects.
-runReader :: forall r effs a. r -> Eff (Reader r ': effs) a -> Eff effs a
+runReader :: forall r effs a. HasLen effs => r -> Eff (Reader r ': effs) a -> Eff effs a
 runReader r = interpret (\Ask -> pure r)
 
 -- | Locally rebind the value in the dynamic environment.

src/Control/Monad/Freer/State.hs

@@ -41,7 +41,7 @@ module Control.Monad.Freer.State
 
 import Data.Proxy (Proxy)
 
-import Control.Monad.Freer (Eff, Member, send)
+import Control.Monad.Freer (Eff, Member, HasLen, send)
 import Control.Monad.Freer.Internal (Arr, handleRelayS, interposeS)
 
 -- | Strict 'State' effects: one can either 'Get' values or 'Put' them.
@@ -68,17 +68,17 @@ gets :: forall s a effs. Member (State s) effs => (s -> a) -> Eff effs a
 gets f = f <$> get
 
 -- | Handler for 'State' effects.
-runState :: forall s effs a. s -> Eff (State s ': effs) a -> Eff effs (a, s)
+runState :: forall s effs a. HasLen effs => s -> Eff (State s ': effs) a -> Eff effs (a, s)
 runState s0 = handleRelayS s0 (\s x -> pure (x, s)) $ \s x k -> case x of
   Get -> k s s
   Put s' -> k s' ()
 
 -- | Run a 'State' effect, returning only the final state.
-execState :: forall s effs a. s -> Eff (State s ': effs) a -> Eff effs s
+execState :: forall s effs a. HasLen effs => s -> Eff (State s ': effs) a -> Eff effs s
 execState s = fmap snd . runState s
 
 -- | Run a State effect, discarding the final state.
-evalState :: forall s effs a. s -> Eff (State s ': effs) a -> Eff effs a
+evalState :: forall s effs a. HasLen effs => s -> Eff (State s ': effs) a -> Eff effs a
 evalState s = fmap fst . runState s
 
 -- | An encapsulated State handler, for transactional semantics. The global

src/Control/Monad/Freer/Writer.hs

@@ -21,7 +21,7 @@ module Control.Monad.Freer.Writer
 import Control.Arrow (second)
 import Data.Monoid ((<>))
 
-import Control.Monad.Freer.Internal (Eff, Member, handleRelay, send)
+import Control.Monad.Freer.Internal (Eff, Member, HasLen, handleRelay, send)
 
 -- | Writer effects - send outputs to an effect environment.
 data Writer w r where
@@ -32,6 +32,6 @@ tell :: forall w effs. Member (Writer w) effs => w -> Eff effs ()
 tell w = send (Tell w)
 
 -- | Simple handler for 'Writer' effects.
-runWriter :: forall w effs a. Monoid w => Eff (Writer w ': effs) a -> Eff effs (a, w)
+runWriter :: forall w effs a. (HasLen effs, Monoid w) => Eff (Writer w ': effs) a -> Eff effs (a, w)
 runWriter = handleRelay (\a -> pure (a, mempty)) $ \(Tell w) k ->
   second (w <>) <$> k ()

src/Data/OpenUnion.hs

@@ -28,6 +28,7 @@ module Data.OpenUnion
   , Member(..)
   , Members
   , LastMember
+  , HasLen
   ) where
 
 import Data.Kind (Constraint)
@@ -40,6 +41,7 @@ import Data.OpenUnion.Internal
   , decomp
   , extract
   , weaken
+  , HasLen
   )
 
 -- | A shorthand constraint that represents a combination of multiple 'Member'