mirror of
https://github.com/lexi-lambda/freer-simple.git
synced 2024-09-11 08:05:51 +03:00
initial commit
This commit is contained in:
commit
7897b40ec9
9
.gitignore
vendored
Normal file
9
.gitignore
vendored
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
# haskell
|
||||||
|
.stack-work
|
||||||
|
.cabal-sandbox
|
||||||
|
dist
|
||||||
|
cabal.sandbox.config
|
||||||
|
|
||||||
|
# emacs
|
||||||
|
TAGS
|
||||||
|
tags
|
30
LICENSE
Normal file
30
LICENSE
Normal file
@ -0,0 +1,30 @@
|
|||||||
|
Copyright (c) 2015, Alej Cabrera
|
||||||
|
|
||||||
|
All rights reserved.
|
||||||
|
|
||||||
|
Redistribution and use in source and binary forms, with or without
|
||||||
|
modification, are permitted provided that the following conditions are met:
|
||||||
|
|
||||||
|
* Redistributions of source code must retain the above copyright
|
||||||
|
notice, this list of conditions and the following disclaimer.
|
||||||
|
|
||||||
|
* Redistributions in binary form must reproduce the above
|
||||||
|
copyright notice, this list of conditions and the following
|
||||||
|
disclaimer in the documentation and/or other materials provided
|
||||||
|
with the distribution.
|
||||||
|
|
||||||
|
* Neither the name of Alej Cabrera nor the names of other
|
||||||
|
contributors may be used to endorse or promote products derived
|
||||||
|
from this software without specific prior written permission.
|
||||||
|
|
||||||
|
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||||
|
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||||
|
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||||
|
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||||
|
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||||
|
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||||
|
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||||
|
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||||
|
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||||
|
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||||
|
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
34
freer.cabal
Normal file
34
freer.cabal
Normal file
@ -0,0 +1,34 @@
|
|||||||
|
-- Initial freer.cabal generated by cabal init. For further documentation,
|
||||||
|
-- see http://haskell.org/cabal/users-guide/
|
||||||
|
|
||||||
|
name: freer
|
||||||
|
version: 0.1.0.0
|
||||||
|
synopsis: Implementation of the Freer Monad
|
||||||
|
-- description:
|
||||||
|
license: BSD3
|
||||||
|
license-file: LICENSE
|
||||||
|
author: Alej Cabrera
|
||||||
|
maintainer: cpp.cabrera@gmail.com
|
||||||
|
-- copyright:
|
||||||
|
category: Control
|
||||||
|
build-type: Simple
|
||||||
|
-- extra-source-files:
|
||||||
|
cabal-version: >=1.10
|
||||||
|
|
||||||
|
library
|
||||||
|
exposed-modules: Control.Monad.Freer.Internal
|
||||||
|
, Data.FTCQueue
|
||||||
|
, Data.Open.Union
|
||||||
|
, Control.Monad.Freer.Reader
|
||||||
|
, Control.Monad.Freer.Writer
|
||||||
|
, Control.Monad.Freer.State
|
||||||
|
, Control.Monad.Freer.StateRW
|
||||||
|
, Control.Monad.Freer.Exception
|
||||||
|
, Control.Monad.Freer.Trace
|
||||||
|
, Control.Monad.Freer.Fresh
|
||||||
|
-- other-modules:
|
||||||
|
-- other-extensions:
|
||||||
|
build-depends: base >=4.8 && <4.9
|
||||||
|
hs-source-dirs: src
|
||||||
|
-- ghc-options: -Wall
|
||||||
|
default-language: Haskell2010
|
121
src/Control/Monad/Freer/Exception.hs
Normal file
121
src/Control/Monad/Freer/Exception.hs
Normal file
@ -0,0 +1,121 @@
|
|||||||
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
|
{-# LANGUAGE ScopedTypeVariables #-}
|
||||||
|
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||||
|
module Control.Monad.Freer.Exception (
|
||||||
|
Exc,
|
||||||
|
throwError,
|
||||||
|
runError,
|
||||||
|
catchError
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Control.Monad
|
||||||
|
import Control.Monad.Freer.Reader -- for examples
|
||||||
|
import Control.Monad.Freer.State -- for examples
|
||||||
|
import Control.Monad.Freer.Internal
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Exceptions --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- | Exceptions of the type e; no resumption
|
||||||
|
newtype Exc e v = Exc e
|
||||||
|
|
||||||
|
-- The type is inferred
|
||||||
|
throwError :: (Member (Exc e) r) => e -> Eff r a
|
||||||
|
throwError e = send (Exc e)
|
||||||
|
|
||||||
|
runError :: Eff (Exc e ': r) a -> Eff r (Either e a)
|
||||||
|
runError =
|
||||||
|
handleRelay (return . Right) (\ (Exc e) _k -> return (Left e))
|
||||||
|
|
||||||
|
-- The handler is allowed to rethrow the exception
|
||||||
|
catchError :: Member (Exc e) r =>
|
||||||
|
Eff r a -> (e -> Eff r a) -> Eff r a
|
||||||
|
catchError m handle = interpose return (\(Exc e) _k -> handle e) m
|
||||||
|
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Tests and Examples --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
add = liftM2 (+)
|
||||||
|
|
||||||
|
-- The type is inferred
|
||||||
|
et1 :: Eff r Int
|
||||||
|
et1 = return 1 `add` return 2
|
||||||
|
|
||||||
|
et1r :: Bool
|
||||||
|
et1r = 3 == run et1
|
||||||
|
|
||||||
|
-- The type is inferred
|
||||||
|
-- et2 :: Member (Exc Int) r => Eff r Int
|
||||||
|
et2 = return 1 `add` throwError (2::Int)
|
||||||
|
|
||||||
|
-- The following won't type: unhandled exception!
|
||||||
|
-- ex2rw = run et2
|
||||||
|
{-
|
||||||
|
No instance for (Member (Exc Int) Void)
|
||||||
|
arising from a use of `et2'
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- The inferred type shows that ex21 is now pure
|
||||||
|
et21 :: Eff r (Either Int Int)
|
||||||
|
et21 = runError et2
|
||||||
|
|
||||||
|
et21r = Left 2 == run et21
|
||||||
|
|
||||||
|
|
||||||
|
-- The example from the paper
|
||||||
|
newtype TooBig = TooBig Int deriving (Eq, Show)
|
||||||
|
-- The type is inferred
|
||||||
|
ex2 :: Member (Exc TooBig) r => Eff r Int -> Eff r Int
|
||||||
|
ex2 m = do
|
||||||
|
v <- m
|
||||||
|
if v > 5 then throwError (TooBig v)
|
||||||
|
else return v
|
||||||
|
|
||||||
|
-- specialization to tell the type of the exception
|
||||||
|
runErrBig :: Eff (Exc TooBig ': r) a -> Eff r (Either TooBig a)
|
||||||
|
runErrBig = runError
|
||||||
|
|
||||||
|
|
||||||
|
-- exceptions and state
|
||||||
|
incr :: Member (State Int) r => Eff r ()
|
||||||
|
incr = get >>= put . (+ (1::Int))
|
||||||
|
|
||||||
|
tes1 :: (Member (State Int) r, Member (Exc [Char]) r) => Eff r b
|
||||||
|
tes1 = do
|
||||||
|
incr
|
||||||
|
throwError "exc"
|
||||||
|
|
||||||
|
ter1 :: Bool
|
||||||
|
ter1 = ((Left "exc" :: Either String Int,2) ==) $
|
||||||
|
run $ runState (runError tes1) (1::Int)
|
||||||
|
|
||||||
|
|
||||||
|
ter2 :: Bool
|
||||||
|
ter2 = ((Left "exc" :: Either String (Int,Int)) ==) $
|
||||||
|
run $ runError (runState tes1 (1::Int))
|
||||||
|
|
||||||
|
|
||||||
|
teCatch :: Member (Exc String) r => Eff r a -> Eff r [Char]
|
||||||
|
teCatch m = catchError (m >> return "done") (\e -> return (e::String))
|
||||||
|
|
||||||
|
ter3 :: Bool
|
||||||
|
ter3 = ((Right "exc" :: Either String String,2) ==) $
|
||||||
|
run $ runState (runError (teCatch tes1)) (1::Int)
|
||||||
|
|
||||||
|
ter4 :: Bool
|
||||||
|
ter4 = ((Right ("exc",2) :: Either String (String,Int)) ==) $
|
||||||
|
run $ runError (runState (teCatch tes1) (1::Int))
|
||||||
|
|
||||||
|
ex2r = runReader (runErrBig (ex2 ask)) (5::Int)
|
||||||
|
|
||||||
|
ex2rr = Right 5 == run ex2r
|
||||||
|
|
||||||
|
ex2rr1 = (Left (TooBig 7) ==) $
|
||||||
|
run $ runReader (runErrBig (ex2 ask)) (7::Int)
|
||||||
|
|
||||||
|
-- Different order of handlers (layers)
|
||||||
|
ex2rr2 = (Left (TooBig 7) ==) $
|
||||||
|
run $ runErrBig (runReader (ex2 ask) (7::Int))
|
42
src/Control/Monad/Freer/Fresh.hs
Normal file
42
src/Control/Monad/Freer/Fresh.hs
Normal file
@ -0,0 +1,42 @@
|
|||||||
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
module Control.Monad.Freer.Fresh (
|
||||||
|
Fresh,
|
||||||
|
fresh,
|
||||||
|
runFresh'
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Control.Monad.Freer.Internal
|
||||||
|
import Control.Monad.Freer.Trace -- for example
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Fresh --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
data Fresh v where
|
||||||
|
Fresh :: Fresh Int
|
||||||
|
|
||||||
|
fresh :: Member Fresh r => Eff r Int
|
||||||
|
fresh = send Fresh
|
||||||
|
|
||||||
|
-- And a handler for it
|
||||||
|
runFresh' :: Eff (Fresh ': r) w -> Int -> Eff r w
|
||||||
|
runFresh' m s =
|
||||||
|
handleRelayS s (\_s x -> return x)
|
||||||
|
(\s Fresh k -> (k $! s+1) s)
|
||||||
|
m
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Tests --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
tfresh' :: IO ()
|
||||||
|
tfresh' = runTrace $ flip runFresh' 0 $ do
|
||||||
|
n <- fresh
|
||||||
|
trace $ "Fresh " ++ show n
|
||||||
|
n <- fresh
|
||||||
|
trace $ "Fresh " ++ show n
|
||||||
|
{-
|
||||||
|
Fresh 0
|
||||||
|
Fresh 1
|
||||||
|
-}
|
566
src/Control/Monad/Freer/Internal.hs
Normal file
566
src/Control/Monad/Freer/Internal.hs
Normal file
@ -0,0 +1,566 @@
|
|||||||
|
{-# LANGUAGE CPP #-}
|
||||||
|
{-# LANGUAGE RankNTypes #-}
|
||||||
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE TypeFamilies #-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
{-# LANGUAGE ScopedTypeVariables #-}
|
||||||
|
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||||
|
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||||
|
|
||||||
|
-- The following is needed to define MonadPlus instance. It is decidable
|
||||||
|
-- (there is no recursion!), but GHC cannot see that.
|
||||||
|
{-# LANGUAGE UndecidableInstances #-}
|
||||||
|
|
||||||
|
module Control.Monad.Freer.Internal (
|
||||||
|
Eff(..),
|
||||||
|
Member(..),
|
||||||
|
Arr,
|
||||||
|
Arrs,
|
||||||
|
Union,
|
||||||
|
|
||||||
|
decomp,
|
||||||
|
tsingleton,
|
||||||
|
|
||||||
|
qApp,
|
||||||
|
qComp,
|
||||||
|
send,
|
||||||
|
run,
|
||||||
|
handleRelay,
|
||||||
|
handleRelayS,
|
||||||
|
interpose,
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Data.Open.Union
|
||||||
|
import Data.FTCQueue
|
||||||
|
|
||||||
|
|
||||||
|
-- The framework of extensible effects
|
||||||
|
|
||||||
|
-- ------------------------------------------------------------------------
|
||||||
|
-- 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
|
||||||
|
|
||||||
|
-- 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
|
||||||
|
-- It is NOT a Free monad! There are no Functor constraints
|
||||||
|
-- Status of a coroutine (client): done with the value of type w,
|
||||||
|
-- or sending a request of type Union r with the continuation
|
||||||
|
-- Arrs r b a.
|
||||||
|
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
|
||||||
|
qApp :: Arrs r b w -> b -> Eff r w
|
||||||
|
qApp q' x =
|
||||||
|
case tviewl q' of
|
||||||
|
TOne k -> k x
|
||||||
|
k :| t -> case k x of
|
||||||
|
Val y -> qApp t y
|
||||||
|
E u q -> E u (q >< t)
|
||||||
|
|
||||||
|
-- Compose effectful arrows (and possibly change the effect!)
|
||||||
|
qComp :: Arrs r a b -> (Eff r b -> Eff r' c) -> Arr r' a c
|
||||||
|
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
|
||||||
|
{-# INLINE pure #-}
|
||||||
|
{-# INLINE (<*>) #-}
|
||||||
|
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 (>>=) #-}
|
||||||
|
return = Val
|
||||||
|
Val x >>= k = k x
|
||||||
|
E u q >>= k = E u (q |> k) -- just accumulates continuations
|
||||||
|
|
||||||
|
|
||||||
|
-- send a request and wait for a reply
|
||||||
|
send :: Member t r => t v -> Eff r v
|
||||||
|
send t = E (inj t) (tsingleton Val)
|
||||||
|
|
||||||
|
-- ------------------------------------------------------------------------
|
||||||
|
-- The initial case, no effects
|
||||||
|
|
||||||
|
-- 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.
|
||||||
|
|
||||||
|
-- A convenient pattern: given a request (open union), either
|
||||||
|
-- handle it or relay it.
|
||||||
|
handleRelay :: (a -> Eff r w) ->
|
||||||
|
(forall v. t v -> Arr r v w -> Eff r w) ->
|
||||||
|
Eff (t ': r) a -> Eff r w
|
||||||
|
handleRelay ret h = loop
|
||||||
|
where
|
||||||
|
loop (Val x) = ret x
|
||||||
|
loop (E u' q) = case decomp u' of
|
||||||
|
Right x -> h x k
|
||||||
|
Left u -> E u (tsingleton k)
|
||||||
|
where k = qComp q loop
|
||||||
|
|
||||||
|
-- Parameterized handle_relay
|
||||||
|
handleRelayS :: 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
|
||||||
|
handleRelayS s' ret h = loop s'
|
||||||
|
where
|
||||||
|
loop s (Val x) = ret s x
|
||||||
|
loop s (E u' q) = case decomp u' of
|
||||||
|
Right x -> h s x k
|
||||||
|
Left u -> E u (tsingleton (k s))
|
||||||
|
where k s'' x = loop s'' $ qApp q x
|
||||||
|
|
||||||
|
-- Add something like Control.Exception.catches? It could be useful
|
||||||
|
-- for control with cut.
|
||||||
|
|
||||||
|
-- Intercept the request and possibly reply to it, but leave it unhandled
|
||||||
|
-- (that's why we use the same r all throuout)
|
||||||
|
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 = loop
|
||||||
|
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
|
||||||
|
|
||||||
|
{- EXAMPLE
|
||||||
|
rdwr :: (Member (Reader Int) r, Member (Writer String) r)
|
||||||
|
=> Eff r Int
|
||||||
|
rdwr = do
|
||||||
|
tell "begin"
|
||||||
|
r <- addN 10
|
||||||
|
tell "end"
|
||||||
|
return r
|
||||||
|
|
||||||
|
rdwrr :: (Int,[String])
|
||||||
|
rdwrr = run . (`runReader` (1::Int)) . runWriter $ rdwr
|
||||||
|
-- (10,["begin","end"])
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- Encapsulation of effects
|
||||||
|
-- The example suggested by a reviewer
|
||||||
|
|
||||||
|
{- The reviewer outlined an MTL implementation below, writing
|
||||||
|
``This hides the state effect and I can layer another state effect on
|
||||||
|
top without getting into conflict with the class system.''
|
||||||
|
|
||||||
|
class Monad m => MonadFresh m where
|
||||||
|
fresh :: m Int
|
||||||
|
|
||||||
|
newtype FreshT m a = FreshT { unFreshT :: State Int m a }
|
||||||
|
deriving (Functor, Monad, MonadTrans)
|
||||||
|
|
||||||
|
instance Monad m => MonadFresh (FreshT m) where
|
||||||
|
fresh = FreshT $ do n <- get; put (n+1); return n
|
||||||
|
|
||||||
|
See EncapsMTL.hs for the complete code.
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- There are three possible implementations
|
||||||
|
-- The first one uses State Fresh where
|
||||||
|
-- newtype Fresh = Fresh Int
|
||||||
|
-- We get the `private' effect layer (State Fresh) that does not interfere
|
||||||
|
-- with with other layers.
|
||||||
|
-- This is the easiest implementation.
|
||||||
|
|
||||||
|
-- The second implementation defines a new effect Fresh
|
||||||
|
|
||||||
|
{-
|
||||||
|
-- Finally, the worst implementation but the one that answers
|
||||||
|
-- reviewer's question: implementing Fresh in terms of State
|
||||||
|
-- but not revealing that fact.
|
||||||
|
|
||||||
|
runFresh :: Eff (Fresh :> r) w -> Int -> Eff r w
|
||||||
|
runFresh m s = runState m' s >>= return . fst
|
||||||
|
where
|
||||||
|
m' = loop m
|
||||||
|
loop (Val x) = return x
|
||||||
|
loop (E u q) = case decomp u of
|
||||||
|
Right Fresh -> do
|
||||||
|
n <- get
|
||||||
|
put (n+1::Int)
|
||||||
|
k n
|
||||||
|
Left u -> send (\k -> weaken $ fmap k u) >>= loop
|
||||||
|
|
||||||
|
tfresh = runTrace $ flip runFresh 0 $ do
|
||||||
|
n <- fresh
|
||||||
|
-- (x::Int) <- get
|
||||||
|
trace $ "Fresh " ++ show n
|
||||||
|
n <- fresh
|
||||||
|
trace $ "Fresh " ++ show n
|
||||||
|
|
||||||
|
{-
|
||||||
|
If we try to meddle with the encapsulated state, by uncommenting the
|
||||||
|
get statement above, we get:
|
||||||
|
No instance for (Member (State Int) Void)
|
||||||
|
arising from a use of `get'
|
||||||
|
-}
|
||||||
|
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- ------------------------------------------------------------------------
|
||||||
|
-- Lifting: emulating monad transformers
|
||||||
|
|
||||||
|
-- newtype Lift m a = Lift (m a)
|
||||||
|
|
||||||
|
|
||||||
|
{-
|
||||||
|
-- ------------------------------------------------------------------------
|
||||||
|
-- Co-routines
|
||||||
|
-- The interface is intentionally chosen to be the same as in transf.hs
|
||||||
|
|
||||||
|
-- The yield request: reporting the value of type a and suspending
|
||||||
|
-- the coroutine. Resuming with the value of type b
|
||||||
|
data Yield a b v = Yield a (b -> v)
|
||||||
|
deriving (Typeable, Functor)
|
||||||
|
|
||||||
|
-- The signature is inferred
|
||||||
|
yield :: (Typeable a, Typeable b, Member (Yield a b) r) => a -> Eff r b
|
||||||
|
yield x = send (inj . Yield x)
|
||||||
|
|
||||||
|
-- Status of a thread: done or reporting the value of the type a
|
||||||
|
-- and resuming with the value of type b
|
||||||
|
data Y r a b = Done | Y a (b -> Eff r (Y r a b))
|
||||||
|
|
||||||
|
-- Launch a thread and report its status
|
||||||
|
runC :: (Typeable a, Typeable b) =>
|
||||||
|
Eff (Yield a b :> r) w -> Eff r (Y r a b)
|
||||||
|
runC m = loop (admin m) where
|
||||||
|
loop (Val x) = return Done
|
||||||
|
loop (E u) = handle_relay u loop $
|
||||||
|
\(Yield x k) -> return (Y x (loop . k))
|
||||||
|
|
||||||
|
|
||||||
|
-- First example of coroutines
|
||||||
|
yieldInt :: Member (Yield Int ()) r => Int -> Eff r ()
|
||||||
|
yieldInt = yield
|
||||||
|
|
||||||
|
th1 :: Member (Yield Int ()) r => Eff r ()
|
||||||
|
th1 = yieldInt 1 >> yieldInt 2
|
||||||
|
|
||||||
|
|
||||||
|
c1 = runTrace (loop =<< runC th1)
|
||||||
|
where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
|
||||||
|
loop Done = trace "Done"
|
||||||
|
{-
|
||||||
|
1
|
||||||
|
2
|
||||||
|
Done
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- Add dynamic variables
|
||||||
|
-- The code is essentially the same as that in transf.hs (only added
|
||||||
|
-- a type specializtion on yield). The inferred signature is different though.
|
||||||
|
-- Before it was
|
||||||
|
-- th2 :: MonadReader Int m => CoT Int m ()
|
||||||
|
-- Now it is more general:
|
||||||
|
th2 :: (Member (Yield Int ()) r, Member (Reader Int) r) => Eff r ()
|
||||||
|
th2 = ask >>= yieldInt >> (ask >>= yieldInt)
|
||||||
|
|
||||||
|
|
||||||
|
-- Code is essentially the same as in transf.hs; no liftIO though
|
||||||
|
c2 = runTrace $ runReader (loop =<< runC th2) (10::Int)
|
||||||
|
where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
|
||||||
|
loop Done = trace "Done"
|
||||||
|
{-
|
||||||
|
10
|
||||||
|
10
|
||||||
|
Done
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- locally changing the dynamic environment for the suspension
|
||||||
|
c21 = runTrace $ runReader (loop =<< runC th2) (10::Int)
|
||||||
|
where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
|
||||||
|
loop Done = trace "Done"
|
||||||
|
{-
|
||||||
|
10
|
||||||
|
11
|
||||||
|
Done
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- Real example, with two sorts of local rebinding
|
||||||
|
th3 :: (Member (Yield Int ()) r, Member (Reader Int) r) => Eff r ()
|
||||||
|
th3 = ay >> ay >> local (+(10::Int)) (ay >> ay)
|
||||||
|
where ay = ask >>= yieldInt
|
||||||
|
|
||||||
|
c3 = runTrace $ runReader (loop =<< runC th3) (10::Int)
|
||||||
|
where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
|
||||||
|
loop Done = trace "Done"
|
||||||
|
{-
|
||||||
|
10
|
||||||
|
10
|
||||||
|
20
|
||||||
|
20
|
||||||
|
Done
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- locally changing the dynamic environment for the suspension
|
||||||
|
c31 = runTrace $ runReader (loop =<< runC th3) (10::Int)
|
||||||
|
where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
|
||||||
|
loop Done = trace "Done"
|
||||||
|
{-
|
||||||
|
10
|
||||||
|
11
|
||||||
|
21
|
||||||
|
21
|
||||||
|
Done
|
||||||
|
-}
|
||||||
|
-- The result is exactly as expected and desired: the coroutine shares the
|
||||||
|
-- dynamic environment with its parent; however, when the environment
|
||||||
|
-- is locally rebound, it becomes private to coroutine.
|
||||||
|
|
||||||
|
-- We now make explicit that the client computation, run by th4,
|
||||||
|
-- is abstract. We abstract it out of th4
|
||||||
|
c4 = runTrace $ runReader (loop =<< runC (th4 client)) (10::Int)
|
||||||
|
where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
|
||||||
|
loop Done = trace "Done"
|
||||||
|
|
||||||
|
-- cl, client, ay are monomorphic bindings
|
||||||
|
th4 cl = cl >> local (+(10::Int)) cl
|
||||||
|
client = ay >> ay
|
||||||
|
ay = ask >>= yieldInt
|
||||||
|
|
||||||
|
{-
|
||||||
|
10
|
||||||
|
11
|
||||||
|
21
|
||||||
|
21
|
||||||
|
Done
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- Even more dynamic example
|
||||||
|
c5 = runTrace $ runReader (loop =<< runC (th client)) (10::Int)
|
||||||
|
where loop (Y x k) = trace (show (x::Int)) >> local (\y->x+1) (k ()) >>= loop
|
||||||
|
loop Done = trace "Done"
|
||||||
|
|
||||||
|
-- cl, client, ay are monomorphic bindings
|
||||||
|
client = ay >> ay >> ay
|
||||||
|
ay = ask >>= yieldInt
|
||||||
|
|
||||||
|
-- There is no polymorphic recursion here
|
||||||
|
th cl = do
|
||||||
|
cl
|
||||||
|
v <- ask
|
||||||
|
(if v > (20::Int) then id else local (+(5::Int))) cl
|
||||||
|
if v > (20::Int) then return () else local (+(10::Int)) (th cl)
|
||||||
|
{-
|
||||||
|
10
|
||||||
|
11
|
||||||
|
12
|
||||||
|
18
|
||||||
|
18
|
||||||
|
18
|
||||||
|
29
|
||||||
|
29
|
||||||
|
29
|
||||||
|
29
|
||||||
|
29
|
||||||
|
29
|
||||||
|
Done
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- And even more
|
||||||
|
c7 = runTrace $
|
||||||
|
runReader (runReader (loop =<< runC (th client)) (10::Int)) (1000::Double)
|
||||||
|
where loop (Y x k) = trace (show (x::Int)) >>
|
||||||
|
local (\y->fromIntegral (x+1)::Double) (k ()) >>= loop
|
||||||
|
loop Done = trace "Done"
|
||||||
|
|
||||||
|
-- cl, client, ay are monomorphic bindings
|
||||||
|
client = ay >> ay >> ay
|
||||||
|
ay = ask >>= \x -> ask >>=
|
||||||
|
\y -> yieldInt (x + round (y::Double))
|
||||||
|
|
||||||
|
-- There is no polymorphic recursion here
|
||||||
|
th cl = do
|
||||||
|
cl
|
||||||
|
v <- ask
|
||||||
|
(if v > (20::Int) then id else local (+(5::Int))) cl
|
||||||
|
if v > (20::Int) then return () else local (+(10::Int)) (th cl)
|
||||||
|
|
||||||
|
{-
|
||||||
|
1010
|
||||||
|
1021
|
||||||
|
1032
|
||||||
|
1048
|
||||||
|
1064
|
||||||
|
1080
|
||||||
|
1101
|
||||||
|
1122
|
||||||
|
1143
|
||||||
|
1169
|
||||||
|
1195
|
||||||
|
1221
|
||||||
|
1252
|
||||||
|
1283
|
||||||
|
1314
|
||||||
|
1345
|
||||||
|
1376
|
||||||
|
1407
|
||||||
|
Done
|
||||||
|
-}
|
||||||
|
|
||||||
|
c7' = runTrace $
|
||||||
|
runReader (runReader (loop =<< runC (th client)) (10::Int)) (1000::Double)
|
||||||
|
where loop (Y x k) = trace (show (x::Int)) >>
|
||||||
|
local (\y->fromIntegral (x+1)::Double) (k ()) >>= loop
|
||||||
|
loop Done = trace "Done"
|
||||||
|
|
||||||
|
-- cl, client, ay are monomorphic bindings
|
||||||
|
client = ay >> ay >> ay
|
||||||
|
ay = ask >>= \x -> ask >>=
|
||||||
|
\y -> yieldInt (x + round (y::Double))
|
||||||
|
|
||||||
|
-- There is no polymorphic recursion here
|
||||||
|
th cl = do
|
||||||
|
cl
|
||||||
|
v <- ask
|
||||||
|
(if v > (20::Int) then id else local (+(5::Double))) cl
|
||||||
|
if v > (20::Int) then return () else local (+(10::Int)) (th cl)
|
||||||
|
{-
|
||||||
|
1010
|
||||||
|
1021
|
||||||
|
1032
|
||||||
|
1048
|
||||||
|
1048
|
||||||
|
1048
|
||||||
|
1069
|
||||||
|
1090
|
||||||
|
1111
|
||||||
|
1137
|
||||||
|
1137
|
||||||
|
1137
|
||||||
|
1168
|
||||||
|
1199
|
||||||
|
1230
|
||||||
|
1261
|
||||||
|
1292
|
||||||
|
1323
|
||||||
|
Done
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- ------------------------------------------------------------------------
|
||||||
|
-- An example of non-trivial interaction of effects, handling of two
|
||||||
|
-- effects together
|
||||||
|
-- Non-determinism with control (cut)
|
||||||
|
-- For the explanation of cut, see Section 5 of Hinze ICFP 2000 paper.
|
||||||
|
-- Hinze suggests expressing cut in terms of cutfalse
|
||||||
|
-- ! = return () `mplus` cutfalse
|
||||||
|
-- where
|
||||||
|
-- cutfalse :: m a
|
||||||
|
-- satisfies the following laws
|
||||||
|
-- cutfalse >>= k = cutfalse (F1)
|
||||||
|
-- cutfalse | m = cutfalse (F2)
|
||||||
|
-- (note: m `mplus` cutfalse is different from cutfalse `mplus` m)
|
||||||
|
-- In other words, cutfalse is the left zero of both bind and mplus.
|
||||||
|
--
|
||||||
|
-- Hinze also introduces the operation call :: m a -> m a that
|
||||||
|
-- delimits the effect of cut: call m executes m. If the cut is
|
||||||
|
-- invoked in m, it discards only the choices made since m was called.
|
||||||
|
-- Hinze postulates the axioms of call:
|
||||||
|
--
|
||||||
|
-- call false = false (C1)
|
||||||
|
-- call (return a | m) = return a | call m (C2)
|
||||||
|
-- call (m | cutfalse) = call m (C3)
|
||||||
|
-- call (lift m >>= k) = lift m >>= (call . k) (C4)
|
||||||
|
--
|
||||||
|
-- call m behaves like m except any cut inside m has only a local effect,
|
||||||
|
-- he says.
|
||||||
|
|
||||||
|
-- Hinze noted a problem with the `mechanical' derivation of backtracing
|
||||||
|
-- monad transformer with cut: no axiom specifying the interaction of
|
||||||
|
-- call with bind; no way to simplify nested invocations of call.
|
||||||
|
|
||||||
|
-- We use exceptions for cutfalse
|
||||||
|
-- Therefore, the law ``cutfalse >>= k = cutfalse''
|
||||||
|
-- is satisfied automatically since all exceptions have the above property.
|
||||||
|
|
||||||
|
data CutFalse = CutFalse deriving Typeable
|
||||||
|
|
||||||
|
cutfalse = throwError CutFalse
|
||||||
|
|
||||||
|
-- The interpreter -- it is like reify . reflect with a twist
|
||||||
|
-- Compare this implementation with the huge implementation of call
|
||||||
|
-- in Hinze 2000 (Figure 9)
|
||||||
|
-- Each clause corresponds to the axiom of call or cutfalse.
|
||||||
|
-- All axioms are covered.
|
||||||
|
-- The code clearly expresses the intuition that call watches the choice points
|
||||||
|
-- of its argument computation. When it encounteres a cutfalse request,
|
||||||
|
-- it discards the remaining choicepoints.
|
||||||
|
|
||||||
|
-- It completely handles CutFalse effects but not non-determinism
|
||||||
|
call :: Member Choose r => Eff (Exc CutFalse :> r) a -> Eff r a
|
||||||
|
call m = loop [] (admin m) where
|
||||||
|
loop jq (Val x) = return x `mplus'` next jq -- (C2)
|
||||||
|
loop jq (E u) = case decomp u of
|
||||||
|
Right (Exc CutFalse) -> mzero' -- drop jq (F2)
|
||||||
|
Left u -> check jq u
|
||||||
|
|
||||||
|
check jq u | Just (Choose [] _) <- prj u = next jq -- (C1)
|
||||||
|
check jq u | Just (Choose [x] k) <- prj u = loop jq (k x) -- (C3), optim
|
||||||
|
check jq u | Just (Choose lst k) <- prj u = next $ map k lst ++ jq -- (C3)
|
||||||
|
check jq u = send (\k -> fmap k u) >>= loop jq -- (C4)
|
||||||
|
|
||||||
|
next [] = mzero'
|
||||||
|
next (h:t) = loop t h
|
||||||
|
|
||||||
|
-- The signature is inferred
|
||||||
|
tcut1 :: (Member Choose r, Member (Exc CutFalse) r) => Eff r Int
|
||||||
|
tcut1 = (return (1::Int) `mplus'` return 2) `mplus'`
|
||||||
|
((cutfalse `mplus'` return 4) `mplus'`
|
||||||
|
return 5)
|
||||||
|
|
||||||
|
tcut1r = run . makeChoice $ call tcut1
|
||||||
|
-- [1,2]
|
||||||
|
|
||||||
|
tcut2 = return (1::Int) `mplus'`
|
||||||
|
call (return 2 `mplus'` (cutfalse `mplus'` return 3) `mplus'`
|
||||||
|
return 4)
|
||||||
|
`mplus'` return 5
|
||||||
|
|
||||||
|
-- Here we see nested call. It poses no problems...
|
||||||
|
tcut2r = run . makeChoice $ call tcut2
|
||||||
|
-- [1,2,5]
|
||||||
|
|
||||||
|
-- More nested calls
|
||||||
|
tcut3 = call tcut1 `mplus'` call (tcut2 `mplus'` cutfalse)
|
||||||
|
tcut3r = run . makeChoice $ call tcut3
|
||||||
|
-- [1,2,1,2,5]
|
||||||
|
|
||||||
|
tcut4 = call tcut1 `mplus'` (tcut2 `mplus'` cutfalse)
|
||||||
|
tcut4r = run . makeChoice $ call tcut4
|
||||||
|
-- [1,2,1,2,5]
|
||||||
|
-}
|
150
src/Control/Monad/Freer/Reader.hs
Normal file
150
src/Control/Monad/Freer/Reader.hs
Normal file
@ -0,0 +1,150 @@
|
|||||||
|
{-# LANGUAGE RankNTypes #-}
|
||||||
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
{-# LANGUAGE ScopedTypeVariables #-}
|
||||||
|
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||||
|
module Control.Monad.Freer.Reader (
|
||||||
|
Reader(..),
|
||||||
|
|
||||||
|
ask,
|
||||||
|
runReader',
|
||||||
|
runReader,
|
||||||
|
local
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Control.Applicative
|
||||||
|
import Control.Monad.Freer.Internal
|
||||||
|
|
||||||
|
-- ------------------------------------------------------------------------
|
||||||
|
-- The Reader monad
|
||||||
|
|
||||||
|
-- The request for a value of type e from the current environment
|
||||||
|
-- This is a GADT because the type of values
|
||||||
|
-- returned in response to a (Reader e a) request is not any a;
|
||||||
|
-- we expect in reply the value of type 'e', the value from the
|
||||||
|
-- environment. So, the return type is restricted: 'a ~ e'
|
||||||
|
data Reader e v where
|
||||||
|
Reader :: Reader e e
|
||||||
|
|
||||||
|
-- One can also define this as
|
||||||
|
-- data Reader e v = (e ~ v) => Reader
|
||||||
|
-- and even without GADTs, using explicit coercion:
|
||||||
|
-- newtype Reader e v = Reader (e->v)
|
||||||
|
-- In the latter case, when we make the request, we make it as Reader id.
|
||||||
|
-- So, strictly speaking, GADTs are not really necessary.
|
||||||
|
|
||||||
|
|
||||||
|
-- The signature is inferred
|
||||||
|
ask :: (Member (Reader e) r) => Eff r e
|
||||||
|
ask = send Reader
|
||||||
|
|
||||||
|
-- The handler of Reader requests. The return type shows that
|
||||||
|
-- all Reader requests are fully handled.
|
||||||
|
runReader' :: Eff (Reader e ': r) w -> e -> Eff r w
|
||||||
|
runReader' m e = loop m where
|
||||||
|
loop (Val x) = return x
|
||||||
|
loop (E u' q) = case decomp u' of
|
||||||
|
Right Reader -> loop $ qApp q e
|
||||||
|
Left u -> E u (tsingleton (qComp q loop))
|
||||||
|
|
||||||
|
-- A different way of writing the above
|
||||||
|
runReader :: Eff (Reader e ': r) w -> e -> Eff r w
|
||||||
|
runReader m e = handleRelay return (\Reader k -> k e) m
|
||||||
|
|
||||||
|
-- Locally rebind the value in the dynamic environment
|
||||||
|
-- This function is like a relay; it is both an admin for Reader requests,
|
||||||
|
-- and a requestor of them
|
||||||
|
local :: forall e a r. Member (Reader e) r =>
|
||||||
|
(e -> e) -> Eff r a -> Eff r a
|
||||||
|
local f m = do
|
||||||
|
e0 <- ask
|
||||||
|
let e = f e0
|
||||||
|
-- Local signature is needed, as always with GADTs
|
||||||
|
let h :: Reader e v -> Arr r v a -> Eff r a
|
||||||
|
h Reader g = g e
|
||||||
|
interpose return h m
|
||||||
|
|
||||||
|
|
||||||
|
-- Examples
|
||||||
|
add :: Applicative f => f Int -> f Int -> f Int
|
||||||
|
add = liftA2 (+)
|
||||||
|
|
||||||
|
|
||||||
|
-- The type is inferred
|
||||||
|
t1 :: Member (Reader Int) r => Eff r Int
|
||||||
|
t1 = ask `add` return (1 :: Int)
|
||||||
|
|
||||||
|
t1' :: Member (Reader Int) r => Eff r Int
|
||||||
|
t1' = do v <- ask; return (v + 1 :: Int)
|
||||||
|
|
||||||
|
-- t1r :: Eff r Int
|
||||||
|
t1r = runReader t1 (10::Int)
|
||||||
|
|
||||||
|
t1rr = 11 == run t1r
|
||||||
|
|
||||||
|
{-
|
||||||
|
t1rr' = run t1
|
||||||
|
No instance for (Member (Reader Int) Void)
|
||||||
|
arising from a use of `t1'
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- Inferred type
|
||||||
|
-- t2 :: (Member (Reader Int) r, Member (Reader Float) r) => Eff r Float
|
||||||
|
t2 = do
|
||||||
|
v1 <- ask
|
||||||
|
v2 <- ask
|
||||||
|
return $ fromIntegral (v1 + (1::Int)) + (v2 + (2::Float))
|
||||||
|
|
||||||
|
-- t2r :: Member (Reader Float) r => Eff r Float
|
||||||
|
t2r = runReader t2 (10::Int)
|
||||||
|
-- t2rr :: Eff r Float
|
||||||
|
t2rr = flip runReader (20::Float) . flip runReader (10::Int) $ t2
|
||||||
|
|
||||||
|
t2rrr = 33.0 == run t2rr
|
||||||
|
|
||||||
|
-- The opposite order of layers
|
||||||
|
{- If we mess up, we get an error
|
||||||
|
t2rrr1' = run $ runReader (runReader t2 (20::Float)) (10::Float)
|
||||||
|
No instance for (Member (Reader Int) [])
|
||||||
|
arising from a use of `t2'
|
||||||
|
-}
|
||||||
|
t2rrr' = (33.0 ==) $
|
||||||
|
run $ runReader (runReader t2 (20 :: Float)) (10 :: Int)
|
||||||
|
|
||||||
|
-- The type is inferred
|
||||||
|
t3 :: Member (Reader Int) r => Eff r Int
|
||||||
|
t3 = t1 `add` local (+ (10::Int)) t1
|
||||||
|
t3r = (212 ==) $ run $ runReader t3 (100::Int)
|
||||||
|
|
||||||
|
|
||||||
|
-- The following example demonstrates true interleaving of Reader Int
|
||||||
|
-- and Reader Float layers
|
||||||
|
{-
|
||||||
|
t4
|
||||||
|
:: (Member (Reader Int) r, Member (Reader Float) r) =>
|
||||||
|
() -> Eff r Float
|
||||||
|
-}
|
||||||
|
t4 = liftA2 (+) (local (+ (10::Int)) t2)
|
||||||
|
(local (+ (30::Float)) t2)
|
||||||
|
|
||||||
|
t4rr = (106.0 ==) $ run $ runReader (runReader t4 (10::Int)) (20::Float)
|
||||||
|
|
||||||
|
-- The opposite order of layers gives the same result
|
||||||
|
t4rr' = (106.0 ==) $ run $ runReader (runReader t4 (20 :: Float)) (10 :: Int)
|
||||||
|
|
||||||
|
addGet :: Member (Reader Int) r => Int -> Eff r Int
|
||||||
|
addGet x = ask >>= \i -> return (i+x)
|
||||||
|
|
||||||
|
addN n = foldl (>>>) return (replicate n addGet) 0
|
||||||
|
where f >>> g = (>>= g) . f
|
||||||
|
|
||||||
|
-- Map an effectful function
|
||||||
|
-- The type is inferred
|
||||||
|
tmap :: Member (Reader Int) r => Eff r [Int]
|
||||||
|
tmap = mapM f [1..5]
|
||||||
|
where f x = ask `add` return x
|
||||||
|
|
||||||
|
tmapr = ([11,12,13,14,15] ==) $
|
||||||
|
run $ runReader tmap (10::Int)
|
97
src/Control/Monad/Freer/State.hs
Normal file
97
src/Control/Monad/Freer/State.hs
Normal file
@ -0,0 +1,97 @@
|
|||||||
|
{-# LANGUAGE RankNTypes #-}
|
||||||
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE ScopedTypeVariables #-}
|
||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
|
module Control.Monad.Freer.State (
|
||||||
|
State,
|
||||||
|
get,
|
||||||
|
put,
|
||||||
|
runState',
|
||||||
|
runState,
|
||||||
|
transactionState
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Control.Monad.Freer.Internal
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- State, strict --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
{- Initial design:
|
||||||
|
-- The state request carries with it the state mutator function
|
||||||
|
-- We can use this request both for mutating and getting the state.
|
||||||
|
-- But see below for a better design!
|
||||||
|
data State s v where
|
||||||
|
State :: (s->s) -> State s s
|
||||||
|
|
||||||
|
In this old design, we have assumed that the dominant operation is
|
||||||
|
modify. Perhaps this is not wise. Often, the reader is most nominant.
|
||||||
|
-}
|
||||||
|
-- See also below, for decomposing the State into Reader and Writer!
|
||||||
|
|
||||||
|
-- The conventional design of State
|
||||||
|
data State s v where
|
||||||
|
Get :: State s s
|
||||||
|
Put :: !s -> State s ()
|
||||||
|
|
||||||
|
-- The signatures are inferred
|
||||||
|
get :: Member (State s) r => Eff r s
|
||||||
|
get = send Get
|
||||||
|
|
||||||
|
put :: Member (State s) r => s -> Eff r ()
|
||||||
|
put s = send (Put s)
|
||||||
|
|
||||||
|
runState' :: Eff (State s ': r) w -> s -> Eff r (w,s)
|
||||||
|
runState' m s =
|
||||||
|
handleRelayS s (\s x -> return (x,s))
|
||||||
|
(\s sreq k -> case sreq of
|
||||||
|
Get -> k s s
|
||||||
|
Put s' -> k s' ())
|
||||||
|
m
|
||||||
|
|
||||||
|
-- Since State is so frequently used, we optimize it a bit
|
||||||
|
runState :: Eff (State s ': r) w -> s -> Eff r (w,s)
|
||||||
|
runState (Val x) s = return (x,s)
|
||||||
|
runState (E u q) s = case decomp u of
|
||||||
|
Right Get -> runState (qApp q s) s
|
||||||
|
Right (Put s) -> runState (qApp q ()) s
|
||||||
|
Left u -> E u (tsingleton (\x -> runState (qApp q x) s))
|
||||||
|
|
||||||
|
|
||||||
|
-- An encapsulated State handler, for transactional semantics
|
||||||
|
-- The global state is updated only if the transactionState finished
|
||||||
|
-- successfully
|
||||||
|
data ProxyState s = ProxyState
|
||||||
|
transactionState :: forall s r w. Member (State s) r =>
|
||||||
|
ProxyState s -> Eff r w -> Eff r w
|
||||||
|
transactionState _ m = do s <- get; loop s m
|
||||||
|
where
|
||||||
|
loop :: s -> Eff r w -> Eff r w
|
||||||
|
loop s (Val x) = put s >> return x
|
||||||
|
loop s (E (u :: Union r b) q) = case prj u :: Maybe (State s b) of
|
||||||
|
Just Get -> loop s (qApp q s)
|
||||||
|
Just (Put s') -> loop s'(qApp q ())
|
||||||
|
_ -> E u (tsingleton k) where k = qComp q (loop s)
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Tests and Examples --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
ts1 :: Member (State Int) r => Eff r Int
|
||||||
|
ts1 = do
|
||||||
|
put (10 ::Int)
|
||||||
|
x <- get
|
||||||
|
return (x::Int)
|
||||||
|
|
||||||
|
ts1r = ((10,10) ==) $ run (runState ts1 (0::Int))
|
||||||
|
|
||||||
|
ts2 :: Member (State Int) r => Eff r Int
|
||||||
|
ts2 = do
|
||||||
|
put (10::Int)
|
||||||
|
x <- get
|
||||||
|
put (20::Int)
|
||||||
|
y <- get
|
||||||
|
return (x+y)
|
||||||
|
|
||||||
|
ts2r = ((30,20) ==) $ run (runState ts2 (0::Int))
|
58
src/Control/Monad/Freer/StateRW.hs
Normal file
58
src/Control/Monad/Freer/StateRW.hs
Normal file
@ -0,0 +1,58 @@
|
|||||||
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
module Control.Monad.Freer.StateRW (
|
||||||
|
runStateR
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Control.Monad.Freer.Reader
|
||||||
|
import Control.Monad.Freer.Writer
|
||||||
|
import Control.Monad.Freer.Internal
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- State: Using Reader and Writer --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- A different representation of State: decomposing State into
|
||||||
|
-- mutation (Writer) and Reading. We don't define any new effects:
|
||||||
|
-- we just handle the existing ones.
|
||||||
|
-- Thus we define a handler for two effects together.
|
||||||
|
|
||||||
|
runStateR :: Eff (Writer s ': Reader s ': r) w -> s -> Eff r (w,s)
|
||||||
|
runStateR m s = loop s m
|
||||||
|
where
|
||||||
|
loop :: s -> Eff (Writer s ': Reader s ': r) w -> Eff r (w,s)
|
||||||
|
loop s (Val x) = return (x,s)
|
||||||
|
loop s (E u q) = case decomp u of
|
||||||
|
Right (Writer o) -> k o ()
|
||||||
|
Left u -> case decomp u of
|
||||||
|
Right Reader -> k s s
|
||||||
|
Left u -> E u (tsingleton (k s))
|
||||||
|
where k s = qComp q (loop s)
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Tests and Examples --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- If we had a Writer, we could have decomposed State into Writer and Reader
|
||||||
|
-- requests.
|
||||||
|
|
||||||
|
ts11 :: (Member (Reader Int) r, Member (Writer Int) r) => Eff r Int
|
||||||
|
ts11 = do
|
||||||
|
tell (10 ::Int)
|
||||||
|
x <- ask
|
||||||
|
return (x::Int)
|
||||||
|
|
||||||
|
ts11r :: Bool
|
||||||
|
ts11r = ((10,10) ==) $ run (runStateR ts11 (0::Int))
|
||||||
|
|
||||||
|
|
||||||
|
ts21 :: (Member (Reader Int) r, Member (Writer Int) r) => Eff r Int
|
||||||
|
ts21 = do
|
||||||
|
tell (10::Int)
|
||||||
|
x <- ask
|
||||||
|
tell (20::Int)
|
||||||
|
y <- ask
|
||||||
|
return (x+y)
|
||||||
|
|
||||||
|
ts21r :: Bool
|
||||||
|
ts21r = ((30,20) ==) $ run (runStateR ts21 (0::Int))
|
75
src/Control/Monad/Freer/Trace.hs
Normal file
75
src/Control/Monad/Freer/Trace.hs
Normal file
@ -0,0 +1,75 @@
|
|||||||
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||||
|
module Control.Monad.Freer.Trace (
|
||||||
|
Trace,
|
||||||
|
trace,
|
||||||
|
runTrace
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Control.Monad
|
||||||
|
import Control.Monad.Freer.Internal
|
||||||
|
import Control.Monad.Freer.Reader -- for examples
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Tracing (debug printing) --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
data Trace v where
|
||||||
|
Trace :: String -> Trace ()
|
||||||
|
|
||||||
|
-- Printing a string in a trace
|
||||||
|
trace :: Member Trace r => String -> Eff r ()
|
||||||
|
trace = send . Trace
|
||||||
|
|
||||||
|
-- The handler for IO request: a terminal handler
|
||||||
|
runTrace :: Eff '[Trace] w -> IO w
|
||||||
|
runTrace (Val x) = return x
|
||||||
|
runTrace (E u q) = case decomp u of
|
||||||
|
Right (Trace s) -> putStrLn s >> runTrace (qApp q ())
|
||||||
|
-- Nothing more can occur
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Tests and Examples --
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Higher-order effectful function
|
||||||
|
-- The inferred type shows that the Trace affect is added to the effects
|
||||||
|
-- of r
|
||||||
|
mapMdebug:: (Show a, Member Trace r) =>
|
||||||
|
(a -> Eff r b) -> [a] -> Eff r [b]
|
||||||
|
mapMdebug f [] = return []
|
||||||
|
mapMdebug f (h:t) = do
|
||||||
|
trace $ "mapMdebug: " ++ show h
|
||||||
|
h' <- f h
|
||||||
|
t' <- mapMdebug f t
|
||||||
|
return (h':t')
|
||||||
|
|
||||||
|
add = liftM2 (+)
|
||||||
|
|
||||||
|
tMd :: IO [Int]
|
||||||
|
tMd = runTrace $ runReader (mapMdebug f [1..5]) (10::Int)
|
||||||
|
where f x = ask `add` return x
|
||||||
|
{-
|
||||||
|
mapMdebug: 1
|
||||||
|
mapMdebug: 2
|
||||||
|
mapMdebug: 3
|
||||||
|
mapMdebug: 4
|
||||||
|
mapMdebug: 5
|
||||||
|
[11,12,13,14,15]
|
||||||
|
-}
|
||||||
|
|
||||||
|
-- duplicate layers
|
||||||
|
tdup :: IO ()
|
||||||
|
tdup = runTrace $ runReader m (10::Int)
|
||||||
|
where
|
||||||
|
m = do
|
||||||
|
runReader tr (20::Int)
|
||||||
|
tr
|
||||||
|
tr = do
|
||||||
|
v <- ask
|
||||||
|
trace $ "Asked: " ++ show (v::Int)
|
||||||
|
{-
|
||||||
|
Asked: 20
|
||||||
|
Asked: 10
|
||||||
|
-}
|
33
src/Control/Monad/Freer/Writer.hs
Normal file
33
src/Control/Monad/Freer/Writer.hs
Normal file
@ -0,0 +1,33 @@
|
|||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
module Control.Monad.Freer.Writer (
|
||||||
|
Writer(..),
|
||||||
|
tell,
|
||||||
|
runWriter
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Control.Monad.Freer.Internal
|
||||||
|
|
||||||
|
-- ------------------------------------------------------------------------
|
||||||
|
-- The Writer monad
|
||||||
|
|
||||||
|
-- In MTL's Writer monad, the told value must have a |Monoid| type. Our
|
||||||
|
-- writer has no such constraints. If we write a |Writer|-like
|
||||||
|
-- interpreter to accumulate the told values in a monoid, it will have
|
||||||
|
-- the |Monoid o| constraint then
|
||||||
|
|
||||||
|
data Writer o x where
|
||||||
|
Writer :: o -> Writer o ()
|
||||||
|
|
||||||
|
tell :: Member (Writer o) r => o -> Eff r ()
|
||||||
|
tell o = send $ Writer o
|
||||||
|
|
||||||
|
-- We accumulate the told data in a list, hence no Monoid constraints
|
||||||
|
-- The code is written to be simple, not optimized.
|
||||||
|
-- If performance matters, we should convert it to accumulator
|
||||||
|
|
||||||
|
runWriter :: Eff (Writer o ': r) a -> Eff r (a,[o])
|
||||||
|
runWriter = handleRelay (\x -> return (x,[]))
|
||||||
|
(\ (Writer o) k -> k () >>= \ (x,l) -> return (x,o:l))
|
62
src/Data/FTCQueue.hs
Normal file
62
src/Data/FTCQueue.hs
Normal file
@ -0,0 +1,62 @@
|
|||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
|
||||||
|
-- A repackaging of: http://okmij.org/ftp/Haskell/extensible/FTCQueue1.hs
|
||||||
|
module Data.FTCQueue (
|
||||||
|
FTCQueue,
|
||||||
|
tsingleton,
|
||||||
|
(|>),
|
||||||
|
snoc,
|
||||||
|
(><),
|
||||||
|
append,
|
||||||
|
ViewL(..),
|
||||||
|
tviewl
|
||||||
|
) where
|
||||||
|
|
||||||
|
-- Fast type-aligned queue optimized to effectful functions
|
||||||
|
-- (a -> m b)
|
||||||
|
-- (monad continuations have this type).
|
||||||
|
-- Constant-time append and snoc and
|
||||||
|
-- average constant-time left-edge deconstruction
|
||||||
|
|
||||||
|
-- Non-empty tree. Deconstruction operations make it more and more
|
||||||
|
-- left-leaning
|
||||||
|
data FTCQueue m a b where
|
||||||
|
Leaf :: (a -> m b) -> FTCQueue m a b
|
||||||
|
Node :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
|
||||||
|
|
||||||
|
|
||||||
|
-- Exported operations
|
||||||
|
|
||||||
|
-- There is no tempty: use (tsingleton return), which works just the same.
|
||||||
|
-- The names are chosen for compatibility with FastTCQueue
|
||||||
|
|
||||||
|
-- tempty = tsingleton return
|
||||||
|
|
||||||
|
{-# INLINE tsingleton #-}
|
||||||
|
tsingleton :: (a -> m b) -> FTCQueue m a b
|
||||||
|
tsingleton r = Leaf r
|
||||||
|
|
||||||
|
{-# INLINE (|>) #-}
|
||||||
|
(|>) :: FTCQueue m a x -> (x -> m b) -> FTCQueue m a b
|
||||||
|
snoc :: FTCQueue m a x -> (x -> m b) -> FTCQueue m a b
|
||||||
|
t |> r = Node t (Leaf r)
|
||||||
|
snoc = (|>)
|
||||||
|
|
||||||
|
{-# INLINE (><) #-}
|
||||||
|
(><) :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
|
||||||
|
append :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
|
||||||
|
t1 >< t2 = Node t1 t2
|
||||||
|
append = (><)
|
||||||
|
|
||||||
|
-- Left-edge deconstruction
|
||||||
|
data ViewL m a b where
|
||||||
|
TOne :: (a -> m b) -> ViewL m a b
|
||||||
|
(:|) :: (a -> m x) -> (FTCQueue m x b) -> ViewL m a b
|
||||||
|
|
||||||
|
tviewl :: FTCQueue m a b -> ViewL m a b
|
||||||
|
tviewl (Leaf r) = TOne r
|
||||||
|
tviewl (Node t1 t2) = go t1 t2
|
||||||
|
where
|
||||||
|
go :: FTCQueue m a x -> FTCQueue m x b -> ViewL m a b
|
||||||
|
go (Leaf r) tr = r :| tr
|
||||||
|
go (Node tl1 tl2) tr = go tl1 (Node tl2 tr)
|
91
src/Data/Open/Union.hs
Normal file
91
src/Data/Open/Union.hs
Normal file
@ -0,0 +1,91 @@
|
|||||||
|
{-# LANGUAGE TypeOperators #-}
|
||||||
|
{-# LANGUAGE GADTs #-}
|
||||||
|
{-# LANGUAGE TypeFamilies #-}
|
||||||
|
{-# LANGUAGE DataKinds, PolyKinds #-}
|
||||||
|
{-# LANGUAGE ConstraintKinds #-}
|
||||||
|
{-# LANGUAGE ScopedTypeVariables #-}
|
||||||
|
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
|
||||||
|
{-# LANGUAGE UndecidableInstances #-}
|
||||||
|
|
||||||
|
-- repackaging of: http://okmij.org/ftp/Haskell/extensible/OpenUnion41.hs
|
||||||
|
module Data.Open.Union (
|
||||||
|
Union(..),
|
||||||
|
decomp,
|
||||||
|
weaken,
|
||||||
|
Member(..)
|
||||||
|
) where
|
||||||
|
|
||||||
|
|
||||||
|
-- Open unions (type-indexed co-products) for extensible effects
|
||||||
|
-- This implementation relies on _closed_ type families added
|
||||||
|
-- to GHC 7.8
|
||||||
|
-- It has NO overlapping instances and NO Typeable
|
||||||
|
-- Alas, the absence of Typeable means the projections and injections
|
||||||
|
-- generally take linear time.
|
||||||
|
-- The code illustrate how to use closed type families to
|
||||||
|
-- disambiguate otherwise overlapping instances.
|
||||||
|
|
||||||
|
-- The interface is the same as of other OpenUnion*.hs
|
||||||
|
|
||||||
|
-- The data constructors of Union are not exported
|
||||||
|
|
||||||
|
-- Essentially, the nested Either data type
|
||||||
|
-- t is can be a GADT and hence not necessarily a Functor
|
||||||
|
data Union (r :: [ * -> * ]) v where
|
||||||
|
UNow :: t v -> Union (t ': r) v
|
||||||
|
UNext :: Union r v -> Union (any ': r) v
|
||||||
|
|
||||||
|
{-
|
||||||
|
instance Functor (Union r) where
|
||||||
|
{-# INLINE fmap #-}
|
||||||
|
fmap f (UNow x) = UNow (f x)
|
||||||
|
fmap f (UNext x) = UNext (fmap f x)
|
||||||
|
-}
|
||||||
|
|
||||||
|
data P (n :: Nat) = P
|
||||||
|
|
||||||
|
-- injecting/projecting at a specified position P n
|
||||||
|
class Member' t r (n :: Nat) where
|
||||||
|
inj' :: P n -> t v -> Union r v
|
||||||
|
prj' :: P n -> Union r v -> Maybe (t v)
|
||||||
|
|
||||||
|
instance (r ~ (t ': r')) => Member' t r 'Z where
|
||||||
|
inj' _ = UNow
|
||||||
|
prj' _ (UNow x) = Just x
|
||||||
|
prj' _ _ = Nothing
|
||||||
|
|
||||||
|
instance (r ~ (t' ': r'), Member' t r' n) => Member' t r ('S n) where
|
||||||
|
inj' _ = UNext . inj' (P::P n)
|
||||||
|
prj' _ (UNow _) = Nothing
|
||||||
|
prj' _ (UNext x) = prj' (P::P n) x
|
||||||
|
|
||||||
|
class (Member' t r (FindElem t r)) => Member t r where
|
||||||
|
inj :: t v -> Union r v
|
||||||
|
prj :: Union r v -> Maybe (t v)
|
||||||
|
|
||||||
|
instance (Member' t r (FindElem t r)) => Member t r where
|
||||||
|
inj = inj' (P :: P (FindElem t r))
|
||||||
|
prj = prj' (P :: P (FindElem t r))
|
||||||
|
|
||||||
|
{-# INLINE decomp #-}
|
||||||
|
decomp :: Union (t ': r) v -> Either (Union r v) (t v)
|
||||||
|
decomp (UNow x) = Right x
|
||||||
|
decomp (UNext v) = Left v
|
||||||
|
|
||||||
|
{-# INLINE weaken #-}
|
||||||
|
weaken :: Union r w -> Union (any ': r) w
|
||||||
|
weaken = UNext
|
||||||
|
|
||||||
|
data Nat = Z | S Nat
|
||||||
|
|
||||||
|
-- Find an index of an element in a `list'
|
||||||
|
-- The element must exist
|
||||||
|
-- This closed type family disambiguates otherwise overlapping
|
||||||
|
-- instances
|
||||||
|
type family FindElem (t :: * -> *) r :: Nat where
|
||||||
|
FindElem t (t ': r) = 'Z
|
||||||
|
FindElem t (any ': r) = 'S (FindElem t r)
|
||||||
|
|
||||||
|
type family EQU (a :: k) (b :: k) :: Bool where
|
||||||
|
EQU a a = 'True
|
||||||
|
EQU a b = 'False
|
5
stack.yaml
Normal file
5
stack.yaml
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
flags: {}
|
||||||
|
packages:
|
||||||
|
- '.'
|
||||||
|
extra-deps: []
|
||||||
|
resolver: lts-3.4
|
Loading…
Reference in New Issue
Block a user