Meeting 2016

• Dates: January 25-29, 2016
• Venue: UCLA, Los Angeles, CA
• Host: Alex Warth

Food

Lunches: grab some food in food court in Ackerman auditorium and eat outside.

Group dinners @ 7pm

• Monday: Bollywood Bites

• Tuesday: Wolfgang Puck Express (same building as the meeting room)

• Wednesday: CDG Pizza Party

• Thursday: Shamshiri Grill

All restaurants are within walking distance from the meeting room.

Wednesday: expedition to Getty center

(We will have lunch there, and dinner at CDG @ 7pm.)

Participants

Organization

• Eelco Visser (Chair)
• Jonathan Edwards (Secretary)
• Alessandro Warth (Local Organizer)

Members

• Jonathan Aldrich
• Andrew Black
• Gilad Bracha
• Kim Bruce
• Adam Chlipala
• Erik Ernst
• Robby Findler
• Matthew Flatt
• Crista Lopes
• Jan-Willem Maessen
• Sean McDirmid
• Tijs van der Storm
• Sam Tobin-Hochstadt

Visitors

• Nada Amin
• Michael Greenberg
• Heather Miller
• Todd Millstein
• Martin Odersky
• Jens Palsberg
• Manuel Serrano
• Ross Tate
• Evan Czaplicki

Monday

Introduction

• Chair's opening
• Brief round of introductions: just your name and affiliation are fine
• Local organizer's instructions

Talks

• Adam Chlipala
• Jonathan Edwards
• Andrew Black

• Robby Findler
• Jan-Willem Maessen
• Sean McDirmid

Tuesday

• Martin Odersky
• Michael Greenberg
• Todd Millstein

• Evan Czaplicki
• Jens Palsberg
• Ross Tate

Wednesday

• Alessandro Warth
• Eelco Visser
• Jonathan Aldrich

Thursday

• Tijs van der Storm
• Nada Amin
• Kim Bruce

• Crista Lopes
• Heather Miller
• Manuel Serrano

• Business meeting

Friday

• Erik Ernst

Abstracts

Kim Bruce: Teaching with Grace: First evaluations.

The pedagogical programming language Grace was designed for novices to programming. This fall was the second time we have used Grace for an intro course at Pomona College (Andrew Black has also used it with some slightly different courses at PSU).

In this talk I’ll give a quick outline of some of the features of the Grace design that make it especially helpful in an introductory course. I’ll then talk about the head-to-head comparison we ran this fall with the Grace version against a Java version of the same course with parallel texts, assignments, and exams. While we have not yet run a careful statistical analysis of the detailed results, early indications are that Grace is a considerable help to novices in learning.

Erik Ernst: Reflection Quantification

This talk is about the design of a small embedded DSL, intended to specify the subset of the dynamic semantics of the host language which is supported by mirror based reflection. The main concepts of the DSL are capabilities (concerned with the selection of mirror operations) and annotation (concerned with the selection of host language entities covered by mirrors). The host is the Dart programming language, and the context is the Reflectable package. The toughest balancing act in the design of this DSL was the level of detail: With a detailed level of control the simple usages may be inconveniently verbose to specify, but with a coarse-grained level of control, the larger applications may be forced to have intolerable overhead.

Ross Tate: How Not to Add Type Classes to Type OO Languages

Material-shape separation makes it obvious that typed-OO programmers are naturally dividing their classes and interfaces into types (materials) and type classes (shapes). Material-shape separation also ensures that recursing through types will terminate even when incorporating inheritance. This suggests an obvious solution to adding type classes to OO. Unfortunately, the obvious solution doesn't work. Although it is sound and decidable, it clashes with important usage patterns and OO principles. This is not apparent even after finishing such a design, so in this talk I will illustrate precisely how this solution is surprisingly deceptive.

Martin Odersky: Effects as Implicit Capabilities

