effin 0.2.1.3 → 0.3.0.3

raw patch · 18 files changed

Files

LICENSE +30/−30
Setup.hs +2/−2
effin.cabal +3/−3
src/Control/Effect/Bracket.hs +6/−7
src/Control/Effect/Coroutine.hs +3/−3
src/Control/Effect/Exception.hs +12/−15
src/Control/Effect/Lift.hs +3/−3
src/Control/Effect/List.hs +8/−8
src/Control/Effect/Reader.hs +5/−6
src/Control/Effect/State.hs +6/−7
src/Control/Effect/Thread.hs +6/−7
src/Control/Effect/Witness.hs +3/−3
src/Control/Effect/Writer.hs +7/−6
src/Control/Monad/Effect.hs +206/−203
src/Data/Index.hs +11/−11
src/Data/Type/Nat.hs +2/−2
src/Data/Type/Row.hs +86/−86
src/Data/Union.hs +89/−89

LICENSE view

@@ -1,30 +1,30 @@-Copyright (c) 2014, Anthony Vandikas--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 Anthony Vandikas 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.+Copyright (c) 2014, Anthony Vandikas
+
+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 Anthony Vandikas 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.

Setup.hs view

@@ -1,2 +1,2 @@-import Distribution.Simple-main = defaultMain+import Distribution.Simple
+main = defaultMain

effin.cabal view

@@ -1,5 +1,5 @@ name:                effin
-version:             0.2.1.3
+version:             0.3.0.3
 synopsis:            A Typeable-free implementation of extensible effects
 homepage:            https://github.com/YellPika/effin
 license:             BSD3
@@ -11,7 +11,7 @@ build-type:          Simple
 cabal-version:       >=1.10
 description:
-  This package implements extensible effects, and alternative to monad
+  This package implements extensible effects, an alternative to monad
   transformers. The original paper can be found at
   <http://okmij.org/ftp/Haskell/extensible/exteff.pdf>. The main differences
   between this library and the one described in the paper are that this library
@@ -66,7 +66,7 @@     Data.Type.Nat
     Data.Union
 
-  build-depends: base >= 4.7 && < 4.8
+  build-depends: base >= 4.7 && < 4.11
   if flag(mtl)
     build-depends: mtl >= 2.1 && < 3

src/Control/Effect/Bracket.hs view

@@ -14,7 +14,6 @@     Handler, exceptAny, bracket, finally
 ) where
 
-import Control.Applicative ((<$>))
 import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
 import Data.Type.Equality ((:~:) (..), TestEquality (..))
 import Control.Effect.Witness
@@ -35,8 +34,8 @@ type instance Is Bracket f = IsBracket f
 
 type family IsBracket f where
-    IsBracket (Bracket s) = True
-    IsBracket f = False
+    IsBracket (Bracket s) = 'True
+    IsBracket f = 'False
 
 class MemberEffect Bracket (Bracket s) l => EffectBracket s l
 instance MemberEffect Bracket (Bracket s) l => EffectBracket s l
@@ -44,7 +43,7 @@ -- | Creates a new tag. The function parameter describes the error message that
 -- is shown in the case of an uncaught exception.
 newTag :: EffectBracket s l => (a -> String) -> Effect l (Tag s a)
-newTag toString = conceal $ Tag toString <$> rename BWitness newToken
+newTag toString = conceal $ fmap (Tag toString) (rename BWitness newToken)
 
 -- | Raises an exception of the specified class and value.
 raiseWith :: EffectBracket s l => Tag s b -> b -> Effect l a
@@ -66,7 +65,7 @@ -- because @h2@ could catch exceptions thrown by @h1@.
 exceptAny :: EffectBracket s l => Effect l a -> [Handler s l a] -> Effect l a
 exceptAny effect handlers = effect `exceptAll` \i x ->
-    let try (Handler j f) = (\Refl -> f x) <$> testEquality i j
+    let try (Handler j f) = fmap (\Refl -> f x) (testEquality i j)
         results = mapMaybe try handlers
     in fromMaybe (raiseWith i x) (listToMaybe results)
 
@@ -108,10 +107,10 @@ 
 -- | Executes a `Bracket` effect. The Rank-2 type ensures that `Tag`s do not
 -- escape their scope.
