effin 0.3.0.1 → 0.3.0.2

raw patch · 6 files changed

+495/−495 lines, 6 filesdep ~basesetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• LICENSE +30/−30
• Setup.hs +2/−2
• effin.cabal +82/−82
• src/Control/Monad/Effect.hs +206/−206
• src/Data/Type/Row.hs +86/−86
• src/Data/Union.hs +89/−89

@@ -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.

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

@@ -1,82 +1,82 @@-name:                effin-version:             0.3.0.1-synopsis:            A Typeable-free implementation of extensible effects-homepage:            https://github.com/YellPika/effin-license:             BSD3-license-file:        LICENSE-author:              Anthony Vandikas-maintainer:          yellpika@gmail.com-copyright:           (c) 2014 Anthony Vandikas-category:            Control, Effect-build-type:          Simple-cabal-version:       >=1.10-description:-  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-  does not use the Typeable type class, does not require that effects implement-  the Functor type class, and has a simpler API for handling-  effects.-  .-  For example, the following code implements a handler for exceptions:-  .-  > newtype Exception e = Throw e-  >-  > runException :: Effect (Exception e :+ es) a -> Effect es (Either e a)-  > runException = eliminate-  >     (\x -> return (Right x))-  >     (\(Throw e) k -> return (Left e))-  .-  Compare this to the corresponding code in extensible-effects-  (<http://hackage.haskell.org/package/extensible-effects>):-  .-  > runExc :: Typeable e => Eff (Exc e :> r) a -> Eff r (Either e a)-  > runExc = loop . admin-  >   where-  >     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,-  thereby making effect handlers more composeable.--flag mtl-  description: Enable MTL support-  default: True-  manual: True--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.State,-    Control.Effect.Thread,-    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.9-  if flag(mtl)-    build-depends: mtl >= 2.1 && < 3--  hs-source-dirs: src-  default-language: Haskell2010-  ghc-options: -Wall--  if flag(mtl)-    cpp-options: -DMTL--source-repository head-  type:     git-  location: git://github.com/YellPika/effin.git+name:                effin
+version:             0.3.0.2
+synopsis:            A Typeable-free implementation of extensible effects
+homepage:            https://github.com/YellPika/effin
+license:             BSD3
+license-file:        LICENSE
+author:              Anthony Vandikas
+maintainer:          yellpika@gmail.com
+copyright:           (c) 2014 Anthony Vandikas
+category:            Control, Effect
+build-type:          Simple
+cabal-version:       >=1.10
+description:
+  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
+  does not use the Typeable type class, does not require that effects implement
+  the Functor type class, and has a simpler API for handling
+  effects.
+  .
+  For example, the following code implements a handler for exceptions:
+  .
+  > newtype Exception e = Throw e
+  >
+  > runException :: Effect (Exception e :+ es) a -> Effect es (Either e a)
+  > runException = eliminate
+  >     (\x -> return (Right x))
+  >     (\(Throw e) k -> return (Left e))
+  .
+  Compare this to the corresponding code in extensible-effects
+  (<http://hackage.haskell.org/package/extensible-effects>):
+  .
+  > runExc :: Typeable e => Eff (Exc e :> r) a -> Eff r (Either e a)
+  > runExc = loop . admin
+  >   where
+  >     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,
+  thereby making effect handlers more composeable.
+
+flag mtl
+  description: Enable MTL support
+  default: True
+  manual: True
+
+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.State,
+    Control.Effect.Thread,
+    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.10
+  if flag(mtl)
+    build-depends: mtl >= 2.1 && < 3
+
+  hs-source-dirs: src
+  default-language: Haskell2010
+  ghc-options: -Wall
+
+  if flag(mtl)
+    cpp-options: -DMTL
+
+source-repository head
+  type:     git
+  location: git://github.com/YellPika/effin.git

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

@@ -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

@@ -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