@@ -83,7 +83,7 @@ effectful program ``f`` has a type of the following form:
8383
8484.. code-block:: idris
8585
86− f : (x1 : a1) -> (x2 : a2) -> ... -> { effs } Eff t
86+ f : (x1 : a1) -> (x2 : a2) -> ... -> Eff t effs
8787
8888That is, the return type gives the effects that ``f`` supports
8989(``effs``, of type ``List EFFECT``) and the type the computation
@@ -92,7 +92,7 @@ following type:
9292
9393.. code-block:: idris
9494
95− treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))
95+ treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]
9696
9797That is, ``treeTagAux`` has access to an integer state, because the
9898list of available effects includes ``STATE Int``. ``STATE`` is
@@ -141,8 +141,8 @@ following types, polymorphic in the state ``t`` they manage:
141141
142142.. code-block:: idris
143143
144− get : { [STATE t] } Eff t
145− put : t -> { [STATE t] } Eff ()
144+ get : Eff t [STATE t]
145+ put : t -> Eff () [STATE t]
146146
147147A program in ``Eff`` can call any other function in ``Eff`` provided
148148that the calling function supports at least the effects required by
@@ -168,7 +168,7 @@ instead of ``runPure``:
168168
169169.. code-block:: idris
170170
171− treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))
171+ treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]
172172 ...
173173
174174 treeTag : (i : Int) -> BTree a -> IO (BTree (Int, a))
@@ -202,7 +202,7 @@ shown in Listing [introprog].
202202 "Sheila"
203203 (Node Leaf "Bob" Leaf))
204204
205− treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))
205+ treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]
206206 treeTagAux Leaf = pure Leaf
207207 treeTagAux (Node l x r) = do l' <- treeTagAux l
208208 i <- get
@@ -227,8 +227,8 @@ here for illustrative purposes):
227227
228228.. code-block:: idris
229229
230− runPure : {env : Env id xs} -> { xs } Eff a -> a
231− run : Applicative m => {env : Env m xs} -> { xs } Eff a -> m a
230+ runPure : {env : Env id xs} -> Eff a xs -> a
231+ run : Applicative m => {env : Env m xs} -> Eff a xs -> m a
232232
233233The ``env`` argument is implicit, and initialised automatically where
234234possible using default values given by instances of the following type
@@ -248,8 +248,8 @@ using one of the following functions:
248248
249249.. code-block:: idris
250250
251− runPureInit : Env id xs -> { xs } Eff a -> a
252− runInit : Applicative m => Env m xs -> { xs } Eff a -> m a
251+ runPureInit : Env id xs -> Eff a xs -> a
252+ runInit : Applicative m => Env m xs -> Eff a xs -> m a
253253
254254To be well-typed, the environment must contain resources corresponding
255255exactly to the effects in ``xs``. For example, we could also have
@@ -272,8 +272,7 @@ captured both of these values, e.g.:
272272
273273.. code-block:: idris
274274
275− treeTagAux : BTree a
276− -> { [STATE (Int, Int)] } Eff (BTree (Int, a))
275+ treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE (Int, Int)]
277276
278277Doing this, however, ties the two states together throughout (as well
279278as not indicating which integer is which). It would be nice to be able
@@ -288,9 +287,9 @@ leaves and update the tag separately, by labelling them as follows:
288287
289288.. code-block:: idris
290289
291− treeTagAux : BTree a
292− -> {['Tag ::: STATE Int,
293− 'Leaves ::: STATE Int]} Eff (BTree (Int, a))
290+ treeTagAux : BTree a -> Eff (BTree (Int, a))
291+ ['Tag ::: STATE Int,
292+ 'Leaves ::: STATE Int]
294293
295294The ``:::`` operator allows an arbitrary label to be given to an
296295effect. This label can be any type—it is simply used to identify an
@@ -320,7 +319,7 @@ applying a function to the current state.
320319
321320.. code-block:: idris
322321
323− update : (x -> x) -> { [STATE x] } Eff ()
322+ update : (x -> x) -> Eff () [STATE x]
324323
325324Finally, our top level ``treeTag`` function now returns a pair of the
326325number of leaves, and the new tree. Resources for labelled effects are
@@ -339,8 +338,7 @@ To summarise, we have:
339338
340339- ``:::`` to convert an effect to a labelled effect.
341340
342−- ``:-`` to convert an effectful operation to a labelled effectful
343− operation.
341+- ``:-`` to convert an effectful operation to a labelled effectful operation.
344342
345343- ``:=`` to initialise a resource for a labelled effect.
346344
@@ -350,7 +348,7 @@ only for the situation where available effects are not updated):
350348.. code-block:: idris
351349
352350 (:::) : lbl -> EFFECT -> EFFECT
353− (:-) : (l : lbl) -> { [x] } Eff a -> { [l ::: x] } Eff a
351+ (:-) : (l : lbl) -> Eff a [x] -> Eff a [l ::: x]
354352 (:=) : (l : lbl) -> res -> LRes l res
355353
356354Here, ``LRes`` is simply the resource type associated with a labelled
@@ -367,7 +365,7 @@ immediately. The following program returns the length of the
367365
368366.. code-block:: idris
369367
370− stateLength : { [STATE String] } Eff Nat
368+ stateLength : Eff Nat [STATE String]
371369 stateLength = do x <- get
372370 pure (length x)
373371
@@ -377,7 +375,7 @@ this. The above program can be written instead as:
377375
378376.. code-block:: idris
379377
380− stateLength : { [STATE String] } Eff Nat
378+ stateLength : Eff Nat [STATE String]
381379 stateLength = pure (length !get)
382380
383381The notation ``!expr`` means that the expression ``expr`` should be
@@ -386,7 +384,7 @@ evaluated and then implicitly bound. Conceptually, we can think of
386384
387385.. code-block:: idris
388386
389− (!) : { xs } Eff a -> a
387+ (!) : Eff a xs -> a
390388
391389Note, however, that it is not really a function, merely syntax! In
392390practice, a subexpression ``!expr`` will lift ``expr`` as high as
@@ -411,22 +409,22 @@ is lifted to:
411409 g' <- g y' x'
412410 f g'
413411
414−Syntactic Sugar and ``Eff``
415−===========================
412+The Type ``Eff``
413+================
416414
417−By now, you may be wondering about the syntax we are using for
418−``Eff``, because it doesn’t look like a normal type! (If not, you may
419−safely skip this section and return to it later.) In fact, the type of
420−``Eff`` is the following:
415+Underneath, ``Eff`` is an overloaded function which translates to an
416+underlying type ``EffM``:
421417
422418.. code-block:: idris
423419
424− Eff : (x : Type) ->
425− List EFFECT -> (x -> List EFFECT) -> Type
420+ EffM : (m : Type -> Type) -> (t : Type)
421+ -> (List EFFECT)
422+ -> (t -> List EFFECT) -> Type
426423
427424This is more general than the types we have been writing so far. It is
428−parameterised over a result type ``x``, as we have already seen, but
429−also a ``List EFFECT`` and a function type ``x -> List EFFECT``.
425+parameterised over an underying computation context ``m``, a
426+result type ``t`` as we have already seen, as well as a ``List EFFECT`` and a
427+function type ``t -> List EFFECT``.
430428
431429These additional parameters are the list of *input* effects, and a
432430list of *output* effects, computed from the result of an effectful
@@ -435,8 +433,7 @@ of effects available! This is a particularly powerful idea, and we
435433will see its consequences in more detail later. Some examples of
436434operations which can change the set of available effects are:
437435
438−- Updating a state containing a dependent type (for example adding an
439− element to a vector).
436+- Updating a state containing a dependent type (for example adding an element to a vector).
440437
441438- Opening a file for reading is an effect, but whether the file really
442439 *is* open afterwards depends on whether the file was successfully
@@ -445,19 +442,25 @@ operations which can change the set of available effects are:
445442- Closing a file means that reading from the file should no longer be
446443 possible.
447444
448−While powerful, this can make uses of the ``Eff`` type hard to read.
449−Therefore, the library provides syntactic sugar which is translated
450−such that:
445+While powerful, this can make uses of the ``EffM`` type hard to read.
446+Therefore the library provides an overloaded function ``Eff``
447+There are the following three versions:
451448
452449.. code-block:: idris
453450
454− { xs } Eff a
451+ SimpleEff.Eff : (t : Type) -> (input_effs : List EFFECT) -> Type
452+ TransEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->
453+ (output_effs : List EFFECT) -> Type
454+ DepEff.Eff : (t : Type) -> (input_effs : List EFFECT) ->
455+ (output_effs_fn : x -> List EFFECT) -> Type
455456
456−is expanded to
457+So far, we have used only the first version, ``SimpleEff.Eff``, which
458+is defined as follows:
457459
458460.. code-block:: idris
459461
460− Eff a xs (\_ => xs)
462+ Eff : (x : Type) -> (es : List EFFECT) -> Type
463+ Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)
461464
462465i.e. the set of effects remains the same on output. This suffices for
463466the ``STATE`` example we have seen so far, and for many useful
@@ -467,19 +470,19 @@ with the expanded type:
467470.. code-block:: idris
468471
469472 treeTagAux : BTree a ->
470− Eff (BTree (Int, a)) [STATE Int] (\x => [STATE Int])
473+ EffM m (BTree (Int, a)) [STATE Int] (\x => [STATE Int])
471474
472475Later, we will see programs which update effects:
473476
474477.. code-block:: idris
475478
476− { xs ==> xs' } Eff a
479+ Eff a xs xs'
477480
478481which is expanded to
479482
480483.. code-block:: idris
481484
482− Eff a xs (\_ => xs')
485+ EffM m a xs (\_ => xs')
483486
484487i.e. the set of effects is updated to ``xs’`` (think of a transition
485488in a state machine). There is, for example, a version of ``put`` which
@@ -487,22 +490,27 @@ updates the type of the state:
487490
488491.. code-block:: idris
489492
490− putM : y -> { [STATE x] ==> [STATE y] } Eff ()
493+ putM : y -> Eff () [STATE x] [STATE y]
491494
492495Also, we have:
493496
494497.. code-block:: idris
495498
496− { xs ==> {res} xs' } Eff a
499+ Eff t xs (\res => xs')
497500
498501which is expanded to
499502
500503.. code-block:: idris
501504
502− Eff a xs (\res => xs')
505+ EffM m t xs (\res => xs')
503506
504507i.e. the set of effects is updated according to the result of the
505−operation ``res``.
508+operation ``res``, of type ``t``.
509+
510+Parameterising ``EffM`` over an underlying computation context allows us
511+to write effectful programs which are specific to one context, and in some
512+cases to write programs which *extend* the list of effects available using
513+the ``new`` function, though this is beyond the scope of this tutorial.
506514
507515.. [1] The earlier paper [3]_ describes the essential implementation
508516 details, although the library presented there is an earlier version