commit 7897b40ec926936c67e58e707e2635462cad8867
Author: Alej Cabrera <cpp.cabrera@gmail.com>
Date:   Sat Sep 12 00:38:18 2015 -0500

    initial commit

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..dfda60e
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,9 @@
+# haskell
+.stack-work
+.cabal-sandbox
+dist
+cabal.sandbox.config
+
+# emacs
+TAGS
+tags
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..711a0ce
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Alej Cabrera
+
+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 Alej Cabrera 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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/freer.cabal b/freer.cabal
new file mode 100644
index 0000000..4d09343
--- /dev/null
+++ b/freer.cabal
@@ -0,0 +1,34 @@
+-- Initial freer.cabal generated by cabal init.  For further documentation,
+--  see http://haskell.org/cabal/users-guide/
+
+name:                freer
+version:             0.1.0.0
+synopsis:            Implementation of the Freer Monad
+-- description:
+license:             BSD3
+license-file:        LICENSE
+author:              Alej Cabrera
+maintainer:          cpp.cabrera@gmail.com
+-- copyright:
+category:            Control
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Control.Monad.Freer.Internal
+                     , Data.FTCQueue
+                     , Data.Open.Union
+                     , Control.Monad.Freer.Reader
+                     , Control.Monad.Freer.Writer
+                     , Control.Monad.Freer.State
+                     , Control.Monad.Freer.StateRW
+                     , Control.Monad.Freer.Exception
+                     , Control.Monad.Freer.Trace
+                     , Control.Monad.Freer.Fresh
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base >=4.8 && <4.9
+  hs-source-dirs:      src
+  -- ghc-options:         -Wall
+  default-language:    Haskell2010
diff --git a/src/Control/Monad/Freer/Exception.hs b/src/Control/Monad/Freer/Exception.hs
new file mode 100644
index 0000000..d38ecde
--- /dev/null
+++ b/src/Control/Monad/Freer/Exception.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+module Control.Monad.Freer.Exception (
+  Exc,
+  throwError,
+  runError,
+  catchError
+) where
+
+import Control.Monad
+import Control.Monad.Freer.Reader -- for examples
+import Control.Monad.Freer.State  -- for examples
+import Control.Monad.Freer.Internal
+
+--------------------------------------------------------------------------------
+                           -- Exceptions --
+--------------------------------------------------------------------------------
+-- | Exceptions of the type e; no resumption
+newtype Exc e v = Exc e
+
+-- The type is inferred
+throwError :: (Member (Exc e) r) => e -> Eff r a
+throwError e = send (Exc e)
+
+runError :: Eff (Exc e ': r) a -> Eff r (Either e a)
+runError =
+   handleRelay (return . Right) (\ (Exc e) _k -> return (Left e))
+
+-- The handler is allowed to rethrow the exception
+catchError :: Member (Exc e) r =>
+        Eff r a -> (e -> Eff r a) -> Eff r a
+catchError m handle = interpose return (\(Exc e) _k -> handle e) m
+
+
+--------------------------------------------------------------------------------
+                       -- Tests and Examples --
+--------------------------------------------------------------------------------
+add = liftM2 (+)
+
+-- The type is inferred
+et1 :: Eff r Int
+et1 = return 1 `add` return 2
+
+et1r :: Bool
+et1r = 3 == run et1
+
+-- The type is inferred
+-- et2 :: Member (Exc Int) r => Eff r Int
+et2 = return 1 `add` throwError (2::Int)
+
+-- The following won't type: unhandled exception!
+-- ex2rw = run et2
+{-
+    No instance for (Member (Exc Int) Void)
+      arising from a use of `et2'
+-}
+
+-- The inferred type shows that ex21 is now pure
+et21 :: Eff r (Either Int Int)
+et21 = runError et2
+
+et21r = Left 2 == run et21
+
+
+-- The example from the paper
+newtype TooBig = TooBig Int deriving (Eq, Show)
+-- The type is inferred
+ex2 :: Member (Exc TooBig) r => Eff r Int -> Eff r Int
+ex2 m = do
+  v <- m
+  if v > 5 then throwError (TooBig v)
+     else return v
+
+-- specialization to tell the type of the exception
+runErrBig :: Eff (Exc TooBig ': r) a -> Eff r (Either TooBig a)
+runErrBig = runError
+
+
+-- exceptions and state
+incr :: Member (State Int) r => Eff r ()
+incr = get >>= put . (+ (1::Int))
+
+tes1 :: (Member (State Int) r, Member (Exc [Char]) r) => Eff r b
+tes1 = do
+ incr
+ throwError "exc"
+
+ter1 :: Bool
+ter1 = ((Left "exc" :: Either String Int,2) ==) $
+       run $ runState (runError tes1) (1::Int)
+
+
+ter2 :: Bool
+ter2 = ((Left "exc" :: Either String (Int,Int)) ==) $
+       run $ runError (runState tes1 (1::Int))
+
+
+teCatch :: Member (Exc String) r => Eff r a -> Eff r [Char]
+teCatch m = catchError (m >> return "done") (\e -> return (e::String))
+
+ter3 :: Bool
+ter3 = ((Right "exc" :: Either String String,2) ==) $
+       run $ runState (runError (teCatch tes1)) (1::Int)
+
+ter4 :: Bool
+ter4 = ((Right ("exc",2) :: Either String (String,Int)) ==) $
+       run $ runError (runState (teCatch tes1) (1::Int))
+
+ex2r = runReader (runErrBig (ex2 ask)) (5::Int)
+
+ex2rr = Right 5 == run ex2r
+
+ex2rr1 = (Left (TooBig 7) ==) $
+         run $ runReader (runErrBig (ex2 ask)) (7::Int)
+
+-- Different order of handlers (layers)
+ex2rr2 = (Left (TooBig 7) ==) $
+         run $ runErrBig (runReader (ex2 ask) (7::Int))
diff --git a/src/Control/Monad/Freer/Fresh.hs b/src/Control/Monad/Freer/Fresh.hs
new file mode 100644
index 0000000..6e43642
--- /dev/null
+++ b/src/Control/Monad/Freer/Fresh.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+module Control.Monad.Freer.Fresh (
+  Fresh,
+  fresh,
+  runFresh'
+) where
+
+import Control.Monad.Freer.Internal
+import Control.Monad.Freer.Trace  -- for example
+
+--------------------------------------------------------------------------------
+                             -- Fresh --
+--------------------------------------------------------------------------------
+data Fresh v where
+  Fresh :: Fresh Int
+
+fresh :: Member Fresh r => Eff r Int
+fresh = send Fresh
+
+-- And a handler for it
+runFresh' :: Eff (Fresh ': r) w -> Int -> Eff r w
+runFresh' m s =
+  handleRelayS s (\_s x -> return x)
+                 (\s Fresh k -> (k $! s+1) s)
+                 m
+
+--------------------------------------------------------------------------------
+                             -- Tests --
+--------------------------------------------------------------------------------
+tfresh' :: IO ()
+tfresh' = runTrace $ flip runFresh' 0 $ do
+  n <- fresh
+  trace $ "Fresh " ++ show n
+  n <- fresh
+  trace $ "Fresh " ++ show n
+{-
+Fresh 0
+Fresh 1
+-}
diff --git a/src/Control/Monad/Freer/Internal.hs b/src/Control/Monad/Freer/Internal.hs
new file mode 100644
index 0000000..9967e00
--- /dev/null
+++ b/src/Control/Monad/Freer/Internal.hs
@@ -0,0 +1,566 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+-- The following is needed to define MonadPlus instance. It is decidable
+-- (there is no recursion!), but GHC cannot see that.
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Monad.Freer.Internal (
+  Eff(..),
+  Member(..),
+  Arr,
+  Arrs,
+  Union,
+
+  decomp,
+  tsingleton,
+
+  qApp,
+  qComp,
+  send,
+  run,
+  handleRelay,
+  handleRelayS,
+  interpose,
+) where
+
+import Data.Open.Union
+import Data.FTCQueue
+
+
+-- The framework of extensible effects
+
+-- ------------------------------------------------------------------------
+-- A monadic library for communication between a handler and
+-- its client, the administered computation
+
+-- Effectful arrow type: a function from a to b that also does effects
+-- denoted by r
+type Arr r a b = a -> Eff r b
+
+-- An effectful function from 'a' to 'b' that is a composition
+-- of several effectful functions. The paremeter r describes the overall
+-- effect.
+-- The composition members are accumulated in a type-aligned queue
+type Arrs r a b = FTCQueue (Eff r) a b
+
+-- The Eff monad (not a transformer!)
+-- It is a fairly standard coroutine monad
+-- It is NOT a Free monad! There are no Functor constraints
+-- Status of a coroutine (client): done with the value of type w,
+-- or sending a request of type Union r with the continuation
+-- Arrs r b a.
+data Eff r a = Val a
+             | forall b. E (Union r b) (Arrs r b a)
+
+-- Application to the `generalized effectful function' Arrs r b w
+qApp :: Arrs r b w -> b -> Eff r w
+qApp q' x =
+   case tviewl q' of
+   TOne k  -> k x
+   k :| t -> case k x of
+     Val y -> qApp t y
+     E u q -> E u (q >< t)
+
+-- Compose effectful arrows (and possibly change the effect!)
+qComp :: Arrs r a b -> (Eff r b -> Eff r' c) -> Arr r' a c
+qComp g h a = h $ qApp g a
+
+-- Eff is still a monad and a functor (and Applicative)
+-- (despite the lack of the Functor constraint)
+
+instance Functor (Eff r) where
+  {-# INLINE fmap #-}
+  fmap f (Val x) = Val (f x)
+  fmap f (E u q) = E u (q |> (Val . f)) -- does no mapping yet!
+
+instance Applicative (Eff r) where
+  {-# INLINE pure #-}
+  {-# INLINE (<*>) #-}
+  pure = Val
+  Val f <*> Val x = Val $ f x
+  Val f <*> E u q = E u (q |> (Val . f))
+  E u q <*> Val x = E u (q |> (Val . ($ x)))
+  E u q <*> m     = E u (q |> (`fmap` m))
+
+instance Monad (Eff r) where
+  {-# INLINE return #-}
+  {-# INLINE (>>=) #-}
+  return = Val
+  Val x >>= k = k x
+  E u q >>= k = E u (q |> k)          -- just accumulates continuations
+
+
+-- send a request and wait for a reply
+send :: Member t r => t v -> Eff r v
+send t = E (inj t) (tsingleton Val)
+
+-- ------------------------------------------------------------------------
+-- The initial case, no effects
+
+-- The type of run ensures that all effects must be handled:
+-- only pure computations may be run.
+run :: Eff '[] w -> w
+run (Val x) = x
+-- the other case is unreachable since Union [] a cannot be
+-- constructed.
+-- Therefore, run is a total function if its argument terminates.
+
+-- A convenient pattern: given a request (open union), either
+-- handle it or relay it.
+handleRelay :: (a -> Eff r w) ->
+               (forall v. t v -> Arr r v w -> Eff r w) ->
+               Eff (t ': r) a -> Eff r w
+handleRelay ret h = loop
+ where
+  loop (Val x)  = ret x
+  loop (E u' q)  = case decomp u' of
+    Right x -> h x k
+    Left  u -> E u (tsingleton k)
+   where k = qComp q loop
+
+-- Parameterized handle_relay
+handleRelayS :: s ->
+                (s -> a -> Eff r w) ->
+                (forall v. s -> t v -> (s -> Arr r v w) -> Eff r w) ->
+                Eff (t ': r) a -> Eff r w
+handleRelayS s' ret h = loop s'
+  where
+    loop s (Val x)  = ret s x
+    loop s (E u' q)  = case decomp u' of
+      Right x -> h s x k
+      Left  u -> E u (tsingleton (k s))
+     where k s'' x = loop s'' $ qApp q x
+
+-- Add something like Control.Exception.catches? It could be useful
+-- for control with cut.
+
+-- Intercept the request and possibly reply to it, but leave it unhandled
+-- (that's why we use the same r all throuout)
+interpose :: Member t r =>
+             (a -> Eff r w) -> (forall v. t v -> Arr r v w -> Eff r w) ->
+             Eff r a -> Eff r w
+interpose ret h = loop
+ where
+   loop (Val x)  = ret x
+   loop (E u q)  = case prj u of
+     Just x -> h x k
+     _      -> E u (tsingleton k)
+    where k = qComp q loop
+
+{- EXAMPLE
+rdwr :: (Member (Reader Int) r, Member (Writer String) r)
+     => Eff r Int
+rdwr = do
+  tell "begin"
+  r <- addN 10
+  tell "end"
+  return r
+
+rdwrr :: (Int,[String])
+rdwrr = run . (`runReader` (1::Int)) . runWriter $ rdwr
+-- (10,["begin","end"])
+-}
+
+-- Encapsulation of effects
+-- The example suggested by a reviewer
+
+{- The reviewer outlined an MTL implementation below, writing
+  ``This hides the state effect and I can layer another state effect on
+  top without getting into conflict with the class system.''
+
+class Monad m => MonadFresh m where
+    fresh :: m Int
+
+newtype FreshT m a = FreshT { unFreshT :: State Int m a }
+      deriving (Functor, Monad, MonadTrans)
+
+    instance Monad m => MonadFresh (FreshT m) where
+      fresh = FreshT $ do n <- get; put (n+1); return n
+
+See EncapsMTL.hs for the complete code.
+-}
+
+-- There are three possible implementations
+-- The first one uses State Fresh where
+--    newtype Fresh = Fresh Int
+-- We get the `private' effect layer (State Fresh) that does not interfere
+-- with with other layers.
+-- This is the easiest implementation.
+
+-- The second implementation defines a new effect Fresh
+
+{-
+-- Finally, the worst implementation but the one that answers
+-- reviewer's question: implementing Fresh in terms of State
+-- but not revealing that fact.
+
+runFresh :: Eff (Fresh :> r) w -> Int -> Eff r w
+runFresh m s = runState m' s >>= return . fst
+ where
+ m' = loop m
+ loop (Val x) = return x
+ loop (E u q)   = case decomp u of
+  Right Fresh -> do
+                 n <- get
+                 put (n+1::Int)
+                 k n
+  Left u  -> send (\k -> weaken $ fmap k u) >>= loop
+
+tfresh = runTrace $ flip runFresh 0 $ do
+  n <- fresh
+  -- (x::Int) <- get
+  trace $ "Fresh " ++ show n
+  n <- fresh
+  trace $ "Fresh " ++ show n
+
+{-
+If we try to meddle with the encapsulated state, by uncommenting the
+get statement above, we get:
+    No instance for (Member (State Int) Void)
+      arising from a use of `get'
+-}
+
+-}
+
+-- ------------------------------------------------------------------------
+-- Lifting: emulating monad transformers
+
+-- newtype Lift m a = Lift (m a)
+
+
+{-
+ -- ------------------------------------------------------------------------
+-- Co-routines
+-- The interface is intentionally chosen to be the same as in transf.hs
+
+-- The yield request: reporting the value of type a and suspending
+-- the coroutine. Resuming with the value of type b
+data Yield a b v = Yield a (b -> v)
+    deriving (Typeable, Functor)
+
+-- The signature is inferred
+yield :: (Typeable a, Typeable b, Member (Yield a b) r) => a -> Eff r b
+yield x = send (inj . Yield x)
+
+-- Status of a thread: done or reporting the value of the type a
+-- and resuming with the value of type b
+data Y r a b = Done | Y a (b -> Eff r (Y r a b))
+
+-- Launch a thread and report its status
+runC :: (Typeable a, Typeable b) =>
+        Eff (Yield a b :> r) w -> Eff r (Y r a b)
+runC m = loop (admin m) where
+ loop (Val x) = return Done
+ loop (E u)   = handle_relay u loop $
+                 \(Yield x k) -> return (Y x (loop . k))
+
+
+-- First example of coroutines
+yieldInt :: Member (Yield Int ()) r => Int -> Eff r ()
+yieldInt = yield
+
+th1 :: Member (Yield Int ()) r => Eff r ()
+th1 = yieldInt 1 >> yieldInt 2
+
+
+c1 = runTrace (loop =<< runC th1)
+ where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
+       loop Done    = trace "Done"
+{-
+1
+2
+Done
+-}
+
+-- Add dynamic variables
+-- The code is essentially the same as that in transf.hs (only added
+-- a type specializtion on yield). The inferred signature is different though.
+-- Before it was
+--    th2 :: MonadReader Int m => CoT Int m ()
+-- Now it is more general:
+th2 :: (Member (Yield Int ()) r, Member (Reader Int) r) => Eff r ()
+th2 = ask >>= yieldInt >> (ask >>= yieldInt)
+
+
+-- Code is essentially the same as in transf.hs; no liftIO though
+c2 = runTrace $ runReader (loop =<< runC th2) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
+       loop Done    = trace "Done"
+{-
+10
+10
+Done
+-}
+
+-- locally changing the dynamic environment for the suspension
+c21 = runTrace $ runReader (loop =<< runC th2) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
+       loop Done    = trace "Done"
+{-
+10
+11
+Done
+-}
+
+-- Real example, with two sorts of local rebinding
+th3 :: (Member (Yield Int ()) r, Member (Reader Int) r) => Eff r ()
+th3 = ay >> ay >> local (+(10::Int)) (ay >> ay)
+ where ay = ask >>= yieldInt
+
+c3 = runTrace $ runReader (loop =<< runC th3) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
+       loop Done    = trace "Done"
+{-
+10
+10
+20
+20
+Done
+-}
+
+-- locally changing the dynamic environment for the suspension
+c31 = runTrace $ runReader (loop =<< runC th3) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
+       loop Done    = trace "Done"
+{-
+10
+11
+21
+21
+Done
+-}
+-- The result is exactly as expected and desired: the coroutine shares the
+-- dynamic environment with its parent; however, when the environment
+-- is locally rebound, it becomes private to coroutine.
+
+-- We now make explicit that the client computation, run by th4,
+-- is abstract. We abstract it out of th4
+c4 = runTrace $ runReader (loop =<< runC (th4 client)) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
+       loop Done    = trace "Done"
+
+       -- cl, client, ay are monomorphic bindings
+       th4 cl = cl >> local (+(10::Int)) cl
+       client = ay >> ay
+       ay     = ask >>= yieldInt
+
+{-
+10
+11
+21
+21
+Done
+-}
+
+-- Even more dynamic example
+c5 = runTrace $ runReader (loop =<< runC (th client)) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> local (\y->x+1) (k ()) >>= loop
+       loop Done    = trace "Done"
+
+       -- cl, client, ay are monomorphic bindings
+       client = ay >> ay >> ay
+       ay     = ask >>= yieldInt
+
+       -- There is no polymorphic recursion here
+       th cl = do
+         cl
+         v <- ask
+         (if v > (20::Int) then id else local (+(5::Int))) cl
+         if v > (20::Int) then return () else local (+(10::Int)) (th cl)
+{-
+10
+11
+12
+18
+18
+18
+29
+29
+29
+29
+29
+29
+Done
+-}
+
+-- And even more
+c7 = runTrace $
+      runReader (runReader (loop =<< runC (th client)) (10::Int)) (1000::Double)
+ where loop (Y x k) = trace (show (x::Int)) >>
+                      local (\y->fromIntegral (x+1)::Double) (k ()) >>= loop
+       loop Done    = trace "Done"
+
+       -- cl, client, ay are monomorphic bindings
+       client = ay >> ay >> ay
+       ay     = ask >>= \x -> ask >>=
+                 \y -> yieldInt (x + round (y::Double))
+
+       -- There is no polymorphic recursion here
+       th cl = do
+         cl
+         v <- ask
+         (if v > (20::Int) then id else local (+(5::Int))) cl
+         if v > (20::Int) then return () else local (+(10::Int)) (th cl)
+
+{-
+1010
+1021
+1032
+1048
+1064
+1080
+1101
+1122
+1143
+1169
+1195
+1221
+1252
+1283
+1314
+1345
+1376
+1407
+Done
+-}
+
+c7' = runTrace $
+      runReader (runReader (loop =<< runC (th client)) (10::Int)) (1000::Double)
+ where loop (Y x k) = trace (show (x::Int)) >>
+                      local (\y->fromIntegral (x+1)::Double) (k ()) >>= loop
+       loop Done    = trace "Done"
+
+       -- cl, client, ay are monomorphic bindings
+       client = ay >> ay >> ay
+       ay     = ask >>= \x -> ask >>=
+                 \y -> yieldInt (x + round (y::Double))
+
+       -- There is no polymorphic recursion here
+       th cl = do
+         cl
+         v <- ask
+         (if v > (20::Int) then id else local (+(5::Double))) cl
+         if v > (20::Int) then return () else local (+(10::Int)) (th cl)
+{-
+1010
+1021
+1032
+1048
+1048
+1048
+1069
+1090
+1111
+1137
+1137
+1137
+1168
+1199
+1230
+1261
+1292
+1323
+Done
+-}
+
+-- ------------------------------------------------------------------------
+-- An example of non-trivial interaction of effects, handling of two
+-- effects together
+-- Non-determinism with control (cut)
+-- For the explanation of cut, see Section 5 of Hinze ICFP 2000 paper.
+-- Hinze suggests expressing cut in terms of cutfalse
+--  ! = return () `mplus` cutfalse
+-- where
+--  cutfalse :: m a
+-- satisfies the following laws
+--   cutfalse >>= k  = cutfalse              (F1)
+--   cutfalse | m    = cutfalse              (F2)
+-- (note: m `mplus` cutfalse is different from cutfalse `mplus` m)
+-- In other words, cutfalse is the left zero of both bind and mplus.
+--
+-- Hinze also introduces the operation call :: m a -> m a that
+-- delimits the effect of cut: call m executes m. If the cut is
+-- invoked in m, it discards only the choices made since m was called.
+-- Hinze postulates the axioms of call:
+--
+--   call false = false                          (C1)
+--   call (return a | m) = return a | call m     (C2)
+--   call (m | cutfalse) = call m                (C3)
+--   call (lift m >>= k) = lift m >>= (call . k) (C4)
+--
+-- call m behaves like m except any cut inside m has only a local effect,
+-- he says.
+
+-- Hinze noted a problem with the `mechanical' derivation of backtracing
+-- monad transformer with cut: no axiom specifying the interaction of
+-- call with bind; no way to simplify nested invocations of call.
+
+-- We use exceptions for cutfalse
+-- Therefore, the law ``cutfalse >>= k       = cutfalse''
+-- is satisfied automatically since all exceptions have the above property.
+
+data CutFalse = CutFalse deriving Typeable
+
+cutfalse = throwError CutFalse
+
+-- The interpreter -- it is like reify . reflect with a twist
+-- Compare this implementation with the huge implementation of call
+-- in Hinze 2000 (Figure 9)
+-- Each clause corresponds to the axiom of call or cutfalse.
+-- All axioms are covered.
+-- The code clearly expresses the intuition that call watches the choice points
+-- of its argument computation. When it encounteres a cutfalse request,
+-- it discards the remaining choicepoints.
+
+-- It completely handles CutFalse effects but not non-determinism
+call :: Member Choose r => Eff (Exc CutFalse :> r) a -> Eff r a
+call m = loop [] (admin m) where
+ loop jq (Val x) = return x `mplus'` next jq          -- (C2)
+ loop jq (E u) = case decomp u of
+    Right (Exc CutFalse) -> mzero'  -- drop jq (F2)
+    Left u -> check jq u
+
+ check jq u | Just (Choose [] _) <- prj u  = next jq  -- (C1)
+ check jq u | Just (Choose [x] k) <- prj u = loop jq (k x)  -- (C3), optim
+ check jq u | Just (Choose lst k) <- prj u = next $ map k lst ++ jq -- (C3)
+ check jq u = send (\k -> fmap k u) >>= loop jq      -- (C4)
+
+ next []    = mzero'
+ next (h:t) = loop t h
+
+-- The signature is inferred
+tcut1 :: (Member Choose r, Member (Exc CutFalse) r) => Eff r Int
+tcut1 = (return (1::Int) `mplus'` return 2) `mplus'`
+         ((cutfalse `mplus'` return 4) `mplus'`
+          return 5)
+
+tcut1r = run . makeChoice $ call tcut1
+-- [1,2]
+
+tcut2 = return (1::Int) `mplus'`
+         call (return 2 `mplus'` (cutfalse `mplus'` return 3) `mplus'`
+               return 4)
+       `mplus'` return 5
+
+-- Here we see nested call. It poses no problems...
+tcut2r = run . makeChoice $ call tcut2
+-- [1,2,5]
+
+-- More nested calls
+tcut3 = call tcut1 `mplus'` call (tcut2 `mplus'` cutfalse)
+tcut3r = run . makeChoice $ call tcut3
+-- [1,2,1,2,5]
+
+tcut4 = call tcut1 `mplus'`  (tcut2 `mplus'` cutfalse)
+tcut4r = run . makeChoice $ call tcut4
+-- [1,2,1,2,5]
+-}
diff --git a/src/Control/Monad/Freer/Reader.hs b/src/Control/Monad/Freer/Reader.hs
new file mode 100644
index 0000000..1d30f95
--- /dev/null
+++ b/src/Control/Monad/Freer/Reader.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+module Control.Monad.Freer.Reader (
+  Reader(..),
+
+  ask,
+  runReader',
+  runReader,
+  local
+) where
+
+import Control.Applicative
+import Control.Monad.Freer.Internal
+
+-- ------------------------------------------------------------------------
+-- The Reader monad
+
+-- The request for a value of type e from the current environment
+-- This is a GADT because the type of values
+-- returned in response to a (Reader e a) request is not any a;
+-- we expect in reply the value of type 'e', the value from the
+-- environment. So, the return type is restricted: 'a ~ e'
+data Reader e v where
+  Reader :: Reader e e
+
+-- One can also define this as
+--    data Reader e v = (e ~ v) => Reader
+-- and even without GADTs, using explicit coercion:
+--    newtype Reader e v = Reader (e->v)
+-- In the latter case, when we make the request, we make it as Reader id.
+-- So, strictly speaking, GADTs are not really necessary.
+
+
+-- The signature is inferred
+ask :: (Member (Reader e) r) => Eff r e
+ask = send Reader
+
+-- The handler of Reader requests. The return type shows that
+-- all Reader requests are fully handled.
+runReader' :: Eff (Reader e ': r) w -> e -> Eff r w
+runReader' m e = loop m where
+ loop (Val x) = return x
+ loop (E u' q) = case decomp u' of
+                  Right Reader -> loop $ qApp q e
+                  Left  u      -> E u (tsingleton (qComp q loop))
+
+-- A different way of writing the above
+runReader :: Eff (Reader e ': r) w -> e -> Eff r w
+runReader m e = handleRelay return (\Reader k -> k e) m
+
+-- Locally rebind the value in the dynamic environment
+-- This function is like a relay; it is both an admin for Reader requests,
+-- and a requestor of them
+local :: forall e a r. Member (Reader e) r =>
+         (e -> e) -> Eff r a -> Eff r a
+local f m = do
+  e0 <- ask
+  let e = f e0
+  -- Local signature is needed, as always with GADTs
+  let h :: Reader e v -> Arr r v a -> Eff r a
+      h Reader g = g e
+  interpose return h m
+
+
+-- Examples
+add :: Applicative f => f Int -> f Int -> f Int
+add = liftA2 (+)
+
+
+-- The type is inferred
+t1 :: Member (Reader Int) r => Eff r Int
+t1 = ask `add` return (1 :: Int)
+
+t1' :: Member (Reader Int) r => Eff r Int
+t1' = do v <- ask; return (v + 1 :: Int)
+
+-- t1r :: Eff r Int
+t1r = runReader t1 (10::Int)
+
+t1rr = 11 == run t1r
+
+{-
+t1rr' = run t1
+    No instance for (Member (Reader Int) Void)
+      arising from a use of `t1'
+-}
+
+-- Inferred type
+-- t2 :: (Member (Reader Int) r, Member (Reader Float) r) => Eff r Float
+t2 = do
+  v1 <- ask
+  v2 <- ask
+  return $ fromIntegral (v1 + (1::Int)) + (v2 + (2::Float))
+
+-- t2r :: Member (Reader Float) r => Eff r Float
+t2r = runReader t2 (10::Int)
+-- t2rr :: Eff r Float
+t2rr = flip runReader (20::Float) . flip runReader (10::Int) $ t2
+
+t2rrr = 33.0 == run t2rr
+
+-- The opposite order of layers
+{- If we mess up, we get an error
+t2rrr1' = run $ runReader (runReader t2 (20::Float)) (10::Float)
+    No instance for (Member (Reader Int) [])
+      arising from a use of `t2'
+-}
+t2rrr' = (33.0 ==) $
+         run $ runReader (runReader t2 (20 :: Float)) (10 :: Int)
+
+-- The type is inferred
+t3 :: Member (Reader Int) r => Eff r Int
+t3 = t1 `add` local (+ (10::Int)) t1
+t3r = (212 ==) $ run $ runReader t3 (100::Int)
+
+
+-- The following example demonstrates true interleaving of Reader Int
+-- and Reader Float layers
+{-
+t4
+  :: (Member (Reader Int) r, Member (Reader Float) r) =>
+     () -> Eff r Float
+-}
+t4 = liftA2 (+) (local (+ (10::Int)) t2)
+                (local (+ (30::Float)) t2)
+
+t4rr = (106.0 ==) $ run $ runReader (runReader t4 (10::Int)) (20::Float)
+
+-- The opposite order of layers gives the same result
+t4rr' = (106.0 ==) $ run $ runReader (runReader t4 (20 :: Float)) (10 :: Int)
+
+addGet :: Member (Reader Int) r => Int -> Eff r Int
+addGet x = ask >>= \i -> return (i+x)
+
+addN n = foldl (>>>) return (replicate n addGet) 0
+ where f >>> g = (>>= g) . f
+
+-- Map an effectful function
+-- The type is inferred
+tmap :: Member (Reader Int) r => Eff r [Int]
+tmap = mapM f [1..5]
+ where f x = ask `add` return x
+
+tmapr = ([11,12,13,14,15] ==) $
+        run $ runReader tmap (10::Int)
diff --git a/src/Control/Monad/Freer/State.hs b/src/Control/Monad/Freer/State.hs
new file mode 100644
index 0000000..55c2ce0
--- /dev/null
+++ b/src/Control/Monad/Freer/State.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+module Control.Monad.Freer.State (
+  State,
+  get,
+  put,
+  runState',
+  runState,
+  transactionState
+) where
+
+import Control.Monad.Freer.Internal
+
+--------------------------------------------------------------------------------
+                         -- State, strict --
+--------------------------------------------------------------------------------
+
+{- Initial design:
+-- The state request carries with it the state mutator function
+-- We can use this request both for mutating and getting the state.
+-- But see below for a better design!
+data State s v where
+  State :: (s->s) -> State s s
+
+In this old design, we have assumed that the dominant operation is
+modify. Perhaps this is not wise. Often, the reader is most nominant.
+-}
+-- See also below, for decomposing the State into Reader and Writer!
+
+-- The conventional design of State
+data State s v where
+  Get :: State s s
+  Put :: !s -> State s ()
+
+-- The signatures are inferred
+get :: Member (State s) r => Eff r s
+get = send Get
+
+put :: Member (State s) r => s -> Eff r ()
+put s = send (Put s)
+
+runState' :: Eff (State s ': r) w -> s -> Eff r (w,s)
+runState' m s =
+  handleRelayS s (\s x -> return (x,s))
+                 (\s sreq k -> case sreq of
+                     Get    -> k s s
+                     Put s' -> k s' ())
+                 m
+
+-- Since State is so frequently used, we optimize it a bit
+runState :: Eff (State s ': r) w -> s -> Eff r (w,s)
+runState (Val x) s = return (x,s)
+runState (E u q) s = case decomp u of
+  Right Get     -> runState (qApp q s) s
+  Right (Put s) -> runState (qApp q ()) s
+  Left  u -> E u (tsingleton (\x -> runState (qApp q x) s))
+
+
+-- An encapsulated State handler, for transactional semantics
+-- The global state is updated only if the transactionState finished
+-- successfully
+data ProxyState s = ProxyState
+transactionState :: forall s r w. Member (State s) r =>
+                    ProxyState s -> Eff r w -> Eff r w
+transactionState _ m = do s <- get; loop s m
+ where
+   loop :: s -> Eff r w -> Eff r w
+   loop s (Val x) = put s >> return x
+   loop s (E (u :: Union r b) q) = case prj u :: Maybe (State s b) of
+     Just Get      -> loop s (qApp q s)
+     Just (Put s') -> loop s'(qApp q ())
+     _      -> E u (tsingleton k) where k = qComp q (loop s)
+
+--------------------------------------------------------------------------------
+                       -- Tests and Examples --
+--------------------------------------------------------------------------------
+ts1 :: Member (State Int) r => Eff r Int
+ts1 = do
+  put (10 ::Int)
+  x <- get
+  return (x::Int)
+
+ts1r = ((10,10) ==) $ run (runState ts1 (0::Int))
+
+ts2 :: Member (State Int) r => Eff r Int
+ts2 = do
+  put (10::Int)
+  x <- get
+  put (20::Int)
+  y <- get
+  return (x+y)
+
+ts2r = ((30,20) ==) $ run (runState ts2 (0::Int))
diff --git a/src/Control/Monad/Freer/StateRW.hs b/src/Control/Monad/Freer/StateRW.hs
new file mode 100644
index 0000000..767c4e1
--- /dev/null
+++ b/src/Control/Monad/Freer/StateRW.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+module Control.Monad.Freer.StateRW (
+  runStateR
+) where
+
+import Control.Monad.Freer.Reader
+import Control.Monad.Freer.Writer
+import Control.Monad.Freer.Internal
+
+--------------------------------------------------------------------------------
+                 -- State: Using Reader and Writer --
+--------------------------------------------------------------------------------
+-- A different representation of State: decomposing State into
+-- mutation (Writer) and Reading. We don't define any new effects:
+-- we just handle the existing ones.
+-- Thus we define a handler for two effects together.
+
+runStateR :: Eff (Writer s ': Reader s ': r) w -> s -> Eff r (w,s)
+runStateR m s = loop s m
+ where
+   loop :: s -> Eff (Writer s ': Reader s ': r) w -> Eff r (w,s)
+   loop s (Val x) = return (x,s)
+   loop s (E u q) = case decomp u of
+     Right (Writer o) -> k o ()
+     Left  u  -> case decomp u of
+       Right Reader -> k s s
+       Left u -> E u (tsingleton (k s))
+    where k s = qComp q (loop s)
+
+--------------------------------------------------------------------------------
+                       -- Tests and Examples --
+--------------------------------------------------------------------------------
+-- If we had a Writer, we could have decomposed State into Writer and Reader
+-- requests.
+
+ts11 :: (Member (Reader Int) r, Member (Writer Int) r) => Eff r Int
+ts11 = do
+  tell (10 ::Int)
+  x <- ask
+  return (x::Int)
+
+ts11r :: Bool
+ts11r = ((10,10) ==) $ run (runStateR ts11 (0::Int))
+
+
+ts21 :: (Member (Reader Int) r, Member (Writer Int) r) => Eff r Int
+ts21 = do
+  tell (10::Int)
+  x <- ask
+  tell (20::Int)
+  y <- ask
+  return (x+y)
+
+ts21r :: Bool
+ts21r = ((30,20) ==) $ run (runStateR ts21 (0::Int))
diff --git a/src/Control/Monad/Freer/Trace.hs b/src/Control/Monad/Freer/Trace.hs
new file mode 100644
index 0000000..775c140
--- /dev/null
+++ b/src/Control/Monad/Freer/Trace.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+module Control.Monad.Freer.Trace (
+  Trace,
+  trace,
+  runTrace
+) where
+
+import Control.Monad
+import Control.Monad.Freer.Internal
+import Control.Monad.Freer.Reader -- for examples
+
+--------------------------------------------------------------------------------
+                    -- Tracing (debug printing) --
+--------------------------------------------------------------------------------
+data Trace v where
+  Trace :: String -> Trace ()
+
+-- Printing a string in a trace
+trace :: Member Trace r => String -> Eff r ()
+trace = send . Trace
+
+-- The handler for IO request: a terminal handler
+runTrace :: Eff '[Trace] w -> IO w
+runTrace (Val x) = return x
+runTrace (E u q) = case decomp u of
+     Right (Trace s) -> putStrLn s >> runTrace (qApp q ())
+     -- Nothing more can occur
+
+--------------------------------------------------------------------------------
+                       -- Tests and Examples --
+--------------------------------------------------------------------------------
+-- Higher-order effectful function
+-- The inferred type shows that the Trace affect is added to the effects
+-- of r
+mapMdebug:: (Show a, Member Trace r) =>
+     (a -> Eff r b) -> [a] -> Eff r [b]
+mapMdebug f [] = return []
+mapMdebug f (h:t) = do
+ trace $ "mapMdebug: " ++ show h
+ h' <- f h
+ t' <- mapMdebug f t
+ return (h':t')
+
+add = liftM2 (+)
+
+tMd :: IO [Int]
+tMd = runTrace $ runReader (mapMdebug f [1..5]) (10::Int)
+ where f x = ask `add` return x
+{-
+mapMdebug: 1
+mapMdebug: 2
+mapMdebug: 3
+mapMdebug: 4
+mapMdebug: 5
+[11,12,13,14,15]
+-}
+
+-- duplicate layers
+tdup :: IO ()
+tdup = runTrace $ runReader m (10::Int)
+ where
+ m = do
+     runReader tr (20::Int)
+     tr
+ tr = do
+      v <- ask
+      trace $ "Asked: " ++ show (v::Int)
+{-
+Asked: 20
+Asked: 10
+-}
diff --git a/src/Control/Monad/Freer/Writer.hs b/src/Control/Monad/Freer/Writer.hs
new file mode 100644
index 0000000..50f0330
--- /dev/null
+++ b/src/Control/Monad/Freer/Writer.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+module Control.Monad.Freer.Writer (
+  Writer(..),
+  tell,
+  runWriter
+) where
+
+import Control.Monad.Freer.Internal
+
+-- ------------------------------------------------------------------------
+-- The Writer monad
+
+-- In MTL's Writer monad, the told value must have a |Monoid| type. Our
+-- writer has no such constraints. If we write a |Writer|-like
+-- interpreter to accumulate the told values in a monoid, it will have
+-- the |Monoid o| constraint then
+
+data Writer o x where
+  Writer :: o -> Writer o ()
+
+tell :: Member (Writer o) r => o -> Eff r ()
+tell o = send $ Writer o
+
+-- We accumulate the told data in a list, hence no Monoid constraints
+-- The code is written to be simple, not optimized.
+-- If performance matters, we should convert it to accumulator
+
+runWriter :: Eff (Writer o ': r) a -> Eff r (a,[o])
+runWriter = handleRelay (\x -> return (x,[]))
+                  (\ (Writer o) k -> k () >>= \ (x,l) -> return (x,o:l))
diff --git a/src/Data/FTCQueue.hs b/src/Data/FTCQueue.hs
new file mode 100644
index 0000000..8924aa8
--- /dev/null
+++ b/src/Data/FTCQueue.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE GADTs #-}
+
+-- A repackaging of: http://okmij.org/ftp/Haskell/extensible/FTCQueue1.hs
+module Data.FTCQueue (
+  FTCQueue,
+  tsingleton,
+  (|>),
+  snoc,
+  (><),
+  append,
+  ViewL(..),
+  tviewl
+) where
+
+-- Fast type-aligned queue optimized to effectful functions
+-- (a -> m b)
+-- (monad continuations have this type).
+-- Constant-time append and snoc and
+-- average constant-time left-edge deconstruction
+
+-- Non-empty tree. Deconstruction operations make it more and more
+-- left-leaning
+data FTCQueue m a b where
+  Leaf :: (a -> m b) -> FTCQueue m a b
+  Node :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
+
+
+-- Exported operations
+
+-- There is no tempty: use (tsingleton return), which works just the same.
+-- The names are chosen for compatibility with FastTCQueue
+
+-- tempty = tsingleton return
+
+{-# INLINE tsingleton #-}
+tsingleton :: (a -> m b) -> FTCQueue m a b
+tsingleton r = Leaf r
+
+{-# INLINE (|>) #-}
+(|>) :: FTCQueue m a x -> (x -> m b) -> FTCQueue m a b
+snoc :: FTCQueue m a x -> (x -> m b) -> FTCQueue m a b
+t |> r = Node t (Leaf r)
+snoc = (|>)
+
+{-# INLINE (><) #-}
+(><)   :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
+append :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
+t1 >< t2 = Node t1 t2
+append = (><)
+
+-- Left-edge deconstruction
+data ViewL m a b where
+  TOne  :: (a -> m b) -> ViewL m a b
+  (:|)  :: (a -> m x) -> (FTCQueue m x b) -> ViewL m a b
+
+tviewl :: FTCQueue m a b -> ViewL m a b
+tviewl (Leaf r) = TOne r
+tviewl (Node t1 t2) = go t1 t2
+ where
+   go :: FTCQueue m a x -> FTCQueue m x b -> ViewL m a b
+   go (Leaf r) tr = r :| tr
+   go (Node tl1 tl2) tr = go tl1 (Node tl2 tr)
diff --git a/src/Data/Open/Union.hs b/src/Data/Open/Union.hs
new file mode 100644
index 0000000..62da247
--- /dev/null
+++ b/src/Data/Open/Union.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- repackaging of: http://okmij.org/ftp/Haskell/extensible/OpenUnion41.hs
+module Data.Open.Union (
+  Union(..),
+  decomp,
+  weaken,
+  Member(..)
+) where
+
+
+-- Open unions (type-indexed co-products) for extensible effects
+-- This implementation relies on _closed_ type families added
+-- to GHC 7.8
+-- It has NO overlapping instances and NO Typeable
+-- Alas, the absence of Typeable means the projections and injections
+-- generally take linear time.
+-- The code illustrate how to use closed type families to
+-- disambiguate otherwise overlapping instances.
+
+-- The interface is the same as of other OpenUnion*.hs
+
+-- The data constructors of Union are not exported
+
+-- Essentially, the nested Either data type
+-- t is can be a GADT and hence not necessarily a Functor
+data Union (r :: [ * -> * ]) v where
+  UNow  :: t v -> Union (t ': r) v
+  UNext :: Union r v -> Union (any ': r) v
+
+{-
+instance Functor (Union r) where
+    {-# INLINE fmap #-}
+    fmap f (UNow x)  = UNow (f x)
+    fmap f (UNext x) = UNext (fmap f x)
+-}
+
+data P (n :: Nat) = P
+
+-- injecting/projecting at a specified position P n
+class Member' t r (n :: Nat) where
+  inj' :: P n -> t v -> Union r v
+  prj' :: P n -> Union r v -> Maybe (t v)
+
+instance (r ~ (t ': r')) => Member' t r 'Z where
+  inj' _ = UNow
+  prj' _ (UNow x) = Just x
+  prj' _ _        = Nothing
+
+instance (r ~ (t' ': r'), Member' t r' n) => Member' t r ('S n) where
+  inj' _ = UNext . inj' (P::P n)
+  prj' _ (UNow _)  = Nothing
+  prj' _ (UNext x) = prj' (P::P n) x
+
+class (Member' t r (FindElem t r)) => Member t r where
+  inj :: t v -> Union r v
+  prj :: Union r v -> Maybe (t v)
+
+instance (Member' t r (FindElem t r)) => Member t r where
+  inj = inj' (P :: P (FindElem t r))
+  prj = prj' (P :: P (FindElem t r))
+
+{-# INLINE decomp #-}
+decomp :: Union (t ': r) v -> Either (Union r v) (t v)
+decomp (UNow x)  = Right x
+decomp (UNext v) = Left v
+
+{-# INLINE weaken #-}
+weaken :: Union r w -> Union (any ': r) w
+weaken = UNext
+
+data Nat = Z | S Nat
+
+-- Find an index of an element in a `list'
+-- The element must exist
+-- This closed type family disambiguates otherwise overlapping
+-- instances
+type family FindElem (t :: * -> *) r :: Nat where
+  FindElem t (t ': r)  = 'Z
+  FindElem t (any ': r)  = 'S (FindElem t r)
+
+type family EQU (a :: k) (b :: k) :: Bool where
+  EQU a a = 'True
+  EQU a b = 'False
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
index 0000000..bee0443
--- /dev/null
+++ b/stack.yaml
@@ -0,0 +1,5 @@
+flags: {}
+packages:
+- '.'
+extra-deps: []
+resolver: lts-3.4