Home

The Disciplined Disciple Compiler

Disciple is an explicitly lazy dialect of Haskell which includes:
  • first class destructive update of arbitrary data.
  • computational effects without the need for state monads.
  • type directed field projections.
All this and more through the magic of effect typing.

The wiki page has more information, unfortunately there's no paper yet summarizing the ideas and results. Their effect system is quite interesting. Some of the ideas recently discussed here are implemented in Disciple.

via Haskell Cafe

By Daniel Yokomizo at 2008-03-20 14:19 | Functional | Semantics | Type Theory | other blogs | 13634 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Talks about Disciple

A couple of talks about Disciple are available:

via Jim Apple

By Daniel Yokomizo at Sun, 2008-03-23 19:34 | login or register to post comments

"for the most part"

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.

anybody have experience with this? like, how often does one have to really know what is going on, and how painful is it when it is required?

By raould at Mon, 2008-03-24 22:23 | login or register to post comments

No actual experience...

I didn't use Disciple so far but from my experience with effect systems and region inference (I never toyed with closure typing), one can ignore regions/effects as long as your code is parametric on them (i.e. doesn't care about their effects and just propagate them), the system will infer them correctly. When your code does effects though, you can get away without having to really know sometimes but most of the times you have to be able to understand the region/effect system and be able to read the notation. IMHO it's easier to read region/effect annotations than heavily categorical code (e.g. monad transformers, adjunctions), which doesn't say much though. I'm quite excited by this kind of research, but I think we are still quite far from it being simple enough for daily use.

By Daniel Yokomizo at Tue, 2008-03-25 01:51 | login or register to post comments

Type inference?

I was able to view the result of type inference by using the -dump-core-recon flag. However, the resulting types are mixed in with the definitions.

mods a = do a := 1

was turned into:

/\  %rTS4 ->
/\ (+xC3             :: Base.Mutable %rTS4) ->
\  (a :: Base.Int %rTS4)
                     of !{!Read %rTS4; !Write %rTS4} ->
[** Base.Unit ]
local %rTC2  with {+wCB2 = Const %rTC2; +wCB3 = Direct %rTC2} in
do {
        xCS1    = prim{Box} %rTC2 1#32i;
        
        primInt32_update %rTC2 %rTS4
                (Mutable %rTS4) a xCS1;
};

Giving mods an explicit type signature of Int -> () doesn't change the dumped result (modulo α renaming).

By Jim Apple at Tue, 2008-03-25 07:32 | login or register to post comments

Type inferencer output

You can get a list of all the types exported by the inferencer to the core language with -dump-type-solve

Compiling with this flag drops a file Main.dump-type-solve--types.dc which contains:

mods ::
        forall %rTS0
        .  Base.Int %rTS0 -(!eTC0do)> Base.Unit
        :- !eTC0do    = !{Base.!Read %rTS0; Base.!Write %rTS0}
        ,  Base.Mutable %rTS0

The file Main.dump-type-sove--trace.dc also gives a type inferencer trace for that module.

By Ben Lippmeier at Wed, 2008-03-26 07:34 | login or register to post comments

coercion...

It appears that "effects coercion" is okay in this system, but type coercion is not. So it's not like they're using unsafePerformIO all over the place.

Is it merely a matter of taste, whether we prefer a type error for this code or not? 

  s = getContents
  putStrLn s

While type errors for common things is annoying, I guess I've come to believe -- maybe I'm just drinking the KoolAid -- that it's one of the benefits of the monadic approach. It encourages us to stay stateless, to get out of IO and basically be really picky about purity. So even though the Disciplined Disciple approach maintains the optimization benefits of purity, it seems to punt on the (admittedly non-concrete) engineering benefits, by allowing free (careless?) interleaving of IO code and other code.

I'm not saying the way monads are handled in Haskell is beyond reproach, by the way -- it would be nice if mapM, forM and their ilk were deriveable somehow, maybe through a magical operator (#$^&*@(^ ?).

By Jason Dusek at Fri, 2008-03-28 03:56 | login or register to post comments

it would be nice if mapM,

it would be nice if mapM, forM and their ilk were deriveable somehow, maybe through a magical operator (#$^&*@(^ ?).

Most of them can be built with sequence (or sequence_). I wouldn't be surprised if equivalents for non-list structures can be built via sequence and the right pair of transformations (of which many may be possible), either.

By Philippa Cowderoy at Fri, 2008-03-28 18:07 | login or register to post comments

enforcing taste

If your prefer enforced purity, in all or part of a program, you can just declare a toplevel Pure specification. If you declare main as Pure, for example, you rule out the use of IO effects in anything called by main.

By Geoffrey Irving at Sat, 2008-03-29 00:26 | login or register to post comments

Ben's PhD thesis is now available

here

A very interesting read on the general topic of purity and destructive update in functional languages, plus lots of detail about DDC.

By tom davies at Mon, 2009-07-27 23:26 | login or register to post comments