Intuitively, I like to think of it as:

- Extensible effects describe what we permit (read from console, print to console) - Indexed monads describe what we demand (you must auth before you can access db, you must open file before you can read it)

I'm actually working on doing a version of this in Haskell. You can see Oleg's version of it here: http://okmij.org/ftp/Haskell/extensible/ParamEff1.hs

I may have a more informed opinion after I read the states-all-the-way paper.

Normal extensible effects looks like:

    data Union :: [Type] -> Type -> Type where
      ...

    data Free :: (Type -> Type) -> Type -> Type where
      ...
    
    type Eff fs = Free (Union fs)
    
    class Inject f fs where
      inj :: f a -> Union fs a
    
    data File :: Type -> Type where
      Open :: FilePath -> File ()
      Close :: FilePath -> File ()
    
    send :: (Inject f fs) => f a -> Eff fs a
    
    -- The inferred type would be more general
    openClose :: Eff '[File] ()
    openClose = do
      send (Open "foo.txt")
      send (Close "foo.txt")

    data HList :: [Type] -> Type where
      Nil :: HList '[]
      (:>) :: a -> HList as -> HList (a ': as)

    data Union :: HList fs -> HList is -> HList is -> Type -> Type where
      ...

    data Free :: (is -> is -> Type -> Type) -> is -> is -> Type -> Type where
      ...
    
    type Eff fs = Free (Union fs)
    
    class Inject f i o fs is os where
      inj :: f i o a -> Union fs is os a
    
    data FileStatus = Open | Closed
    
    data File :: FileStatus -> FileStatus -> Type -> Type where
      Open :: FilePath -> File 'Closed 'Open ()
      Close :: FilePath -> File 'Open 'Closed ()
    
    send :: (Inject f i o fs is os) => f i o a -> Eff fs is os a
    
    -- The inferred type would be more general
    openClose :: Eff (File ':> 'Nil) ('Closed ':> 'Nil) ('Closed ':> Nil) ()
    openClose = do
      send (Open "foo.txt")
      send (Close "foo.txt")

The proliferation of type params looks intimidating from a user perspective though - is there some way to make it easier on folks? Would it look nicer in a language with row polymorphism perhaps?

There are two main differences at the moment:

- Everything has to be labelled - There's no 'implicit' lifting of smaller sets of states

The first is annoying for things like Console IO, so I might change that. The second means that we have a much better chance of providing decent error messages, one day.