It seems obvious that one should track the effects of a piece of code just as one tracks the types of its inputs and outputs. But despite 30 years of research on effect systems, very little of it has been applied in practice, and what was put in practice is sometimes regarded as a failure. A central difficulty is how to express *effect polymorphism*, the ability to write a function once, and to have it interact with arguments that can have arbitrary effects.

I will talk about a new approach to effect checking which has an elegant solution to the effect polymorphism problem and promises to be quite usable in practice. The central idea is that instead of talking about effects we talk about capabilities. For instance, instead of saying a function ``throws an IOException'' we say that the function ``needs the capability to throw an IOException''. Capabilities are modeled as values of some set of capability types. I will talk about two new language features that make this approach attractive.

To cut down on boilerplate, capabilities are passed as implicit parameters to the functions that need them. Implicit parameters make call-site annotations unnecessary, but they still have to be declared just like normal parameters. The new construct of implicit function types makes parameters abstractable and thus eliminates declaration-side boilerplate.

Second, there is one fundamental difference between the usual notions of capabilities and effects: Capabilities can be captured in closures. This means that a capability present at closure construction time can be preserved and accessed when the closure is applied. Effects on the other hand, are temporal: it generally does make a difference whether an effect occurs when a closure is constructed or when it is used. We propose to address this discrepancy by introducing a ``pure function'' type, instances of which are not allowed to close over effect capabilities.

Jens Palsberg: Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega

According to conventional wisdom, a self-interpreter for a strongly normalizing lambda-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. I will show how to break through the normalization barrier and define a self-interpreter for a widely used strongly normalizing lambda-calculus. After a careful analysis of the classical theorem, we show that static type checking can exclude the proof's diagonalization gadget and leave open the possibility for a self-interpreter. Our self-interpreter relies on a novel program representation that may be useful in theorem provers and compilers. Joint work with Matt Brown; presented at POPL 2016.

Manuel Serrano: Hop.js

Hop.js is a multitier extension of JavaScript^?. It allows a single JavaScript^? program to describe the client-side and the server-side components of a Web application. Its runtime environment ensures a consistent execution of the application on the server and on the client. This talk will shows its minimal set of JavaScript^? extensions that makes Web programming easier. It will present its runtime environment, with an emphasize on the handling of server-side parallelism.

Crista Lopes: Yet another SQL-OO integration (YASOO) with dependent types and differential computation (YASOO-DT)

I've been working in large-scale, decentralized simulations of urban areas [1], and a problem has come up repeatedly: how to partition the load and how to share data between the partitions. In these kinds of systems, if you are not careful you end up with APIs that don't align well with stakeholders and expert developers and that, therefore, are very painful to develop for. In trying to improve the development process of these simulations, I am converging to a solution that has roots in relational algebra, dependent types and differential computation. It works in the lab! [2]

[1] https://www.youtube.com/user/encitravideos [2] Applicability in the wild is still TBD

Sean McDirmid^?: The past, present, and future of live programming

This talk will present the promise of live programming as I currently see it. Narrowly defined, live programming has been about providing feedback about how a program executes while it is being written by the programmer, combining the phases of debugging and editing for a more fluid feedback loop. However, as Chris Hancock and Bret Victor have pointed out, this really isn’t good enough to move the needle on better programmer experiences. Through multiple demos, I will show what works and what hasn’t worked, and more importantly provide context on why these results occurred. I will then present some future directions for this field.

Andrew Black: The Essence of Inheritance

Programming languages serve a dual purpose: to communicate programs to computers, and to communicate programs to humans. Indeed, it is this dual purpose that makes programming language design a constrained and challenging problem. Inheritance is an essential aspect of that second purpose: it is a tool to improve communication. Humans understand new concepts most readily by first looking at a number of concrete examples, and later abstracting over those examples. The essence of inheritance is that it mirrors this process: it provides a formal mechanism for moving from the concrete to the abstract.

Todd Millstein: Why Do Language Designers Tolerate Weak Memory Consistency Models?

