effect-monad 0.7.0.0 → 0.8.0.0

raw patch · 12 files changed

+346/−81 lines, 12 filesdep ~type-level-setsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: type-level-sets

API changes (from Hackage documentation)

Files

• effect-monad.cabal +30/−11
• examples/AtomicState.hs +23/−0
• examples/ExtensibleState.hs +40/−0
• examples/Inc.hs +0/−35
• examples/SafeFiles.hs +34/−0
• examples/WriterM.hs +0/−17
• src/Control/Effect/Parameterised.hs +24/−18
• src/Control/Effect/Parameterised/AtomicState.hs +22/−0
• src/Control/Effect/Parameterised/ExtensibleState.hs +29/−0
• src/Control/Effect/Parameterised/SafeFiles.hs +99/−0
• src/Control/Effect/Parameterised/State.hs +20/−0
• src/Control/Effect/ParameterisedAsGraded.hs +25/−0

@@ -1,20 +1,34 @@ name:                   effect-monad-version:                0.7.0.0-synopsis:               Embeds effect systems into Haskell using graded monads-description:            -   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). +version:                0.8.0.0+synopsis:               Embeds effect systems and program logics into Haskell using graded monads and parameterised monads+description:+   Provides the graded monad structure to Haskell via Control.Effect+   with a number of analogs of familiar monads and some new things:+        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 the paper+   \"Embedding effect systems in Haskell\" by Orchard and Petricek+   <http://dorchard.co.uk/publ/haskell14-effects.pdf> (Haskell, 2014)++   Also provides the parameterised monad structure due to Atkey in+   Control.Effect.Parameterised along with some instances:+       AtomicState, SafeFiles, ExtensibleState++   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-16 University of Cambridge+copyright:              2013-18 University of Kent author:                 Dominic Orchard maintainer:             Dominic Orchard stability:              experimental build-type:             Simple cabal-version:          >= 1.6-tested-with:            GHC == 7.10.3, GHC == 8.0.1+tested-with:            GHC == 7.10.3, GHC == 8.0.1, GHC == 8.2.2  extra-source-files:     examples/*.hs @@ -35,15 +49,20 @@                         Control.Effect.CounterNat                         Control.Effect.Maybe                         Control.Effect.Monad-                        Control.Effect.Parameterised+                        Control.Effect.ParameterisedAsGraded                         Control.Effect.Reader                         Control.Effect.ReadOnceReader-                        Control.Effect.State	+                        Control.Effect.State                         Control.Effect.Update                         Control.Effect.Vector                         Control.Effect.WriteOnceWriter                         Control.Effect.Writer                         Control.Effect.Helpers.List-                        +                        Control.Effect.Parameterised+                        Control.Effect.Parameterised.AtomicState+                        Control.Effect.Parameterised.ExtensibleState+                        Control.Effect.Parameterised.SafeFiles+                        Control.Effect.Parameterised.State+   build-depends:        base < 5,-                        type-level-sets == 0.8.0.0+                        type-level-sets >= 0.8.7.0

