Personal tools


From HaskellWiki

Jump to: navigation, search

1 Effect typing vs State monads

Instead of state monads (like
), 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 :: 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. This is even more of a problem when a library (like
) 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. In Haskell, because
prints to the screen it has the
constructor in its return type:
    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,
is an effect variable, much like
is a type variable.
is an effect constructor which tells us what else happens when
is called, besides evaluating the return value. Because this second version of
doesn't have the monad in its type, we can just use the plain version of
and not have to worry about
    main () 
     = do   map putStr ["one", "two", "three"]   -- print 'onetwothree'

2 Extended type information

But wait, that's evil isn't it?

From the previous example, it might look as though we've lost the information that
has an effect and descended into the quagmire of untracked side effects and imperative programming. This would be true if
had only the simple type as it does in Haskell, because there'd be no way to track the fact that this application of
also causes a
effect like its argument does. In Disciple, the complete type of
    map  :: forall a b %r0 %r1 !e0 $c0
         .  (a -(!e0 $c0)> b) -> List %r0 a -(!e1 $c1)> List %r1 b
         :- !e1        = !{ !Read %r0; !e0 }
         ,  $c1        = f : $c0

Which is a lot more information!

Ignoring the closure information (starting with
) for now, we'll say briefly that the variables starting with
are region variables. The type
(List %r0 a)
represents a list in a region of memory called
and has elements of type
. If we restrict the type of
to just (value) type, region and effect information then we have:
    map :: forall a b %r0 %r1 !e0
        .  (a -(!e0)> b) -> List %r0 a -(!e1)> List %r1 b
        :- !e1         = !{ !Read %r0; !e0 }
We see now that the effect sum
 !{!Read %r0; !e0}
records the fact that the
function, when applied to both its arguments, has the effect of reading the input list as well as doing whatever the argument function does.

The Disciplined Disciple Compiler (DDC) uses this effect discipline to track which parts of the program cause computational effects and which are pure. This allows it to check the type safety of programs that use these effects, and to perform the same sort of code transformation style optimizations as done by other Haskell compilers such as GHC.

3 Behind the scenes

None of this would be useful if you actually had to write these extended types in regular programs. It's a good thing then that, for the most part, you can ignore the extended region, effect and closure information when writing code.

The definition of
in Disciple is just the same as in Haskell, including the type signature.
   map :: (a -> b) -> [a] -> [b]
   map f []        = []
   map f (x : xs)  = f x : map f xs

Because all the extra information is orthogonal to the main shape of the type, ie its argument and return data types, the compiler can fill this in for you behind the scenes. We call this type elaboration. The extra information is present in the interface files and core language, but you'll only have to worry about it if you import foreign functions from C land or start to mix laziness with destructive update in the same program.