Effects as GADTs #365
Effects as GADTs #365
Conversation
This doesn’t change its semantics at all.
This does not change its semantics.
|
Is this change mostly syntactic, or are there other implications for how effects are defined? It looks like the GADT syntax will be a lot more straightforward and friendly compared to the old continuation style 🙂 I'm looking forward to it. |
Purely syntactic; it’s equivalent to the continuation style with a continuation of
Glad to hear it! I’m quite pleased with how it’s turning out. |
| 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 () |
There was a problem hiding this comment.
One consequence of this change is that first-order effects in general require kind annotations for the m parameter. (This is documented in the common errors document.)
| write :: Has Teletype sig m => String -> m () | ||
| write s = send (Write s (pure ())) | ||
| write s = send (Write s) |
There was a problem hiding this comment.
Having to provide continuations in smart constructors was a flaw that I am very glad to see removed.
| 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. |
There was a problem hiding this comment.
Figured I’d document using Labelled for mtl interop while I was in here.
| @@ -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. | |||
|
|
|||
|
|
|||
There was a problem hiding this comment.
double 👏 space 👏 above 👏 headings
| c:cs | p c -> ParseC (put cs) *> hdl (k c <$ ctx) | ||
| c:cs | p c -> c <$ ctx <$ ParseC (put cs) |
There was a problem hiding this comment.
I really like the left-associativity of <$ here ✨
| alg hdl sig ctx = case sig of | ||
| L Empty -> [] | ||
| R (Choose k) -> hdl (k True <$ ctx) ++ hdl (k False <$ ctx) | ||
| alg _ sig ctx = case sig of | ||
| L Empty -> [] | ||
| R Choose -> [ True <$ ctx, False <$ ctx ] |
There was a problem hiding this comment.
This is one of the best examples of how cool this change turned out to be. Lacking a continuation means we have to return a value instead of calling k with it, and that value is ctx a (whatever a is for that constructor). Since Choose :: Choose m Bool, that means we need to return [ctx Bool]. Hence, instead of concatenating the lists produced by the continuations, we produce the two-element list above and let the Monad instance for [] take care of the rest externally to alg.
All in all, this change should result in far fewer binds being issued. Many of these would ideally have been compiled away anyhow, but there’s now that much less work for the simplifier to do. And since the algebras themselves are (often dramatically!) simpler as a result, it’s win-win-win.
| @@ -91,8 +92,8 @@ instance MonadTrans ChooseC where | |||
|
|
|||
| instance Algebra sig m => Algebra (Choose :+: sig) (ChooseC m) where | |||
| alg (hdl :: forall x . ctx (n x) -> ChooseC m (ctx x)) sig (ctx :: ctx ()) = case sig of | |||
| L (Choose k) -> ChooseC $ \ fork leaf -> fork (runChoose fork leaf (hdl (k True <$ ctx))) (runChoose fork leaf (hdl (k False <$ ctx))) | |||
| R other -> ChooseC $ \ fork leaf -> thread dst hdl other (pure ctx) >>= runIdentity . runChoose (coerce fork) (coerce leaf) | |||
| L Choose -> ChooseC $ \ fork leaf -> fork (leaf (True <$ ctx)) (leaf (False <$ ctx)) | |||
There was a problem hiding this comment.
This is the Church-encoded binary tree version of that algebra for lists above.
|
|
||
| -- | @since 0.1.0.0 | ||
| newtype Fresh m k = Fresh (Int -> m k) | ||
| deriving (Functor) | ||
| data Fresh (m :: Type -> Type) k where |
There was a problem hiding this comment.
I’ve gone out of my way to use Type instead of * for the new kind signatures. I’m planning on turning the star is type warning back on at some point this release.
This PR redefines all the effects as GADTs, simplifying and tidying the smart constructors and algebras considerably.