@@ -0,0 +1,23 @@+{-# LANGUAGE RebindableSyntax #-}++-- Bye Monads... as we know them+import Prelude hiding (Monad(..))+-- Hello parameterised monads+import Control.Effect.Parameterised+import Control.Effect.Parameterised.AtomicState++-----------------------------+-- Examples++myProgram :: State (Closed Int) (Closed Int) String+myProgram = do+  x <- get+  put (x+1)+  a <- somethingPurish x+  return (a ++ show x)++somethingPurish :: Int -> State (Closed Int) (Closed Int) String+somethingPurish n = do+  x <- get+  put (x + 1)+  return $ if n == 0 then "hello" else "goodbye"

@@ -0,0 +1,40 @@+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}++import Prelude hiding (Monad(..))+import Control.Effect.Parameterised+import Control.Effect.Parameterised.ExtensibleState+import GHC.TypeLits+import Data.Type.Map++-- Example map+exMap :: Map '["x" ':-> Int, "flag" ':-> Bool]+exMap = Ext (Var @ "x") (42 :: Int)+      $ Ext (Var @ "flag") False+        Empty++increment :: (Update "x" Int m) => State (Map m) (Map m) ()+increment = do+   (n :: Int) <- get (Var @ "x")+   put (Var @ "x") (n+1)++example = do+   flag <- get (Var @ "flag")+   increment+   (n :: Int) <- get (Var @"x")+   put (Var @ "flag") ((n > 0) || flag)+++go :: ((), Map '["x" ':-> Int, "flag" ':-> Bool])+go = runState example exMap++example2 :: (Get "flag" Bool m, Update "x" Int m, Put "y" Int m m) => State (Map m) (Map m) ()+example2 = do+   flag <- get (Var @ "flag")+   if flag+     then modify (Var @ "x") (\(x :: Int) -> x + 1)+     else put (Var @ "y") (42 :: Int)

