## Non-determinism: a sublanguage rather than a monad

Non-determinism: a sublanguage rather than a monad

A puzzlingly named, exceedingly technical device introduced to structure the denotational semantics has by now achieved cult status. It has been married to effects -- more than once. It is compulsively looked for in all manner of things, including burritos. At least two ICFP papers brought it up without a rhyme or reason (or understanding), as the authors later admitted. I am talking about monads.

In truth, effects are not married to monads and approachable directly. The profound insight behind monads is the structuring, the separation of pure' (context-independent) and effectful computations. The structuring can be done without explicating mathematical monads, and especially without resorting to vernacular monads such as State, etc. This article gives an example: a simple, effectful, domain-specific sublanguage embedded into an expressive macro' metalanguage. Abstraction facilities of the metalanguage such higher-order functions and modules help keep the DSL to the bare minimum, often to the first order, easier to reason about and implement.

The key insight predates monads and goes all the way back to the origins of ML, as a scripting language for the Edinburgh LCF theorem prover. What has not been clear is how simple an effectful DSL may be while remaining useful. How convenient it is, especially compared to the monadic encodings. How viable it is to forsake the generality of first-class functions and monads and what benefits it may bring. We report on an experiment set out to explore these questions.

We pick a rather complex effect -- non-determinism -- and use it in OCaml, which at first blush seems unsuitable since it is call-by-value and has no monadic sugar. And yet, we can write non-deterministic programs just as naturally and elegantly as in Haskell or Curry.

The running tutorial example is computing all permutations of a given list of integers. The reader may want to try doing that in their favorite language or plain OCaml. Albeit a simple exercise, the code is often rather messy and not obviously correct. In the functional-logic language Curry, it is strikingly elegant: mere foldr insert []. It is the re-statement of the specification: a permutation is moving the elements of the source list one-by-one into some position in the initially empty list. The code immediately tells that the number of possible permutations of n elements is n!. From its very conception in the 1959 Rabin and Scott's paper, non-determinism was called for to write clear specifications -- and then to make them executable. That is what will shall do.

## A unified approach to solving seven programming problems

A fun pearl by William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might from ICFP: seven programming challenges solved (easily!) using a relational interpreter. One challenge, for example, is to find quines. Another is to find programs that produce different results with lexical vs. dynamic scope.

The interpreter is implemented in miniKanren (of course), inside Racket (of course).

## ICFP 2017 live streaming

If you are one of the few LtU-ers not presenting (just kidding...), you can get your functional programming fix by following the live stream from ICFP, starting tomorrow at 11:00 (UK). Want to know when to tune in? Check out the incredible program!

## Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages (PACMPL) is a Gold Open Access journal publishing research on all aspects of programming languages, from design to implementation and from mathematical formalisms to empirical studies. Each issue of the journal is devoted to a particular subject area within programming languages and will be announced through publicized Calls for Papers.

See the ToC of the September 2017, ICFP issue, here. Some very cool stuff.

Congrats!

## Graydon Hoare: What next for compiled languages?

