Effects as GADTs

benchmark/Bench.hs

@@ -1,6 +1,8 @@
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -30,34 +32,28 @@ main = defaultMain
     , bench "1000"  $ whnf (run . execWriter @(Sum Int) . tellLoop) 1000
     , bench "10000" $ whnf (run . execWriter @(Sum Int) . tellLoop) 10000
     ]
-  ,
-    bgroup "Strict StateC"
-    [ bench "100"   $ whnf (run . execState @(Sum Int) 0 . modLoop) 100
-    , bench "1000"  $ whnf (run . execState @(Sum Int) 0 . modLoop) 1000
-    , bench "10000" $ whnf (run . execState @(Sum Int) 0 . modLoop) 10000
-    ]
-  ,
-    bgroup "InterpretC vs InterpretStateC vs StateC"
+
+  , bgroup "InterpretC vs InterpretStateC vs StateC"
     [ bgroup "InterpretC"
-      [ bench "100"   $ whnf (\n -> run $ evalState @(Sum Int) 0 $ runInterpret (\ hdl sig ctx -> case sig of { Get k -> get @(Sum Int) >>= hdl . (<$ ctx) . k ; Put s k -> put s >> hdl (k <$ ctx) }) $ modLoop n) 100
-      , bench "1000"  $ whnf (\n -> run $ evalState @(Sum Int) 0 $ runInterpret (\ hdl sig ctx -> case sig of { Get k -> get @(Sum Int) >>= hdl . (<$ ctx) . k ; Put s k -> put s >> hdl (k <$ ctx) }) $ modLoop n) 1000
-      , bench "10000" $ whnf (\n -> run $ evalState @(Sum Int) 0 $ runInterpret (\ hdl sig ctx -> case sig of { Get k -> get @(Sum Int) >>= hdl . (<$ ctx) . k ; Put s k -> put s >> hdl (k <$ ctx) }) $ modLoop n) 10000
+      [ bench "100"   $ whnf (\n -> run $ execState @Int 0 $ runInterpret (\ _ (sig :: State Int m k) ctx -> case sig of { Get -> gets @Int (<$ ctx) ; Put s -> ctx <$ put s }) $ modLoop n) 100
+      , bench "1000"  $ whnf (\n -> run $ execState @Int 0 $ runInterpret (\ _ (sig :: State Int m k) ctx -> case sig of { Get -> gets @Int (<$ ctx) ; Put s -> ctx <$ put s }) $ modLoop n) 1000
+      , bench "10000" $ whnf (\n -> run $ execState @Int 0 $ runInterpret (\ _ (sig :: State Int m k) ctx -> case sig of { Get -> gets @Int (<$ ctx) ; Put s -> ctx <$ put s }) $ modLoop n) 10000
       ]
     , bgroup "InterpretStateC"
-      [ bench "100"   $ whnf (\n -> run $ runInterpretState (\ hdl sig s ctx -> case sig of { Get k -> runState @(Sum Int) s (hdl (k s <$ ctx)) ; Put s k -> runState s (hdl (k <$ ctx)) }) 0 $ modLoop n) 100
-      , bench "1000"  $ whnf (\n -> run $ runInterpretState (\ hdl sig s ctx -> case sig of { Get k -> runState @(Sum Int) s (hdl (k s <$ ctx)) ; Put s k -> runState s (hdl (k <$ ctx)) }) 0 $ modLoop n) 1000
-      , bench "10000" $ whnf (\n -> run $ runInterpretState (\ hdl sig s ctx -> case sig of { Get k -> runState @(Sum Int) s (hdl (k s <$ ctx)) ; Put s k -> runState s (hdl (k <$ ctx)) }) 0 $ modLoop n) 10000
+      [ bench "100"   $ whnf (\n -> fst . run $ runInterpretState (\ _ (sig :: State Int m k) (s :: Int) ctx -> case sig of { Get -> pure (s, s <$ ctx) ; Put s -> pure (s, ctx) }) 0 $ modLoop n) 100
+      , bench "1000"  $ whnf (\n -> fst . run $ runInterpretState (\ _ (sig :: State Int m k) (s :: Int) ctx -> case sig of { Get -> pure (s, s <$ ctx) ; Put s -> pure (s, ctx) }) 0 $ modLoop n) 1000
+      , bench "10000" $ whnf (\n -> fst . run $ runInterpretState (\ _ (sig :: State Int m k) (s :: Int) ctx -> case sig of { Get -> pure (s, s <$ ctx) ; Put s -> pure (s, ctx) }) 0 $ modLoop n) 10000
       ]
     , bgroup "StateC"
-      [ bench "100"   $ whnf (run . evalState @(Sum Int) 0 . modLoop) 100
-      , bench "1000"  $ whnf (run . evalState @(Sum Int) 0 . modLoop) 1000
-      , bench "10000" $ whnf (run . evalState @(Sum Int) 0 . modLoop) 10000
+      [ bench "100"   $ whnf (run . execState @Int 0 . modLoop) 100
+      , bench "1000"  $ whnf (run . execState @Int 0 . modLoop) 1000
+      , bench "10000" $ whnf (run . execState @Int 0 . modLoop) 10000
       ]
     ]
   ]
 
 tellLoop :: Has (Writer (Sum Int)) sig m => Int -> m ()
 tellLoop i = replicateM_ i (tell (Sum (1 :: Int)))
 
-modLoop :: Has (State (Sum Int)) sig m => Int -> m ()
-modLoop i = replicateM_ i (modify (+ Sum (1 :: Int)))
+modLoop :: Has (State Int) sig m => Int -> m ()
+modLoop i = replicateM_ i (modify (+ (1 :: Int)))

docs/common_errors.md

@@ -6,14 +6,14 @@ is an attempt to enumerate and explicate the things that can go wrong
 when using or extending this library. (It is also very much a work in
 progress.)
 
+
 ## I'm getting kind errors when implementing an `Algebra` instance!
 
 Given an effect datatype that doesn’t use the `m` parameter:
 
 ```haskell
-data Fail m k
-  = Fail String
-  deriving (Functor)
+data Fail m k where
+  Fail :: String -> Fail m a
 
 newtype FailC m a = FailC { runFailC :: m (Either String a) }
 ```
@@ -39,7 +39,6 @@ the definition of `Fail`, so GHC makes an understandable but incorrect inference
 An explicit kind annotation on `m` fixes the problem.
 
 ```haskell
-data Fail (m :: * -> *) k
-  = Fail String
-  deriving (Functor)
+data Fail (m :: * -> *) k where
+  Fail :: String -> Fail m a
 ```

docs/defining_effects.md

@@ -5,7 +5,7 @@ Effects are a powerful mechanism for abstraction, and so defining new effects is
 It’s often helpful to start by specifying the types of the desired operations. For our example, we’re going to define a `Teletype` effect, with `read` and `write` operations, which read a string from some input and write a string to some output, respectively:
 
 ```haskell
-data Teletype m k
+data Teletype (m :: Type -> Type) k
 read :: Has Teletype sig m => m String
 write :: Has Teletype sig m => String -> m ()
 ```
@@ -15,54 +15,45 @@ Effect types must have two type parameters: `m`, denoting any computations which
 Next, we can flesh out the definition of the `Teletype` effect by providing constructors for each primitive operation:
 
 ```haskell
-data Teletype m k
-  = Read (String -> m k)
-  | Write String (m k)
-  deriving (Functor)
+data Teletype (m :: Type -> Type) k where
+  Read  ::           Teletype m String
+  Write :: String -> Teletype m ()
 ```
 
-The `Read` operation returns a `String`, and hence its continuation is represented as a function _taking_ a `String`. Thus, to continue the computation, a handler will have to provide a `String`. But since the effect type doesn’t say anything about where that `String` should come from, handlers are free to read from `stdin`, use a constant value, etc.
-
-On the other hand, the `Write` operation returns `()`. Since a function `() -> k` is equivalent to a (non-strict) `k`, we can omit the function parameter.
+The `Read` operation returns a `String`, and hence its result type is `String`. Thus, to interpret this constructor, an algebra will have to produce a `String`. But since the effect type doesn’t say anything about where that `String` should come from, algebras are free to read from `stdin`, use a constant value, etc. By contrast, the `Write` operation takes a `String` and returns `()`.
 
 Now that we have our effect datatype, we can give definitions for `read` and `write`:
 
 ```haskell
 read :: Has Teletype sig m => m String
-read = send (Read pure)
+read = send Read
 
 write :: Has Teletype sig m => String -> m ()
-write s = send (Write s (pure ()))
+write s = send (Write s)
 ```
 
 This gives us enough to write computations using the `Teletype` effect. The next section discusses how to run `Teletype` computations.
 
-## Defining effect handlers
 
-Effects only specify actions, they don’t actually perform them. That task is left up to effect handlers, typically defined as functions calling `interpret` to apply a given `Algebra` instance.
+## Defining algebras
+
+Effects only specify actions, they don’t actually specify how any actions should be performed. That task is left up to algebras, defined as `Algebra` instances.
 
 Following from the above section, we can define a carrier for the `Teletype` effect which runs the calls in an underlying `MonadIO` instance, accessed via our carrier’s own `GenericNewtypeDeriving`-derived instance:
 
 ```haskell
-newtype TeletypeIOC m a = TeletypeIOC { runTeletypeIOC :: m a }
+newtype TeletypeIOC m a = TeletypeIOC { runTeletypeIO :: m a }
   deriving (Applicative, Functor, Monad, MonadIO)
 
 instance (MonadIO m, Algebra sig m) => Algebra (Teletype :+: sig) (TeletypeIOC m) where
   alg hdl sig ctx = case sig of
-    L (Read    k) -> liftIO getLine      >>= hdl . (<$ ctx) . k
-    L (Write s k) -> liftIO (putStrLn s) >>  hdl (k <$ ctx>)
-    R other       -> TeletypeIOC (alg (runTeletypeIOC . hdl) other ctx)
+    L Read      -> (<$ ctx) <$ liftIO getLine
+    L (Write s) -> ctx      <$ liftIO (putStrLn s)
+    R other     -> TeletypeIOC (alg (runTeletypeIO . hdl) other ctx)
 ```
 
-Here, `alg` is responsible for handling effectful computations. Since the `Algebra` instance handles a sum (`:+:`) of `Teletype` and the remaining signature, `alg` has two parts: a handler for `Teletype`, and a handler for teletype effects that might be embedded inside other effects in the signature.
-
-In this case, since the `Teletype` carrier is just a thin wrapper around the underlying computation, we pass `alg` a function to unwrap any embedded `TeletypeIOC` values by simply composing `runTeletypeIOC` onto `hom`.
+Here, `alg` is responsible for handling effectful computations. Since the `Algebra` instance handles a sum (`:+:`) of `Teletype` and the remaining signature, `alg` has two parts: a case for the `Teletype` effect (in `L`), and a case for effects in the tail of the signature (in `R`).
 
-That leaves `Teletype` effects themselves, which are handled with one case per constructor. Since we’re assuming the existence of a `MonadIO` instance for the underlying computation, we can use `liftIO` to inject the `getLine` and `putStrLn` actions into it, and then proceed with the continuations, unwrapping them in the process.
+The `Teletype` effect is handled with a case per constructor. Since we’re assuming the existence of a `MonadIO` instance for the underlying computation, we use `liftIO` to inject the `getLine` and `putStrLn` actions into it, and simply bundle up the initial state `ctx` with the results.
 
-By convention, we also provide a `runTeletypeIO` function. For `TeletypeIOC` this just unwrapps the carrier, but for more involved carriers it might also apply some arguments. (We could also have used this name for the type’s field selector directly, at the cost of some asymmetry in its name.)
-
-```haskell
-runTeletypeIO :: TeletypeIOC m a -> m a
-runTeletypeIO = runTeletypeIOC
-```
+Since the `Teletype` carrier is just a thin wrapper around the underlying computation, we can handle the tail of the signature by passing `alg` a function to unwrap any embedded `TeletypeIOC` values by simply composing `runTeletypeIO` onto `hdl`.

docs/faqs.md

@@ -2,14 +2,25 @@
 
 ## Why is `Algebra` called `Algebra`, and not something more specific to the interpretation of effects?
 
-In previous versions of `fused-effects`, `Algebra` was called Carrier. The authors chose to rename this to keep it in line with the literature (the corresponding typeclass is called `TermAlgebra` in _Fusion for Free_), emphasize the importance of morphisms over objects, and emphasize its similarity to the common Haskell idiom of [F-algebras](https://www.schoolofhaskell.com/user/bartosz/understanding-algebras). The term “algebra” stems from the Arabic جبر, _jabr_, which roughly translates to “reunion” or “restoration”. This propery is visible in the definition of the `Carrier` class’s `eff` method:
+In previous versions of `fused-effects`, `Algebra` was called `Carrier`. The authors chose to rename this to keep it in line with the literature (the corresponding typeclass is called `TermAlgebra` in _Fusion for Free_), emphasize the importance of morphisms over objects, and emphasize its similarity to the common Haskell idiom of [F-algebras](https://www.schoolofhaskell.com/user/bartosz/understanding-algebras). The term “algebra” stems from the Arabic جبر, _jabr_, which roughly translates to “reunion” or “restoration”. This property is most clearly visible in the `alg` method’s original type signature:
 
 ```haskell
-eff :: sig m a -> m a
+alg :: sig m a -> m a
 ```
 
 Like the traditional encoding of F-algebras (`f a -> a`), this describes a function that reunites an effect signature `sig` with its monadic context `m`.
 
+In 1.1.0.0, `alg` was given an extended signature:
+
+```haskell
+alg :: Functor ctx => Handler ctx n m -> sig n a -> ctx () -> m (ctx a)
+```
+
+Ignoring `ctx` for the moment, this corresponds to higher-order _Mendler iteration_: instead of the algebra receiving a signature containing `m`s, it receives an algebra containing some other (universally quantified) type `n`, plus a handler function lowering `n` to `m`, similar to how `foldMap` takes a structure `t a` and reduces the `a`s to some `Monoid` `m` using a function `a -> m`.
+
+The context occurs in both `alg` and the handler in order to correctly lower stateful monad transformers `t m` to `m` while carrying along whatever context they need to resume: for `ExceptT e` this is `Either e`, for `StateT s` it’s `(,) s`, and so on. So all told, `alg` is a state-preserving Mendler-style `sig`-algebra.
+
+
 ## When do I need to use the type application (`@Foo`) syntax?
 
 Because a given effectful operation can have multiple `State` or `Reader` effects, your code may fail to typecheck if it invokes an ambiguous state or reader effect, such as follows:
@@ -32,22 +43,37 @@ okay = do
 
 The `@Int` syntax—an _explicit type application_ specifies that the return type of `get` must in this case be an `Int`. For more information about type applications, consult the [GHC manual](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeApplications).
 
+
 ## How can I build effect stacks that interoperate correctly with `mtl`?
 
-There are two approaches: the first is to use the monadic types defined by `transformers` as the carriers for your effects. The resulting composition of monads will interoperate with `mtl` and any `mtl`-compatible library. The second is to wrap an existing monad stack with a phantom type representing some relevant effect information:
+There are three approaches:
 
-```haskell
-newtype Wrapper s m a = Wrapper { runWrapper :: m a }
-  deriving (Algebra sig, Applicative, Functor, Monad)
+1. Use the monadic types defined by `transformers` as the carriers for your effects. The resulting composition of monads will interoperate with `mtl` and any `mtl`-compatible library.
 
-getState :: Has (State s) sig m => Wrapper s m s
-getState = get
-```
+2. Wrap an existing monad stack with a phantom type representing some relevant effect information:
 
-Indeed, `Wrapper` can now be made an instance of `MonadState`:
+    ```haskell
+    newtype Wrapper s m a = Wrapper { runWrapper :: m a }
+      deriving (Algebra sig, Applicative, Functor, Monad)
 
-```haskell
-instance Has (State s) sig m => MTL.MonadState s (Wrapper s m) where
-  get = Control.Carrier.State.Strict.get
-  put = Control.Carrier.State.Strict.put
-```
+    getState :: Has (State s) sig m => Wrapper s m s
+    getState = get
+    ```
+
+    Indeed, `Wrapper` can now be made an instance of `MonadState`:
+
+    ```haskell
+    instance Has (State s) sig m => MTL.MonadState s (Wrapper s m) where
+      get = Control.Effect.State.get
+      put = Control.Effect.State.put
+    ```
+
+3. Use `Control.Effect.Labelled` to define an instance for some specific label:
+
+    ```haskell
+    instance HasLabelled State (State s) sig m => MTL.MonadState s (Wrapper s m) where
+      get = Control.Effect.State.Labelled.get @State
+      put = Control.Effect.State.Labelled.put @State
+    ```
+
+    Now `Wrapper` has a `MonadState` instance whenever `m` has an appropriately-labelled `State` effect, which can be provided by the `Control.Effect.Labelled.Labelled` carrier.

docs/migrating.md

@@ -2,6 +2,7 @@
 
 This file summarizes the changelog and extracts the pieces most relevant to bringing up `fused-effects` applications to use newer versions of the library.
 
+
 ## 0.5 → 1.0
 
 * The library has been divided into two hierarchies: `Control.Effect.*` provides the effect types, and `Control.Carrier.*` provides the carrier monads needed to run said effects. Each carrier exports its relevant effect types, so it suffices to import whichever carrier is needed.
@@ -10,4 +11,3 @@ This file summarizes the changelog and extracts the pieces most relevant to brin
 * The `Resumable` effect has been moved to `fused-effects-resumable`.
 * The `Carrier` class has been renamed to `Algebra` and moved to `Control.Algebra`.
 * In order to save keystrokes in the common case of `(Member eff sig, Algebra sig m)`, there now exists a `Has` constraint that covers this case and which all carrier modules reexport. Using `Has`, the above would be written `Has eff sig m`. Code that uses `Member` and `Algebra` will continue to work.
-