David Darais, University of Maryland, USA, gives the first presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Nicholas Labich, David Van Horn, Phuc C. Nguyen, University of Maryland, USA. In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitional interpreters, especially those written in monadic style, can provide a nice basis for a wide variety of collecting semantics, abstract interpretations, symbolic executions, and their intermixings.

But the real insight of this story is a replaying of an insight from Reynold's landmark paper, Definitional Interpreters for Higher-Order Programming Languages, in which he observes definitional interpreters enable the defined-language to inherit properties of the defining-language. We show the same holds true for definitional abstract interpreters. Remarkably, we observe that abstract definitional interpreters can inherit the so-called 'pushdown control flow' property, wherein function calls and returns are precisely matched in the abstract semantics, simply by virtue of the function call mechanism of the defining-language.

The first approaches to achieve this property for higher-order languages appeared within the last ten years, and have since been the subject of many papers. These approaches start from a state-machine semantics and uniformly involve significant technical engineering to recover the precision of pushdown control flow. In contrast, starting from a definitional interpreter, the pushdown control flow property is inherent in the meta-language and requires no further technical mechanism to achieve. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Praveen Narayanan, Indiana University, USA, gives the third presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Chung-Chief Shan, Indiana University, USA. Probabilistic programming systems make machine learning methods modular by automating inference. Recent work by Shan and Ramsey (2017) makes inference itself modular by automating the common component of conditioning. Their work introduces a symbolic program transformation that treats conditioning generally via the measure-theoretic notion of disintegration. This technique, however, is limited to conditioning a single scalar variable. As a step towards tackling realistic machine learning applications, we have extended the disintegration algorithm to symbolically condition arrays in probabilistic programs. The extended algorithm implements lifted disintegration, where repetition is treated symbolically and without unrolling loops. The technique uses a language of index variables for tracking expressions at various array levels. We find that the method works well for arbitrarily-sized arrays of independent random choices, with the conditioning step taking time linear in the number of indices needed to select an element.

Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Daniel Winograd-Cort University of Pennsylvania, USA, gives the first presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Andreas Haeberlen and Aaron Roth, University of Pennsylvania, USA. Differential privacy is a widely studied theory for analyzing sensitive data with a strong privacy guarantee--any change in an individual's data can have only a small statistical effect on the result--and a growing number of programming languages now support differentially private data analysis. A common shortcoming of these languages is poor support for adaptivity. In practice, a data analyst rarely wants to run just one function over a sensitive database, nor even a predetermined sequence of functions with fixed privacy parameters; rather, she wants to engage in an interaction where, at each step, both the choice of the next function and its privacy parameters are informed by the results of prior functions. Existing languages support this scenario using a simple composition theorem, which often gives rather loose bounds on the actual privacy cost of composite functions, substantially reducing how much computation can be performed within a given privacy budget. The theory of differential privacy includes other theorems with much better bounds, but these have not yet been incorporated into programming languages.

We propose a novel framework for adaptive composition that is elegant, practical, and implementable. It consists of a reformulation based on typed functional programming of the privacy filters of Rogers et al (2016), together with a concrete realization of this framework in the design and implementation of a new language, called Adaptive Fuzz. Adaptive Fuzz transplants the core static type system of Fuzz to the adaptive setting by wrapping the Fuzz typechecker and runtime system in an outer adaptive layer, allowing Fuzz programs to be conveniently constructed and type-checked on the fly. We describe an interpreter for Adaptive Fuzz and report results from two case studies demonstrating its effectiveness for implementing common statistical algorithms over real data sets. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Louis Mandel (IBM) gives the first presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Joshua Auerbach, Martin Hirzel, Avraham Shinnar, Jerome Simeon, IBM Research, USA. Designing and prototyping new features is important in many industrial projects. Functional programming and formal verification tools can prove valuable for that purpose, but lead to challenges when integrating with existing product code or when planning technology transfer.

This article reports on our experience using the Coq proof assistant as a prototyping environment for building a query compiler intended for use in IBM's ODM Insights product. We discuss the pros and cons of using Coq for this purpose and describe our methodology for porting the compiler to Java, as required for product integration. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