-runBracket :: (forall s. Effect (Bracket s :+ l) a) -> Effect l a
+runBracket :: (forall s. Effect (Bracket s ':+ l) a) -> Effect l a
 runBracket effect = runWitness (convert effect)
 
-convert :: Effect (Bracket s :+ l) a -> Effect (Witness s :+ l) a
+convert :: Effect (Bracket s ':+ l) a -> Effect (Witness s ':+ l) a
 convert =
     eliminate
         return

src/Control/Effect/Coroutine.hs view

@@ -19,8 +19,8 @@ type instance Is Coroutine f = IsCoroutine f
 
 type family IsCoroutine f where
-    IsCoroutine (Coroutine i o) = True
-    IsCoroutine f = False
+    IsCoroutine (Coroutine i o) = 'True
+    IsCoroutine f = 'False
 
 class MemberEffect Coroutine (Coroutine i o) l => EffectCoroutine i o l
 instance MemberEffect Coroutine (Coroutine i o) l => EffectCoroutine i o l
@@ -31,7 +31,7 @@ suspend = send . Coroutine id
 
 -- | Converts a `Coroutine` effect into an `Iterator`.
-runCoroutine :: Effect (Coroutine i o :+ l) a -> Effect l (Iterator i o l a)
+runCoroutine :: Effect (Coroutine i o ':+ l) a -> Effect l (Iterator i o l a)
 runCoroutine = eliminate (return . Done) (\(Coroutine f x) k -> return (Next (k . f) x))
 
 -- | A suspended computation.

src/Control/Effect/Exception.hs view

@@ -23,40 +23,37 @@ import Data.Type.Row
 import qualified Control.Monad.Error.Class as E
 
-instance (Member (Exception e) l, Exception e ~ InstanceOf Exception l) => E.MonadError e (Effect l) where
+instance (EffectBracket s l, Member (Exception s e) l, Exception s e ~ InstanceOf Exception l) => E.MonadError e (Effect l) where
     throwError = raise
     catchError = except
 #endif
 
 -- | An effect that describes the possibility of failure.
-data Exception e a = Raise e | Catch a (e -> a)
+newtype Exception s e a = Exception (Tag s e -> a)
 
 type instance Is Exception f = IsException f
 
 type family IsException f where
-    IsException (Exception e) = True
-    IsException f = False
+    IsException (Exception s e) = 'True
+    IsException f = 'False
 
-class MemberEffect Exception (Exception e) l => EffectException e l
-instance MemberEffect Exception (Exception e) l => EffectException e l
+class (EffectBracket s l, MemberEffect Exception (Exception s e) l) => EffectException s e l
+instance (EffectBracket s l, MemberEffect Exception (Exception s e) l) => EffectException s e l
 
 -- | Raises an exception.
-raise :: EffectException e l => e -> Effect l a
-raise = send . Raise
+raise :: EffectException s e l => e -> Effect l a
+raise e = sendEffect (Exception (\tag -> raiseWith tag e))
 
 -- | Handles an exception. Intended to be used in infix form.
 --
 -- > myComputation `except` \ex -> doSomethingWith ex
-except :: EffectException e l => Effect l a -> (e -> Effect l a) -> Effect l a
-except x f = sendEffect (Catch x f)
+except :: EffectException s e l => Effect l a -> (e -> Effect l a) -> Effect l a
+except x f = sendEffect (Exception (\tag -> exceptWith tag x f))
 
 -- | Completely handles an exception effect.
-runException :: (EffectBracket s l, Show e) => Effect (Exception e :+ l) a -> Effect l (Either e a)
+runException :: (EffectBracket s l, Show e) => Effect (Exception s e ':+ l) a -> Effect l (Either e a)
 runException effect = do
     tag <- newTag show
     exceptWith tag
-        (eliminate (return . Right) (bind tag) effect)
+        (eliminate (return . Right) (\(Exception f) k -> k (f tag)) effect)
         (return . Left)
-  where
-    bind tag (Raise e) _ = raiseWith tag e
-    bind tag (Catch x f) k = exceptWith tag (k x) (k . f)

src/Control/Effect/Lift.hs view

@@ -30,8 +30,8 @@ type instance Is Lift f = IsLift f
 
 type family IsLift f where
-    IsLift (Lift m) = True
-    IsLift f = False
+    IsLift (Lift m) = 'True
+    IsLift f = 'False
 
 class (Monad m, MemberEffect Lift (Lift m) l) => EffectLift m l
 instance (Monad m, MemberEffect Lift (Lift m) l) => EffectLift m l
@@ -46,7 +46,7 @@ 
 -- | Converts a computation containing only monadic
 -- effects into a monadic computation.
-runLift :: Monad m => Effect (Lift m :+ Nil) a -> m a
+runLift :: Monad m => Effect (Lift m ':+ 'Nil) a -> m a
 runLift = runEffect . eliminate
     (return . return)
     (\(Lift m) k -> return $ m >>= runEffect . k)

src/Control/Effect/List.hs view

@@ -16,7 +16,7 @@ 
 import Control.Monad.Effect
 import Control.Arrow (second)
-import Control.Applicative (Alternative (..), (<$>))
+import Control.Applicative (Alternative (..))
 import Control.Monad (MonadPlus (..), (<=<), join)
 
 -- | A nondeterminism (backtracking) effect.
@@ -25,8 +25,8 @@ type instance Is List f = IsList f
 
 type family IsList f where
-    IsList List = True
-    IsList f = False
+    IsList List = 'True
+    IsList f = 'False
 
 class Member List l => EffectList l
 instance Member List l => EffectList l
@@ -45,8 +45,8 @@ 
 -- | Obtains all possible values from a computation
 -- parameterized by a nondeterminism effect.
-runList :: Effect (List :+ l) a -> Effect l [a]
-runList = eliminate (return . return) (\(List xs) k -> concat <$> mapM k xs)
+runList :: Effect (List ':+ l) a -> Effect l [a]
+runList = eliminate (return . return) (\(List xs) k -> fmap concat (mapM k xs))
 
 instance EffectList l => Alternative (Effect l) where
     empty = never
@@ -76,7 +76,7 @@ 
 -- | Handles the `Cut` effect. `cut`s have no effect beyond
 -- the scope of the computation passed to this function.
-runCut :: EffectList l => Effect (Cut :+ l) a -> Effect l a
+runCut :: EffectList l => Effect (Cut ':+ l) a -> Effect l a
 runCut = choose . snd <=< reifyCut
   where
     -- Gather the results of a computation into a list (like in runList), but
@@ -86,7 +86,7 @@     -- get a list of computations. We can now execute each computation one by
     -- one, and inspect the Bool after each computation to determine when we
     -- should stop.
-    reifyCut :: EffectList l => Effect (Cut :+ l) a -> Effect l (Bool, [a])
+    reifyCut :: EffectList l => Effect (Cut ':+ l) a -> Effect l (Bool, [a])
     reifyCut =
         intercept return (\(List xs) k -> runAll (map k xs)) .
         eliminate
@@ -98,4 +98,4 @@         (cutRequested, x') <- x
         if cutRequested
         then return (True, x')
-        else second (x' ++) <$> runAll xs
+        else fmap (second (x' ++)) (runAll xs)

src/Control/Effect/Reader.hs view

@@ -20,7 +20,6 @@ 
 import Control.Effect.State
 import Control.Monad.Effect
-import Control.Applicative ((<$>))
 
 #ifdef MTL
 import Data.Type.Row
@@ -39,8 +38,8 @@ type instance Is Reader f = IsReader f
 
 type family IsReader f where
-    IsReader (Reader r) = True
-    IsReader f = False
+    IsReader (Reader r) = 'True
+    IsReader f = 'False
 
 class MemberEffect Reader (Reader r) l => EffectReader r l
 instance MemberEffect Reader (Reader r) l => EffectReader r l
@@ -51,7 +50,7 @@ 
 -- | Retrieves a value that is a function of the current environment.
 asks :: EffectReader r l => (r -> a) -> Effect l a
-asks f = f <$> ask
+asks f = fmap f ask
 
 -- | Runs a computation with a modified environment.
 local :: EffectReader r l => (r -> r) -> Effect l a -> Effect l a
@@ -61,12 +60,12 @@ 
 -- | Executes a reader computation which obtains
 -- its environment value from a state effect.
-stateReader :: EffectState s l => Effect (Reader s :+ l) a -> Effect l a
+stateReader :: EffectState s l => Effect (Reader s ':+ l) a -> Effect l a
 stateReader = eliminate return (\Ask k -> get >>= k)
 
 -- | Completely handles a `Reader` effect by providing an
 -- environment value to be used throughout the computation.
-runReader :: r -> Effect (Reader r :+ l) a -> Effect l a
+runReader :: r -> Effect (Reader r ':+ l) a -> Effect l a
 runReader env = eliminate return (bind env)
 
 bind :: r -> Reader r a -> (a -> s) -> s

src/Control/Effect/State.hs view

@@ -19,7 +19,6 @@     state, withState
 ) where
 
-import Control.Applicative ((<$>))
 import Control.Monad.Effect
 
 #ifdef MTL
@@ -38,8 +37,8 @@ type instance Is State f = IsState f
 
 type family IsState f where
-    IsState (State s) = True
-    IsState f = False
+    IsState (State s) = 'True
+    IsState f = 'False
 
 class MemberEffect State (State s) l => EffectState s l
 instance MemberEffect State (State s) l => EffectState s l
@@ -50,7 +49,7 @@ 
 -- | Gets a value that is a function of the current state.
 gets :: EffectState s l => (s -> a) -> Effect l a
-gets f = f <$> get
+gets f = fmap f get
 
 -- | Replaces the current state.
 put :: EffectState s l => s -> Effect l ()
@@ -79,15 +78,15 @@ 
 -- | Completely handles a `State` effect by providing an
 -- initial state, and making the final state explicit.
-runState :: s -> Effect (State s :+ l) a -> Effect l (a, s)
+runState :: s -> Effect (State s ':+ l) a -> Effect l (a, s)
 runState = flip $ eliminate
     (\x s -> return (x, s))
     (\(State f) k s -> let (x, s') = f s in k x s')
 
 -- | Completely handles a `State` effect, and discards the final state.
-evalState :: s -> Effect (State s :+ l) a -> Effect l a
+evalState :: s -> Effect (State s ':+ l) a -> Effect l a
 evalState s = fmap fst . runState s
 
 -- | Completely handles a `State` effect, and discards the final value.
-execState :: s -> Effect (State s :+ l) a -> Effect l s
+execState :: s -> Effect (State s ':+ l) a -> Effect l s
 execState s = fmap snd . runState s

src/Control/Effect/Thread.hs view

@@ -12,7 +12,6 @@ 
 import Control.Effect.Lift
 import Control.Monad.Effect
-import Control.Applicative ((<$>))
 import Control.Monad (void)
 import qualified Control.Concurrent as IO
 
@@ -36,7 +35,7 @@ 
 -- | Executes a threaded computation synchronously.
 -- Completes when the main thread exits.
-runMain :: Effect (Thread :+ l) () -> Effect l ()
+runMain :: Effect (Thread ':+ l) () -> Effect l ()
 runMain = run [] . toAST
   where
     run auxThreads thread = do
@@ -55,12 +54,12 @@         result <- thread
         case result of
             AbortAST -> runAll xs
-            YieldAST k -> (k:) <$> runAll xs
-            ForkAST child parent -> (parent:) <$> runAll (child:xs)
+            YieldAST k -> fmap (k:) (runAll xs)
+            ForkAST child parent -> fmap (parent:) (runAll (child:xs))
 
 -- | Executes a threaded computation synchronously.
 -- Does not complete until all threads have exited.
-runSync :: Effect (Thread :+ l) () -> Effect l ()
+runSync :: Effect (Thread ':+ l) () -> Effect l ()
 runSync = run . (:[]) . toAST
   where
     run [] = return ()
@@ -72,7 +71,7 @@             ForkAST child parent -> run (child:xs ++ [parent])
 
 -- | Executes a threaded computation asynchronously.
-runAsync :: Effect (Thread :+ Lift IO :+ Nil) () -> IO ()
+runAsync :: Effect (Thread ':+ Lift IO ':+ 'Nil) () -> IO ()
 runAsync = run . toAST
   where
     run thread = do
@@ -94,7 +93,7 @@ -- Converts a threaded computation into its corresponding AST. This allows
 -- different backends to interpret calls to fork/yield/abort as they please. See
 -- the implementations of runAsync, runSync, and runMain.
-toAST :: Effect (Thread :+ l) () -> Effect l (ThreadAST l)
+toAST :: Effect (Thread ':+ l) () -> Effect l (ThreadAST l)
 toAST = eliminate (\_ -> return AbortAST) bind
   where
     bind Abort _ = return AbortAST

src/Control/Effect/Witness.hs view

@@ -40,8 +40,8 @@ type instance Is Witness f = IsWitness f
 
 type family IsWitness f where
-    IsWitness (Witness s) = True
-    IsWitness f = False
+    IsWitness (Witness s) = 'True
+    IsWitness f = 'False
 
 class MemberEffect Witness (Witness s) l => EffectWitness s l
 instance MemberEffect Witness (Witness s) l => EffectWitness s l
@@ -56,7 +56,7 @@ 
 -- | Completely handles a `Witness` effect. The Rank-2 quantifier ensures that
 -- unique identifiers cannot escape the context in which they were created.
-runWitness :: (forall s. Effect (Witness s :+ l) a) -> Effect l a
+runWitness :: (forall s. Effect (Witness s ':+ l) a) -> Effect l a
 runWitness effect = run effect
   where
     run = eliminate return $ \NewToken k ->

src/Control/Effect/Writer.hs view

@@ -19,9 +19,10 @@ ) where
 
 import Control.Monad.Effect
-import Control.Applicative ((<$>))
 import Control.Arrow (second)
+#if !MIN_VERSION_base(4, 8, 0)
 import Data.Monoid (Monoid (..))
+#endif
 import Control.Effect.State
 
 #ifdef MTL
@@ -41,8 +42,8 @@ type instance Is Writer f = IsWriter f
 
 type family IsWriter f where
-    IsWriter (Writer w) = True
-    IsWriter f = False
+    IsWriter (Writer w) = 'True
+    IsWriter f = 'False
 
 class (Monoid w, MemberEffect Writer (Writer w) l) => EffectWriter w l
 instance (Monoid w, MemberEffect Writer (Writer w) l) => EffectWriter w l
@@ -79,17 +80,17 @@     return (a, f)
 
 -- | Executes a writer computation which sends its output to a state effect.
-stateWriter :: (Monoid s, EffectState s l) => Effect (Writer s :+ l) a -> Effect l a
+stateWriter :: (Monoid s, EffectState s l) => Effect (Writer s ':+ l) a -> Effect l a
 stateWriter = eliminate return (\(Tell l) k -> modify (mappend l) >> k ())
 
 -- | Completely handles a writer effect. The writer value must be a `Monoid`.
 -- `mempty` is used as an initial value, and `mappend` is used to combine values.
 -- Returns the result of the computation and the final output value.
-runWriter :: Monoid w => Effect (Writer w :+ l) a -> Effect l (a, w)
+runWriter :: Monoid w => Effect (Writer w ':+ l) a -> Effect l (a, w)
 runWriter = eliminate point bind
 
 point :: Monoid w => a -> Effect l (a, w)
 point x = return (x, mempty)
 
 bind :: Monoid w => Writer w a -> (a -> Effect l (b, w)) -> Effect l (b, w)
-bind (Tell l) k = second (mappend l) <$> k ()
+bind (Tell l) k = second (mappend l) `fmap` k ()

src/Control/Monad/Effect.hs view

@@ -1,203 +1,206 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--module Control.Monad.Effect (-    -- * The Effect Monad-    Effect, runEffect,-    send, sendEffect,--    -- * Effect Handlers-    Effectful (EffectsOf),--    eliminate, intercept,-    extend, enable,-    conceal, reveal, rename,-    swap, rotate,-    mask, unmask,--    -- * Unions-    Union, flatten, unflatten,--    -- * Membership-    Member, MemberEffect, Is,--    -- * Effect Rows-    Row (..), type (:++),-    KnownLength, Inclusive-) where--import Data.Union (Union)-import qualified Data.Union as Union--import Data.Type.Row--import Control.Applicative (Applicative (..))-import Control.Monad (join)---- | An effectful computation. An @Effect l a@ may perform any of the effects--- specified by the list of effects @l@ before returning a result of type @a@.--- The definition is isomorphic to the following GADT:------ @--- data Effect l a where---     Done :: a -> Effect l a---     Side :: `Union` l (Effect l a) -> Effect l a--- @-newtype Effect l a = Effect (forall r. (a -> r) -> (forall b. Union l b -> (b -> r) -> r) -> r)--unEffect :: (a -> r) -> (forall b. Union l b -> (b -> r) -> r) -> Effect l a -> r-unEffect point bind (Effect f) = f point bind--instance Functor (Effect l) where-    fmap f (Effect g) = Effect $ \point -> g (point . f)--instance Applicative (Effect l) where-    pure x = Effect $ \point _ -> point x-    Effect f <*> Effect x = Effect $ \point bind ->-        f (\f' -> x (point . f') bind) bind--instance Monad (Effect l) where-    return = pure-    Effect f >>= g = Effect $ \point bind ->-        f (unEffect point bind . g) bind---- | Converts an computation that produces no effects into a regular value.-runEffect :: Effect Nil a -> a-runEffect (Effect f) = f id Union.absurd---- | Executes an effect of type @f@ that produces a return value of type @a@.-send :: Member f l => f a -> Effect l a-send x = Effect $ \point bind -> bind (Union.inject x) point---- | Executes an effect of type @f@ that produces a return value of type @r@.--- Note that a specific instance of this function is of type--- @Member f l => f (Effect l a) -> Effect l a@, which allows users--- to send effects parameterized by effects.-sendEffect :: (Member f l, Effectful l r) => f r -> r-sendEffect x = relay (Union.inject x) id---- | The class of types which result in an effect. That is:------ > Effect l r--- > a -> Effect l r--- > a -> b -> Effect l r--- > ...-class l ~ EffectsOf r => Effectful l r where-    -- | Determines the effects associated with the return type of a function.-    type family EffectsOf r :: Row (* -> *)--    relay :: Union l a -> (a -> r) -> r--    -- Prevents the `Minimal Complete Definition` box from showing.-    relay = undefined--instance Effectful l (Effect l a) where-    type EffectsOf (Effect l a) = l-    relay u f = join $ Effect $ \point bind -> bind u (point . f)--instance Effectful l r => Effectful l (a -> r) where-    type EffectsOf (a -> r) = EffectsOf r-    relay u f y = relay u (\x -> f x y)---- | Handles an effect without eliminating it. The second function parameter is--- passed an effect value and a continuation function.------ The most common instantiation of this function is:------ > (a -> Effect l b) -> (f (Effect l b) -> Effect l b) -> Effect l a -> Effect l b-intercept :: (Effectful l r, Member f l) => (a -> r) -> (forall b. f b -> (b -> r) -> r) -> Effect l a -> r-intercept point bind = unEffect point $ \u -> maybe (relay u) bind (Union.project u)---- | Completely handles an effect. The second function parameter is passed an--- effect value and a continuation function.------ The most common instantiation of this function is:------ > (a -> Effect l b) -> (f (Effect l b) -> Effect l b) -> Effect (f ': l) a -> Effect l b-eliminate :: Effectful l r => (a -> r) -> (forall b. f b -> (b -> r) -> r) -> Effect (f :+ l) a -> r-eliminate point bind = unEffect point (either bind relay . Union.pop)---- | Adds an arbitrary effect to the head of the effect list.-extend :: Effect l a -> Effect (f :+ l) a-extend = translate Union.push---- | Enables an effect that was previously disabled.-enable :: Effect (f :- l) a -> Effect l a-enable = translate Union.enable---- | Hides an effect @f@ by translating each instance of the effect into an--- equivalent effect further into the effect list.------ prop> conceal = eliminate return (\x k -> send x >>= k)-conceal :: Member f l => Effect (f :+ l) a -> Effect l a-conceal = translate Union.conceal---- | Hides an effect @f@ by translating each instance of the effect into an--- equivalent effect at the head of the effect list.-reveal :: Member f l => Effect l a -> Effect (f :+ l) a-reveal = translate Union.reveal---- | Translates the first effect in the effect list into another effect.------ prop> rename f = eliminate return (\x k -> send (f x) >>= k) . swap . extend-rename :: (forall r. f r -> g r) -> Effect (f :+ l) a -> Effect (g :+ l) a-rename f = translate (either (Union.inject . f) Union.push . Union.pop)---- | Reorders the first two effects in a computation.-swap :: Effect (f :+ g :+ l) a -> Effect (g :+ f :+ l) a-swap = translate Union.swap---- | Rotates the first three effects in a computation.-rotate :: Effect (f :+ g :+ h :+ l) a -> Effect (g :+ h :+ f :+ l) a-rotate = translate Union.rotate---- | Distributes the sub-effects of a `Union` effect across a computation.-flatten :: Inclusive l => Effect (Union l :+ m) a -> Effect (l :++ m) a-flatten = translate Union.flatten---- | Collects some effects in a computation into a `Union` effect.-unflatten :: KnownLength l => Effect (l :++ m) a -> Effect (Union l :+ m) a-unflatten = translate Union.unflatten--translate :: (forall r. Union l r -> Union m r) -> Effect l a -> Effect m a-translate f = unEffect return (relay . f)---- | Converts a set of effects @l@ into a single effect @f@.------ @ mask f = `conceal` . `rename` f . `unflatten` @-mask :: (KnownLength l, Member f m) => (forall r. Union l r -> f r) -> Effect (l :++ m) a -> Effect m a-mask f = conceal . rename f . unflatten---- | Converts an effect @f@ into a set of effects @l@.------ @ unmask f = `flatten` . `rename` f . `reveal` @-unmask :: (Inclusive l, Member f m) => (forall r. f r -> Union l r) -> Effect m a -> Effect (l :++ m) a-unmask f = flatten . rename f . reveal---- | A refined `Member`ship constraint that can infer @f@ from @l@, given--- @name@. In order for this to be used, @`Is` name f@ must be defined.--- For example:------ > data Reader r a = ...--- >--- > type instance Is Reader f = IsReader f--- >--- > type IsReader f where--- >     IsReader (Reader r) = True--- >     IsReader f = False--- >--- > type ReaderEffect r l = MemberEffect Reader (Reader r) l--- >--- > ask :: ReaderEffect r l => Effect l r--- > ask = ...------ Given the constraint @ReaderEffect r l@ in the above example, @r@ can be--- inferred from @l@.-class (Member f l, f ~ InstanceOf name l) => MemberEffect name f l-instance (Member f l, f ~ InstanceOf name l) => MemberEffect name f l+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Control.Monad.Effect (
+    -- * The Effect Monad
+    Effect, runEffect,
+    send, sendEffect,
+
+    -- * Effect Handlers
+    Effectful (EffectsOf),
+
+    eliminate, intercept,
+    extend, enable,
+    conceal, reveal, rename,
+    swap, rotate,
+    mask, unmask,
+
+    -- * Unions
+    Union, flatten, unflatten,
+
+    -- * Membership
+    Member, MemberEffect, Is,
+
+    -- * Effect Rows
+    Row (..), type (:++),
+    KnownLength, Inclusive
+) where
+
+import Data.Union (Union)
+import qualified Data.Union as Union
+
+import Data.Type.Row
+
+#if !MIN_VERSION_base(4,8,0)
+import Control.Applicative (Applicative (..))
+#endif
+import Control.Monad (join)
+
+-- | An effectful computation. An @Effect l a@ may perform any of the effects
+-- specified by the list of effects @l@ before returning a result of type @a@.
+-- The definition is isomorphic to the following GADT:
+--
+-- @
+-- data Effect l a where
+--     Done :: a -> Effect l a
+--     Side :: `Union` l (Effect l a) -> Effect l a
+-- @
+newtype Effect l a = Effect (forall r. (a -> r) -> (forall b. Union l b -> (b -> r) -> r) -> r)
+
+unEffect :: (a -> r) -> (forall b. Union l b -> (b -> r) -> r) -> Effect l a -> r
+unEffect point bind (Effect f) = f point bind
+
+instance Functor (Effect l) where
+    fmap f (Effect g) = Effect $ \point -> g (point . f)
+
+instance Applicative (Effect l) where
+    pure x = Effect $ \point _ -> point x
+    Effect f <*> Effect x = Effect $ \point bind ->
+        f (\f' -> x (point . f') bind) bind
+
+instance Monad (Effect l) where
+    return = pure
+    Effect f >>= g = Effect $ \point bind ->
+        f (unEffect point bind . g) bind
+
+-- | Converts an computation that produces no effects into a regular value.
+runEffect :: Effect 'Nil a -> a
+runEffect (Effect f) = f id Union.absurd
+
+-- | Executes an effect of type @f@ that produces a return value of type @a@.
+send :: Member f l => f a -> Effect l a
+send x = Effect $ \point bind -> bind (Union.inject x) point
+
+-- | Executes an effect of type @f@ that produces a return value of type @r@.
+-- Note that a specific instance of this function is of type
+-- @Member f l => f (Effect l a) -> Effect l a@, which allows users
+-- to send effects parameterized by effects.
+sendEffect :: (Member f l, Effectful l r) => f r -> r
+sendEffect x = relay (Union.inject x) id
+
+-- | The class of types which result in an effect. That is:
+--
+-- > Effect l r
+-- > a -> Effect l r
+-- > a -> b -> Effect l r
+-- > ...
+class l ~ EffectsOf r => Effectful l r where
+    -- | Determines the effects associated with the return type of a function.
+    type family EffectsOf r :: Row (* -> *)
+
+    relay :: Union l a -> (a -> r) -> r
+
+    -- Prevents the `Minimal Complete Definition` box from showing.
+    relay = undefined
+
+instance Effectful l (Effect l a) where
+    type EffectsOf (Effect l a) = l
+    relay u f = join $ Effect $ \point bind -> bind u (point . f)
+
+instance Effectful l r => Effectful l (a -> r) where
+    type EffectsOf (a -> r) = EffectsOf r
+    relay u f y = relay u (\x -> f x y)
+
+-- | Handles an effect without eliminating it. The second function parameter is
+-- passed an effect value and a continuation function.
+--
+-- The most common instantiation of this function is:
+--
+-- > (a -> Effect l b) -> (f (Effect l b) -> Effect l b) -> Effect l a -> Effect l b
+intercept :: (Effectful l r, Member f l) => (a -> r) -> (forall b. f b -> (b -> r) -> r) -> Effect l a -> r
+intercept point bind = unEffect point $ \u -> maybe (relay u) bind (Union.project u)
+
+-- | Completely handles an effect. The second function parameter is passed an
+-- effect value and a continuation function.
+--
+-- The most common instantiation of this function is:
+--
+-- > (a -> Effect l b) -> (f (Effect l b) -> Effect l b) -> Effect (f ': l) a -> Effect l b
+eliminate :: Effectful l r => (a -> r) -> (forall b. f b -> (b -> r) -> r) -> Effect (f ':+ l) a -> r
+eliminate point bind = unEffect point (either bind relay . Union.pop)
+
+-- | Adds an arbitrary effect to the head of the effect list.
+extend :: Effect l a -> Effect (f ':+ l) a
+extend = translate Union.push
+
+-- | Enables an effect that was previously disabled.
+enable :: Effect (f ':- l) a -> Effect l a
+enable = translate Union.enable
+
+-- | Hides an effect @f@ by translating each instance of the effect into an
+-- equivalent effect further into the effect list.
+--
+-- prop> conceal = eliminate return (\x k -> send x >>= k)
+conceal :: Member f l => Effect (f ':+ l) a -> Effect l a
+conceal = translate Union.conceal
+
+-- | Hides an effect @f@ by translating each instance of the effect into an
+-- equivalent effect at the head of the effect list.
+reveal :: Member f l => Effect l a -> Effect (f ':+ l) a
+reveal = translate Union.reveal
+
+-- | Translates the first effect in the effect list into another effect.
+--
+-- prop> rename f = eliminate return (\x k -> send (f x) >>= k) . swap . extend
+rename :: (forall r. f r -> g r) -> Effect (f ':+ l) a -> Effect (g ':+ l) a
+rename f = translate (either (Union.inject . f) Union.push . Union.pop)
+
+-- | Reorders the first two effects in a computation.
+swap :: Effect (f ':+ g ':+ l) a -> Effect (g ':+ f ':+ l) a
+swap = translate Union.swap
+
+-- | Rotates the first three effects in a computation.
+rotate :: Effect (f ':+ g ':+ h ':+ l) a -> Effect (g ':+ h ':+ f ':+ l) a
+rotate = translate Union.rotate
+
+-- | Distributes the sub-effects of a `Union` effect across a computation.
+flatten :: Inclusive l => Effect (Union l ':+ m) a -> Effect (l :++ m) a
+flatten = translate Union.flatten
+
+-- | Collects some effects in a computation into a `Union` effect.
+unflatten :: KnownLength l => Effect (l :++ m) a -> Effect (Union l ':+ m) a
+unflatten = translate Union.unflatten
+
+translate :: (forall r. Union l r -> Union m r) -> Effect l a -> Effect m a
+translate f = unEffect return (relay . f)
+
+-- | Converts a set of effects @l@ into a single effect @f@.
+--
+-- @ mask f = `conceal` . `rename` f . `unflatten` @
+mask :: (KnownLength l, Member f m) => (forall r. Union l r -> f r) -> Effect (l :++ m) a -> Effect m a
+mask f = conceal . rename f . unflatten
+
+-- | Converts an effect @f@ into a set of effects @l@.
+--
+-- @ unmask f = `flatten` . `rename` f . `reveal` @
+unmask :: (Inclusive l, Member f m) => (forall r. f r -> Union l r) -> Effect m a -> Effect (l :++ m) a
+unmask f = flatten . rename f . reveal
+
+-- | A refined `Member`ship constraint that can infer @f@ from @l@, given
+-- @name@. In order for this to be used, @`Is` name f@ must be defined.
+-- For example:
+--
+-- > data Reader r a = ...
+-- >
+-- > type instance Is Reader f = IsReader f
+-- >
+-- > type IsReader f where
+-- >     IsReader (Reader r) = True
+-- >     IsReader f = False
+-- >
+-- > type ReaderEffect r l = MemberEffect Reader (Reader r) l
+-- >
+-- > ask :: ReaderEffect r l => Effect l r
+-- > ask = ...
+--
+-- Given the constraint @ReaderEffect r l@ in the above example, @r@ can be
+-- inferred from @l@.
+class (Member f l, f ~ InstanceOf name l) => MemberEffect name f l
+instance (Member f l, f ~ InstanceOf name l) => MemberEffect name f l

src/Data/Index.hs view

@@ -29,16 +29,16 @@         | i == j = Just (unsafeCoerce Refl)
         | otherwise = Nothing
 
-zero :: Index (e :+ l) e
+zero :: Index (e ':+ l) e
 zero = Index 0
 
 index :: forall e l. Member e l => Index l e
 index = Index $ natVal (Proxy :: Proxy (IndexOf e l))
 
-absurd :: Index Nil e -> a
+absurd :: Index 'Nil e -> a
 absurd (Index i) = i `seq` error "absurd Index"
 
-trivial :: Index (e :+ Nil) f -> f :~: e
+trivial :: Index (e ':+ 'Nil) f -> f :~: e
 trivial (Index i)
     | i == 0 = unsafeCoerce Refl
     | otherwise = error "non-trivial Index"
@@ -46,39 +46,39 @@ size :: forall l proxy. KnownLength l => proxy l -> Integer
 size _ = natVal (Proxy :: Proxy (Length l))
 
-push :: Index l e -> Index (f :+ l) e
+push :: Index l e -> Index (f ':+ l) e
 push (Index i) = Index (i + 1)
 
-pop :: Index (f :+ l) e -> Index l e
+pop :: Index (f ':+ l) e -> Index l e
 pop (Index i) = Index (i - 1)
 
-disable :: Index l e -> Index (f :- l) e
+disable :: Index l e -> Index (f ':- l) e
 disable (Index i) = Index (i + 1)
 
-enable :: Index (f :- l) e -> Index l e
+enable :: Index (f ':- l) e -> Index l e
 enable (Index i) = Index (i - 1)
 
-conceal :: forall e f l. Member f l => Index (f :+ l) e -> Index l e
+conceal :: forall e f l. Member f l => Index (f ':+ l) e -> Index l e
 conceal (Index i)
     | i == 0 = Index j
     | otherwise = Index (i - 1)
   where
     Index j = index :: Index l f
 
-reveal :: forall e f l. Member f l => Index l e -> Index (f :+ l) e
+reveal :: forall e f l. Member f l => Index l e -> Index (f ':+ l) e
 reveal (Index i)
     | i == j = Index 0
     | otherwise = Index (i + 1)
   where
     Index j = index :: Index l f
 
-swap :: Index (e :+ f :+ l) g -> Index (f :+ e :+ l) g
+swap :: Index (e ':+ f ':+ l) g -> Index (f ':+ e ':+ l) g
 swap (Index i)
     | i == 0 = Index 1
     | i == 1 = Index 0
     | otherwise = Index i
 
-rotate :: Index (e :+ f :+ g :+ l) h -> Index (f :+ g :+ e :+ l) h
+rotate :: Index (e ':+ f ':+ g ':+ l) h -> Index (f ':+ g ':+ e ':+ l) h
 rotate (Index i)
     | i == 0 = Index 2
     | i == 1 = Index 0

src/Data/Type/Nat.hs view

@@ -13,8 +13,8 @@ class KnownNat (n :: Nat) where
     natVal :: proxy n -> Integer
 
-instance KnownNat Zero where
+instance KnownNat 'Zero where
     natVal _ = 0
 
-instance KnownNat n => KnownNat (Succ n) where
+instance KnownNat n => KnownNat ('Succ n) where
     natVal _ = 1 + natVal (Proxy :: Proxy n)

src/Data/Type/Row.hs view

@@ -1,86 +1,86 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}--module Data.Type.Row (-    Row (..), (:++),-    Length, KnownLength,-    IndexOf, Member,-    Inclusive,-    Is, InstanceOf-) where--import Data.Type.Nat-import Data.Type.Bool (If)--infixr 5 :+, :-, :++---- | A type level list with explicit removals.-data Row a-    = Nil        -- ^ The empty list.-    | a :+ Row a -- ^ Prepends an element (cons).-    | a :- Row a -- ^ Deletes the first instance an element.---- | Appends two type level `Row`s.-type family l :++ m where-    Nil :++ l = l-    (e :+ l) :++ m = e :+ l :++ m-    (e :- l) :++ m = e :- l :++ m---- | Returns the length of the `Row` @l@.-type family Length l where-    Length Nil = Zero-    Length (h :+ t) = Succ (Length t)-    Length (h :- t) = Succ (Length t)---- | The class of `Row`s with statically known lengths.-class KnownNat (Length l) => KnownLength l-instance KnownNat (Length l) => KnownLength l---- | Returns the index of the first instance of @e@ in the `Row` @l@.-type IndexOf e l = NthIndexOf Zero e l--type family NthIndexOf n e l where-    NthIndexOf Zero     e (e :+ l) = Zero-    NthIndexOf (Succ n) e (e :+ l) = Succ (NthIndexOf n e l)-    NthIndexOf n        e (f :+ l) = Succ (NthIndexOf n e l)-    NthIndexOf n        e (e :- l) = Succ (NthIndexOf (Succ n) e l)-    NthIndexOf n        e (f :- l) = Succ (NthIndexOf n e l)---- | A constraint specifying that @e@ is a member of the `Row` @l@.-class KnownNat (IndexOf e l) => Member e l-instance KnownNat (IndexOf e l) => Member e l---- | The class of `Row`s that do not contain deletions (`:-`).-class KnownLength l => Inclusive l-instance Inclusive Nil-instance Inclusive l => Inclusive (e :+ l)---- | Returns a boolean value indicating whether @f@ belongs to the group of--- effects identified by @name@. This allows `MemberEffect` to infer the--- associated types for arbitrary effects.-type family Is (name :: k) (f :: * -> *) :: Bool--type InstanceOf name l = InstanceOfNone name '[] l---- Any instance of name in l but not in ex.-type family InstanceOfNone name ex l where-    InstanceOfNone name ex (f :- l) = InstanceOfNone name (f ': ex) l-    InstanceOfNone name ex (f :+ l) =-        If (Is name f)-            (If (Elem f ex) (InstanceOfNone name (Remove f ex) l) f)-            (InstanceOfNone name ex l)--type family Elem e l where-    Elem e '[] = False-    Elem e (e ': l) = True-    Elem e (f ': l) = Elem e l--type family Remove e l where-    Remove e (e ': l) = l-    Remove e (f ': l) = f ': Remove e l+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Type.Row (
+    Row (..), (:++),
+    Length, KnownLength,
+    IndexOf, Member,
+    Inclusive,
+    Is, InstanceOf
+) where
+
+import Data.Type.Nat
+import Data.Type.Bool (If)
+
+infixr 5 :+, :-, :++
+
+-- | A type level list with explicit removals.
+data Row a
+    = Nil        -- ^ The empty list.
+    | a :+ Row a -- ^ Prepends an element (cons).
+    | a :- Row a -- ^ Deletes the first instance an element.
+
+-- | Appends two type level `Row`s.
+type family l :++ m where
+    'Nil :++ l = l
+    (e ':+ l) :++ m = e ':+ l :++ m
+    (e ':- l) :++ m = e ':- l :++ m
+
+-- | Returns the length of the `Row` @l@.
+type family Length l where
+    Length 'Nil = 'Zero
+    Length (h ':+ t) = 'Succ (Length t)
+    Length (h ':- t) = 'Succ (Length t)
+
+-- | The class of `Row`s with statically known lengths.
+class KnownNat (Length l) => KnownLength l
+instance KnownNat (Length l) => KnownLength l
+
+-- | Returns the index of the first instance of @e@ in the `Row` @l@.
+type IndexOf e l = NthIndexOf 'Zero e l
+
+type family NthIndexOf n e l where
+    NthIndexOf 'Zero     e (e ':+ l) = 'Zero
+    NthIndexOf ('Succ n) e (e ':+ l) = 'Succ (NthIndexOf n e l)
+    NthIndexOf n         e (f ':+ l) = 'Succ (NthIndexOf n e l)
+    NthIndexOf n         e (e ':- l) = 'Succ (NthIndexOf ('Succ n) e l)
+    NthIndexOf n         e (f ':- l) = 'Succ (NthIndexOf n e l)
+
+-- | A constraint specifying that @e@ is a member of the `Row` @l@.
+class KnownNat (IndexOf e l) => Member e l
+instance KnownNat (IndexOf e l) => Member e l
+
+-- | The class of `Row`s that do not contain deletions (`':-`).
+class KnownLength l => Inclusive l
+instance Inclusive 'Nil
+instance Inclusive l => Inclusive (e ':+ l)
+
+-- | Returns a boolean value indicating whether @f@ belongs to the group of
+-- effects identified by @name@. This allows `MemberEffect` to infer the
+-- associated types for arbitrary effects.
+type family Is (name :: k) (f :: * -> *) :: Bool
+
+type InstanceOf name l = InstanceOfNone name '[] l
+
+-- Any instance of name in l but not in ex.
+type family InstanceOfNone name ex l where
+    InstanceOfNone name ex (f ':- l) = InstanceOfNone name (f ': ex) l
+    InstanceOfNone name ex (f ':+ l) =
+        If (Is name f)
+            (If (Elem f ex) (InstanceOfNone name (Remove f ex) l) f)
+            (InstanceOfNone name ex l)
+
+type family Elem e l where
+    Elem e '[] = 'False
+    Elem e (e ': l) = 'True
+    Elem e (f ': l) = Elem e l
+
+type family Remove e l where
+    Remove e (e ': l) = l
+    Remove e (f ': l) = f ': Remove e l

src/Data/Union.hs view

@@ -1,89 +1,89 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE EmptyCase #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE TypeOperators #-}--module Data.Union (-    Union, absurd,-    wrap, unwrap,-    inject, project,-    swap, rotate,-    push, pop,-    enable, disable,-    conceal, reveal,-    flatten, unflatten-) where--import Data.Index (Index)-import qualified Data.Index as Index--import Data.Type.Row-import Data.Proxy (Proxy (..))-import Data.Type.Equality ((:~:) (..), apply, castWith, gcastWith, testEquality)---- | Represents a union of the list of type constructors in @l@ parameterized--- by @a@. As an effect, it represents the union of each type constructor's--- corresponding effect. From the user's perspective, it provides a way to--- encapsulate multiple effects.-data Union l a where-    Union :: Index l f -> f a -> Union l a--absurd :: Union Nil a -> b-absurd (Union i _) = Index.absurd i--wrap :: f a -> Union (f :+ l) a-wrap = inject--unwrap :: Union (f :+ Nil) a -> f a-unwrap (Union i x) = gcastWith (Index.trivial i) x--inject :: Member f l => f a -> Union l a-inject = Union Index.index--project :: Member f l => Union l a -> Maybe (f a)-project (Union i x) = fmap (\refl -> castWith (apply refl Refl) x) mRefl-  where-    mRefl = testEquality i Index.index--swap :: Union (f :+ g :+ l) a -> Union (g :+ f :+ l) a-swap (Union i x) = Union (Index.swap i) x--rotate :: Union (f :+ g :+ h :+ l) a -> Union (g :+ h :+ f :+ l) a-rotate (Union i x) = Union (Index.rotate i) x--push :: Union l a -> Union (f :+ l) a-push (Union i x) = Union (Index.push i) x--pop :: Union (f :+ l) a -> Either (f a) (Union l a)-pop (Union i x) =-    case testEquality i Index.zero of-        Just Refl -> Left x-        Nothing -> Right (Union (Index.pop i) x)--enable :: Union (f :- l) a -> Union l a-enable (Union i x) = Union (Index.enable i) x--disable :: Member f l => Union l a -> Either (f a) (Union (f :- l) a)-disable u@(Union i x) =-    case project u of-        Just r -> Left r-        Nothing -> Right (Union (Index.disable i) x)--conceal :: Member f l => Union (f :+ l) a -> Union l a-conceal (Union i x) = Union (Index.conceal i) x--reveal :: Member f l => Union l a -> Union (f :+ l) a-reveal (Union i x) = Union (Index.reveal i) x--flatten :: Inclusive l => Union (Union l :+ m) a -> Union (l :++ m) a-flatten = flatten' Proxy Proxy . pop-  where-    flatten' :: KnownLength l => proxy l -> proxy m -> Either (Union l a) (Union m a) -> Union (l :++ m) a-    flatten' _ p (Left (Union i x)) = Union (Index.append i p) x-    flatten' p _ (Right (Union i x)) = Union (Index.prepend p i) x--unflatten :: KnownLength l => Union (l :++ m) a -> Union (Union l :+ m) a-unflatten (Union i x) =-    case Index.split i of-        Left j -> Union Index.zero (Union j x)-        Right j -> Union (Index.push j) x+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Union (
+    Union, absurd,
+    wrap, unwrap,
+    inject, project,
+    swap, rotate,
+    push, pop,
+    enable, disable,
+    conceal, reveal,
+    flatten, unflatten
+) where
+
+import Data.Index (Index)
+import qualified Data.Index as Index
+
+import Data.Type.Row
+import Data.Proxy (Proxy (..))
+import Data.Type.Equality ((:~:) (..), apply, castWith, gcastWith, testEquality)
+
+-- | Represents a union of the list of type constructors in @l@ parameterized
+-- by @a@. As an effect, it represents the union of each type constructor's
+-- corresponding effect. From the user's perspective, it provides a way to
+-- encapsulate multiple effects.
+data Union l a where
+    Union :: Index l f -> f a -> Union l a
+
+absurd :: Union 'Nil a -> b
+absurd (Union i _) = Index.absurd i
+
+wrap :: f a -> Union (f ':+ l) a
+wrap = inject
+
+unwrap :: Union (f ':+ 'Nil) a -> f a
+unwrap (Union i x) = gcastWith (Index.trivial i) x
+
+inject :: Member f l => f a -> Union l a
+inject = Union Index.index
+
+project :: Member f l => Union l a -> Maybe (f a)
+project (Union i x) = fmap (\refl -> castWith (apply refl Refl) x) mRefl
+  where
+    mRefl = testEquality i Index.index
+
+swap :: Union (f ':+ g ':+ l) a -> Union (g ':+ f ':+ l) a
+swap (Union i x) = Union (Index.swap i) x
+
+rotate :: Union (f ':+ g ':+ h ':+ l) a -> Union (g ':+ h ':+ f ':+ l) a
+rotate (Union i x) = Union (Index.rotate i) x
+
+push :: Union l a -> Union (f ':+ l) a
+push (Union i x) = Union (Index.push i) x
+
+pop :: Union (f ':+ l) a -> Either (f a) (Union l a)
+pop (Union i x) =
+    case testEquality i Index.zero of
+        Just Refl -> Left x
+        Nothing -> Right (Union (Index.pop i) x)
+
+enable :: Union (f ':- l) a -> Union l a
+enable (Union i x) = Union (Index.enable i) x
+
+disable :: Member f l => Union l a -> Either (f a) (Union (f ':- l) a)
+disable u@(Union i x) =
+    case project u of
+        Just r -> Left r
+        Nothing -> Right (Union (Index.disable i) x)
+
+conceal :: Member f l => Union (f ':+ l) a -> Union l a
+conceal (Union i x) = Union (Index.conceal i) x
+
+reveal :: Member f l => Union l a -> Union (f ':+ l) a
+reveal (Union i x) = Union (Index.reveal i) x
+
+flatten :: Inclusive l => Union (Union l ':+ m) a -> Union (l :++ m) a
+flatten = flatten' Proxy Proxy . pop
+  where
+    flatten' :: KnownLength l => proxy l -> proxy m -> Either (Union l a) (Union m a) -> Union (l :++ m) a
+    flatten' _ p (Left (Union i x)) = Union (Index.append i p) x
+    flatten' p _ (Right (Union i x)) = Union (Index.prepend p i) x
+
+unflatten :: KnownLength l => Union (l :++ m) a -> Union (Union l ':+ m) a
+unflatten (Union i x) =
+    case Index.split i of
+        Left j -> Union Index.zero (Union j x)
+        Right j -> Union (Index.push j) x