Lambda the Ultimate

Lightweight Monadic Programming in ML

Many useful programming constructions can be expressed as monads. Examples include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionality like state and I/O. In this paper, we present a type-based rewriting algorithm to make programming with arbitrary monads as easy as using ML's built-in support for state and I/O. Developers write programs using monadic values of type M t as if they were of type t, and our algorithm inserts the necessary binds, units, and monad-to-monad morphisms so that the program type checks. Our algorithm, based on Jones' qualified types, produces principal types. But principal types are sometimes problematic: the program's semantics could depend on the choice of instantiation when more than one instantiation is valid. In such situations we are able to simplify the types to remove any ambiguity but without adversely affecting typability; thus we can accept strictly more programs. Moreover, we have proved that this simplification is efficient (linear in the number of constraints) and coherent: while our algorithm induces a particular rewriting, all related rewritings will have the same semantics. We have implemented our approach for a core functional language and applied it successfully to simple examples from the domains listed above, which are used as illustrations throughout the paper.

This is an intriguing paper, with an implementation in about 2,000 lines of OCaml. I'm especially interested in its application to probabilistic computing, yielding a result related to Kiselyov and Shan's Hansei effort, but without requiring delimited continuations (not that there's anything wrong with delimited continuations). On a theoretical level, it's nice to see such a compelling example of what can be done once types are freed from the shackle of "describing how bits are laid out in memory" (another such compelling example, IMHO, is type-directed partial evaluation, but that's literally another story).

Interesting to many of you, I'd imagine -> F*

"F* is a new dependently typed language for secure distributed programming. It's designed to be enable the construction and communication of proofs of program properties and of properties of a program's environment in a verifiably secure way. F* compiles to .NET bytecode in type-preserving style, and interoperates smoothly with other .NET languages, including F#, on which it is based."

C

Here's another interesting project targeting the assembly language of the web...

ClojureScript seeks to address the weak link in the client/embedded application development story by replacing JavaScript with Clojure, a robust, concise and powerful programming language. In its implementation, ClojureScript adopts the strategy of the Google Closure library and compiler, and is able to effectively leverage both tools, gaining a large, production-quality library and whole-program optimization. ClojureScript brings the rich data structure set, functional programming, macros, reader, destructuring, polymorphism constructs, state discipline and many other features of Clojure to every place JavaScript reaches.

Also of interest: Compiling Clojure to Javascript pt. 1 of n.

Andrej Bauer's blog contains the PL Zoo project. In particular, the Levy language, a toy implementation of Paul Levy's CBPV in OCaml.

If you're curious about CBPV, this implementation might be a nice accompaniment to the book, or simply a hands on way to check it out.

It looks like an implementation of CBPV without sum and product types, with complex values, and without effects. I guess a more hands-on way to get to grips with CBPV would be to implement any of these missing features.

The posts are are 3 years old, but I've only just noticed them. The PL Zoo project was briefly mentioned here.

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 .

A short essay by Tom Van Cutsem, Why Programming Languages?:

When I present my research work on programming languages, people often ask me "why do you need a new programming language to solve this problem? Why not just implement it as a library?" Or, I get asked "why didn't you implement it as an extension to {some existing language}?" In this essay I try to make explicit some of the goals and motivations behind language design.

Van Cutsem is the author of AmbientTalk, which has been discussed obliquely on LtU a few months ago.

I am happy to announce the release of Ozma, a conservative extension to Scala that adds Oz concurrency. Ozma was developed as a master's thesis by Sébastien Doeraene under my supervision (see the implementation and the master's thesis).

Oz is a multi-paradigm language that has strong support for concurrent and distributed programming. It compiles to its own virtual machine (called Mozart) that supports dataflow synchronization and lightweight threads.

Scala is a functional and object-oriented language with implementations for the JVM and .Net. It is completely interoperable with Java.

Ozma is an attempt at making the concurrency concepts of Oz available to a larger public. Ozma implements the full Scala specification and runs on the Mozart VM. It can therefore be seen as a new implementation of Scala. Ozma extends Scala with dataflow variables (allowing tail-recursive list functions), declarative (deterministic) concurrency, lazy declarative concurrency, and message-passing concurrency based on ports. Almost all the concurrency examples of CTM can be translated easily to Ozma. We can say that Ozma lifts the duality of Scala, namely the combination of functional and object styles, to concurrent programming.

I understand this has been tweeted all over tarnation and discussed on Reddit, but a quick Google search of LtU seems to show that it hasn't been mentioned here. Which is a shame. So, here goes: Types Are Anti-Modular by Gilad Bracha. A nice followup on some of the theses that Gilad put forth in FLOSS Weekly 159: Newspeak where he was interviewed by Randal Schwartz.

A couple of quotes from the interview:

Learning is brain damage. I've spent the last 18 to 20 years unlearning the things I learned in my Ph.D. studies.

Also:

[The fact that Newspeak is not mainstream] is actually a competitive advantage.

Not exactly a new sentiment but still… Overall, the FLOSS interview with Bracha was almost as good as the one with Ingalls.

I don't recall a discussion here on ISO/IEC TR 24772, "Guidance to avoiding vulnerabilities in programming languages through language selection and use." This report describes programming language vulnerabilities in a generic way, and is supported by language specific annexes.

An introduction to this report can be found on page 46 of this issue of the Ada User Journal (how unweb like!). A lengthier discussion can be found in this issue of the same publication.

50 in 50 is another amusing episode of the Guy Steele and Richard Gabriel show.

Each of them make 50 remarks of 50 words in their alotted 50 minutes. The topic is a fond walk through programming language history, punctuated by awkward pauses. I'm not sure whether it's merely good or really great. Unfortunately only available in flash; the HTML5 trick didn't work for me.