effin 0.1.1.0 → 0.2.0.0

raw patch · 18 files changed

+1146/−812 lines, 18 files

Files

• effin.cabal +12/−13
• src/Control/Effect.hs +4/−4
• src/Control/Effect/Bracket.hs +126/−0
• src/Control/Effect/Coroutine.hs +52/−40
• src/Control/Effect/Exception.hs +64/−74
• src/Control/Effect/Lift.hs +23/−14
• src/Control/Effect/List.hs +104/−93
• src/Control/Effect/Reader.hs +72/−69
• src/Control/Effect/State.hs +95/−92
• src/Control/Effect/Thread.hs +0/−105
• src/Control/Effect/Union.hs +0/−33
• src/Control/Effect/Witness.hs +67/−0
• src/Control/Effect/Writer.hs +95/−93
• src/Control/Monad/Effect.hs +164/−92
• src/Data/Index.hs +99/−0
• src/Data/Type/Nat.hs +20/−0
• src/Data/Type/Row.hs +86/−0
• src/Data/Union.hs +63/−90

@@ -1,5 +1,5 @@ name:                effin-version:             0.1.1.0+version:             0.2.0.0 synopsis:            A Typeable-free implementation of extensible effects homepage:            https://github.com/YellPika/effin license:             BSD3@@ -21,10 +21,9 @@   For example, the following code implements a handler for exceptions:   .   > runException :: Effect (Exception e ': es) a -> Effect es (Either e a)-  > runException =-  >     handle (\x -> return (Right x))-  >     $ eliminate (\(Exception e) -> return (Left e))-  >     $ defaultRelay+  > runException = eliminate+  >     (\x -> return (Right x))+  >     (\(Exception e) -> return (Left e))   .   Compare this to the corresponding code in extensible-effects   (<http://hackage.haskell.org/package/extensible-effects>):@@ -35,11 +34,8 @@   >     loop (Val x) = return (Right x)   >     loop (E u)   = handleRelay u loop (\(Exc e) -> return (Left e))   .-  In particular:-  .-  * Effect implementors are not required to do any recursion.-  .-  * The functions for writing effect handlers can be easily composed.+  In particular, effect implementors are not required to do any recursion,+  thereby making effect handlers more composeable.  flag mtl   description: Enable MTL support@@ -49,18 +45,21 @@ library   exposed-modules:     Control.Effect,+    Control.Effect.Bracket,     Control.Effect.Coroutine,     Control.Effect.Exception,+    Control.Effect.Reader,     Control.Effect.Lift,     Control.Effect.List,-    Control.Effect.Reader,     Control.Effect.State,-    Control.Effect.Thread,-    Control.Effect.Union,+    Control.Effect.Witness,     Control.Effect.Writer,     Control.Monad.Effect    other-modules:+    Data.Index,+    Data.Type.Row,+    Data.Type.Nat     Data.Union    build-depends: base >= 4.7 && < 4.8

@@ -1,23 +1,23 @@ module Control.Effect (
+    module Control.Effect.Bracket,
     module Control.Effect.Coroutine,
     module Control.Effect.Exception,
     module Control.Effect.Lift,
     module Control.Effect.List,
     module Control.Effect.Reader,
     module Control.Effect.State,
-    module Control.Effect.Thread,
-    module Control.Effect.Union,
+    module Control.Effect.Witness,
     module Control.Effect.Writer,
     module Control.Monad.Effect
 ) where
 
+import Control.Effect.Bracket
 import Control.Effect.Coroutine
 import Control.Effect.Exception
 import Control.Effect.Lift
 import Control.Effect.List
 import Control.Effect.Reader
 import Control.Effect.State
-import Control.Effect.Thread
-import Control.Effect.Union
+import Control.Effect.Witness
 import Control.Effect.Writer
 import Control.Monad.Effect

@@ -0,0 +1,126 @@+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Effect.Bracket (
+    EffectBracket, Bracket, runBracket,
+    Tag, newTag, raiseWith, exceptWith,
+    Handler, exceptAny, bracket, finally
+) where
+
+import Control.Applicative ((<$>))
+import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
+import Data.Type.Equality ((:~:) (..), TestEquality (..))
+import Control.Effect.Witness
+import Control.Monad.Effect
+
+-- | Provides a base effect for exceptions. This effect allows the dynamic
+-- generation of exception classes at runtime.
+newtype Bracket s a = Bracket { unBracket :: Union (Raise s :+ Witness s :+ Nil) a }
+  deriving Functor
+
+-- | The type of placeholder values indicating an exception class.
+data Tag s a = Tag (a -> String) (Token s a)
+
+instance TestEquality (Tag s) where
+    testEquality (Tag _ i) (Tag _ j) = testEquality i j
+
+type instance Is Bracket f = IsBracket f
+
+type family IsBracket f where
+    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
+
+-- | 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 = mask' $ Tag toString <$> newToken
+
+-- | Raises an exception of the specified class and value.
+raiseWith :: EffectBracket s l => Tag s b -> b -> Effect l a
+raiseWith tag value = mask' $ send $ Raise tag value
+
+-- | Specifies a handler for exceptions of a given class.
+exceptWith :: EffectBracket s l => Tag s b -> Effect l a -> (b -> Effect l a) -> Effect l a
+exceptWith tag effect handler = exceptAny effect [Handler tag handler]
+
+-- | A handler for an exception. Use with `exceptAny`.
+data Handler s l a where
+    Handler :: Tag s b -> (b -> Effect l a) -> Handler s l a
+
+-- | Specifies a number of handlers for exceptions thrown by the given
+-- computation. This is prefered over chained calles to `exceptWith`, i.e.
+--
+-- > exceptWith t2 (exceptWith t1 m h1) h2
+--
+-- 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
+        results = mapMaybe try handlers
+    in fromMaybe (raiseWith i x) (listToMaybe results)
+
+-- | Intercepts all exceptions. Used to implement `exceptWith` and `bracket`.
+-- Not exported. Is it really a good thing to allow catching all exceptions?
+-- The most common use case for catching all exceptions is to do cleanup, which
+-- is what bracket is for.
+exceptAll :: EffectBracket s l => Effect l a -> (forall b. Tag s b -> b -> Effect l a) -> Effect l a
+exceptAll effect handler = mask' $ run $ unmask' effect
+  where
+    run = intercept return $ \(Raise t x) -> unmask' (handler t x)
+
+-- | Executes a computation with a resource, and ensures that the resource is
+-- cleaned up afterwards.
+bracket :: EffectBracket s l
+        => Effect l a -- ^ The 'acquire' operation.
+        -> (a -> Effect l ()) -- ^ The 'release' operation.
+        -> (a -> Effect l b) -- ^ The computation to perform.
+        -> Effect l b
+bracket acquire destroy run = do
+    resource <- acquire
+    result <- run resource `exceptAll` \e x -> do
+        destroy resource
+        raiseWith e x
+    destroy resource
+    return result
+
+-- | A specialized version of `bracket` which
+-- does not require an 'acquire' operation.
+finally :: EffectBracket s l => Effect l a -> Effect l () -> Effect l a
+finally effect finalizer = bracket
+    (return ())
+    (const finalizer)
+    (const effect)
+
+-- | 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 effect =
+    runWitness
+    $ eliminate return (\(Raise (Tag f _) x) -> error (f x))
+    $ flatten
+    $ rename unBracket effect
+
+-- A couple helper functions for getting in and out of the base effects.
+mask' :: EffectBracket s l => Effect (Raise s :+ Witness s :+ l) a -> Effect l a
+mask' = mask Bracket
+
+unmask' :: EffectBracket s l => Effect l a -> Effect (Raise s :+ Witness s :+ l) a
+unmask' = unmask unBracket
+
+-- Quick and dirty exceptions (because Union works with existing functors).
+data Raise s a where
+    Raise :: Tag s b -> b -> Raise s a
+
+instance Functor (Raise s) where
+    fmap _ (Raise n x) = Raise n x

