Lambda the Ultimate

Also, his signature MONAD doesn't get you what you have in Haskell. In particular, you can't give the State monad such an interface because State is kind * -> * -> *. The Jane Street Core library offers a separate signature for monads with an additional type parameter; quite unsatisfying. A signature that covers the general case is possible but rather awkward to work with.

I'm not sure I agree. State per se is not a monad, but for all `s`, `State s` is. This is nice and compact in Haskell thanks to higher-kinded types, but you can do the same thing with a functor with parameter `s`.

In practice functors are much less nice to manipulate than parametrized types, so I suppose the two-parameters Monad signature is mostly a matter of convenience. I agree that a ML language with higher-kinded types in the core language would probably be better than what we currently have, but I think this is orthogonal to the monadic considerations at play here.

Indeed you are correct. I ran into the problem when trying to implement State previously and settled on the functor solution in preference to Core's Monad2. Being the infrequent O'Caml user that I am, I remembered running into the problem but forgot that I found a decent enough solution...

This isn't the case at all. Is mapM_ (putStrLn . show) really Algol-style imperative programming?

Yes, it is. Idealized Algol is almost exactly Haskell-style imperative programming -- the difference is basically that the IO type constructor is restricted to unit type.

Where I differ from Bob is that I think the Algol/Haskell style is a more convenient style of imperative programming than the ML/Scheme style.

the difference is basically that the IO type constructor is restricted to unit type.

That's quite a difference, isn't it? An example not using mapM_ would have been more appropriate to illustrate the difference then. I confess that Idealized Algol is not what I typically associate with the phrase "Algol-style imperative programming".

i find that when things in the system are explicit it is much easier to not make horrible mistakes, or to at least be able to trace back from some bad thing to the source code and have the lightbulb turn on over my head. so i say here here, and how.

I favor layered structural control, for example in RDP: pure function < RDP behavior < multi-agent system. Only agents can introduce state. Only RDP behaviors can introduce communication between agents and delay (along with asynchronous computation - different delay on different paths - and synchronization). Pure functions are real-time and bounded space, in the sense that they can only do a fixed amount of work per instant. Non real-time (and potentially divergent) computations must be explicitly modeled via incremental stateful loops over time, thus discouraging non real-time apps but also (when they prove necessary) simplifying support for job control and use of partial results.

I might end up introducing an intermediate layer between pure functions and full behaviors, restricted to delay and synchronization effects, but developers can achieve this much by use of object capabilities.

Object capabilities mean developers control access to specific agents via parameter, and thus control access to the specific side-effects those agents permit.

Basic effects are also limited: communication in RDP is spatially commutative and idempotent, reactive, continuous, declarative. It is easy to understand, compose, and control these constrained effects at scale or in face of concurrency. Developers must use stateful agents if they want to model any 'fire and forget' effects, such as setting a variable or passing a message

I favor the most effective, composable approaches I know. We could use effect typing instead of precise structural controls over generic classes of effect, but I feel effect typing hurts simplicity and code reuse, and becomes difficult to validate at runtime in an open system. We could use ADTs or user access control or sandboxes instead of object capabilities, but those severely hurt our ability to freely delegate and precisely attenuate authority.

To model multi-layer languages in Haskell, with limits such as 'real-time, bounded space' functions and behaviors (as opposed to Haskell functions with Turing-complete recursion) we can use generalized arrows. The main trouble, though, is the same any new language has: adapting 'legacy' models at the appropriate structural layer.

Interestingly, if you model an embedded language in a GC'd language, you get something close to an embedded application - i.e. you can make guarantees about how much is collected per cycle. Similarly, you can get near real-time even without a real-time collector or scheduler.

ship it! (kidding.)

We've been able to write programs that look like pure functions but in fact have "benign effects" without unsafePerformIO for a long time now - using the ST monad.

... which is not to dispute your desire for more control over where effects are allowed to occur.

