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! This is 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 the shape of its type. In Haskell, because putStr prints to the screen it has the IO constructor in its 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 us what else happens when this function is called, besides evaluating the return value.

Because this second version of putStr doesn't have the monad in its type, we can just use the plain version of map and not have to worry about mapM.

    
    main () 
     = do   map putStr ["one", "two", "three"]   -- print 'onetwothree'
            ...

Behind the scenes

But wait, that's evil isn't it? From the previous example, it might look as though we've lost the information that putStr has an effect and descended into the quagmire of untracked side effects and imperative programming. This would be true if map had only the simple type as it does in Haskell, because there'd be no way to track the fact that this application of map also causes a !Console effect like its argument does.

In Disciple, the complete map type of map is:

   map  :: forall t0 t1 %r0 %r1 !e0 $c0
        .  (t1 -(!e0 $c0)> t0) -> List %r0 t1 -(!e1 $c1)> List %r1 t0
        :- !e1        = !{ !Read %r0; !e0 }
        ,  $c1        = f : $c0

Which is a lot more information! Ignoring the closure ($) for now, we'll say briefly that the variables starting with (%) are region variables - so List %r0 t1 is a list in some region of memory called %r0 and has elements of type t1.

If we restrict the type of map to just type, region and effect information the have:

  map :: forall t0 r1 %r0 %r1 !e0
      .  (t1 -(!e0)> t0) -> List %r0 t1 -(!e1)> List %r1 t0
      :- !e1         = !{ !Read %r0; !e0 }