packages feed

effect-monad 0.6.1 → 0.7.0.0

raw patch · 26 files changed

+395/−264 lines, 26 filesdep −ghc-primdep ~basedep ~type-level-sets

Dependencies removed: ghc-prim

Dependency ranges changed: base, type-level-sets

Files

effect-monad.cabal view
@@ -1,21 +1,20 @@ name:                   effect-monad-version:                0.6.1-synopsis:               Embeds effect systems into Haskell using parameteric effect monads+version:                0.7.0.0+synopsis:               Embeds effect systems into Haskell using graded monads description:            -   Provides the 'parametric effect monad' structure to Haskell with a number of analogous of familiar monads (Reader, Writer, State, Maybe, Counter, Update) and a wrapper over normal monads (Control.Effect.Monad). This provides a way to embed effect systems into Haskell. For more information see with paper \"Embedding effect systems in Haskell\" by Orchard and Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell, 2014) and the examples in <https://github.com/dorchard/effect-monad/tree/master/examples>. -  .+   Provides the graded monad structure to Haskell with a number of analogs of familiar monads (Reader, Writer, State, Maybe, Counter, Update) and a wrapper over normal monads (Control.Effect.Monad). This provides a way to embed effect systems into Haskell. For more information see with paper \"Embedding effect systems in Haskell\" by Orchard and Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell, 2014) and the examples in <https://github.com/dorchard/effect-monad/tree/master/examples>.    (note, this package was previously called 'ixmonad' until September 2014).   license:                BSD3 license-file:           LICENSE category:               Control, Monads-copyright:              2013-14 University of Cambridge+copyright:              2013-16 University of Cambridge author:                 Dominic Orchard maintainer:             Dominic Orchard stability:              experimental build-type:             Simple cabal-version:          >= 1.6-tested-with:            GHC == 7.8.2+tested-with:            GHC == 7.10.3, GHC == 8.0.1  extra-source-files:     examples/*.hs @@ -39,7 +38,7 @@                         Control.Effect.Parameterised                         Control.Effect.Reader                         Control.Effect.ReadOnceReader-                        Control.Effect.State+                        Control.Effect.State	                         Control.Effect.Update                         Control.Effect.Vector                         Control.Effect.WriteOnceWriter@@ -47,6 +46,4 @@                         Control.Effect.Helpers.List                            build-depends:        base < 5,-                        ghc-prim,-                        type-level-sets >= 0.5-+                        type-level-sets == 0.8.0.0
examples/ArrayReader.hs view
@@ -1,18 +1,17 @@ {-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances,              FlexibleContexts, DataKinds, UndecidableInstances, ScopedTypeVariables #-} -module ArrayReader where +module ArrayReader where -import GHC.TypeLits +import GHC.TypeLits import Data.Array-import Prelude hiding (Monad(..)) +import Prelude hiding (Monad(..)) -import Data.Proxy import Control.Effect import Data.Type.Set  -- Array with a cursor-data CArray (x::[*]) a = MkA (Array Int a, Int) +data CArray (x::[*]) a = MkA (Array Int a, Int)  -- Computations from 'a' to 'b' with an array parameter data Stencil a (r::[*]) b = Stencil (CArray r a -> b)@@ -26,7 +25,7 @@     type Plus (Stencil a) s t = Union s t -- append specs     type Unit (Stencil a)     = '[]       -- empty spec -    (Stencil f) >>= k = +    (Stencil f) >>= k =         Stencil (\(MkA a) -> let (Stencil f') = k (f (MkA a))                                  in f' (MkA a))     return a = Stencil (\_ -> a)@@ -47,4 +46,3 @@ type instance Cmp (IntT (Neg n)) (IntT (Neg m)) = CmpNat n m type instance Cmp (IntT (Pos n)) (IntT (Neg m)) = GT type instance Cmp (IntT (Neg n)) (IntT (Pos m)) = LT-
examples/Counter.hs view
@@ -1,19 +1,19 @@-{-# LANGUAGE RebindableSyntax, EmptyDataDecls, GADTs, TypeFamilies, UndecidableInstances, MultiParamTypeClasses, TypeOperators #-}+{-# LANGUAGE RebindableSyntax, EmptyDataDecls, GADTs, TypeFamilies, UndecidableInstances, MultiParamTypeClasses, TypeOperators, ScopedTypeVariables, ImplicitParams #-} -import Prelude hiding (Monad(..))+import Prelude hiding (Monad(..),map) import Control.Effect import Control.Effect.Counter  import Debug.Trace -{- +{- -The 'Counter' indexed monad is useful for counting computations+The 'Counter' graded monad is useful for counting computations of a particular kind (e.g., counting number of calls to a websocket) or estimating resource usage (e.g., a websocket call is more expensive-than a disk write). +than a disk write). -By default, zero counts are tracked, e.g., +By default, zero counts are tracked, e.g.,  -} @@ -29,9 +29,14 @@           y <- return 3           return (x * y) -{- This can be used for other cool things, like proving that 'map' has - linear complexity of 'map' at the type-level! +zero :: Counter Z Int+zero = do x <- return 2+          y <- return 4+          return (x + y) +{- This can be used for other cool things, like proving that 'map' has+ linear complexity of 'map' at the type-level!+ For this we need sized lists: -} @@ -39,11 +44,9 @@     Nil :: Vector Z a     Cons :: a -> Vector n a -> Vector (S n) a -type family n :* m -type instance Z :* m = Z-type instance (S n) :* m = m :+ (n :* m)--{- map' is then defined as follows -}+type family n :* m where+            Z     :* m = Z+            (S n) :* m = m :+ (n :* m)  map' :: (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b) map' f Nil         = return Nil@@ -51,7 +54,36 @@                         xs' <- map' f xs                         return (Cons x' xs') -{- The types show us that if the function counts 't' things, then applying 'map'+++++++++++map :: (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b)+map f Nil         = return Nil+map f (Cons x xs) = do x' <- f x+                       xs' <- map f xs+                       return (Cons x' xs')++class Bar n where+instance Bar Z where+instance Bar n => Bar (S n) where++data Listy n a where+    Nily :: Listy Z a+    Consy :: (Bar n) => a -> Listy n a -> Listy (S n) a++fooo :: Listy n a -> Int+fooo Nily = 0+fooo (Consy x (Consy y xs)) = 2 + (fooo xs)+fooo (Consy x xs) = 1 + (fooo xs)++{- The types show us that if the function counts 't' things, then applying 'map to an n-vector counts 'tn' things -}  {- Example: web socket calls- how many do we do per instances #-}@@ -59,12 +91,15 @@ call :: Int -> Counter (S Z) () call = undefined -singleCall = map' call (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))+singleCall = map call (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))) -doubleCall x = map' (\n -> do {a <- call n; b <- call n; return ()}) x+doubleCall x = map (\n -> do {a <- call n; b <- call n; return ()}) x  doubleCallExample = doubleCall (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))) +++ {- are we definitely linear in the number of elements, even if we have closed over the vector? -}  class LT n m@@ -72,4 +107,4 @@ instance LT n m => LT (S n) (S m)  lineraMap :: LT t n => (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b)-lineraMap = map'+lineraMap = map
examples/CounterNat.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, GADTs, TypeFamilies, UndecidableInstances #-}+{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, GADTs,+             TypeFamilies, UndecidableInstances #-}  import Prelude hiding (Monad(..)) import Control.Effect@@ -8,12 +9,12 @@  import Debug.Trace -{- +{- -The 'Counter' indexed monad is useful for counting computations+The 'Counter' graded monad is useful for counting computations of a particular kind (e.g., counting number of calls to a websocket) or estimating resource usage (e.g., a websocket call is more expensive-than a disk write). +than a disk write).  By default, zero counts are tracked, e.g., -} @@ -27,10 +28,10 @@ -- foo2 :: Counter (S Z) Int foo2 = do x <- tick 2           y <- return 3-          return (x * y) +          return (x * y) -{- This can be used for other cool things, like proving that 'map' has - linear complexity of 'map' at the type-level! +{- This can be used for other cool things, like proving that 'map' has+ linear complexity of 'map' at the type-level!  For this we need sized lists: -}@@ -46,7 +47,7 @@  {- map' is then defined as follows -} -{- CAN'T TYPE CHECK, see Counter.hs +{- CAN'T TYPE CHECK, see Counter.hs  map' :: (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b) map' f Nil         = return Nil@@ -55,4 +56,3 @@                         return (Cons x' xs')  -}-
examples/ImplicitP.hs view
@@ -4,31 +4,33 @@ import Control.Effect import Control.Effect.Reader -foo :: (Num a, ?x :: a, ?y :: a) => a -> a-foo z = ?x + ?y -fooM :: (Num a) => a -> Reader '["?x" :-> a, "?y" :-> a] a-fooM z = do x <- ask (Var::(Var "?x"))-            y <- ask (Var::(Var "?y"))-            return (x + y + z)+example1 :: (Num a, ?x :: a, ?y :: a) => a -> a+example1 z = ?x + ?y -foo' :: (Num a, ?y :: a) => a -> a-foo' = let ?x = 42-       in \z -> ?x + ?y + z+example1M :: (Num a) => a -> Reader '["?x" :-> a, "?y" :-> a] a+example1M z = do x <- ask (Var::(Var "?x"))+                 y <- ask (Var::(Var "?y"))+                 return (x + y + z) -fooM' :: Num a => Reader '["?x" :-> a] (a -> Reader '["?y" :-> a] a)-fooM' = merge (\z -> do x <- ask (Var::(Var "?x"))-                        y <- ask (Var::(Var "?y"))-                        return (x + y + z))+example2 :: (Num a, ?y :: a) => a -> a+example2 = let ?x = 42+            in \z -> ?x + ?y + z +example2M :: Num a => Reader '["?x" :-> a] (a -> Reader '["?y" :-> a] a)+example2M = merge (\z -> do x <- ask (Var::(Var "?x"))+                            y <- ask (Var::(Var "?y"))+                            return (x + y + z))+ with f x = runReader f x+runExample2 = example2M `with` (Ext Var (42 :: Int) Empty)+runExample2' x y z = (example2M `with` (Ext Var (x :: Int) Empty) $ z)+                                `with` (Ext Var y Empty) -fooM'' = fooM' `with` (Ext (Var :-> 42) Empty) -sum2 :: Num a => a -> Reader '["?y" :-> a] a-sum2 = let x = (Ext ((Var::(Var "?x")) :-> 42) Empty) -       in runReader (merge (\z -> do x <- ask (Var::(Var "?x"))-                                     y <- ask (Var::(Var "?y"))-                                     return (x + y + z))) x--     +example3M :: Int -> Reader '["?y" :-> Int] Int+example3M =+  let x = Ext (Var::(Var "?x")) (42 :: Int) Empty+  in runReader (merge (\z -> do x <- ask (Var::(Var "?x"))+                                y <- ask (Var::(Var "?y"))+                                return (x + y + z))) x
+ examples/Inc.hs view
@@ -0,0 +1,35 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+module EffectsInHaskellProblem where++import           Control.Effect+import           Control.Effect.State+import           GHC.TypeLits+import           Prelude               hiding (log, Monad(..), (>>))++varX :: Var "x"+varX = Var++inc :: State '["x" :-> Int :! 'RW] ()+inc =+    get varX >>= (put varX . (+1))++-- No instance for (Control.Effect.State.Nubable '["x" :-> (Int :! 'W)] '[])+inc2 =+    inc >>=+    \_ ->+         inc
examples/Monad.hs view
@@ -1,8 +1,8 @@-{-# LANGUAGE TypeFamilies, RebindableSyntax #-}+{-# Language TypeFamilies, RebindableSyntax #-}  import Control.Effect import Control.Effect.Monad-import Prelude hiding (Monad(..)) +import Prelude hiding (Monad(..))  putStrLn' = Wrap . putStrLn
examples/Problem1.hs view
@@ -2,6 +2,13 @@  import Control.Monad.State.Lazy +appendBuffer x = do buff <- get+                    put (buff ++ x)++hello :: Monad m => StateT String (StateT String m) ()+hello = do name <- get+           lift $ appendBuffer $ "hello " ++ name+ incSC :: (Monad m) => StateT Int m () incSC = do x <- get            put (x + 1)@@ -26,5 +33,3 @@                  lift $ lift $ incSC  runHellowCount = runStateT (runStateT (runStateT hellowCount "") 0) 1--
examples/ReadOnceReader.hs view
@@ -6,17 +6,17 @@ import Control.Effect.ReadOnceReader  foo = do x <- ask-         y <- ask +         y <- ask          return ("Name " ++ x ++ " age " ++ (show y))  --foo_eval = foo (HCons' 'a' (HCons' "bc" HNil')) -foo2 = do x <- ask +foo2 = do x <- ask           y <- ask           xs <- ask           return (x : (y : xs)) -foo2' = do x <- ask +foo2' = do x <- ask            xs' <- do y <- ask                      xs <- ask                      return (y:xs)
examples/Reader.hs view
@@ -1,40 +1,30 @@-{-# LANGUAGE RebindableSyntax, NoMonomorphismRestriction, DataKinds, TypeOperators, -   FlexibleContexts, ConstraintKinds #-}+{-# LANGUAGE ImplicitParams, DataKinds, RebindableSyntax, TypeOperators, ScopedTypeVariables #-} import Prelude hiding (Monad(..)) import Control.Effect import Control.Effect.Reader +import Data.Type.Map+ import GHC.TypeLits  {- Examples -} --- foo :: Reader '["x" :-> a, "xs" :-> [a]] [a]-foo = do x <- ask (Var::(Var "x"))-         xs <- ask (Var::(Var "xs"))-         x' <- ask (Var::(Var "x"))-         return (x:x':xs)+-- example :: Reader '["x" :-> a, "xs" :-> [a]] [a]+example = do+  x  <- ask (Var::(Var "x"))+  xs <- ask (Var::(Var "xs"))+  x' <- ask (Var::(Var "x"))+  return (x:x':xs) -init1 = Ext (Var :-> 1) (Ext (Var :-> [2, 3]) Empty)-runFoo = runReader foo init1+init1 = Ext Var 1 (Ext Var [2, 3] Empty)+runExample = runReader example init1  -- Examples with subeffecting (need to refine the types a bit to 'run') -bar :: (Subset '["x" :-> Int, "xs" :-> [Int]] t) => Reader t [Int]-bar = sub foo+example' :: (Submap '["x" :-> Int, "xs" :-> [Int]] t) => Reader t [Int]+example' = sub example -init2 :: Set '["x" :-> Int, "xs" :-> [Int], "z" :-> a]-init2 =  Ext (Var :-> 1) (Ext (Var :-> [2, 3]) (Ext (Var :-> undefined) Empty))-runBar = runReader bar init2 --- Note: GHC currently has trouble with---init2a = asSet (append init1 (Ext (Var :-> undefined) Empty))--{--foo_b = do x <- ask (Var::(Var "x"))-           y <- ask (Var::(Var "x"))-           return (not x,not y)--foo_b = --}---- runFoob = runReader foo_b (Ext (Var :-> 1) (Ext (Var :-> [1,2,3]) Empty))+init2 :: Map '["x" :-> Int, "xs" :-> [Int], "z" :-> a]+init2 =  Ext Var 1 (Ext Var [2, 3] (Ext Var undefined Empty))+runExample' = runReader example' init2
− examples/Solution1-alt.hs 
@@ -1,22 +0,0 @@-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}--import Control.Monad.State.Lazy--class Monad m => Streaming a m where-    writeS :: [a] -> m ()--class Monad m => Counting m where-    incC :: m ()---- write :: (Streaming a m, Counting m) => [a] -> m ()-write x = do { writeS x; incC }--instance Monad m => Streaming a (StateT [a] m) where-    writeS y = do x <- get-                  put (x ++ y)--instance Monad m => Counting (StateT Int m) where-    incC = do x <- get-              put (x + 1)--foo = runStateT 0 $ runStateT "" $ write "message"
examples/Solution1.hs view
@@ -1,47 +1,61 @@-{-# LANGUAGE FlexibleContexts, DataKinds, TypeOperators, +{-# LANGUAGE FlexibleContexts, DataKinds, TypeOperators,               RebindableSyntax, FlexibleInstances #-}  import Prelude hiding (Monad(..)) import Control.Effect import Control.Effect.State -c1_var = Var::(Var "c1")-c2_var = Var::(Var "c2")-o_var  = Var::(Var "out")--instance Show (Var "out") where-    show _ = "out"--instance Show (Var "c1") where-    show _ = "c1"--instance Show (Var "c2") where-    show _ = "c2"+c1 = Var::(Var "c1")+c2 = Var::(Var "c2")+out  = Var::(Var "out")  incC :: Var v -> State '[v :-> Int :! RW] () incC var = do x <- get var               put var (x + 1)  writeS :: [a] -> State '["out" :-> [a] :! RW] ()-writeS y = do x <- get o_var-              put o_var (x ++ y)+writeS y = do x <- get out+              put out (x ++ y)  write ::  [a] -> State '["c1" :-> Int :! RW, "out" :-> [a] :! RW] () write x = do  writeS x-              incC c1_var+              incC c1 -initState0 = Ext (c1_var :-> ((0::Int) :! Eff)) (Ext (o_var :-> ("" :! Eff)) Empty)+initState0 = Ext (c1 :-> ((0::Int) :! Eff)) (Ext (out :-> ("" :! Eff)) Empty) runWrite = runState (write "hello") initState0 +hellow :: State '["c1" :-> Int :! RW, "nom" :-> String :! R, "out" :-> String :! RW] () hellow = do write "hello"             write " "-            write "world"+            name <- get (Var::(Var "nom"))+            write (name::String) -initState = Ext (c1_var :-> ((0::Int) :! Eff)) (Ext (o_var :-> ("" :! Eff)) Empty)++-- appendBuffer :: String -> State '["buff" :-> String :! RW] ()+appendBuffer x = do let bvar = Var::(Var "buff")+                    buff <- get bvar+                    put bvar (buff ++ x)++hello :: State '["buff" :-> String :! RW, "name" :-> String :! R] ()+hello = do name <- get (Var::(Var "name"))+           appendBuffer $ "hello " ++ name++initState = Ext (c1 :-> ((0::Int) :! Eff)) (Ext (out :-> ("" :! Eff)) Empty) runHellow = runState hellow initState  hellowCount = do hellow-                 incC c2_var+                 incC c2 -initState' = Ext (c1_var :-> ((0::Int) :! Eff)) (Ext (c2_var :-> ((1::Int) :! Eff)) (Ext (o_var :-> ("" :! Eff)) Empty))+initState' = Ext (c1 :-> ((0::Int) :! Eff)) (Ext (c2 :-> ((1::Int) :! Eff)) (Ext (out :-> ("" :! Eff)) Empty)) runHellowCount = runState hellowCount initState'++-- Show instances++instance Show (Var "out") where+    show _ = "out"++instance Show (Var "c1") where+    show _ = "c1"++instance Show (Var "c2") where+    show _ = "c2"
examples/Solution2.hs view
@@ -1,5 +1,6 @@-{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, FlexibleInstances, -              ConstraintKinds, FlexibleContexts, TypeFamilies #-}+{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures,+             FlexibleInstances, ConstraintKinds, FlexibleContexts,+             TypeFamilies #-}  import Prelude hiding (Monad(..)) import Control.Effect@@ -7,7 +8,7 @@ import Control.Effect.State import GHC.Conc.Sync -parMap :: (IsSet f, StateSet f, Writes f ~ '[]) => (a -> State f b) -> [a] -> State f [b] +parMap :: (IsSet f, StateSet f, Writes f ~ '[]) => (a -> State f b) -> [a] -> State f [b] -- parMap k [] = sub (return []) parMap k [x] = do y <- k x                   return [y]@@ -16,7 +17,7 @@                      return (y : ys)  -parMap2 :: (StateSet f, Writes f ~ '[]) => (a -> State f b) -> [a] -> State f [b] +parMap2 :: (StateSet f, Writes f ~ '[]) => (a -> State f b) -> [a] -> State f [b] parMap2 k [] = sub (return []) parMap2 k (x:xs) = do (y, ys)  <- (k x) `par` parMap2 k xs                       return (y : ys)
examples/State.hs view
@@ -7,21 +7,28 @@ x_var = Var::(Var "x") y_var = Var::(Var "y") --{- Computation with a read effect on variable "x" and a read-write (update) effect on variable "y" -}--- foo :: State '["x" :-> Int :! R, "y" :-> [Int] :! RW] [Int]-foo = do x <- get x_var-         y <- get y_var-         put y_var (x:y)-         z <- get y_var-         return (x:z)+{- Computation with a read effect on variable "x" and a+   read-write (update) effect on variable "y" -}+-- example :: State '["x" :-> Int :! R, "y" :-> [Int] :! RW] [Int]+example = do+  x <- get x_var+  y <- get y_var+  put y_var (x:y)+  z <- get y_var+  return (x:z) -foo_run = runState foo (Ext (x_var :-> (1 :! Eff)) (Ext (y_var :-> ([2,3] :! Eff)) Empty))+initS =  Ext (x_var :-> (1 :! Eff)) (Ext (y_var :-> ([2,3] :! Eff)) Empty)+example_run = runState example initS ---foo2 :: State '["x" :-> Int :! RW] Int-foo2 = do x <- get (Var::(Var "x"))-          put (Var::(Var "x")) (x+1)-          return x+--example2 :: State '["x" :-> Int :! RW] Int+example2 = do+  x <- get (Var::(Var "x"))+  put (Var::(Var "x")) (x+1)+  return x -foo2_run = (runState foo2) (Ext (x_var :-> 10 :! Eff) Empty)+example2_run = (runState example2) (Ext (x_var :-> 10 :! Eff) Empty) +example3 :: State '["x" :-> String :! RW] ()+example3 = do+  x <- get x_var+  put x_var (x ++ " ok !")
examples/StencilSpecs.hs view
@@ -27,7 +27,7 @@ fooSymBroken :: (Num a) => StencilM a (Symmetrical (S Z)) a a fooSymBroken = StencilM $ do a <- ix (Pos Z)                              b <- ix (Pos (S Z))-                             return $ a + b +                             return $ a + b -}  -- fooFwd has a 'forward' pattern to depth of 2@@ -46,7 +46,7 @@  -- Symmetrical stencils (derived from Forward and Backward stencils of the same depth) -type Symmetrical depth = AsSet ((IntT (Pos 0)) ': (Append (ForwardP depth) (BackwardP depth)))+type Symmetrical depth = AsSet ((IntT (Pos 0)) ': ((ForwardP depth) :++ (BackwardP depth)))  -- Backward-oriented stencils @@ -54,4 +54,4 @@  type family  BackwardP depth where              BackwardP 0 = '[]-             BackwardP n = (IntT (Neg n)) ': (BackwardP (n - 1)) +             BackwardP n = (IntT (Neg n)) ': (BackwardP (n - 1))
examples/WriteOnceWriter.hs view
@@ -2,7 +2,7 @@  import Prelude hiding (Monad(..)) import Control.Effect-import Control.Effect.WriteOnceWriter +import Control.Effect.WriteOnceWriter  foo = do put 42          put "hello"
examples/Writer.hs view
@@ -1,13 +1,13 @@-{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, RebindableSyntax, FlexibleInstances, -             ConstraintKinds, FlexibleContexts, TypeFamilies, ScopedTypeVariables-  #-}+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, RebindableSyntax,+             FlexibleInstances, ConstraintKinds, FlexibleContexts,+             TypeFamilies, ScopedTypeVariables #-} +import Prelude hiding (Monad(..)) import Control.Effect import Control.Effect.Writer  import Data.Monoid -import Prelude hiding (Monad(..))  instance Monoid Int where     mappend = (+)@@ -17,30 +17,33 @@ var_y = Var::(Var "y")  test :: Writer '["x" :-> Int, "y" :-> String] ()-test = do put var_x (42::Int)-          put var_y "hello"-          put var_x (58::Int)-          put var_y " world"+test = do+   put var_x (42::Int)+   put var_y "hello"+   put var_x (58::Int)+   put var_y " world"  --test' :: forall a . (Monoid a, Num a) => a -> Writer '["x" :-> a, "y" :-> String] ()-test' (n::a) = do put var_x (42::a)-                  put var_y "hello"-                  put var_x (n::a)-                  put var_y " world"+test' (n::a) = do+   put var_x (42::a)+   put var_y "hello"+   put var_x (n::a)+   put var_y " world"  {-- Polymorphism test -}-test2 :: (IsSet f, Unionable f '["y" :-> String]) => +test2 :: (IsMap f, Unionable f '["y" :-> String]) =>          (Int -> Writer f t) -> Writer (Union f '["y" :-> String]) ()-test2 f = do f 3 -             put var_y ". hi"+test2 f = do+   f 3+   put var_y ". hi"  {-- Subeffecting test -} test3 :: Writer '["x" :-> Int, "y" :-> String, "z" :-> Int] () test3 = sub (test2 test') -foo2 :: (IsSet f, Unionable f '["x" :-> Int, "y" :-> t], Num a) => +foo2 :: (IsMap f, Unionable f '["x" :-> Int, "y" :-> t], Num a) =>        (a -> Writer f t) -> Writer (Union f '["x" :-> Int, "y" :-> t]) ()-foo2 f = do y <- f 3-            put var_x (42::Int)-            put var_y y-+foo2 f = do+    y <- f 3+    put var_x (42::Int)+    put var_y y
src/Control/Coeffect.hs view
@@ -3,7 +3,7 @@  module Control.Coeffect where  -import GHC.Prim+import GHC.Exts ( Constraint )  {- Coeffect parameterised comonad
src/Control/Coeffect/Coreader.hs view
@@ -1,14 +1,15 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs, +{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs,              ConstraintKinds, TypeOperators, DataKinds, UndecidableInstances #-}  module Control.Coeffect.Coreader where  import Control.Coeffect-import Data.Type.Set+import Data.Type.Map+import GHC.TypeLits  {-| Provides 'reader monad'-like behaviour but as a comonad, using an indexed     version of the product comonad -}-data IxCoreader s a = IxR { runCoreader :: (a, Set s) }+data IxCoreader (s :: [Mapping Symbol *]) a = IxR { runCoreader :: (a, Map s) }  instance Coeffect IxCoreader where     type Inv IxCoreader s t = (Unionable s t, Split s t (Union s t))@@ -29,5 +30,4 @@  {-| 'ask' for the value of variable 'v', e.g., 'ask (Var::(Var "x"))' -} ask :: Var v -> IxCoreader '[v :-> a] b -> a-ask _ = \(IxR (_, Ext (Var :-> a) Empty)) -> a-+ask _ = \(IxR (_, Ext Var a Empty)) -> a
src/Control/Effect.hs view
@@ -3,8 +3,7 @@ module Control.Effect where   import Prelude hiding (Monad(..))-import GHC.Prim-+import GHC.Exts ( Constraint )      {-| Specifies "parametric effect monads" which are essentially monads but      annotated by a type-level monoid formed by 'Plus' and 'Unit' -}@@ -25,6 +24,7 @@     {-| Effect-parameterise version of '>>=' (bind). Combines      two effect annotations 'f' and 'g' on its parameter computations into 'Plus' -}+    (>>=) :: (Inv m f g) => m f a -> (a -> m g b) -> m (Plus m f g) b     (>>) :: (Inv m f g) => m f a -> m g b -> m (Plus m f g) b@@ -35,3 +35,4 @@ {-| Specifies subeffecting behaviour -} class Subeffect (m :: k -> * -> *) f g where     sub :: m f a -> m g a+
src/Control/Effect/Cond.hs view
@@ -2,7 +2,7 @@  module Control.Effect.Cond where -import GHC.Prim+import GHC.Exts ( Constraint )  {-| Provides a conditional using an 'alternation' operation, as opposed to using    'Subeffect' -}
src/Control/Effect/Helpers/List.hs view
@@ -1,21 +1,23 @@-{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, -             MultiParamTypeClasses, FlexibleInstances #-}+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts, +             MultiParamTypeClasses, FlexibleInstances, PolyKinds, KindSignatures #-}  module Control.Effect.Helpers.List where +import Data.Proxy + data List (l::[*]) where     Nil   :: List '[]     Cons  :: x -> List xs -> List (x ': xs) -type family (:++) (s :: [*]) (t :: [*]) :: [*]-type instance '[] :++ ys       = ys-type instance (x ': xs) :++ ys = x ': (xs :++ ys)+type family (:++) (s :: [*]) (t :: [*]) :: [*] where+    '[] :++ ys       = ys+    (x ': xs) :++ ys = x ': (xs :++ ys)  append :: List s -> List t -> List (s :++ t) append Nil xs = xs append (Cons x xs) ys = Cons x (append xs ys) -class Split s t where+class Split (s :: [*]) (t :: [*]) where     split :: List (s :++ t) -> (List s, List t)  instance Split '[] xs where@@ -24,3 +26,27 @@ instance Split xs ys => Split (x ': xs) ys where     split (Cons x xs) = let (xs', ys') = split xs                     in (Cons x xs', ys')++lengthL :: List xs -> Int+lengthL Nil = 0+lengthL (Cons _ xs) = 1 + lengthL xs++type family LookupT  k xs where+    LookupT k '[] = Maybe ()+    LookupT k ((k , x) ': xs) = Maybe x+    LookupT k ((j , x) ': xs) = LookupT k xs++class LookUpA k xs (LookupT k xs) => Lookup k xs where+    lookup :: List xs -> Proxy k -> Maybe (LookupT k xs) +    lookup = lookupA++class LookUpA k xs x where+    lookupA :: List xs -> Proxy k -> Maybe x++instance LookUpA k ((k, x) ': xs) x where+    lookupA (Cons (_, x) _) k = Just x ++instance LookUpA k xs y => LookUpA k ((j, x) ': xs) y where+    lookupA (Cons _ xs) k = lookupA xs k++
src/Control/Effect/Monad.hs view
@@ -12,11 +12,11 @@ -}  {-| Wrap regular monads up -}-data Monad m t a where+data Monad m f a where     Wrap :: P.Monad m => m a -> Monad m () a  {-| Unwrap a monad -}-unWrap :: P.Monad m => Monad m t a -> m a+unWrap :: P.Monad m => Monad m f a -> m a unWrap (Wrap m) = m  instance (P.Monad m) => Effect (Monad m) where
src/Control/Effect/Reader.hs view
@@ -1,22 +1,24 @@-{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, -             UndecidableInstances, RebindableSyntax, DataKinds, TypeOperators, PolyKinds, -             ConstraintKinds #-}+{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts,+             MultiParamTypeClasses, UndecidableInstances, RebindableSyntax,+             DataKinds, TypeOperators, PolyKinds, ConstraintKinds,+             KindSignatures #-} -module Control.Effect.Reader (Reader(..), ask, merge, (:->)(..), Var(..), Subset, Set(..)) where+module Control.Effect.Reader (Reader(..), ask, merge, Mapping(..),+                              Var(..), Submap, Map(..)) where  import Control.Effect-import Data.Type.Set+import Data.Type.Map import Prelude hiding (Monad(..)) import GHC.TypeLits-import GHC.Prim+import GHC.Exts ( Constraint )  {-| Provides a effect-parameterised version of the class reader monad. Effects    are sets of variable-type pairs, providing an effect system for reader effects. -} -data Reader s a = IxR { runReader :: Set s -> a }+newtype Reader (s :: [Mapping Symbol *]) a = IxR { runReader :: Map s -> a }  instance Effect Reader where-    type Inv Reader f g = (IsSet f, IsSet g, Split f g (Union f g))+    type Inv Reader f g = (IsMap f, IsMap g, Split f g (Union f g))      {-| A trivial effect is the empty set -}     type Unit Reader = '[]@@ -29,17 +31,20 @@     (IxR e) >>= k = IxR $ \fg -> let (f, g) = split fg                                  in (runReader $ k (e f)) g +-- Values of the same type can be combined+type instance Combine v v = v+ {-| 'ask' for a variable 'v' of type 'a', raising an effect -} ask :: Var v -> Reader '[v :-> a] a-ask Var = IxR $ \(Ext (Var :-> a) Empty) -> a+ask Var = IxR $ \(Ext Var a Empty) -> a  {-| Provides a way to emulated the ImplicitParams features of GHC/Haskell -} merge :: (Unionable s t) => (a -> Reader (Union s t) b) -> Reader s (a -> Reader t b) merge k = IxR $ \s -> \a -> IxR $ \t -> runReader (k a) (union s t)  {-| If 's' is a subset of 't' then, 's' is a subeffect of 't' -}-instance Subset s t => Subeffect Reader s t where-    sub (IxR e) = IxR $ \st -> let s = subset st in e s+instance Submap s t => Subeffect Reader s t where+    sub (IxR e) = IxR $ \st -> let s = submap st in e s  {- {-| Define the operation for removing duplicates using mappend -}
src/Control/Effect/State.hs view
@@ -1,25 +1,26 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,  -             UndecidableInstances, RebindableSyntax,  DataKinds, -             TypeOperators, PolyKinds, FlexibleContexts, ConstraintKinds, -             OverlappingInstances, IncoherentInstances +{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,+             UndecidableInstances, RebindableSyntax,  DataKinds,+             TypeOperators, PolyKinds, FlexibleContexts, ConstraintKinds,+             IncoherentInstances, GADTs              #-}  module Control.Effect.State (Set(..), get, put, State(..), (:->)(..), (:!)(..),-                                  Eff(..), Action(..), Var(..), union, UnionS, -                                     Reads(..), Writes(..), Unionable, Sortable, SetLike, -                                      StateSet, +                                  Eff(..), Action(..), Var(..), union, UnionS,+                                     Reads(..), Writes(..), Unionable, Sortable, SetLike,+                                      StateSet,                                           --- may not want to export these                                           IntersectR, Update, Sort, Split) where  import Control.Effect import Data.Type.Set hiding (Unionable, union, SetLike, Nub, Nubable(..)) import qualified Data.Type.Set as Set+--import Data.Type.Map (Mapping(..), Var(..))  import Prelude hiding (Monad(..),reads) import GHC.TypeLits -{-| Provides an effect-parameterised version of the state monad, which gives an -   effect system for stateful computations with annotations that are sets of +{-| Provides an effect-parameterised version of the state monad, which gives an+   effect system for stateful computations with annotations that are sets of    variable-type-action triples. -}  @@ -35,8 +36,38 @@ instance Show (Action RW) where     show _ = "RW" +infixl 2 :->+data (k :: Symbol) :-> (v :: *) = (Var k) :-> v++data Var (k :: Symbol) where Var :: Var k+                             {- Some special defaults for some common names -}+                             X   :: Var "x"+                             Y   :: Var "y"+                             Z   :: Var "z"+++instance (Show (Var k), Show v) => Show (k :-> v) where+    show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"+instance Show (Var "x") where+    show X   = "x"+    show Var = "Var"+instance Show (Var "y") where+    show Y   = "y"+    show Var = "Var"+instance Show (Var "z") where+    show Z   = "z"+    show Var = "Var"+instance Show (Var v) where+    show _ = "Var"++{-| Symbol comparison -}+type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u+++ {-| Describes an effect action 's' on a value of type 'a' -}-data (:!) (a :: *) (s :: Eff) = a :! (Action s) +--data EffMapping a (s :: Eff) = a :! (Action s)+data a :! (s :: Eff) = a :! (Action s)  instance (Show (Action f), Show a) => Show (a :! f) where     show (a :! f) = show a ++ " ! " ++ show f@@ -44,8 +75,8 @@ infixl 3 :!  type SetLike s = Nub (Sort s)-type UnionS s t = Nub (Sort (Append s t))-type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)) (Nub (Sort (Append s t))),+type UnionS s t = Nub (Sort (s :++ t))+type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)) (Nub (Sort (s :++ t))),                       Split s t (Union s t))  {-| Union operation for state effects -}@@ -70,15 +101,15 @@ instance Nubable '[e] '[e] where     nub (Ext e Empty) = (Ext e Empty) -instance Nubable ((k :-> b :! s) ': as) as' => +instance Nubable ((k :-> b :! s) ': as) as' =>     Nubable ((k :-> a :! s) ': (k :-> b :! s) ': as) as' where     nub (Ext _ (Ext x xs)) = nub (Ext x xs) -instance Nubable ((k :-> a :! RW) ': as) as' => +instance Nubable ((k :-> a :! RW) ': as) as' =>     Nubable ((k :-> a :! s) ': (k :-> a :! t) ': as) as' where     nub (Ext _ (Ext (k :-> (a :! _)) xs)) = nub (Ext (k :-> (a :! (Eff::(Action RW)))) xs) -instance Nubable ((j :-> b :! t) ': as) as' => +instance Nubable ((j :-> b :! t) ': as) as' =>     Nubable ((k :-> a :! s) ': (j :-> b :! t) ': as) ((k :-> a :! s) ': as') where     nub (Ext (k :-> (a :! s)) (Ext (j :-> (b :! t)) xs)) = Ext (k :-> (a :! s)) (nub (Ext (j :-> (b :! t)) xs)) @@ -90,7 +121,7 @@ instance Update xs '[] where     update _ = Empty -instance Update '[e] '[e] where +instance Update '[e] '[e] where     update s = s  {-@@ -106,7 +137,7 @@ instance Update ((u :-> b :! s) ': as) as' => Update ((v :-> a :! R) ': (u :-> b :! s) ': as) ((v :-> a :! R) ': as') where     update (Ext e (Ext e' xs)) = Ext e $ update (Ext e' xs) -type IntersectR s t = (Sortable (Append s t), Update (Sort (Append s t)) t)+type IntersectR s t = (Sortable (s :++ t), Update (Sort (s :++ t)) t)  {-| Intersects a set of write effects and a set of read effects, updating any read effects with     any corresponding write value -}@@ -141,19 +172,19 @@ {-| Captures what it means to be a set of state effects -} type StateSet f = (StateSetProperties f, StateSetProperties (Reads f), StateSetProperties (Writes f)) type StateSetProperties f = (IntersectR f '[], IntersectR '[] f,-                             UnionS f '[] ~ f, Split f '[] f, -                             UnionS '[] f ~ f, Split '[] f f, +                             UnionS f '[] ~ f, Split f '[] f,+                             UnionS '[] f ~ f, Split '[] f f,                              UnionS f f ~ f, Split f f f,                              Unionable f '[], Unionable '[] f)-                   + -- Indexed monad instance instance Effect State where     type Inv State s t = (IsSet s, IsSet (Reads s), IsSet (Writes s),                           IsSet t, IsSet (Reads t), IsSet (Writes t),-                          Reads (Reads t) ~ Reads t, Writes (Writes s) ~ Writes s, -                            Split (Reads s) (Reads t) (Reads (UnionS s t)), -                            Unionable (Writes s) (Writes t), -                            IntersectR (Writes s) (Reads t), +                          Reads (Reads t) ~ Reads t, Writes (Writes s) ~ Writes s,+                            Split (Reads s) (Reads t) (Reads (UnionS s t)),+                            Unionable (Writes s) (Writes t),+                            IntersectR (Writes s) (Reads t),                             Writes (UnionS s t) ~ UnionS (Writes s) (Writes t))      {-| Pure state effect is the empty state -}@@ -164,17 +195,16 @@      return x = State $ \Empty -> (x, Empty) -    (State e) >>= k = +    (State e) >>= k =         State $ \st -> let (sR, tR) = split st                            (a, sW)  = e sR                            (b, tW) = (runState $ k a) (sW `intersectR` tR)-                       in  (b, sW `union` tW) +                       in  (b, sW `union` tW)   {- instance (Split s t (Union s t), Sub s t) => Subeffect State s t where-    sub (State e) = IxR $ \st -> let (s, t) = split st -                                           _ = ReflP p t +    sub (State e) = IxR $ \st -> let (s, t) = split st+                                           _ = ReflP p t                                  in e s -}-
src/Control/Effect/Writer.hs view
@@ -1,57 +1,61 @@-{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, -             MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, +{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,+             MultiParamTypeClasses, FlexibleInstances, UndecidableInstances,              ScopedTypeVariables, PolyKinds, FlexibleContexts #-} -module Control.Effect.Writer(Writer(..), Symbol, put, (:->), IsSet, Set(..), union, Var(..), -                              Union, Unionable) where+module Control.Effect.Writer(Writer(..), Symbol, put, Mapping(..),+                             IsMap, Map(..), union, Var(..),+                             Union, Unionable) where -import Control.Effect -import Data.Type.Set+import Control.Effect+import Data.Type.Map import Data.Monoid import GHC.TypeLits import Prelude hiding (Monad(..))  {-| Provides an effect-parameterised version of the writer monad. Effects-   are sets of variable-type pairs, providing an effect system for writer effects. -}+   are maps of variable-type pairs, providing an effect system for writer effects. -} -data Writer w a = Writer { runWriter :: (a, Set w) }+data Writer (w :: [Mapping Symbol *]) a = Writer { runWriter :: (a, Map w) }  instance Effect Writer where-    type Inv Writer s t = (IsSet s, IsSet t, Unionable s t)+    type Inv Writer s t = (IsMap s, IsMap t, Unionable s t) -    {-| A trivial effect is the empty set -}+    {-| A trivial effect is the empty map -}     type Unit Writer = '[]-    {-| Effects are combined by set union -}+    {-| Effects are combined by map union -}     type Plus Writer s t = Union s t      {-| Trivially pure computation produces an empty state -}     return x = Writer (x, Empty)-    {-| Composing copmutations takes the union of the writer states, using the monoid +    {-| Composing copmutations takes the union of the writer states, using the monoid         operation to combine writes to the same variable -}     (Writer (a, w)) >>= k = let Writer (b, w') = k a                             in  Writer (b, w `union` w')  {-| Write to variable 'v' with value of type 'a' -} put :: Var v -> a -> Writer '[v :-> a] ()-put v a = Writer ((), Ext (v :-> a) Empty)+put v a = Writer ((), Ext v a Empty) +-- Values of the same type can be combined+type instance Combine v v = v+ {-| Define the operation for removing duplicates using mappend -} instance (Monoid u, Nubable ((k :-> u) ': s)) => Nubable ((k :-> u) ': (k :-> u) ': s) where-    nub (Ext (_ :-> u) (Ext (k :-> v) s)) = nub (Ext (k :-> (u `mappend` v)) s)+    nub (Ext _ u (Ext k v s)) = nub (Ext k (u `mappend` v) s)  {- Sub effecting for the parametric effect monad -}-instance Superset s t => Subeffect Writer s t where-    sub (Writer (a, w)) = Writer (a, (superset w)::(Set t))+instance Supermap s t => Subeffect Writer s t where+    sub (Writer (a, w)) = Writer (a, (supermap w)::(Map t)) -{-| Computes supersets of sets of variable-type mappings, using the 'mempty' operation  -}-class Superset s t where-    superset :: Set s -> Set t+{-| Computes supermaps of maps of variable-type mappings, using the 'mempty' operation  -}+class Supermap s t where+    supermap :: Map s -> Map t -instance Superset '[] '[] where-    superset Empty = Empty+instance Supermap '[] '[] where+    supermap Empty = Empty -instance (Monoid x, Superset '[] s) => Superset '[] ((k :-> x) ': s) where-    superset Empty = Ext (Var :-> mempty) (superset Empty)+instance (Monoid x, Supermap '[] s) => Supermap '[] ((k :-> x) ': s) where+    supermap Empty = Ext Var mempty (supermap Empty) -instance Superset s t => Superset ((k :-> v) ': s) ((k :-> v) ': t) where-    superset (Ext x xs) = Ext x (superset xs)+instance Supermap s t => Supermap ((k :-> v) ': s) ((k :-> v) ': t) where+    supermap (Ext k x xs) = Ext k x (supermap xs)