I think there an important difference between "benign effects", that are observed but we choose to ignore (non-termination, logging, asking for a machine-dependent configuration value...), and "non-observable effects" (or "observational purity") which is observationally completely pure. Indeed, the decision of which effects are benign depends on the problem domain -- see dmbarbour's opinion that no effects are benign, even encompassing some things that one does not usually consider as effects, such as time consumption -- while I suppose there is no arguing that having systems that can handle some amount of observational purity is always a good thing.

Using parametricity to characterize a class of unobservable effects is indeed a very neat trick. It has however all the downside of a fixed type system: it is a restricted analysis that will reject some correct programs. Unless you are ready to sacrifice expressivity for correctness, escape hatches such as Haskell's `unsafePerformIO` or OCaml's `Obj.magic` are necessary. And this is true even in the presence of sound analyses such as the ST monad, or even more refined systems (type-system capabilities, etc.).

Two questions after skimming over the paper (introduction plus related works).

I do not understand well why `Beh (Prb a)` is less acceptable than `BehPrb a`. Your explanation is that `Prb a` is not a value, but the usual way to think about monads used for programming in Haskell or ML is to consider them as values -- indeed this is different from the take on monads in Moggi's paper, when monads are used at the semantic levels to represent non-value computations. That monadic values can be manipulated as a first-class value in the language is moreover an advantage of this programming style over usual imperative languages: any expression, even of a monadic type, can be abstracted over.

The examples also left me wondering on how the choice of monad works in practice. Can I enclose a specific bit of code with a structure asking for monads to be inferred? Is it still possible to use the usual "let" and applications in some part of the program, without getting monad polymorphism inferred? How should the monad descriptions be fed to the type system? Is it possible to define a monad locally instead of globally? To abstract (eg. in a module signature) over a monad morphism description?

On an aesthetic level, I'm a bit uncomfortable with a notation that is so implicit. I would rather have `let` and application with their usual ML meaning, and different keywords like `let!` -- as in F# computational expressions -- and some syntax for application, akin to the banana-like syntax proposed for Applicative/Idioms for monadic pieces of code. On the other hand, having a system that infers monad polymorphism for pure code may help with the problem of "I just noticed that I need to do something monadic in this deeply nested call, so I need to monadify all that intermediate code".

Thanks for the comments!

Re: (Beh (Prb a)) being less acceptable than BehPrb a:

We think of expressions with monadic type as being computations, so a computation parameterized by a computation would be like a function whose arguments could be computations rather than values, which is not in the call-by-value style. You therefore have to work out the evaluation order/composition yourself to make sure the effects go as you would expect (see Filinski's work for more on this). Just as in ML, you could "thunkify" your arguments, e.g., you can write Beh (unit -> Prb a) in our system if you don't want to define BehPrb (but we expect you would to control effects; again, see Filinski).

Re: the examples:

The paper presents several detailed examples, so I would encourage you to additionally read at least section 2 and section 6. The prototype implementation of the system, called Coco, is a current work in progress. So far Coco inputs a single core-ML file that contains the type signatures of external values, monad declarations, and the code to be rewritten. To make Coco usable in practice, we plan to support partial rewriting of code, just in some user-delimited sections. We also plan to support standard signatures of external values, for example a .mli type interface. Monad declarations (including the name of the monad constructor, the names of its bind and unit functions, as well as declarations of morphisms) could still be given using some special syntax in a separate file since in practice they are not many. Another possibility is to input monad modules, of a pre-agreed non-surprising module type MONAD.

We're not sure why you'd want local morphisms. Seems to us, again drawing inspiration from the implicit IO+State+etc. monad for ML, that for program understanding you want just one interpretation of monads and their interrelationships, and thus global morphisms.

We support the option of generating well-formed OCaml code, and there monad morphism are abstracted over in monad-polymorphic values.

Can you do a similar transformation to make use of comonads implicit, so that you can add comonadic language features to the language? (like laziness)

Interesting question. Not something we've looked at, but we've added it to the list.