Of Course ML Has Monads!

Of Course ML Has Monads! from Bob Harper's Blog:

A popular meme in the world of PL’s is that “Haskell has monads”, with the implication that this is a distinctive feature of the language, separate from all others. While it is true that Haskell has popularized the use of monads as a program structuring device, the idea of a monad is not so much an issue of language design (apart from the ad hoc syntactic support provided by Haskell), but rather one of library design.
In an ironic twist the emphasis on monads in Haskell means that programming in Haskell is rather like programming in an updated dialect of Algol with a richer type structure than the original, but the same overall structure.

Examined from the point of view of ML, monads are but a particular of use of modules. [..]

While some LtU regulars have noticed and replied to this post, I guess not everyone has noticed it.

I found of particular interest the comments by Andreas Rossberg and Andrej Bauer .

Comment viewing options

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

Very Strange

Yes, I know it sounds wonderful at first, but then you realize that it’s pretty horrible. Once you’re in the IO monad, you’re stuck there forever, and are reduced to Algol-style imperative programming.

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

And you inevitably need unsafePerformIO to get anything serious done.

This unsupported claim is easily refuted by looking through Hackage.

In practical terms, you are deprived of the useful concept of a benign effect, and that just stinks!

But... he just mentioned unsafePerformIO! What does he think it does then if not allow benign effects?

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.

Robert Harper should know better! Or have I missed something?

Type parameters

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.

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.

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

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

Concept of a "Benign Effect"?

The phrase 'benign effect' is used in Harper's dialog:

In practical terms, you are deprived of the useful concept of a benign effect, and that just stinks!

I've formed the opinion that there is no such thing as benign implicit effects. In modeling RDP in Haskell, I've had difficulty controlling several effects that are 'implicit' in pure Haskell functions: delay, divergence, failure, and synchronization. More broadly, I've found considerable benefits to securely modeling and controlling access to effects, eliminating ambient access to IO in favor of explicit capabilities.

I would present an opinion opposite Professor Harper and argue that Haskell's monadic model isn't precise enough in controlling effects, that its pure functions allow too many effects, and that unsafePerformIO is both undesirable and unnecessary. Don't mistake this: I'm not saying we should program without effects, but rather that the more explicitly and precisely we model and control effects, the better.

as a perpetually slow learner

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.

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

"Benign Effects"

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.

ST monad is a type system: safe but limited

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

ML has monads implicitly

In case it's of interest, I'll mention our upcoming ICFP paper, Lightweight Monadic Programming in ML.

Our observation is that an ML program uses the IO+State+Partiality+Exception monad (and possibly other effects I've forgotten) implicitly, rather than explicitly. For this monad, ML treats normal lets as uses of bind, and treats values where computations are allowed as uses of unit. Building on this observation, we extend ML so that programmers may use any monad in this implicit style; why should IO+State+etc. be special? Our system also inserts (programmer-defined) morphisms where needed to lift from one monad to another, while ensuring coherent program semantics.

Our system is not as flexible as it could be (we are looking into how to support parameterized monads in a similar manner) and not really vetted yet (just toy examples so far), but I think it has potential. Comments (including suggestions for extensions) very welcome!

Two questions

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

Lightweight ML monads clarifications

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 the same be done for comonads?

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

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