@@ -1,40 +1,52 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--module Control.Effect.Coroutine (-    EffectCoroutine, Coroutine, Iterator (..), runCoroutine, suspend-) where--import Control.Monad.Effect---- | An effect describing a suspendable computation.-data Coroutine i o a = Coroutine (o -> a) i-  deriving Functor---- | A suspended computation.-data Iterator i o es a-    = Done a -- ^ Describes a finished computation.-    | Next (o -> Effect es (Iterator i o es a)) i-    -- ^ Describes a computation that provided a value-    -- of type `i` and awaits a value of type `o`.--type EffectCoroutine i o es = (Member (Coroutine i o) es, '(i, o) ~ CoroutineType es)-type family CoroutineType es where-    CoroutineType (Coroutine i o ': es) = '(i, o)-    CoroutineType (e ': es) = CoroutineType es---- | Suspends the current computation by providing a value--- of type `i` and then waiting for a value of type `o`.-suspend :: EffectCoroutine i o es => i -> Effect es o-suspend = send . Coroutine id---- | Converts a `Coroutine` effect into an `Iterator`.-runCoroutine :: Effect (Coroutine i o ': es) a -> Effect es (Iterator i o es a)-runCoroutine =-    handle (return . Done)-    $ eliminate (\(Coroutine f k) -> return (Next f k))-    $ defaultRelay+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Effect.Coroutine (
+    EffectCoroutine, Coroutine, runCoroutine, suspend,
+    Iterator (..), evalIterator
+) where
+
+import Control.Monad.Effect
+
+-- | An effect describing a suspendable computation.
+data Coroutine i o a = Coroutine (o -> a) i
+  deriving Functor
+
+type instance Is Coroutine f = IsCoroutine f
+
+type family IsCoroutine f where
+    IsCoroutine (Coroutine i o) = True
+    IsCoroutine f = False
+
+class MemberEffect Coroutine (Coroutine i o) es => EffectCoroutine i o es
+instance MemberEffect Coroutine (Coroutine i o) es => EffectCoroutine i o es
+
+-- | Suspends the current computation by providing a value
+-- of type `i` and then waiting for a value of type `o`.
+suspend :: EffectCoroutine i o es => i -> Effect es o
+suspend = send . Coroutine id
+
+-- | Converts a `Coroutine` effect into an `Iterator`.
+runCoroutine :: Effect (Coroutine i o :+ es) a -> Effect es (Iterator i o es a)
+runCoroutine = eliminate (return . Done) (\(Coroutine f k) -> return (Next f k))
+
+-- | A suspended computation.
+data Iterator i o es a
+    = Done a -- ^ Describes a finished computation.
+    | Next (o -> Effect es (Iterator i o es a)) i
+    -- ^ Describes a computation that provided a value
+    -- of type `i` and awaits a value of type `o`.
+
+-- | Evaluates an iterator by providing it with an input stream.
+evalIterator :: Iterator i o es a -> [o] -> Effect es (Iterator i o es a, [i])
+evalIterator (Next f v) (x:xs) = do
+    i <- f x
+    (r, vs) <- evalIterator i xs
+    return (r, v:vs)
+evalIterator i _ = return (i, [])

@@ -1,74 +1,64 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--#if MTL-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}-#endif--module Control.Effect.Exception (-    EffectException, Exception, runException,-    raise, except, finally-) where--import Control.Monad.Effect--#ifdef MTL-import qualified Control.Monad.Error.Class as E--instance EffectException e es => E.MonadError e (Effect es) where-    throwError = raise-    catchError = except-#endif---- | An effect that describes the possibility of failure.-newtype Exception e a = Exception { unException :: e }-  deriving Functor--type EffectException e es = (Member (Exception e) es, e ~ ExceptionType es)-type family ExceptionType es where-    ExceptionType (Exception e ': es) = e-    ExceptionType (e ': es) = ExceptionType es---- | Raises an exception.-raise :: EffectException e es => e -> Effect es a-raise = send . Exception---- | Handles an exception. Intended to be used in infix form.------ > myComputation `except` \ex -> doSomethingWith ex-except :: EffectException e es => Effect es a -> (e -> Effect es a) -> Effect es a-except = flip run-  where-    run handler =-        handle return-        $ intercept (handler . unException)-        $ defaultRelay---- | Ensures that a computation is run after another one completes,--- regardless of whether an exception was raised. Intended to be--- used in infix form.------ > do x <- loadSomeResource--- >    doSomethingWith x `finally` unload x-finally :: EffectException e es => Effect es a -> Effect es () -> Effect es a-finally effect finalizer = do-    result <- effect `except` \e -> do-        finalizer-        raise e-    finalizer-    return result---- | Completely handles an exception effect.-runException :: Effect (Exception e ': es) a -> Effect es (Either e a)-runException =-    handle (return . Right)-    $ eliminate (return . Left . unException)-    $ defaultRelay+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MTL
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Exception (
+    EffectException, Exception, runException,
+    raise, except
+) where
+
+import Control.Effect.Bracket
+import Control.Monad.Effect
+
+#ifdef MTL
+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
+    throwError = raise
+    catchError = except
+#endif
+
+-- | An effect that describes the possibility of failure.
+data Exception e a = Raise e | Catch a (e -> a)
+  deriving Functor
+
+type instance Is Exception f = IsException f
+
+type family IsException f where
+    IsException (Exception e) = True
+    IsException f = False
+
+class MemberEffect Exception (Exception e) l => EffectException e l
+instance MemberEffect Exception (Exception e) l => EffectException e l
+
+-- | Raises an exception.
+raise :: EffectException e l => e -> Effect l a
+raise = send . Raise
+
+-- | 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)
+
+-- | Completely handles an exception effect.
+runException :: (EffectBracket s l, Show e) => Effect (Exception e :+ l) a -> Effect l (Either e a)
+runException effect = do
+    tag <- newTag show
+    exceptWith tag
+        (eliminate (return . Right) (bind tag) effect)
+        (return . Left)
+  where
+    bind tag (Raise e) = raiseWith tag e
+    bind tag (Catch x f) = exceptWith tag x f

