DDC/EffectSystem

Effect typing vs State monads

Instead of state monads (like IO), Disciple uses default strict evaluation and effect typing to deal with computational effects. Effect typing helps us write less code because the types of effectful functions have the same shape as their 'pure' counterparts.

For example, in Haskell the 'pure' map function has type:

    map :: (a -> b) -> [a] -> [b]

but if we need to pass an effectful function defined in terms of a state monad, we must use the monadic version, mapM instead.

    mapM :: Monad m => (a -> m b) -> [a] -> m [b]

This puts us in a situation where we really need two copies of every higher-order function, one 'pure' and one monadic - that's a lot of duplication! It's even more of a problem when a library (like Data.Map) exports a 'pure' version but not a monadic one, in this case we either have to refactor our code to be less monadic, or spend time writing a function that should really be in the library.

With effect typing, the fact that function might cause an effect is orthogonal to its 'shape'. In Haskell, the fact that the putStr prints to the screen is encoded in the type of the return value:

    putStr :: String -> IO ()

In Disciple this fact is encoded as an effect on the function arrow instead:

    putStr :: String -(!e1)> ()
           :- !e1 = !Console

In this type, !e1 is an _effect variable_, much like a is a _type_ variable. !Console is an _effect constructor_ and it tells tells us what _else_ happens when this function is evaluated besides constructing the return value.