Lambda the Ultimate

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.

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).

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.

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.

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.