@@ -1,35 +0,0 @@-{-# 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

@@ -0,0 +1,34 @@+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE FlexibleContexts #-}++-- Bye Monads... as we know them+import Prelude hiding (Monad(..))+import Control.Effect.Parameterised.SafeFiles+import qualified System.IO as IO++example :: IO ()+example = runSafeFiles $ do+  h  <- openFile "foo" IO.ReadWriteMode+  h' <- openFile "bar" IO.ReadWriteMode+  x <- hGetChar h+  hPutChar h' x+  hClose h'+  hClose h+  return ()++example2 :: IO ()+example2 = runSafeFiles $ do+  h1  <- openFile "foo" IO.ReadWriteMode+  h2 <- openFile "bar" IO.ReadWriteMode+  loopy h1 h2++loopy h1 h2 = do+  isEmpty <- hIsEOF h1+  if isEmpty+    then do+      hClose h1+      hClose h2+    else do+      x <- hGetChar h1+      hPutChar h2 x+      loopy h1 h2

@@ -1,17 +0,0 @@-{-# LANGUAGE FlexibleInstances #-}--import Data.Monoid--data Writer w a = Writer { runWriter :: (a, w) }--instance Monoid w => Monad (Writer w) where-   return a = Writer (a, mempty)-   (Writer (a, w)) >>= k = let (b, w') = runWriter (k a)-                           in Writer (b, w `mappend` w')--instance Monad (Writer (Maybe a)) where-   return a = Writer (a, Nothing)-   (Writer (a, w)) >>= k = let (b, w') = runWriter (k a)-                           in case w' of -                                Nothing -> Writer (b, w)-                                Just w' -> Writer (b, Just w')

@@ -1,25 +1,31 @@-{-# LANGUAGE KindSignatures, TypeFamilies, ConstraintKinds, PolyKinds, DataKinds #-}+-- Used to make the types extra clear+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-} -module Control.Effect.Parameterised where+-- This module implement parameterised monads due to Bob Atkey+-- (see 'Parameterised Notions of Computing' JFP 2009)+-- also defined in Control.Monad.Indexed (category-extras) -import Control.Effect+module Control.Effect.Parameterised ((>>), PMonad(..), fail, ifThenElse) where -{-| Implements Bob Atkey's 'parametric monads', -    and also the Control.Monad.Indexed package, by emulating-    indexing by morphisms -}+-- Bye Monads... as we know them+import Prelude hiding (Monad(..)) -{-| Data type of morphisms -}-newtype T (i :: Morph * *) a = T a+-- Hello Parameterised Monads+class PMonad (pm :: k -> k -> * -> *) where+  -- Lift pure values into effect-invariant computations+  return :: a -> pm inv inv a -{-| Data type denoting either a morphisms with source and target types, or identity -}-data Morph a b = M a b | Id+  -- Sequentially compose effectful computations+  (>>=) :: pm pre interm t -> (t -> pm interm post t') -> pm pre post t' -instance Effect (T :: ((Morph * *) -> * -> *)) where-    type Unit T = Id-    type Plus T (M a b) (M c d) = M a d-    type Plus T Id (M a b) = M a b-    type Plus T (M a b) Id = M a b-    type Inv  T (M a b) (M c d) = c ~ d+-- Other boilerplate+(>>) :: PMonad pm => pm pre mid t -> pm mid post t' -> pm pre post t'+x >> y = x >>= const y -    return a = T a-    (T x) >>= k = let T y = k x in T y+fail :: String -> m inv inv a+fail = error++ifThenElse :: Bool -> a -> a -> a+ifThenElse True x _ = x+ifThenElse False _ y = y

@@ -0,0 +1,22 @@+-- For clarity in type classes instances+{-# LANGUAGE InstanceSigs #-}++module Control.Effect.Parameterised.AtomicState+        (get, put, Closed, Open, State(..)) where++-- Bye Monads... as we know them+import Prelude hiding (Monad(..))+-- Hello parameterised monads+import Control.Effect.Parameterised+import Control.Effect.Parameterised.State++newtype Closed s = Closed s deriving Show+newtype Open   s = Open s   deriving Show++-- get :: State s s+get :: State (Closed s) (Open s) s+get = State $ \(Closed s) -> (s, Open s)++-- put :: s -> State s ()+put :: t -> State (Open s) (Closed t) ()+put tx = State $ \(Open _) -> ((), Closed tx)

@@ -0,0 +1,29 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RebindableSyntax #-}++module Control.Effect.Parameterised.ExtensibleState+          (State(..), Get, Put, Update, get, put, modify+          , PMonad(..), (>>), ifThenElse, fail) where++import Prelude hiding (Monad(..))+import Control.Effect.Parameterised+import Control.Effect.Parameterised.State+import Data.Type.Map++-- Fine-grained get, put, and modify+get :: IsMember v t m => Var v -> State (Map m) (Map m) t+get v = State $ \s -> (lookp v s, s)++put :: Updatable v t m n => Var v -> t -> State (Map m) (Map n) ()+put v t = State $ \s -> ((), update s v t)++modify :: (IsMember v s m, Updatable v t m n) => Var v -> (s -> t) -> State (Map m) (Map n) ()+modify v f = do+  x <- get v+  put v (f x)++-- Aliases for our operations+type Get v t m = IsMember v t m+type Put v t m n = Updatable v t m n+type Update v t m = (Get v t m, Put v t m m)

@@ -0,0 +1,99 @@+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}++{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}++module Control.Effect.Parameterised.SafeFiles+         (openFile, hGetChar, hPutChar, hClose, hIsEOF, runSafeFiles+         , SafeFiles, SafeHandle, St+         , PMonad(..), (>>), ifThenElse, fail) where++-- Bye Monads... as we know them+import Prelude hiding (Monad(..))+import Control.Effect.Parameterised++-- Import qualified versions of standard code we want to wrap+import qualified Prelude as P+import qualified System.IO as IO++import GHC.TypeLits -- gives us type-level natural numbers++{-++-- openFile :: FilePath -> IOMode -> IO Handle+-- hGetChar :: Handle -> IO Char+-- hPutChar :: Handle -> Char -> IO ()+-- hClose :: Handle -> IO ()++-- hIsOpen :: Handle -> IO Bool+-- hIsClosed :: Handle -> IO Bool++-}++-- Wrap the IO monad+newtype SafeFiles pre post a = SafeFiles { unSafeFiles :: IO a }++instance PMonad SafeFiles where+   -- return :: a -> SafeFiles p p a+   return = SafeFiles . P.return+   -- (>>=) :: SafeFiles p q a -> (a -> SafeFiles q r b) -> SafeFiles p r b+   (SafeFiles m) >>= k = SafeFiles (m P.>>= (unSafeFiles . k))++-- Safe handlers are indexed by a (unique) number+newtype SafeHandle (n :: Nat) =+       SafeHandle { unsafeHandle :: IO.Handle }++-- Protocol states are a pair of a type-level nat and list of naturals+data St (n :: Nat) (opens :: [Nat])++-- openFile :: FilePath -> IOMode -> IO Handle+-- Opens a file, returns a handler with a fresh name+openFile ::+    IO.FilePath+ -> IO.IOMode+ -> SafeFiles (St h opens) (St (h + 1) (h ': opens)) (SafeHandle h)+openFile f mode = SafeFiles $ fmap SafeHandle (IO.openFile f mode)++-- hClose :: Handle -> IO ()+hClose :: Member h opens =>+     SafeHandle h+  -> SafeFiles (St n opens) (St n (Delete h opens)) ()+hClose (SafeHandle h) = SafeFiles (IO.hClose h)++-- Delete a handler name from a list+type family Delete (n :: Nat) (ns :: [Nat]) where+            Delete n '[] = '[]+            Delete n (n ': ns) = ns+            Delete n (m ': ns) = m ': Delete n ns++-- Membership predicate+class Member (x :: Nat) (xs :: [Nat]) where+instance {-# OVERLAPS #-} Member x (x ': xs) where+instance Member x xs => Member x (y ': xs)++-- hGetChar :: Handle -> IO Char+hGetChar :: Member h opens =>+     SafeHandle h+  -> SafeFiles (St n opens) (St n opens) Char+hGetChar (SafeHandle h) = SafeFiles (IO.hGetChar h)++-- hPutChar :: Handle -> Char -> IO ()+hPutChar :: Member h opens =>+     SafeHandle h+  -> Char -> SafeFiles (St n opens) (St n opens) ()+hPutChar (SafeHandle h) c = SafeFiles (IO.hPutChar h c)++-- hIsEOF :: Handler -> IO Bool+hIsEOF :: Member h opens =>+  SafeHandle h -> SafeFiles (St n opens) (St n opens) Bool+hIsEOF (SafeHandle h) = SafeFiles (IO.hIsEOF h)++-- Only allow running when every file is closed at the end+runSafeFiles :: SafeFiles (St 0 '[]) (St n '[]) () -> IO ()+runSafeFiles = unSafeFiles

@@ -0,0 +1,20 @@+{-# LANGUAGE InstanceSigs #-}++module Control.Effect.Parameterised.State where++-- Bye Monads... as we know them+import Prelude hiding (Monad(..))+import Control.Effect.Parameterised++newtype State s1 s2 a = State { runState :: s1 -> (a, s2) }++-- State parameterised monad+-- ... just like the+instance PMonad State where+  return :: a -> State s s a+  return x = State (\s -> (x, s))++  (>>=) :: State s1 s2 a -> (a -> State s2 s3 b) -> State s1 s3 b+  (State m) >>= k =+      State $ \s0 -> let (a, s1) = m s0+                         State m' = k a in m' s1

@@ -0,0 +1,25 @@+{-# LANGUAGE KindSignatures, TypeFamilies, ConstraintKinds, PolyKinds, DataKinds #-}++module Control.Effect.ParameterisedAsGraded where++import Control.Effect++{-| Implements Bob Atkey's 'parametric monads',+    and also the Control.Monad.Indexed package, by emulating+    indexing by morphisms -}++{-| Data type of morphisms -}+newtype T (i :: Morph * *) a = T a++{-| Data type denoting either a morphisms with source and target types, or identity -}+data Morph a b = M a b | Id++instance Effect (T :: ((Morph * *) -> * -> *)) where+    type Unit T = Id+    type Plus T (M a b) (M c d) = M a d+    type Plus T Id (M a b) = M a b+    type Plus T (M a b) Id = M a b+    type Inv  T (M a b) (M c d) = c ~ d++    return a = T a+    (T x) >>= k = let T y = k x in T y