Key topics discussed: modules(you know, real ones); errors ("there are serious abstraction leakages and design trade-offs in nearly every known approach"); Coroutines, async/await, "user-visible" asynchronicity; effect systems, more generally (you could see that coming, couldn't you?); Extended static checking (ESC), refinement types, general dependent-typed languages; and formalization ("we have to get to the point where we ship languages -- and implementations -- with strong, proven foundations").

He goes on to discuss a whole grab bag of "potential extras" for mainstream languages, including the all time favorite: units of measure.

Feel free to link to the relevant discussions from the LtU archive...

## Review of Graham Hutton's Programming in Haskell, 2e

A concise review by Simon Thompson of the second edition of Graham Hutton's Programming in Haskell. The first edition was published in 2007, but chapters were written earlier, and the review focuses on how the language has changed since then, embracing the "categorical / algebraic approach more fully".

## Happy Birthday, dear Lambda: 17 is good edition

Seventeen years ago to the day, LtU was born. I guess it's about time I stop opening these birthday messages by saying how remarkable this longevity is (this being the fate of Hollywood actresses over 25). Still, I cannot resist mentioning that 17 is "good" (טוב) in gematria, which after all is one of the oldest codes there are. It's is very cool that the last couple of weeks had a flurry of activity. This old site still got game.

I will not try to summarize or pontificate. The community has grown too big and too unruly for that and I have been more an absent landlord recently than a true participant (transitioning from CS to being a professional philosopher of science and having kids took a bit more of my free time than I expected).

One thing I always cherished about LtU was that we welcomed both professional, academic work, and everything and anything that was cool and fun in programming languages. It was never a theory only site. So here's a little birthday party game instead of a long summary.

Which new (or old) languages inspire you to think that a good language can smoothly allow people to reach heretofore hard to reach semantic or abstraction levels?

I mean things that affect how the little guy thinks, not formal semantics, category theory, or what have you.

I'll start with two unconventional languages that I have had the pleasure (and exasperation) of using recently. Both are in some respects descendants of Logo, the language through which I was introduced to programming when I was a ten year old child in Brookline. They are NetLogo and ScratchJr.

NetLogo is a language for building agent based models (here's a classic ABM for you to enjoy; if you install NetLogo there's an implementation in the model library). While some aspects of the language semantics (and syntax) are irritating, NetLogo is very good at what it does. I may say more in the comments, but the key is that a simulation consists of multiple agents, who can move and interact, and the language makes building such simulations straightforward. There is a central clock; you can address multiple agents using conditions ("ask guys with [color = red] [die]"); implicitly have code run by each agent etc. In fact, you hardly think about these issues. If you have no previous background in programming, it feels natural that keeping track of these and other details is not part of the task programming.

ScratchJr is for young kids. It allows them to create little animated scenes, which may be responsive to touch and so on. You can record sounds and take pictures and use them as first class elements in your animations. But the nice thing for me was to notice how natural it is for kids to use the event-driven model (you can "write" several bits of code, and each will execute when the triggering event happens; no need to think about orchestrating this) as well as intuitively understand how this may involves things happening concurrently. These things just emerge from the way the animations are built, they are not concepts the programmer has to explicitly be aware of (which is a good thing, considering she is typically a five year old).

When I see philosophy students writing netlogo and reasoning about the behavior of the agents and when I see kids playing with ScratchJr, I am reminded why I found this business of "engineering abstractions" so enticing when I first used structured programming to design vocabulary for the program I was writing and when I heard some language described as a language for stratified design.

So which are your nominations for cool language based abstractions, for the little guy? Just to give us all some motivation and maybe get me worked up enough to finally delve into algebraic effects?

Happy birthday, LtU-ers. Keep fighting the good fight!

## Implementing Algebraic Effects in C

Implementing Algebraic Effects in C by Daan Leijen:

We describe a full implementation of algebraic effects and handlers as a library in standard and portable C99, where effect operations can be used just like regular C functions. We use a formal operational semantics to guide the C implementation at every step where an evaluation context corresponds directly to a particular C execution context. Finally we show a novel extension to the formal semantics to describe optimized tail resumptions and prove that the extension is sound. This gives two orders of magnitude improvement to the performance of tail resumptive operations (up to about 150 million operations per second on a Core i7@2.6GHz)

Another great paper by Daan Leijen, this time on a C library with immediate practical applications at Microsoft. The applicability is much wider though, since it's an ordinary C library for defining and using arbitrary algebraic effects. It looks pretty usable and is faster and more general than most of the C coroutine libraries that already exist.

It's a nice addition to your toolbox for creating language runtimes in C, particularly since it provides a unified, structured way of creating and handling a variety of sophisticated language behaviours, like async/await, in ordinary C with good performance. There has been considerable discussion here of C and low-level languages with green threads, coroutines and so on, so hopefully others will find this useful!

## Project Snowflake: Non-blocking safe manual memory management in .NET

Project Snowflake: Non-blocking safe manual memory management in .NET by Matthew Parkinson, Kapil Vaswani, Manuel Costa, Pantazis Deligiannis, Aaron Blankstein, Dylan McDermott, Jonathan Balkind, Dimitrios Vytiniotis:

Garbage collection greatly improves programmer productivity and ensures memory safety. Manual memory management on the other hand often delivers better performance but is typically unsafe and can lead to system crashes or security vulnerabilities. We propose integrating safe manual memory management with garbage collection in the .NET runtime to get the best of both worlds. In our design, programmers can choose between allocating objects in the garbage collected heap or the manual heap. All existing applications run unmodified, and without any performance degradation, using the garbage collected heap. Our programming model for manual memory management is flexible: although objects in the manual heap can have a single owning pointer, we allow deallocation at any program point and concurrent sharing of these objects amongst all the threads in the program. Experimental results from our .NET CoreCLR implementation on real-world applications show substantial performance gains especially in multithreaded scenarios: up to 3x savings in peak working sets and 2x improvements in runtime.

Rather than trying to solve safe manual memory management using compile-time reasoning, you can move some of it into the runtime and raise dynamic failures on use-after-free and other hazards. With some judicious special types that track ownership and a type of borrowing, and some reasonable restrictions on how these types can be handled, you can achieve a nice framework for integrating manual and automatic memory management. The performance benefits for large heaps looks pretty clear.

## The Syntax and Semantics of Quantitative Type Theory

The Syntax and Semantics of Quantitative Type Theory by Robert Atkey:

Type Theory offers a tantalising promise: that we can program and reason within a single unified system. However, this promise slips away when we try to produce efficient programs. Type Theory offers little control over the intensional aspect of programs: how are computational resources used, and when can they be reused. Tracking resource usage via types has a long history, starting with Girard's Linear Logic and culminating with recent work in contextual effects, coeffects, and quantitative type theories. However, there is conflict with full dependent Type Theory when accounting for the difference between usages in types and terms. Recently, McBride has proposed a system that resolves this conflict by treating usage in types as a zero usage, so that it doesn't affect the usage in terms. This leads to a simple expressive system, which we have named Quantitative Type Theory (QTT).

McBride presented a syntax and typing rules for the system, as well as an erasure property that exploits the difference between “not used” and “used”, but does not do anything with the finer usage information. In this paper, we present present a semantic interpretation of a variant of McBride's system, where we fully exploit the usage information. We interpret terms simultaneously as having extensional (compile-time) content and intensional (runtime) content. In our example models, extensional content is set-theoretic functions, representing the compile-time or type-level content of a type-theoretic construction. Intensional content is given by realisers for the extensional content. We use Abramsky et al.'s Linear Combinatory Algebras as realisers, yield a large range of potential models from Geometry of Interaction, graph models, and syntactic models. Read constructively, our models provide a resource sensitive compilation method for QTT.

To rigorously define the structure required for models of QTT, we introduce the concept of a Quantitative Category with Families, a generalisation of the standard Category with Families class of models of Type Theory, and show that this class of models soundly interprets Quantitative Type Theory.

Resource-aware programming is a hot topic these days, with Rust exploiting affine and ownership types to scope and track resource usage, and with Ethereum requiring programs to spend "gas" to execute. Combining linear and dependent types has proven difficult though, so making it easier to track and reason about resource usage in dependent type theories would then be a huge benefit to making verification more practical in domains where resources are limited.