@@ -1,18 +1,20 @@-{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 #ifdef MTL
-{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 #endif
 
 module Control.Effect.Lift (
-    EffectLift, Lift, runLift, lift
+    EffectLift, Lift (..), runLift, lift, liftEffect
 ) where
 
 import Control.Monad.Effect
@@ -21,7 +23,7 @@ #ifdef MTL
 import Control.Monad.Trans (MonadIO (..))
 
-instance EffectLift IO es => MonadIO (Effect es) where
+instance EffectLift IO l => MonadIO (Effect l) where
     liftIO = lift
 #endif
 
@@ -34,19 +36,26 @@ instance Monad m => Functor (Lift m) where
     fmap f = Lift . liftM f . unLift
 
-type EffectLift m es = (Member (Lift m) es, m ~ LiftType es, Monad m)
-type family LiftType es where
-    LiftType (Lift m ': es) = m
-    LiftType (e ': es) = LiftType es
+type instance Is Lift f = IsLift f
 
+type family IsLift f where
+    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
+
 -- | Lifts a monadic value into an effect.
-lift :: EffectLift m es => m a -> Effect es a
+lift :: EffectLift m l => m a -> Effect l a
 lift = send . Lift
 
+-- | Lifts a monadic value into an effect.
+liftEffect :: EffectLift m l => m (Effect l a) -> Effect l a
+liftEffect = sendEffect . Lift
+
 -- | Converts a computation containing only monadic
 -- effects into a monadic computation.
-runLift :: Monad m => Effect '[Lift m] a -> m a
-runLift =
-    handle return
-    $ eliminate (join . unLift)
-    $ emptyRelay
+runLift :: Monad m => Effect (Lift m :+ Nil) a -> m a
+runLift = runEffect . eliminate
+    (return . return)
+    (return . join . liftM runEffect . unLift)

@@ -1,93 +1,104 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}--module Control.Effect.List (-    EffectList, List, runList,-    choose, never, select,--    EffectCut, Cut,-    cut, runCut-) where--import Control.Monad.Effect-import Control.Arrow (second)-import Control.Applicative (Alternative (..), (<$>))-import Control.Monad (MonadPlus (..), (<=<), join)---- | Describes a nondeterminism (backtracking) effect.-newtype List a = List { unList :: [a] }-  deriving Functor--type EffectList = Member List---- | Nondeterministically chooses a value from the input list.-choose :: EffectList es => [a] -> Effect es a-choose = send . List---- | Describes a nondeterministic computation that never returns a value.-never :: EffectList es => Effect es a-never = choose []---- | Nondeterministically chooses a value from a list of computations.-select :: EffectList es => [Effect es a] -> Effect es a-select = join . choose---- | Obtains all possible values from a computation--- parameterized by a nondeterminism effect.-runList :: Effect (List ': es) a -> Effect es [a]-runList =-    handle (\x -> return [x])-    $ eliminate (fmap concat . sequence . unList)-    $ defaultRelay--instance EffectList es => Alternative (Effect es) where-    empty = never-    x <|> y = select [x, y]--instance EffectList es => MonadPlus (Effect es) where-    mzero = empty-    mplus = (<|>)---- | Describes a Prolog-like cut effect.--- This effect must be used with the `List` effect.-data Cut a = Cut-  deriving Functor--type EffectCut = Member Cut---- | Prevents backtracking past the point this value was invoked.--- Unlike Prolog's '!' operator, `cut` will cause the current--- computation to fail immediately, instead of when it backtracks.-cut :: (EffectList es, EffectCut es) => Effect es a-cut = send Cut---- | Handles the `Cut` effect. `cut`s have no effect beyond--- the scope of the computation passed to this function.-runCut :: EffectList es => Effect (Cut ': es) a -> Effect es a-runCut = choose . snd <=< reifyCut-  where-    -- Gather the results of a computation into a list (like in runList), but-    -- also return a Bool indicating whether a cut was performed in the-    -- computation. When we intercept the List effect, we get a continuation and-    -- a list of values. If we map the continuation to the list of values, then-    -- we 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 es => Effect (Cut ': es) a -> Effect es (Bool, [a])-    reifyCut =-        handle (\x -> return (False, [x]))-        $ eliminate (\Cut -> return (True, []))-        $ intercept (\(List xs) -> runAll xs)-        $ defaultRelay--    runAll [] = return (False, [])-    runAll (x:xs) = do-        (cutRequested, x') <- x-        if cutRequested-        then return (True, x')-        else second (x' ++) <$> runAll xs+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Control.Effect.List (
+    EffectList, List, runList,
+    choose, never, select,
+
+    CutEffect, Cut, runCut,
+    cut, cutFalse
+) where
+
+import Control.Monad.Effect
+import Control.Arrow (second)
+import Control.Applicative (Alternative (..), (<$>))
+import Control.Monad (MonadPlus (..), (<=<), join)
+
+-- | A nondeterminism (backtracking) effect.
+newtype List a = List { unList :: [a] }
+  deriving Functor
+
+type instance Is List f = IsList f
+
+type family IsList f where
+    IsList List = True
+    IsList f = False
+
+class Member List l => EffectList l
+instance Member List l => EffectList l
+
+-- | Nondeterministically chooses a value from the input list.
+choose :: EffectList l => [a] -> Effect l a
+choose = send . List
+
+-- | Describes a nondeterministic computation that never returns a value.
+never :: EffectList l => Effect l a
+never = choose []
+
+-- | Nondeterministically chooses a value from a list of computations.
+select :: EffectList l => [Effect l a] -> Effect l a
+select = join . choose
+
+-- | Obtains all possible values from a computation
+-- parameterized by a nondeterminism effect.
+runList :: Effect (List :+ l) a -> Effect l [a]
+runList = eliminate (return . return) (fmap concat . sequence . unList)
+
+instance EffectList l => Alternative (Effect l) where
+    empty = never
+    x <|> y = select [x, y]
+
+instance EffectList l => MonadPlus (Effect l) where
+    mzero = empty
+    mplus = (<|>)
+
+-- | Describes a Prolog-like cut effect.
+-- This effect must be used with the `List` effect.
+data Cut a = CutFalse
+  deriving Functor
+
+class (EffectList l, Member Cut l) => CutEffect l
+instance (EffectList l, Member Cut l) => CutEffect l
+
+-- | Prevents backtracking past the point this value was invoked,
+-- in the style of Prolog's "!" operator.
+cut :: CutEffect l => Effect l ()
+cut = return () <|> cutFalse
+
+-- | Prevents backtracking past the point this value was invoked.
+-- Unlike Prolog's "!" operator, `cutFalse` will cause the current
+-- computation to fail immediately, instead of when it backtracks.
+cutFalse :: CutEffect l => Effect l a
+cutFalse = send CutFalse
+
+-- | 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 = choose . snd <=< reifyCut
+  where
+    -- Gather the results of a computation into a list (like in runList), but
+    -- also return a Bool indicating whether a cut was performed in the
+    -- computation. When we intercept the List effect, we get a continuation and a
+    -- list of values. If we map the continuation to the list of values, then we
+    -- 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 =
+        intercept return (runAll . unList) .
+        eliminate
+            (\x -> return (False, [x]))
+            (\CutFalse -> return (True, []))
+
+    runAll [] = return (False, [])
+    runAll (x:xs) = do
+        (cutRequested, x') <- x
+        if cutRequested
+        then return (True, x')
+        else second (x' ++) <$> runAll xs

@@ -1,69 +1,72 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--#if MTL-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}-#endif--module Control.Effect.Reader (-	EffectReader, Reader, runReader,-    ask, asks, local-) where--import Control.Monad.Effect--#ifdef MTL-import qualified Control.Monad.Reader.Class as R--instance EffectReader r es => R.MonadReader r (Effect es) where-    ask = ask-    local = local-    reader = asks-#endif---- | An effect that describes an implicit environment.-newtype Reader r a = Reader (r -> a)-  deriving Functor--type EffectReader r es = (Member (Reader r) es, r ~ ReaderType es)-type family ReaderType es where-    ReaderType (Reader r ': es) = r-    ReaderType (e ': es) = ReaderType es---- | Retrieves the current environment.-ask :: EffectReader r es => Effect es r-ask = asks id---- | Retrieves a value that is a function of the current environment.-asks :: EffectReader r es => (r -> a) -> Effect es a-asks = send . Reader---- | Runs a computation with a modified environment.-local :: EffectReader r es => (r -> r) -> Effect es a -> Effect es a-local f effect = do-    env <- asks f-    run env effect-  where-    run env =-        handle return-        $ intercept (bind env)-        $ defaultRelay---- | Completely handes a `Reader` effect by providing an--- environment value to be used throughout the computation.-runReader :: r -> Effect (Reader r ': es) a -> Effect es a-runReader env =-    handle return-    $ eliminate (bind env)-    $ defaultRelay--bind :: r -> Reader r (Effect es b) -> Effect es b-bind env (Reader k) = k env+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MTL
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Reader (
+    EffectReader, Reader, runReader,
+    ask, asks, local,
+    stateReader
+) where
+
+import Control.Effect.State
+import Control.Monad.Effect
+
+#ifdef MTL
+import Data.Type.Row
+import qualified Control.Monad.Reader.Class as R
+
+instance (Member (Reader r) l, Reader r ~ InstanceOf Reader l) => R.MonadReader r (Effect l) where
+    ask = ask
+    local = local
+    reader = asks
+#endif
+
+-- | An effect that provides an implicit environment.
+newtype Reader r a = Reader (r -> a)
+  deriving Functor
+
+unReader :: r -> Reader r a -> a
+unReader x (Reader f) = f x
+
+type instance Is Reader f = IsReader f
+
+type family IsReader f where
+    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
+
+-- | Retrieves the current environment.
+ask :: EffectReader r l => Effect l r
+ask = asks id
+
+-- | Retrieves a value that is a function of the current environment.
+asks :: EffectReader r l => (r -> a) -> Effect l a
+asks = send . Reader
+
+-- | Runs a computation with a modified environment.
+local :: EffectReader r l => (r -> r) -> Effect l a -> Effect l a
+local f effect = do
+    env <- asks f
+    intercept return (unReader env) effect
+
+-- | 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 = eliminate return (\(Reader f) -> get >>= f)
+
+-- | 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 env = eliminate return (unReader env)

@@ -1,92 +1,95 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--#if MTL-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}-#endif--module Control.Effect.State (-    EffectState, State, runState,-    evalState, execState,-    get, gets, put,-    modify, modify',-    state, withState-) where--import Control.Applicative ((<$>))-import Control.Monad.Effect--#ifdef MTL-import qualified Control.Monad.State.Class as S--instance EffectState s es => S.MonadState s (Effect es) where-    get = get-    put = put-    state = state-#endif---- | An effect where a state value is threaded throughout the computation.-newtype State s a = State (s -> (a, s))-  deriving Functor--type EffectState s es = (Member (State s) es, s ~ StateType es)-type family StateType es where-    StateType (State s ': es) = s-    StateType (e ': es) = StateType es---- | Gets the current state.-get :: EffectState s es => Effect es s-get = state $ \s -> (s, s)---- | Gets a value that is a function of the current state.-gets :: EffectState s es => (s -> a) -> Effect es a-gets f = f <$> get---- | Replaces the current state.-put :: EffectState s es => s -> Effect es ()-put x = state $ const ((), x)---- | Applies a pure modifier to the state value.-modify :: EffectState s es => (s -> s) -> Effect es ()-modify f = get >>= put . f---- | Applies a pure modifier to the state value.--- The modified value is converted to weak head normal form.-modify' :: EffectState s es => (s -> s) -> Effect es ()-modify' f = do-    x <- get-    put $! f x---- | Lifts a stateful computation to the `Effect` monad.-state :: EffectState s es => (s -> (a, s)) -> Effect es a-state = send . State---- | Runs a computation with a modified state value.------ prop> withState f x = modify f >> x-withState :: EffectState s es => (s -> s) -> Effect es a -> Effect es a-withState f x = modify f >> x---- | Completely handles a `State` effect by providing an--- initial state, and making the final state explicit.-runState :: s -> Effect (State s ': es) a -> Effect es (a, s)-runState = flip $-    handle (\x s -> return (x, s))-    $ eliminate (\(State k) s -> let (k', s') = k s in k' s')-    $ relay (\x s -> sendEffect $ fmap ($ s) x)---- | Completely handles a `State` effect, and discards the final state.-evalState :: s -> Effect (State s ': es) a -> Effect es a-evalState s = fmap fst . runState s---- | Completely handles a `State` effect, and discards the final value.-execState :: s -> Effect (State s ': es) a -> Effect es s-execState s = fmap snd . runState s+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MTL
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.State (
+    EffectState, State, runState,
+    evalState, execState,
+    get, gets, put,
+    modify, modify',
+    state, withState
+) where
+
+import Control.Applicative ((<$>))
+import Control.Monad.Effect
+
+#ifdef MTL
+import qualified Control.Monad.State.Class as S
+import Data.Type.Row
+
+instance (Member (State s) l, State s ~ InstanceOf State l) => S.MonadState s (Effect l) where
+    get = get
+    put = put
+    state = state
+#endif
+
+-- | An effect where a state value is threaded throughout the computation.
+newtype State s a = State (s -> (a, s))
+  deriving Functor
+
+type instance Is State f = IsState f
+
+type family IsState f where
+    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
+
+-- | Gets the current state.
+get :: EffectState s l => Effect l s
+get = state $ \s -> (s, s)
+
+-- | Gets a value that is a function of the current state.
+gets :: EffectState s l => (s -> a) -> Effect l a
+gets f = f <$> get
+
+-- | Replaces the current state.
+put :: EffectState s l => s -> Effect l ()
+put x = state $ const ((), x)
+
+-- | Applies a pure modifier to the state value.
+modify :: EffectState s l => (s -> s) -> Effect l ()
+modify f = get >>= put . f
+
+-- | Applies a pure modifier to the state value.
+-- The modified value is converted to weak head normal form.
+modify' :: EffectState s l => (s -> s) -> Effect l ()
+modify' f = do
+    x <- get
+    put $! f x
+
+-- | Lifts a stateful computation to the `Effect` monad.
+state :: EffectState s l => (s -> (a, s)) -> Effect l a
+state = send . State
+
+-- | Runs a computation with a modified state value.
+--
+-- prop> withState f x = modify f >> x
+withState :: EffectState s l => (s -> s) -> Effect l a -> Effect l a
+withState f x = modify f >> x
+
+-- | 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 = flip $ eliminate
+    (\x s -> return (x, s))
+    (\(State k) s -> let (k', s') = k s in k' s')
+
+-- | Completely handles a `State` effect, and discards the final state.
+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 = fmap snd . runState s

@@ -1,105 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeOperators #-}
-
-module Control.Effect.Thread (
-    EffectThread, Thread,
-    runMain, runSync, runAsync,
-    yield, fork, abort,
-) where
-
-import Control.Effect.Lift
-import Control.Monad.Effect
-import Control.Applicative ((<$>))
-import Control.Monad (void)
-import qualified Control.Concurrent as IO
-
--- | An effect that describes concurrent computation.
-data Thread a = Yield a | Fork a a | Abort
-  deriving Functor
-
-type EffectThread = Member Thread
-
--- | Yields to the next available thread.
-yield :: EffectThread es => Effect es ()
-yield = send (Yield ())
-
--- | Forks a child thread.
-fork :: EffectThread es => Effect es () -> Effect es ()
-fork child = sendEffect $ Fork child (return ())
-
--- | Immediately terminates the current thread.
-abort :: EffectThread es => Effect es ()
-abort = send Abort
-
--- | Executes a threaded computation synchronously.
--- Completes when the main thread exits.
-runMain :: Effect (Thread ': es) () -> Effect es ()
-runMain = run [] . toAST
-  where
-    run auxThreads thread = do
-        result <- thread
-        case result of
-            AbortAST -> return ()
-            YieldAST k -> do
-                auxThreads' <- runAll auxThreads
-                run auxThreads' k
-            ForkAST child parent -> do
-                auxThreads' <- runAll [child]
-                run (auxThreads ++ auxThreads') parent
-
-    runAll [] = return []
-    runAll (thread:xs) = do
-        result <- thread
-        case result of
-            AbortAST -> runAll xs
-            YieldAST k -> (k:) <$> runAll xs
-            ForkAST child parent -> (parent:) <$> runAll (child:xs)
-
--- | Executes a threaded computation synchronously.
--- Does not complete until all threads have exited.
-runSync :: Effect (Thread ': es) () -> Effect es ()
-runSync = run . (:[]) . toAST
-  where
-    run [] = return ()
-    run (thread:xs) = do
-        result <- thread
-        case result of
-            AbortAST -> run xs
-            YieldAST k -> run (xs ++ [k])
-            ForkAST child parent -> run (child:xs ++ [parent])
-
--- | Executes a threaded computation asynchronously.
-runAsync :: Effect '[Thread, Lift IO] () -> IO ()
-runAsync = run . toAST
-  where
-    run thread = do
-        result <- runLift thread
-        case result of
-            AbortAST -> return ()
-            YieldAST k -> do
-                IO.yield
-                run k
-            ForkAST child parent -> do
-                void $ IO.forkIO $ run child
-                run parent
-
-data ThreadAST es
-    = YieldAST (Effect es (ThreadAST es))
-    | ForkAST (Effect es (ThreadAST es)) (Effect es (ThreadAST es))
-    | AbortAST
-
--- 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 ': es) () -> Effect es (ThreadAST es)
-toAST =
-    handle (\() -> return AbortAST)
-    $ eliminate (\thread ->
-        case thread of
-            Abort -> return AbortAST
-            Yield k -> return (YieldAST k)
-            Fork child parent -> return (ForkAST child parent))
-    $ defaultRelay

@@ -1,33 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-module Control.Effect.Union (
-    EffectUnion, Union, runUnion, nest,
-    KnownList, type (++),
-) where
-
-import Control.Monad.Effect
-import Data.Union
-
-type EffectUnion es fs = (KnownList es, Member (Union es) fs, es ~ UnionType fs)
-type family UnionType fs where
-    UnionType (Union es ': fs) = es
-    UnionType (f ': fs) = UnionType fs
-
--- | Nests an effect with another.
-nest :: EffectUnion es fs => Effect es a -> Effect fs a
-nest =
-    handle return
-    $ relayUnion sendEffect
-
--- | Flattens a nested list of effects.
-runUnion :: KnownList es => Effect (Union es ': fs) a -> Effect (es ++ fs) a
-runUnion =
-    handle return
-    $ relayUnion (withUnion sendEffect . flatten)
-
-relayUnion :: (Union es b -> b) -> Handler es b
-relayUnion f = relay (f . inject)

@@ -0,0 +1,67 @@+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Effect.Witness (
+    EffectWitness, Witness, runWitness,
+    Token, newToken
+) where
+
+import Control.Monad.Effect
+import Data.Type.Equality ((:~:) (..), TestEquality (..))
+import Data.Unique (Unique, newUnique)
+import System.IO.Unsafe (unsafePerformIO)
+import Unsafe.Coerce (unsafeCoerce)
+
+-- | A unique identifier associated with a type @a@.
+-- If two tokens are equal, then so are their associated types.
+-- Use `testEquality` to safely cast between types.
+newtype Token s a = Token Unique
+  deriving Eq
+
+instance TestEquality (Token s) where
+    testEquality (Token i) (Token j)
+        | i == j = Just unsafeRefl
+        | otherwise = Nothing
+
+unsafeRefl :: a :~: b
+unsafeRefl = unsafeCoerce Refl
+
+-- | An effect describing the generation of unique identifiers.
+data Witness s a where
+    Witness :: (Token s b -> a) -> Witness s a
+
+instance Functor (Witness s) where
+    fmap f (Witness g) = Witness (f . g)
+
+type instance Is Witness f = IsWitness f
+
+type family IsWitness f where
+    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
+
+type family WitnessType l where
+    WitnessType (Witness s ': l) = s
+    WitnessType (e ': l) = WitnessType l
+
+-- | Generates a new, unique `Token`.
+newToken :: EffectWitness s l => Effect l (Token s a)
+newToken = send (Witness id)
+
+-- | 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 effect = run effect
+  where
+    run = eliminate return $ \(Witness k) ->
+        k $ Token $ unsafePerformIO newUnique

@@ -1,93 +1,95 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--#if MTL-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}-#endif--module Control.Effect.Writer (-    EffectWriter, Writer, runWriter,-    tell, listen, listens, pass, censor-) where--import Control.Monad.Effect-import Control.Applicative ((<$>))-import Control.Arrow (second)-import Data.Monoid (Monoid (..))--#ifdef MTL-import qualified Control.Monad.Writer.Class as W--instance EffectWriter e es => W.MonadWriter e (Effect es) where-    tell = tell-    listen = listen-    pass = pass-#endif---- | An effect that allows accumulating output.-data Writer w a = Writer w a-  deriving Functor--type EffectWriter w es = (Monoid w, Member (Writer w) es, w ~ WriterType es)-type family WriterType es where-    WriterType (Writer w ': es) = w-    WriterType (t ': es) = WriterType es---- | Writes a value to the output.-tell :: EffectWriter w es => w -> Effect es ()-tell x = send (Writer x ())---- | Executes a computation, and obtains the writer output.--- The writer output of the inner computation is still--- written to the writer output of the outer computation.-listen :: EffectWriter w es => Effect es a -> Effect es (a, w)-listen effect = do-    value@(_, output) <- run effect-    tell output-    return value-  where-    run =-        handle point-        $ intercept bind-        $ defaultRelay---- | Like `listen`, but the writer output is run through a function.-listens :: EffectWriter w es => (w -> b) -> Effect es a -> Effect es (a, b)-listens f = fmap (second f) . listen---- | Runs a computation that returns a value and a function,--- applies the function to the writer output, and then returns the value.-pass :: EffectWriter w es => Effect es (a, w -> w) -> Effect es a-pass effect = do-    ((x, f), l) <- listen effect-    tell (f l)-    return x---- | Applies a function to the writer output of a computation.-censor :: EffectWriter w es => (w -> w) -> Effect es a -> Effect es a-censor f effect = pass $ do-    a <- effect-    return (a, f)---- | 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 ': es) a -> Effect es (a, w)-runWriter =-    handle point-    $ eliminate bind-    $ defaultRelay--point :: Monoid w => a -> Effect es (a, w)-point x = return (x, mempty)--bind :: Monoid w => Writer w (Effect es (b, w)) -> Effect es (b, w)-bind (Writer l k) = second (mappend l) <$> k+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MTL
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Writer (
+    EffectWriter, Writer, runWriter,
+    tell, listen, listens, pass, censor,
+    stateWriter
+) where
+
+import Control.Monad.Effect
+import Control.Applicative ((<$>))
+import Control.Arrow (second)
+import Data.Monoid (Monoid (..))
+import Control.Effect.State
+
+#ifdef MTL
+import Data.Type.Row
+import qualified Control.Monad.Writer.Class as W
+
+instance (Monoid w, Member (Writer w) l, Writer w ~ InstanceOf Writer l) => W.MonadWriter w (Effect l) where
+    tell = tell
+    listen = listen
+    pass = pass
+#endif
+
+-- | An effect that allows accumulating output.
+data Writer w a = Writer w a
+  deriving Functor
+
+type instance Is Writer f = IsWriter f
+
+type family IsWriter f where
+    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
+
+-- | Writes a value to the output.
+tell :: EffectWriter w l => w -> Effect l ()
+tell x = send (Writer x ())
+
+-- | Executes a computation, and obtains the writer output.
+-- The writer output of the inner computation is still
+-- written to the writer output of the outer computation.
+listen :: EffectWriter w l => Effect l a -> Effect l (a, w)
+listen effect = do
+    value@(_, output) <- intercept point bind effect
+    tell output
+    return value
+
+-- | Like `listen`, but the writer output is run through a function.
+listens :: EffectWriter w l => (w -> b) -> Effect l a -> Effect l (a, b)
+listens f = fmap (second f) . listen
+
+-- | Runs a computation that returns a value and a function,
+-- applies the function to the writer output, and then returns the value.
+pass :: EffectWriter w l => Effect l (a, w -> w) -> Effect l a
+pass effect = do
+    ((x, f), l) <- listen effect
+    tell (f l)
+    return x
+
+-- | Applies a function to the writer output of a computation.
+censor :: EffectWriter w l => (w -> w) -> Effect l a -> Effect l a
+censor f effect = pass $ do
+    a <- effect
+    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 = eliminate return (\(Writer l x) -> modify (mappend l) >> x)
+
+-- | 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 = eliminate point bind
+
+point :: Monoid w => a -> Effect l (a, w)
+point x = return (x, mempty)
+
+bind :: Monoid w => Writer w (Effect l (b, w)) -> Effect l (b, w)
+bind (Writer l k) = second (mappend l) <$> k

@@ -1,128 +1,200 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} --- | This module provides three things:------ 1. An `Effect` monad for representing effectful computations,--- 2. A DSL for effect handling that lets you cleanly handle an arbitrary number of effects, and--- 3. A type-level list membership constraint. module Control.Monad.Effect (     -- * The Effect Monad-    Effect,-    runEffect, send, sendEffect,+    Effect, runEffect,+    send, sendEffect,      -- * Effect Handlers-    -- | The following types and functions form a small DSL that allows users to-    -- specify how to handle effects. A handler can be formed by a call to-    -- `handle`, followed by a chain of calls to `eliminate`, `intercept`, and-    -- ended by either a `defaultRelay`, `emptyRelay`, or a call to `relay`.-    ---    -- For example, a possible handler for the state effect would be:-    ---    -- > data State s a = State (s -> (s, a))-    -- >-    -- > runState :: Effect (State s ': es) a -> s -> Effect es (s, a)-    -- > runState =-    -- >     handle (\output state -> return (state, output))-    -- >     $ eliminate (\(State transform) state ->-    -- >         let (state', continue) = transform state-    -- >         in continue state')-    -- >     $ relay (\effect state -> do-    -- >         continue <- sendEffect effect-    -- >         return (continue state))-    ---    -- As an analogy to monads, `handle` lets you specify the return function,-    -- while `eliminate`, `intercept`, and `relay`, let you specify the bind-    -- function.-    Handler, handle,+    Effectful (EffectsOf),+     eliminate, intercept,-    relay, defaultRelay, emptyRelay,+    extend, enable,+    conceal, reveal, rename,+    swap, rotate,+    mask, unmask, +    -- * Unions+    Union, flatten, unflatten,+     -- * Membership-    Member+    Member, MemberEffect, Is,++    -- * Effect Rows+    Row (..), type (:++),+    KnownLength, Inclusive ) where -import Data.Union+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 es a@ may perform any of the effects--- specified by the list of effects @es@ before returning a result of type @a@.+-- | 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 es a where--- >     Done :: a -> Effect es a--- >     Side :: `Union` es (Effect es a) -> Effect es a-data Effect es a = Effect {-    unEffect :: forall r. (a -> r) -> (Union es r -> r) -> r-} deriving Functor+-- @+-- 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) -> (Union l r -> r) -> r) -instance Applicative (Effect es) where-    pure x = Effect $ \p _ -> p x-    Effect f <*> Effect x = Effect $ \p b ->-        f (\f' -> x (p . f') b) b+unEffect :: (a -> r) -> (Union l r -> r) -> Effect l a -> r+unEffect point bind (Effect f) = f point bind -instance Monad (Effect es) where+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 x >>= f = Effect $ \p b ->-        x (\x' -> unEffect (f x') p b) b+    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 '[] a -> a-runEffect (Effect f) = f id absurdUnion+runEffect :: Effect Nil a -> a+runEffect (Effect f) = f id Union.absurd --- | Executes an effect of type @e@ that produces a return value of type @a@.-send :: Member e es => e a -> Effect es a-send x = Effect $ \point bind -> bind $ inject $ point <$> x+-- | Executes an effect of type @f@ that produces a return value of type @a@.+send :: (Functor f, Member f l) => f a -> Effect l a+send x = Effect $ \point bind -> bind $ point <$> Union.inject x -- Inlined for efficiency (from relay). --- | Executes an effect of type @e@ that produces a return value of type @a@.-sendEffect :: Member e es => e (Effect es a) -> Effect es a-sendEffect = join . send+-- | 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+-- @(Functor f, Member f l) => f (Effect l a) -> Effect l a@, which allows users+-- to send effects parameterized by effects.+sendEffect :: (Functor f, Member f l, Effectful l r) => f r -> r+sendEffect = relay . Union.inject --- | A handler for an effectful computation.--- Combined with 'handle', allows one to convert a computation--- parameterized by the effect list @es@ to a value of type @a@.-data Handler es a = Handler (Union es a -> a)+-- | 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 (* -> *) --- | @handle p h@ transforms an effect into a value of type @b@.+    relay :: Union l 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 = join $ Effect $ \point bind -> bind $ point <$> u++instance Effectful l r => Effectful l (a -> r) where+    type EffectsOf (a -> r) = EffectsOf r+    relay u x = relay (fmap ($ x) u)++-- | Handles an effect without eliminating it. The given function is passed an+-- effect value parameterized by the output type (i.e. the return type of+-- `handle`). ----- @p@ specifies how to convert pure values. That is,+-- The most common instantiation of this function is: ----- prop> handle p h (return x) = p x+-- > (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) -> (f r -> r) -> Effect l a -> r+intercept point bind = unEffect point $ \u -> maybe (relay u) bind (Union.project u)++-- | Completely handles an effect. The given function is passed an effect value+-- parameterized by the output type (i.e. the return type of `handle`). ----- @h@ specifies how to handle effects.-handle :: (a -> b) -> Handler es b -> Effect es a -> b-handle point (Handler bind) (Effect f) = f point bind+-- 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) -> (f r -> r) -> Effect (f :+ l) a -> r+eliminate point bind = unEffect point (either bind relay . Union.pop) --- | Provides a way to completely handle an effect. The given function is passed--- an effect value parameterized by the output type (i.e. the return type of--- `handle`).-eliminate :: (e b -> b) -> Handler es b -> Handler (e ': es) b-eliminate bind (Handler pass) = Handler (either pass bind . reduce)+-- | Adds an arbitrary effect to the head of the effect list.+extend :: Effect l a -> Effect (f :+ l) a+extend = translate Union.push --- | Provides a way to handle an effect without eliminating it. The given--- function is passed an effect value parameterized by the output type (i.e. the--- return type of `handle`).-intercept :: Member e es => (e b -> b) -> Handler es b -> Handler es b-intercept bind (Handler pass) = Handler $ \u ->-    maybe (pass u) bind (project u)+-- | Enables an effect that was previously disabled.+enable :: Effect (f :- l) a -> Effect l a+enable = translate Union.enable --- | Computes a basis handler. Provides a way to pass on effects of unknown--- types. In most cases, `defaultRelay` is sufficient.-relay :: (forall e. Member e es => e b -> b) -> Handler es b-relay f = Handler (withUnion f)+-- | Hides an effect @g@ by translating each instance of @g@ into an instance of+-- another effect @f@.+conceal :: Member f l => Effect (f :+ l) a -> Effect l a+conceal = translate Union.conceal --- | Relays all effects without examining them.+-- | Hides an effect @g@ by translating each instance of another effect @f@ into+-- an instance of @g@.+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.+rename :: Functor g => (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@. ----- prop> handle id defaultRelay x = x-defaultRelay :: Handler es (Effect es a)-defaultRelay = relay sendEffect+-- @ mask f = `conceal` . `rename` f . `unflatten` @+mask :: (Functor f, 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 --- | A handler for when there are no effects. Since `Handler`s handle effects,--- they cannot be run on a computation that never produces an effect. By the--- principle of explosion, a handler that requires exactly zero effects can--- produce any value.-emptyRelay :: Handler '[] a-emptyRelay = Handler absurdUnion+-- | Converts an effect @f@ into a set of effects @l@.+--+-- @ unmask f = `flatten` . `rename` f . `reveal` @+unmask :: (Functor f, 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

@@ -0,0 +1,99 @@+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Index (
+    Index,
+    zero, index,
+    absurd, trivial,
+    swap, rotate,
+    push, pop,
+    disable, enable,
+    conceal, reveal,
+    prepend, append, split
+) where
+
+import Data.Type.Row
+import Data.Type.Nat
+
+import Data.Proxy (Proxy (..))
+import Data.Type.Equality ((:~:) (..), TestEquality (..))
+import Unsafe.Coerce (unsafeCoerce)
+
+newtype Index (l :: Row k) (e :: k) = Index Integer
+  deriving Show
+
+instance TestEquality (Index l) where
+    testEquality (Index i) (Index j)
+        | i == j = Just (unsafeCoerce Refl)
+        | otherwise = Nothing
+
+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 i) = i `seq` error "absurd Index"
+
+trivial :: Index (e :+ Nil) f -> f :~: e
+trivial (Index i)
+    | i == 0 = unsafeCoerce Refl
+    | otherwise = error "non-trivial Index"
+
+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 i) = Index (i + 1)
+
+pop :: Index (f :+ l) e -> Index l e
+pop (Index i) = Index (i - 1)
+
+disable :: Index l e -> Index (f :- l) e
+disable (Index i) = Index (i + 1)
+
+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 (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 (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 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 i)
+    | i == 0 = Index 2
+    | i == 1 = Index 1
+    | i == 2 = Index 0
+    | otherwise = Index i
+
+prepend :: KnownLength l => proxy l -> Index m e -> Index (l :++ m) e
+prepend p (Index i) = Index (i + size p)
+
+append :: Index l e -> proxy m -> Index (l :++ m) e
+append (Index i) _ = Index i
+
+split :: forall e l m. KnownLength l => Index (l :++ m) e -> Either (Index l e) (Index m e)
+split (Index i)
+    | i < n = Left (Index i)
+    | otherwise = Right (Index (i - 1))
+  where
+    n = size (Proxy :: Proxy l)

@@ -0,0 +1,20 @@+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Data.Type.Nat (
+    Nat (..), KnownNat (..)
+) where
+
+import Data.Proxy (Proxy (..))
+
+data Nat = Zero | Succ Nat
+
+class KnownNat (n :: Nat) where
+    natVal :: proxy n -> Integer
+
+instance KnownNat Zero where
+    natVal _ = 0
+
+instance KnownNat n => KnownNat (Succ n) where
+    natVal _ = 1 + natVal (Proxy :: Proxy n)

@@ -0,0 +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

@@ -1,119 +1,92 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}  module Data.Union (-    Union, Member,+    Union, absurd,+    wrap, unwrap,     inject, project,-    reduce, flatten,-    withUnion, absurdUnion,--    KnownList, type (++)+    swap, rotate,+    push, pop,+    enable, disable,+    conceal, reveal,+    flatten, unflatten ) where -import Data.Proxy (Proxy (..))-import Unsafe.Coerce (unsafeCoerce)+import Data.Index (Index)+import qualified Data.Index as Index --- Union -----------------------------------------------------------------------+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 @es@ parameterized+-- | 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.-data Union es a where-    Union :: Functor e => Index e es -> e a -> Union es a+-- corresponding effect. From the user's perspective, it provides a way to+-- encapsulate multiple effects.+data Union l a where+    Union :: Functor f => Index l f -> f a -> Union l a -instance Functor (Union es) where+instance Functor (Union l) where     fmap f (Union i x) = Union i (fmap f x) -inject :: Member e es => e a -> Union es a-inject = Union index--project :: forall a e es. Member e es => Union es a -> Maybe (e a)-project (Union (Index i) x)-    | i == j = Just (unsafeCoerce x)-    | otherwise = Nothing-  where-    Index j = index :: Index e es--reduce :: Union (e ': es) a -> Either (Union es a) (e a)-reduce (Union (Index 0) x) = Right (unsafeCoerce x)-reduce (Union (Index n) x) = Left (Union (Index (n - 1)) x)--flatten :: KnownList es => Union (Union es ': fs) a -> Union (es ++ fs) a-flatten = flatten' size . reduce-  where-    flatten' :: Size es -> Either (Union fs a) (Union es a) -> Union (es ++ fs) a-    flatten' _ (Right (Union (Index i) x)) = Union (Index i) x-    flatten' (Size n) (Left (Union (Index i) x)) = Union (Index (n + i)) x--withUnion :: (forall e. Member e es => e a -> r) -> Union es a -> r-withUnion f (Union i x) = withIndex (f x) (\Proxy -> i)--absurdUnion :: Union '[] a -> b-absurdUnion _ = error "absurdUnion"---- Membership ---------------------------------------------------------------------- | A constraint that requires that the type constructor @t :: * -> *@ is a--- member of the list of types @ts :: [* -> *]@.-class (Functor t, Member' t ts (IndexOf t ts)) => Member t ts where-    index :: Index t ts+absurd :: Union Nil a -> b+absurd (Union i _) = Index.absurd i -instance (Functor t, Member' t ts (IndexOf t ts)) => Member t ts where-    index = index' (Proxy :: Proxy (IndexOf t ts))+wrap :: Functor f => f a -> Union (f :+ l) a+wrap = inject -class Member' e es (n :: N) where-    index' :: Proxy n -> Index e es+unwrap :: Union (f :+ Nil) a -> f a+unwrap (Union i x) = gcastWith (Index.trivial i) x -instance Member' e (e ': es) Z where-    index' _ = Index 0+inject :: (Functor f, Member f l) => f a -> Union l a+inject = Union Index.index -instance (Member' e es n, IndexOf e (f ': es) ~ S n) => Member' e (f ': es) (S n) where-    index' p = incr (index' (decr p))-      where-        incr :: Index e es -> Index e (f ': es)-        incr (Index i) = Index (i + 1)+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 -        decr :: Proxy (S n) -> Proxy n-        decr Proxy = Proxy+swap :: Union (f :+ g :+ l) a -> Union (g :+ f :+ l) a+swap (Union i x) = Union (Index.swap i) x -newtype Index (e :: * -> *) (es :: [* -> *]) = Index Integer+rotate :: Union (f :+ g :+ h :+ l) a -> Union (g :+ h :+ f :+ l) a+rotate (Union i x) = Union (Index.rotate i) x -withIndex :: (Member' e es (IndexOf e es) => r) -> (Proxy (IndexOf e es) -> Index e es) -> r-withIndex = unsafeCoerce+push :: Union l a -> Union (f :+ l) a+push (Union i x) = Union (Index.push i) x --- Type Level Indices -----------------------------------------------------------data N = Z | S N+pop :: Union (f :+ l) a -> Either (f a) (Union l a)+pop u@(Union i x) =+    case project u of+        Just r -> Left r+        Nothing -> Right (Union (Index.pop i) x) -type family IndexOf (t :: * -> *) ts where-    IndexOf t (t ': ts) = Z-    IndexOf t (u ': ts) = S (IndexOf t ts)+enable :: Union (f :- l) a -> Union l a+enable (Union i x) = Union (Index.enable i) x --- Type Level Lists -------------------------------------------------------------newtype Size (es :: [* -> *]) = Size Integer+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) --- | A 'known list' is a type level list who's size is known at compile time.-class KnownList es where-    size :: Size es+conceal :: Member f l => Union (f :+ l) a -> Union l a+conceal (Union i x) = Union (Index.conceal i) x -instance KnownList '[] where-    size = Size 0+reveal :: Member f l => Union l a -> Union (f :+ l) a+reveal (Union i x) = Union (Index.reveal i) x -instance KnownList es => KnownList (e ': es) where-    size = incr size-      where-        incr :: Size es -> Size (e ': es)-        incr (Size n) = Size (n + 1)+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 --- | Type level list append.-type family es ++ fs :: [* -> *] where-    '[] ++ fs = fs-    (e ': es) ++ fs = e ': (es ++ fs)+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