William E. Byrd, University of Utah, USA, gives the fourth presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. Co-written by Gregory Rosenblatt, Matthew Might, Michael Ballantyne (University of Utah).

We present seven programming challenges in Racket, and an elegant, unified approach to solving them using constraint logic programming in mini Kanren. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Conal Elliott, Target, USA United States, gives the third presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. Parallel programming, whether imperative or functional, has long focused on arrays as the central data type. Meanwhile, typed functional programming has explored a variety of data types, including lists and various forms of trees. Generic functional programming decomposes these data types into a small set of fundamental building blocks: sum, product, composition, and their associated identities. Definitions over these few fundamental type constructions then automatically assemble into algorithms for an infinite set of data types--some familiar and some new. This paper presents generic functional formulations for two important and well-known classes of parallel algorithms: parallel scan (generalized prefix sum) and Fast Fourier Transform (FFT). Notably, arrays play no role in these formulations. Consequent benefits include a simpler and more compositional style, much use of common algebraic patterns--such as Functor, Applicative, Foldable, and Traversable--and freedom from possibility of run-time indexing errors. The functional generic style also clearly reveals deep commonality among what otherwise appears to be quite different algorithms. Instantiating the generic formulations to "top-down" and "bottom-up" trees as well as "bushes", two well-known algorithms for each of parallel scan and FFT naturally emerge, as well as two possibly new algorithms. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Jean-Philippe Bernardy, University of Gothenburg, gives the second presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. This paper proposes a new specification of pretty printing which is stronger than the state of the art: we require the output to be the shortest possible, and we also offer the ability to align sub-documents at will. We argue that our specification precludes a greedy implementation. Yet, we provide an implementation which behaves linearly in the size of the output. The derivation of the implementation demonstrates functional programming methodology. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Mike Spivey, University of Oxford, UK, gives the first presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. Coroutine pipelines provide an attractive structuring mechanism for complex programs that process streams of data, with the advantage over lazy streams that both ends of a pipeline may interact with the I-O system, as may processes in the middle. Two popular Haskell libraries, Pipes and Conduit, support such pipelines. In both libraries, pipelines are implemented in a direct style by combining a free monad of communication events with an interpreter for (pseudo-)parallel composition that interleaves the events of its argument processes. These implementations both suffer from a slow-down when processes are deeply nested in sequence or in parallel. We propose an alternative implementation of pipelines based on continuations that does not suffer from this slow-down. What is more, the implementation is significantly faster on small, communication-intensive examples even where they do not suffer from the slow-down, and faster even than comparable programs based on lazy streams. The continuation-based implementation may be derived from the direct-style implementation by algebraic reasoning. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Roberto Di Cosmo (Inria, France and University of Paris Diderot, France), gives the fourth presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Benjamin Canou (OCamlPro) and Gregoire Henry (OCamlPro).

This article describes the key innovations used in the massive open online course 'Introduction to Functional Programming using OCaml that has run since the fall semester of 2015. A fully in-browser development environment with an integrated grader provides an exceptional level of feedback to the learners. A functional library of grading combinators greatly simplifies the notoriously complex task of writing test suites for the exercises, and provides static type-safety guarantees on the tested user code. Even the error-prone manual process of importing the course content in the learning platform has been replaced by a functional program that describes the course and statically checks its contents. A detailed statistical analysis of the data collected during and after the course assesses the effectiveness of these innovations. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Joachim Breiner, University of Pennsylvania, United States, gives the third presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Chris Smith Google, USA. Implementing multi-player networked games by broadcasting the player's input and letting each client calculate the game state -- a scheme known as lock-step simulation -- is an established technique. However, ensuring that every client in this scheme obtains a consistent state is infamously hard and in general requires great discipline from the game programmer. The thesis of this pearl is that in the realm of functional programming -- in particular with Haskell's purity and static pointers -- this hard problem becomes almost trivially easy.

We support this thesis by implementing lock-step simulation under very adverse conditions. We extended the educational programming environment CodeWorld, which is used to teach math and programming to middle school students, with the ability to create and run interactive, networked multi-user games. Despite providing a very abstract and high-level interface, and without requiring any discipline from the programmer, we can provide consistent lock-step simulation with client prediction. Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/