-
Notifications
You must be signed in to change notification settings - Fork 24
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
8d922c0
commit a6d3dc7
Showing
30 changed files
with
1,042 additions
and
2,593 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,98 +1,200 @@ | ||
{-# OPTIONS_HADDOCK show-extensions #-} | ||
|
||
{-# LANGUAGE TypeOperators #-} | ||
{-# LANGUAGE TupleSections #-} | ||
{-# OPTIONS_GHC -Werror #-} | ||
{-# LANGUAGE Trustworthy #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE UndecidableInstances #-} | ||
{-# LANGUAGE FlexibleInstances #-} | ||
{-# LANGUAGE FlexibleContexts #-} | ||
{-# LANGUAGE MultiParamTypeClasses #-} | ||
{-# LANGUAGE ExistentialQuantification #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
{-# LANGUAGE NoMonomorphismRestriction #-} | ||
{-# LANGUAGE CPP #-} | ||
{-# LANGUAGE Safe #-} | ||
|
||
-- | Original work available at <http://okmij.org/ftp/Haskell/extensible/Eff.hs>. | ||
{-# LANGUAGE TupleSections #-} | ||
{-# LANGUAGE TypeOperators #-} | ||
{-# LANGUAGE GADTs #-} | ||
{-# LANGUAGE DataKinds #-} | ||
|
||
-- | Original work available at <http://okmij.org/ftp/Haskell/extensible/tutorial.html>. | ||
-- This module implements extensible effects as an alternative to monad transformers, | ||
-- as described in <http://okmij.org/ftp/Haskell/extensible/exteff.pdf>. | ||
-- as described in <http://okmij.org/ftp/Haskell/extensible/exteff.pdf> and | ||
-- <http://okmij.org/ftp/Haskell/extensible/more.pdf>. | ||
-- | ||
-- Extensible Effects are implemented as typeclass constraints on an Eff[ect] datatype. | ||
-- A contrived example can be found under "Control.Eff.Example". To run the | ||
-- effects, consult the tests. | ||
module Control.Eff( | ||
Eff | ||
, module Reflection | ||
, Member | ||
, SetMember | ||
, Union | ||
, (:>) | ||
, inj | ||
, prj | ||
, prjForce | ||
, decomp | ||
, send | ||
, run | ||
, interpose | ||
, handleRelay | ||
, unsafeReUnion | ||
) where | ||
|
||
import Control.Monad.Free.Reflection as Reflection | ||
import Data.OpenUnion | ||
import Data.Typeable | ||
import Data.Void | ||
|
||
#if __GLASGOW_HASKELL__ >= 708 | ||
#define Typeable1 Typeable | ||
#endif | ||
|
||
-- | Basic type returned by all computations with extensible effects. The @`Eff` | ||
-- r@ type is a type synonym where the type @r@ is the type of effects that can | ||
-- be handled, and the missing type @a@ (from the type application) is the type | ||
-- of value that is returned. | ||
module Control.Eff where | ||
|
||
import safe Data.OpenUnion51 | ||
import Data.FTCQueue1 | ||
import GHC.Exts (inline) | ||
|
||
-- ------------------------------------------------------------------------ | ||
-- | A monadic library for communication between a handler and | ||
-- its client, the administered computation | ||
-- | ||
-- Effectful arrow type: a function from a to b that also does effects | ||
-- denoted by r | ||
type Arr r a b = a -> Eff r b | ||
|
||
arr :: (a -> b) -> Arrs r a b | ||
arr f = tsingleton (Val . f) | ||
|
||
-- FIXME: convert to 'Arrs' | ||
first :: Arr r a b -> Arr r (a, c) (b, c) | ||
first x = \(a,c) -> (, c) `fmap` x a | ||
|
||
ident :: Arrs r a a | ||
ident = tsingleton $ Val . id | ||
|
||
comp :: Arrs r a b -> Arrs r b c -> Arrs r a c | ||
comp = (><) | ||
|
||
-- | An effectful function from 'a' to 'b' that is a composition | ||
-- of several effectful functions. The paremeter r describes the overall | ||
-- effect. | ||
-- The composition members are accumulated in a type-aligned queue | ||
type Arrs r a b = FTCQueue (Eff r) a b | ||
|
||
-- | The Eff monad (not a transformer!). It is a fairly standard coroutine monad | ||
-- where the type @r@ is the type of effects that can be handled, and the | ||
-- missing type @a@ (from the type application) is the type of value that is | ||
-- returned. It is NOT a Free monad! There are no Functor constraints. | ||
-- | ||
-- Expressed another way: an `Eff` can either be a value (i.e., 'Pure' case), or | ||
-- an effect of type @`Union` r@ producing another `Eff` (i.e., 'Impure' | ||
-- case). The result is that an `Eff` can produce an arbitrarily long chain of | ||
-- @`Union` r@ effects, terminated with a pure value. | ||
-- The two constructors denote the status of a coroutine (client): done with the | ||
-- value of type a, or sending a request of type Union r with the continuation | ||
-- Arrs r b a. Expressed another way: an `Eff` can either be a value (i.e., | ||
-- 'Val' case), or an effect of type @`Union` r@ producing another `Eff` (i.e., | ||
-- 'E' case). The result is that an `Eff` can produce an arbitrarily long chain | ||
-- of @`Union` r@ effects, terminated with a pure value. | ||
-- | ||
-- As is made explicit below, the `Eff` type is simply the Free monad resulting from the | ||
-- @`Union` r@ functor. | ||
-- Potentially, inline Union into E | ||
data Eff r a = Val a | ||
| forall b. E (Union r b) (Arrs r b a) | ||
|
||
-- | Application to the `generalized effectful function' Arrs r b w | ||
{-# INLINABLE qApp #-} | ||
qApp :: Arrs r b w -> b -> Eff r w | ||
qApp q x = | ||
case inline tviewl q of | ||
TOne k -> k x | ||
k :| t -> case k x of | ||
Val y -> qApp t y | ||
E u q0 -> E u (q0 >< t) | ||
|
||
{- | ||
-- A bit more understandable version | ||
qApp :: Arrs r b w -> b -> Eff r w | ||
qApp q x = case tviewl q of | ||
TOne k -> k x | ||
k :| t -> bind' (k x) t | ||
where | ||
bind' :: Eff r a -> Arrs r a b -> Eff r b | ||
bind' (Pure y) k = qApp k y | ||
bind' (Impure u q) k = Impure u (q >< k) | ||
-} | ||
|
||
-- | Compose effectful arrows (and possibly change the effect!) | ||
{-# INLINE qComp #-} | ||
qComp :: Arrs r a b -> (Eff r b -> Eff r' c) -> Arr r' a c | ||
-- qComp g h = (h . (g `qApp`)) | ||
qComp g h = \a -> h $ qApp g a | ||
|
||
-- | Eff is still a monad and a functor (and Applicative) | ||
-- (despite the lack of the Functor constraint) | ||
instance Functor (Eff r) where | ||
{-# INLINE fmap #-} | ||
fmap f (Val x) = Val (f x) | ||
fmap f (E u q) = E u (q |> (Val . f)) -- does no mapping yet! | ||
|
||
instance Applicative (Eff r) where | ||
pure = Val | ||
Val f <*> Val x = Val $ f x | ||
Val f <*> E u q = E u (q |> (Val . f)) | ||
E u q <*> Val x = E u (q |> (Val . ($ x))) | ||
E u q <*> m = E u (q |> (`fmap` m)) | ||
|
||
instance Monad (Eff r) where | ||
{-# INLINE return #-} | ||
{-# INLINE [2] (>>=) #-} | ||
return x = Val x | ||
Val x >>= k = k x | ||
E u q >>= k = E u (q |> k) -- just accumulates continuations | ||
{- | ||
Val _ >> m = m | ||
E u q >> m = E u (q |> const m) | ||
-} | ||
|
||
-- | Send a request and wait for a reply (resulting in an effectful | ||
-- computation). | ||
{-# INLINE [2] send #-} | ||
send :: Member t r => t v -> Eff r v | ||
send t = E (inj t) (tsingleton Val) | ||
-- This seems to be a very beneficial rule! On micro-benchmarks, cuts | ||
-- the needed memory in half and speeds up almost twice. | ||
{-# RULES | ||
"send/bind" [~3] forall t k. send t >>= k = E (inj t) (tsingleton k) | ||
#-} | ||
|
||
|
||
{- | ||
-- The opposite of admin, occasionally useful | ||
-- See the soft-cut for an example | ||
-- It is currently quite inefficient. There are better ways | ||
reflect :: VE a r -> Eff r a | ||
reflect (Val x) = return x | ||
reflect (E u) = Eff (\k -> E $ fmap (loop k) u) | ||
where | ||
loop :: (a -> VE w r) -> VE a r -> VE w r | ||
loop k (Val x) = k x | ||
loop k (E u) = E $ fmap (loop k) u | ||
-} | ||
|
||
|
||
-- ------------------------------------------------------------------------ | ||
-- | The initial case, no effects. Get the result from a pure computation. | ||
-- | ||
-- The type of run ensures that all effects must be handled: | ||
-- only pure computations may be run. | ||
run :: Eff '[] w -> w | ||
run (Val x) = x | ||
-- | the other case is unreachable since Union [] a cannot be | ||
-- constructed. | ||
-- Therefore, run is a total function if its argument terminates. | ||
run (E _ _) = error "extensible-effects: the impossible happened!" | ||
|
||
-- | A convenient pattern: given a request (open union), either | ||
-- handle it or relay it. | ||
{-# INLINE handle_relay #-} | ||
handle_relay :: (a -> Eff r w) -> | ||
(forall v. t v -> Arr r v w -> Eff r w) -> | ||
Eff (t ': r) a -> Eff r w | ||
handle_relay ret h m = loop m | ||
where | ||
loop (Val x) = ret x | ||
loop (E u q) = case decomp u of | ||
Right x -> h x k | ||
Left u0 -> E u0 (tsingleton k) | ||
where k = qComp q loop | ||
|
||
-- | Parameterized handle_relay | ||
{-# INLINE handle_relay_s #-} | ||
handle_relay_s :: s -> | ||
(s -> a -> Eff r w) -> | ||
(forall v. s -> t v -> (s -> Arr r v w) -> Eff r w) -> | ||
Eff (t ': r) a -> Eff r w | ||
handle_relay_s s ret h m = loop s m | ||
where | ||
loop s0 (Val x) = ret s0 x | ||
loop s0 (E u q) = case decomp u of | ||
Right x -> h s0 x k | ||
Left u0 -> E u0 (tsingleton (k s0)) | ||
where k s1 x = loop s1 $ qApp q x | ||
|
||
-- | Add something like Control.Exception.catches? It could be useful | ||
-- for control with cut. | ||
-- | ||
-- @type `Eff` r a = `Free` (`Union` r) a@ | ||
type Eff r = Free (Union r) | ||
|
||
-- | Given a method of turning requests into results, | ||
-- we produce an effectful computation. | ||
send :: Union r a -> Eff r a | ||
send = freeImpure . (fmap freePure) | ||
{-# INLINE send #-} | ||
|
||
-- | Get the result from a pure computation. | ||
run :: Eff Void w -> w | ||
run = freeMap id | ||
(\_ -> error "extensible-effects: the impossible happened!") | ||
{-# INLINE run #-} | ||
-- the other case is unreachable since Void has no constructors | ||
-- Therefore, run is a total function if m Val terminates. | ||
|
||
-- | Given a request, either handle it or relay it. | ||
handleRelay :: Typeable1 t | ||
=> Union (t :> r) v -- ^ Request | ||
-> (v -> Eff r a) -- ^ Relay the request | ||
-> (t v -> Eff r a) -- ^ Handle the request of type t | ||
-> Eff r a | ||
handleRelay u loop h = either passOn h $ decomp u | ||
where passOn u' = send u' >>= loop | ||
{-# INLINE handleRelay #-} | ||
|
||
-- | Given a request, either handle it or relay it. Both the handler | ||
-- and the relay can produce the same type of request that was handled. | ||
interpose :: (Typeable1 t, Functor t, Member t r) | ||
=> Union r v | ||
-> (v -> Eff r a) | ||
-> (t v -> Eff r a) | ||
-> Eff r a | ||
interpose u loop h = maybe (send u >>= loop) h $ prj u | ||
-- Intercept the request and possibly reply to it, but leave it unhandled | ||
-- (that's why we use the same r all throuout) | ||
{-# INLINE interpose #-} | ||
interpose :: Member t r => | ||
(a -> Eff r w) -> (forall v. t v -> Arr r v w -> Eff r w) -> | ||
Eff r a -> Eff r w | ||
interpose ret h m = loop m | ||
where | ||
loop (Val x) = ret x | ||
loop (E u q) = case prj u of | ||
Just x -> h x k | ||
_ -> E u (tsingleton k) | ||
where k = qComp q loop |
Oops, something went wrong.