Almost all languages today are memory safe, thereby providing simple and strong guarantees to all programs, buggy or otherwise. Yet the concurrency semantics of these “safe” languages causes similar problems as arise in memory-unsafe languages: small program errors can expose implementation details, violate fundamental language abstractions, and compromise program safety. Why do language designers tolerate this situation? In this talk I’ll overview the state of concurrency semantics as it exists today and argue that safe languages must support sequential consistency (i.e., the interleaving semantics of threads). Along the way I’ll also debunk a few persistent myths.

Michael Greenberg: The POSIX shell as a programming language

We build intricate systems with complex algorithms and invariants, aiming for guarantees of correctness and performance... and then we maintain and deploy these systems with shell scripts! What are shell scripts? If POSIX shell is a programming language, what are its syntax and semantics? Can we apply PL tools to reason about the shell?

Adam Chlipala: A Micro-Tutorial on Multi-Tier Metaprogramming with Ur/Web

One of the unusual features of the Ur/Web programming language is flexible but statically typed generation of web-application code that needs to coordinate across three different tiers: database, web server, and browser. I will demonstrate the main ideas with a simple generic component for adding rows to an SQL database table.

Jonathan Edwards: Transcript: not programming mobile social apps

Transcript is an experiment to radically simplify programming of mobile social applications. We will demonstrate an early prototype and discuss the key design ideas that simplify the programming experience.

Jonathan Aldrich: Achieving Architectural Control via Language Support for Capabilities

Many important architectural properties of software depend on how resources such as storage or the network are used. Unfortunately, today's software architects have few ways to control those resources, other than by leveraging woefully inadequate software processes. We propose to leverage capabilities--unforgeable tokens that control access to resources--to isolate the enforcement of architectural properties to a few critical resource-using modules, on which assurance efforts can be focused. We also present improvements in language support for capabilities, including a non-transitive model of capability-based authority, a capability-aware module system, and design principles for type systems and reflection systems that are compatible with capabilities.

Alessandro Warth: Growing Language Designers

Despite the high caliber of our students, the recurring Programming Language Design Seminar at UCLA did not consistently generate the kind of output we had hoped for. One issue was that students lacked the PL prototyping chops required to do meaningful work in such a short time — 10 weeks fly by when you’re having fun. Last year we created a new class to address this problem. Thanks in part to a novel framework that aims to minimize unnecessary friction and give students “instant gratification” when possible, the new class was a great success and turned out to be much more popular than we anticipated. (Joint work with Todd Millstein and Alan Kay.)

Eelco Visser: The Name Binding Game

In this talk I explore the expressiveness (or lack thereof) of the scope graph framework for encoding the name binding rules of programming languages.

Evan Czaplicki: Type inference and excellent error messages

The last two release of Elm (0.15.1 and 0.16) focused primarily on producing excellent error messages. The conventional wisdom seemed to be "making nice error messages in type inferred languages is not really feasible, so just get used to how things are." This is not a recipe for growing a successful language in the JS world though. As I began exploring this topic I found that you can make enormous practical improvements for your users without anything particularly fancy. I believe the general technique I used in Elm would work just as well in languages with more complex type systems (like OCaml or Haskell) as long as they use a constraint-based solver.

Heather Miller: Distributed programming via safe closure passing

Scala is a popular implementation language of big data frameworks. Leading frameworks like Spark and Kafka have nodded their hats to Scala, noting that some of their ability to innovate were provided by aspects of Scala’s mixed object-functional design, such as its support for first-class functions. However, problems abound; function closures in Scala weren’t designed with the idea of them being serialized and sent over the wire in mind, resulting in end-user headaches across frameworks. We proposed a solution to the closure serialization problem with spores, a refinement to functions in Scala that make closures more reliable to serialize. I'll discuss ongoing work on a programming model we have built atop of spores which aims to generalize models like MapReduce^? by enabling a more principled way to move "functionality" to immutable data spread across a network.