title: Well-founded recursion with copatterns and sized types

authors:
Andreas Abel
Brigitte Pientka

abstract: Abstract In this paper, we study strong normalization of a core language based on System ${\mathsf{F}_\omega}$ which supports programming with finite and infinite structures. Finite data such as finite lists and trees is defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. Taking a type-based approach to strong normalization, we track size information about finite and infinite data in the type. We exploit the duality of pattern and copatterns to give a unifying semantic framework which allows us to elegantly and uniformly support both well-founded induction and coinduction by rewriting. The strong normalization proof is structured around Girard's reducibility candidates. As such, our system allows for non-determinism and does not rely on coverage. Since System ${\mathsf{F}_\omega}$ is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-based infinite data in proof assistants such as Coq and Agda.


venue: jfp

title: Oracle-guided scheduling for controlling granularity in implicitly parallel languages

authors:
Umut A. Acar
Arthur Charguéraud
Mike Rainey

abstract: Abstract A classic problem in parallel computing is determining whether to execute a thread in parallel or sequentially. If small threads are executed in parallel, the overheads due to thread creation can overwhelm the benefits of parallelism, resulting in suboptimal efficiency and performance. If large threads are executed sequentially, processors may spin idle, resulting again in sub-optimal efficiency and performance. This “granularity problem” is especially important in implicitly parallel languages, where the programmer expresses all potential for parallelism, leaving it to the system to exploit parallelism by creating threads as necessary. Although this problem has been identified as an important problem, it is not well understood—broadly applicable solutions remain elusive. In this paper, we propose techniques for automatically controlling granularity in implicitly parallel programming languages to achieve parallel efficiency and performance. To this end, we first extend a classic result, Brent's theorem (a.k.a. the work-time principle) to include thread-creation overheads. Using a cost semantics for a general-purpose language in the style of lambda calculus with parallel tuples, we then present a precise accounting of thread-creation overheads and bound their impact on efficiency and performance. To reduce such overheads, we propose an oracle-guided semantics by using estimates of the sizes of parallel threads. We show that, if the oracle provides accurate estimates in constant time, then the oracle-guided semantics reduces the thread-creation overheads for a reasonably large class of parallel computations. We describe how to approximate the oracle-guided semantics in practice by combining static and dynamic techniques. We require the programmer to provide the asymptotic complexity cost for each parallel thread and use runtime profiling to determine hardware-specific constant factors. We present an implementation of the proposed approach as an extension of the Manticore compiler for Parallel ML. Our empirical evaluation shows that our techniques can reduce thread-creation overheads, leading to good efficiency and performance.


title: Homotopical patch theory

authors:
Carlo Angiuli
Edward Morehouse
Daniel R. Licata
Robert Harper

abstract: Abstract Homotopy type theory is an extension of Martin-Löf type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type is proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches—syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.


title: PAEAN: Portable and scalable runtime support for parallel Haskell dialects

authors:
Jost Berthold
Hans-Wolfgang Loidl
Kevin Hammond

abstract: Abstract Over time, several competing approaches to parallel Haskell programming have emerged. Different approaches support parallelism at various different scales, ranging from small multicores to massively parallel high-performance computing systems. They also provide varying degrees of control, ranging from completely implicit approaches to ones providing full programmer control. Most current designs assume a shared memory model at the programmer, implementation and hardware levels. This is, however, becoming increasingly divorced from the reality at the hardware level. It also imposes significant unwanted runtime overheads in the form of garbage collection synchronisation etc. What is needed is an easy way to abstract over the implementation and hardware levels, while presenting a simple parallelism model to the programmer. The PArallEl shAred Nothing runtime system design aims to provide a portable and high-level shared-nothing implementation platform for parallel Haskell dialects. It abstracts over major issues such as work distribution and data serialisation, consolidating existing, successful designs into a single framework. It also provides an optional virtual shared-memory programming abstraction for (possibly) shared-nothing parallel machines, such as modern multicore/manycore architectures or cluster/cloud computing systems. It builds on, unifies and extends, existing well-developed support for shared-memory parallelism that is provided by the widely used GHC Haskell compiler. This paper summarises the state-of-the-art in shared-nothing parallel Haskell implementations, introduces the PArallEl shAred Nothing abstractions, shows how they can be used to implement three distinct parallel Haskell dialects, and demonstrates that good scalability can be obtained on recent parallel machines.


title: Safe zero-cost coercions for Haskell

authors:
Joachim Breitner
Richard A. Eisenberg
Simon Peyton Jones
Stephanie Weirich

abstract: Abstract Generative type abstractions – present in Haskell, OCaml, and other languages – are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.


title: OCaml-Java: The Java Virtual Machine as the target of an OCaml compiler

abstract: Abstract This article presents how the compiler from the OCaml-Java project generates Java bytecode from OCaml sources. Targeting the Java Virtual Machine (JVM) is a technological challenge, but gives access to a platform where OCaml can leverage multiple cores and access numerous libraries. We present the main design choices regarding the runtime and the various optimizations performed by the compiler that are crucial to get decent performance on a JVM. The challenge is indeed not only to generate bytecode but to generate efficient bytecode, and to provide a runtime library whose memory footprint does not impede the efficiency of the garbage collector. We focus on the strategies that differ from the original OCaml compiler, as the constraints are quite different on the JVM when compared to native code. The level of performance reached by the OCaml-Java compiler is assessed through benchmarks, comparing with both the original OCaml implementation and the Scala language.


title: Eliminating dependent pattern matching without K

authors:
Jesper Cockx
Dominique Devriese
Frank Piessens

abstract: Abstract Dependent pattern matching is an intuitive way to write programs and proofs in dependently typed languages. It is reminiscent of both pattern matching in functional languages and case analysis in on-paper mathematics. However, in general, it is incompatible with new type theories such as homotopy type theory (HoTT). As a consequence, proofs in such theories are typically harder to write and to understand. The source of this incompatibility is the reliance of dependent pattern matching on the so-called K axiom – also known as the uniqueness of identity proofs – which is inadmissible in HoTT. In this paper, we propose a new criterion for dependent pattern matching without K, and prove it correct by a translation to eliminators in the style of Goguen et al . (2006 Algebra, Meaning, and Computation ). Our criterion is both less restrictive than existing proposals, and solves a previously undetected problem in the old criterion offered by Agda. It has been implemented in Agda and is the first to be supported by a formal proof. Thus, it brings the benefits of dependent pattern matching to contexts where we cannot assume K, such as HoTT.


title: Preface for special section from FLOPS 2014

authors:
Michael Codish
Eijiro Sumii

abstract: The 12th International Symposium on Functional and Logic Programming was held in Kanazawa, Japan, June 4–6, 2014. The aim of the Functional and Logic Programming series of conferences is to bring together researchers interested in declarative programming including functional programming and logic programming. The series aims to promote cross-fertilization and integration between the two paradigms and it is traditionally organized and held in Japan.


title: Skeleton composition versus stable process systems in Eden

authors:
Mischa Dieterle
Thomas Horstmeyer
Rita Loogen
Jost Berthold

abstract: Abstract We compare two inherently different approaches to implement complex process systems in Eden: stable process systems and a compositional approach. A stable process system is characterised by handling several computation stages in each of the participating processes. Often, processes communicate using streams of data, change behaviour with the different computation phases, and more often than not, exactly one process is allocated to each processor element. In contrast, a complex process system can also be achieved by skeleton composition of a number of elementary skeletons, such as parallel transformation, reduction, or special communication patterns. In a compositional implementation, each computation phase leads to a new set of interacting processes. When implementing complex parallel algorithms, skeleton composition is usually easier and more flexible, but has a larger overhead from additional process creation and communication. We present case studies of different parallel application kernels implemented as stable systems and using composition in Eden, including a comprehensive description of Eden's features. Our results show that the compositional performance loss can be alleviated by co-locating processes which directly communicate, and by using Eden's remote data concept to enable such direct communication. Moreover, Eden's parallel runtime system handles communication between co-located processes in an optimised way. EdenTV visualisations of execution traces are invaluable to analyse program characteristics and for targeted optimisations towards better process placement and communication avoidance.


title: Special issue dedicated to ICFP 2014: Editorial

authors:
Derek Dreyer
Mary Sheeran

abstract: The 19th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 1–3, 2014 in Gothenburg, Sweden. After the conference, the programme committee, chaired by Manuel Chakravarty, selected several outstanding papers and invited their authors to submit to this special issue of JFP. We acted as editors for these submissions. This issue includes the six accepted papers, each of which provides substantial new material beyond the original conference version. The selected papers demonstrate both the quality and the breadth of the conference, with a strong emphasis on types and their applications, and ranging from compilation methods through contract verification to homotopy type theory.


title: Unifying structured recursion schemes - An Extended Study

authors:
Ralf Hinze
Nicolas Wu

abstract: Abstract Folds and unfolds have been understood as fundamental building blocks for total programming, and have been extended to form an entire zoo of specialised structured recursion schemes. A great number of these schemes were unified by the introduction of adjoint folds, but more exotic beasts such as recursion schemes from comonads proved to be elusive. In this paper, we show how the two canonical derivations of adjunctions from (co)monads yield recursion schemes of significant computational importance: monadic catamorphisms come from the Kleisli construction, and more astonishingly, the elusive recursion schemes from comonads come from the Eilenberg–Moore construction. Thus, we demonstrate that adjoint folds are more unifying than previously believed.


title: Testing noninterference, quickly

authors:
Catalin Hritcu
Leonidas Lampropoulos
Antal Spector-Zabusky
Arthur Azevedo de Amorim
Maxime Dénès
John Hughes
Benjamin C. Pierce
Dimitrios Vytiniotis

abstract: Abstract Information-flow control mechanisms are difficult both to design and to prove correct. To reduce the time wasted on doomed proof attempts due to broken definitions, we advocate modern random-testing techniques for finding counterexamples during the design process. We show how to use QuickCheck, a property-based random-testing tool, to guide the design of increasingly complex information-flow abstract machines, leading up to a sophisticated register machine with a novel and highly permissive flow-sensitive dynamic enforcement mechanism that is sound in the presence of first-class public labels. We find that both sophisticated strategies for generating well-distributed random programs and readily falsifiable formulations of noninterference properties are critically important for efficient testing. We propose several approaches and evaluate their effectiveness on a collection of injected bugs of varying subtlety. We also present an effective technique for shrinking large counterexamples to minimal, easily comprehensible ones. Taken together, our best methods enable us to quickly and automatically generate simple counterexamples for more than 45 bugs. Moreover, we show how testing guides the discovery of the sophisticated invariants needed for the noninterference proof of our most complex machine.


title: PhD Abstracts

abstract: Many students complete PhDs in functional programming each year. As a service to the community, the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.


title: Reasoning about multi-stage programs

authors:
Jun Inoue
Walid Taha

abstract: Abstract We settle three basic questions that naturally arise when verifying code generators written in multi-stage functional programming languages. First, does adding staging to a language compromise any equalities that hold in the base language? Unfortunately it does, and more care is needed to reason about terms with free variables. Second, staging annotations, as the name “annotations” suggests, are often thought to be orthogonal to the behavior of a program, but when is this formally guaranteed to be true? We give termination conditions that characterize when this guarantee holds. Finally, do multi-stage languages satisfy useful, standard extensional properties, for example, that functions agreeing on all arguments are equivalent? We provide a sound and complete notion of applicative bisimulation, which establishes such properties or, in principle, any valid program equivalence. These results yield important insights into staging and allow us to prove the correctness of quite complicated multi-stage programs.


title: A characterization of lambda-terms transforming numerals

abstract: Abstract It is well known that simply typed λ-terms can be used to represent numbers, as well as some other data types. We show that λ-terms of each fixed (but possibly very complicated) type can be described by a finite piece of information (a set of appropriately defined intersection types) and by a vector of natural numbers. On the one hand, the description is compositional: having only the finite piece of information for two closed λ-terms M and N , we can determine its counterpart for MN , and a linear transformation that applied to the vectors of numbers for M and N gives us the vector for MN . On the other hand, when a λ-term represents a natural number, then this number is approximated by a number in the vector corresponding to this λ-term. As a consequence, we prove that in a λ-term of a fixed type, we can store only a fixed number of natural numbers, in such a way that they can be extracted using λ-terms. More precisely, while representing k numbers in a closed λ-term of some type, we only require that there are k closed λ-terms M 1 ,. . ., M k such that M i takes as argument the λ-term representing the k -tuple, and returns the i -th number in the tuple (we do not require that, using λ-calculus, one can construct the representation of the k -tuple out of the k numbers in the tuple). Moreover, the same result holds when we allow that the numbers can be extracted approximately, up to some error (even when we only want to know whether a set is bounded or not). All the results remain true when we allow the Y combinator (recursion) in our λ-terms, as well as uninterpreted constants.


title: Gradual type-and-effect systems

authors:
Felipe Bañados Schwerter
Ronald Garcia
Éric Tanter

abstract: Abstract Effect systems have the potential to help software developers, but their practical adoption has been very limited. We conjecture that this limited adoption is due in part to the difficulty of transitioning from a system where effects are implicit and unrestricted to a system with a static effect discipline, which must settle for conservative checking in order to be decidable. To address this hindrance, we develop a theory of gradual effect checking, which makes it possible to incrementally annotate and statically check effects, while still rejecting statically inconsistent programs. We extend the generic type-and-effect framework of Marino and Millstein with a notion of unknown effects, which turns out to be significantly more subtle than unknown types in traditional gradual typing. We appeal to abstract interpretation to develop and validate the concepts of gradual effect checking. We also demonstrate how an effect system formulated in the framework of Marino and Millstein can be automatically extended to support gradual checking. We use gradual effect checking to develop a fully gradual type-and-effect framework, which permits interaction between static and dynamic checking for both effects and types.


title: Composable scheduler activations for Haskell

authors:
K. C. Sivaramakrishnan
Tim Harris
Simon Marlow
Simon Peyton Jones

abstract: Abstract The runtime for a modern, concurrent, garbage collected language like Java or Haskell is like an operating system: sophisticated, complex, performant, but alas very hard to change. If more of the runtime system were in the high-level language, it would be far more modular and malleable. In this paper, we describe a novel concurrency substrate design for the Glasgow Haskell Compiler that allows multicore schedulers for concurrent and parallel Haskell programs to be safely and modularly described as libraries in Haskell. The approach relies on abstracting the interface to the user-implemented schedulers through scheduler activations, together with the use of Software Transactional Memory to promote safety in a multicore context.


title: Romeo: A system for more flexible binding-safe programming

authors:
Paul Stansifer
Mitchell Wand

abstract: Abstract Current systems for safely manipulating values containing names only support simple binding structures for those names. As a result, few tools exist to safely manipulate code in those languages for which name problems are the most challenging. We address this problem with Romeo, a language that respects α-equivalence on its values, and which has access to a rich specification language for binding, inspired by attribute grammars. Our work has the complex-binding support of David Herman's λ m , but is a full-fledged binding-safe language like Pure FreshML.


title: Transparent fault tolerance for scalable functional computation

authors:
Robert J. Stewart
Patrick Maier
Phil Trinder

abstract: Abstract Reliability is set to become a major concern on emergent large-scale architectures. While there are many parallel languages, and indeed many parallel functional languages, very few address reliability. The notable exception is the widely emulated Erlang distributed actor model that provides explicit supervision and recovery of actors with isolated state. We investigate scalable transparent fault tolerant functional computation with automatic supervision and recovery of tasks. We do so by developing HdpH-RS , a variant of the Haskell distributed parallel Haskell (HdpH) DSL with Reliable Scheduling. Extending the distributed work stealing protocol of HdpH for task supervision and recovery is challenging. To eliminate elusive concurrency bugs, we validate the HdpH-RS work stealing protocol using the SPIN model checker. HdpH-RS differs from the actor model in that its principal entities are tasks, i.e. independent stateless computations, rather than isolated stateful actors. Thanks to statelessness, fault recovery can be performed automatically and entirely hidden in the HdpH-RS runtime system. Statelessness is also key for proving a crucial property of the semantics of HdpH-RS: fault recovery does not change the result of the program, akin to deterministic parallelism. HdpH-RS provides a simple distributed fork/join-style programming model, with minimal exposure of fault tolerance at the language level, and a library of higher level abstractions such as algorithmic skeletons. In fact, the HdpH-RS DSL is exactly the same as the HdpH DSL, hence users can opt in or out of fault tolerant execution without any refactoring. Computations in HdpH-RS are always as reliable as the root node, no matter how many nodes and cores are actually used. We benchmark HdpH-RS on conventional clusters and an High Performance Computing platform: all benchmarks survive Chaos Monkey random fault injection; the system scales well e.g. up to 1,400 cores on the High Performance Computing; reliability and recovery overheads are consistently low even at scale.


title: Efficiency of lambda-encodings in total type theory

authors:
Aaron Stump
Peng Fu

abstract: Abstract This paper proposes a new typed lambda-encoding for inductive types which, for Peano numerals, has the expected time complexities for basic operations like addition and multiplication, has a constant-time predecessor function, and requires only quadratic space to encode a numeral. This improves on the exponential space required by the Parigot encoding. Like the Parigot encoding, the new encoding is typable in System F-omega plus positive-recursive type definitions, a total type theory. The new encoding is compared with previous ones through a significant case study: mergesort using Braun trees. The practical runtime efficiency of the new encoding, and the Church and Parigot encodings, are compared by two translations, one to Racket and one to Haskell, on a small suite of benchmarks.


title: A language for hierarchical data parallel design-space exploration on GPUs

authors:
Bo Joel Svensson
Ryan R. Newton
Mary Sheeran

abstract: Abstract Graphics Processing Units (GPUs) offer potential for very high performance; they are also rapidly evolving. Obsidian is an embedded language (in Haskell) for implementing high performance kernels to be run on GPUs. We would like to have our cake and eat it too; we want to raise the level of abstraction beyond CUDA code and still give the programmer control over the details relevant to kernel performance. To that end, Obsidian provides array representations that guarantee elimination of intermediate arrays while also using the type system to model the hierarchy of the GPU. Operations are compiled very differently depending on what level of the GPU they target, and as a result, the user is gently constrained to write code that matches the capabilities of the GPU. Thus, we implement not Nested Data Parallelism, but a more limited form that we call Hierarchical Data Parallelism. We walk through case-studies that demonstrate how to use Obsidian for rapid design exploration or auto-tuning, resulting in performance that compares well to the hand-tuned kernels used in Accelerate and NVIDIA Thrust.


title: Review of spreadsheet implementation technology: Basics and extensions, by Peter Sestoft , MIT Press, 2014, ISBN 978-0-262-52664-7


title: Linear lambda terms as invariants of rooted trivalent maps

abstract: Abstract The main aim of the paper is to give a simple and conceptual account for the correspondence (originally described by Bodini, Gardy, and Jacquot) between α-equivalence classes of closed linear lambda terms and isomorphism classes of rooted trivalent maps on compact-oriented surfaces without boundary, as an instance of a more general correspondence between linear lambda terms with a context of free variables and rooted trivalent maps with a boundary of free edges. We begin by recalling a familiar diagrammatic representation for linear lambda terms, while at the same time explaining how such diagrams may be read formally as a notation for endomorphisms of a reflexive object in a symmetric monoidal closed (bi)category. From there, the “easy” direction of the correspondence is a simple forgetful operation which erases annotations on the diagram of a linear lambda term to produce a rooted trivalent map. The other direction views linear lambda terms as complete invariants of their underlying rooted trivalent maps, reconstructing the missing information through a Tutte-style topological recurrence on maps with free edges. As an application in combinatorics, we use this analysis to enumerate bridgeless rooted trivalent maps as linear lambda terms containing no closed proper subterms, and conclude by giving a natural reformulation of the Four Color Theorem as a statement about typing in lambda calculus.


title: Interactive programming in Agda - Objects and graphical user interfaces

authors:
Andreas Abel
Stephan Adelsberger
Anton Setzer

abstract: Abstract We develop a methodology for writing interactive and object-based programs (in the sense of Wegner) in dependently typed functional programming languages. The methodology is implemented in the ooAgda library. ooAgda provides a syntax similar to the one used in object-oriented programming languages, thanks to Agda's copattern matching facility. The library allows for the development of graphical user interfaces (GUIs), including the use of action listeners. Our notion of interactive programs is based on the IO monad defined by Hancock and Setzer, which is a coinductive data type. We use a sized coinductive type which allows us to write corecursive programs in a modular way. Objects are server-side interactive programs that respond to method calls by giving answers and changing their state. We introduce two kinds of objects: simple objects and IO objects. Methods in simple objects are pure, while method calls in IO objects allow for interactions before returning their result. Our approach also allows us to extend interfaces and objects by additional methods. We refine our approach to state-dependent interactive programs and objects through which we can avoid exceptions. For example, with a state-dependent stack object, we can statically disable the pop method for empty stacks. As an example, we develop the implementation of recursive functions using a safe stack. Using a coinductive notion of object bisimilarity, we verify basic correctness properties of stack objects and show the equivalence of different stack implementations. Finally, we give a proof of concept that our interaction model allows to write GUI programs in a natural way: we present a simple drawing program, and a program which allows the users to move a small spaceship using a button.


title: Normal-order reduction grammars

abstract: Abstract We present an algorithm which, for given n , generates an unambiguous regular tree grammar defining the set of combinatory logic terms, over the set {S, K} of primitive combinators, requiring exactly n normal-order reduction steps to normalize. As a consequence of Curry and Feys's standardization theorem, our reduction grammars form a complete syntactic characterization of normalizing combinatory logic terms. Using them, we provide a recursive method of constructing ordinary generating functions counting the number of SK -combinators reducing in n normal-order reduction steps. Finally, we investigate the size of generated grammars giving a primitive recursive upper bound.


title: Contributions to a computational theory of policy advice and avoidability

authors:
Nicola Botta
Patrik Jansson
Cezar Ionescu

abstract: Abstract We present the starting elements of a mathematical theory of policy advice and avoidability. More specifically, we formalize a cluster of notions related to policy advice, such as policy , viability , reachability , and propose a novel approach for assisting decision making, based on the concept of avoidability . We formalize avoidability as a relation between current and future states, investigate under which conditions this relation is decidable and propose a generic procedure for assessing avoidability. The formalization is constructive and makes extensive use of the correspondence between dependent types and logical propositions, decidable judgments are obtained through computations. Thus, we aim for a computational theory, and emphasize the role that computer science can play in global system science.


title: Computation semantics of the functional scientific workflow language Cuneiform

authors:
Jörgen Brandt
Wolfgang Reisig
Ulf Leser

abstract: Abstract Cuneiform is a minimal functional programming language for large-scale scientific data analysis. Implementing a strict black-box view on external operators and data, it allows the direct embedding of code in a variety of external languages like Python or R, provides data-parallel higher order operators for processing large partitioned data sets, allows conditionals and general recursion, and has a naturally parallelizable evaluation strategy suitable for multi-core servers and distributed execution environments like Hadoop, HTCondor, or distributed Erlang. Cuneiform has been applied in several data-intensive research areas including remote sensing, machine learning, and bioinformatics, all of which critically depend on the flexible assembly of pre-existing tools and libraries written in different languages into complex pipelines. This paper introduces the computation semantics for Cuneiform. It presents Cuneiform's abstract syntax, a simple type system, and the semantics of evaluation. Providing an unambiguous specification of the behavior of Cuneiform eases the implementation of interpreters which we showcase by providing a concise reference implementation in Erlang. The similarity of Cuneiform's syntax to the simply typed lambda calculus puts Cuneiform in perspective and allows a straightforward discussion of its design in the context of functional programming. Moreover, the simple type system allows the deduction of the language's safety up to black-box operators. Last, the formulation of the semantics also permits the verification of compilers to and from other workflow languages.


title: The essence of ornaments

abstract: Abstract Functional programmers from all horizons strive to use, and sometimes abuse, their favorite type system in order to capture the invariants of their programs. A widely used tool in that trade consists in defining finely indexed datatypes. Operationally, these types classify the programmer's data, following the ML tradition. Logically, these types enforce the program invariants in a novel manner. This new programming pattern, by which one programs over inductive definitions to account for some invariants, lead to the development of a theory of ornaments (McBride, 2011 Ornamental Algebras, Algebraic Ornaments . Unpublished). However, ornaments originate as a dependently-typed object and may thus appear rather daunting to a functional programmer of the non-dependent kind. This article aims at presenting ornaments from first-principles and, in particular, to declutter their presentation from syntactic considerations. To do so, we shall give a sufficiently abstract model of indexed datatypes by means of many-sorted signatures. In this process, we formalize our intuition that an indexed datatype is the combination of a data- structure and a data- logic . Over this abstraction of datatypes, we shall recast the definition of ornaments, effectively giving a model of ornaments. Benefiting both from the operational and abstract nature of many-sorted signatures, ornaments should appear applicable and, one hopes, of interest beyond the type-theoretic circles, case in point being languages with generalized abstract datatypes or refinement types.


title: An algebra for distributed Big Data analytics

abstract: Abstract We present an algebra for data-intensive scalable computing based on monoid homomorphisms that consists of a small set of operations that capture most features supported by current domain-specific languages for data-centric distributed computing. This algebra is being used as the formal basis of MRQL, which is a query processing and optimization system for large-scale distributed data analysis. The MRQL semantics is given in terms of monoid comprehensions, which support group-by and order-by syntax and can work on heterogeneous collections without requiring any extension to the monoid algebra. We present the syntax and semantics of monoid comprehensions and provide rules to translate them to the monoid algebra. We give evidence of the effectiveness of our algebra by presenting some important optimization rules, such as converting nested queries to joins.


title: Correctness of compiling polymorphism to dynamic typing

authors:
Kuen-Bang Hou (Favonia)
Nick Benton
Robert Harper

abstract: Abstract The connection between polymorphic and dynamic typing was originally considered by Curry et al. (1972, Combinatory Logic , vol. ii) in the form of “polymorphic type assignment” for untyped λ-terms. Types are assigned after the fact to what is, in modern terminology, a dynamic language. Interest in type assignment was revitalized by the proposals of Bracha et al. (1998, OOPSLA) and Bank et al. (1997, POPL) to enrich Java with polymorphism (generics), which in turn sparked the development of other languages, such as Scala, with similar combinations of features. In such a setting, where the target language already has a monomorphic type system, it is desirable to compile polymorphism to dynamic typing in such a way that as much static typing as possible is preserved, relying on dynamics only insofar as genericity is actually required. The basic approach is to compile polymorphism using embeddings from each type into a universal “top” type, ${\mathbb{D}}$ , and partial projections that go in the other direction. This scheme is intuitively reasonable, and, indeed, has been used in practice many times. Proving its correctness, however, is non-trivial. This paper studies the compilation of System F to an extension of Moggi's computational meta-language with a dynamic type and shows how the compilation may be proved correct using a logical relation.


title: PhD Abstracts

abstract: Many students complete PhDs in functional programming each year. As a service to the community, the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.


title: Compiling a 50-year journey

authors:
Graham Hutton
Patrick Bahr

abstract: Abstract Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based machine. In this article, we revisit this example in a modern context, and show how such a compiler can now be calculated directly from a specification of its correctness using simple equational reasoning techniques.


title: Call-by-name extensionality and confluence

authors:
Philip Johnson-Freyd
Paul Downen
Zena M. Ariola

abstract: Abstract Designing rewriting systems that respect functional extensionality for call-by-name languages with effects turns out to be surprisingly challenging. Simply interpreting extensional laws like η as reduction rules easily breaks confluence. We explore these issues in the setting of a sequent calculus. Building on an insight that appears in different aspects of the theory of call-by-name functional languages—confluent rewriting for two independent control calculi and sound continuation-passing style transformations—we give a confluent reduction system for lazy extensional functions. Finally, we consider limitations to this approach when used for strict evaluation and types beyond functions.


title: No value restriction is needed for algebraic effects and handlers

authors:
Ohad Kammar
Matija Pretnar

abstract: Abstract We present a straightforward, sound, Hindley–Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. We first recall that the soundness of unrestricted call-by-value Hindley–Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations, and that many programming examples can be recast to use effect handlers instead of these effects. After presenting the calculus and its soundness proof, formalised in Twelf, we analyse the expressive power of effect handlers with respect to state effects. We conjecture handlers alone cannot express reference cells, but show they can simulate dynamically scoped state, establishing that dynamic binding also does not need a value restriction.


title: Programming with ornaments

authors:
Hsiang-Shang Ko
Jeremy Gibbons

abstract: Abstract Dependently typed programming advocates the use of various indexed versions of the same shape of data, but the formal relationship amongst these structurally similar datatypes usually needs to be established manually and tediously. Ornaments have been proposed as a formal mechanism to manage the relationships between such datatype variants. In this paper, we conduct a case study under an ornament framework; the case study concerns programming binomial heaps and their operations — including insertion and minimum extraction — by viewing them as lifted versions of binary numbers and numeric operations. We show how current dependently typed programming technology can lead to a clean treatment of the binomial heap constraints when implementing heap operations. We also identify some gaps between the current technology and an ideal dependently typed programming language that we would wish to have for our development.


title: Fair enumeration combinators

authors:
Max S. New
Burke Fetscher
Robert Bruce Findler
Jay A. McCarthy

abstract: Abstract Enumerations represented as bijections between the natural numbers and elements of some given type have recently garnered interest in property-based testing because of their efficiency and flexibility. There are, however, many ways of defining these bijections, some of which are better than others. This paper offers a new property of enumeration combinators called fairness that identifies enumeration combinators that are better suited to property-based testing. Intuitively, the result of a fair combinator indexes into its argument enumerations equally when constructing its result. For example, extracting the n th element from our enumeration of three-tuples indexes about $\sqrt[3]{n}$ elements into each of its components instead of, say, indexing $\sqrt[2]{n}$ into one and $\sqrt[4]{n}$ into the other two, as you would if a three-tuple were built out of nested pairs. Similarly, extracting the n th element from our enumeration of a three-way union returns an element that is $\frac{n}{3}$ into one of the argument enumerators. The paper presents a semantics of enumeration combinators, a theory of fairness, proofs establishing fairness of our new combinators and that some combinations of fair combinators are not fair. We also report on an evaluation of fairness for the purpose of finding bugs in programming-language models. We show that fair enumeration combinators have complementary strengths to an existing, well-tuned ad hoc random generator (better on short time scales and worse on long time scales) and that using unfair combinators is worse across the board.


title: Higher order symbolic execution for contract verification and refutation

authors:
Phuc C. Nguyen
Sam Tobin-Hochstadt
David Van Horn

abstract: Abstract We present a new approach to automated reasoning about higher-order programs by endowing symbolic execution with a notion of higher-order, symbolic values. To validate our approach, we use it to develop and evaluate a system for verifying and refuting behavioral software contracts of components in a functional language, which we call soft contract verification . In doing so, we discover a mutually beneficial relation between behavioral contracts and higher-order symbolic execution. Contracts aid symbolic execution by providing a rich language of specifications serving as a basis of symbolic higher-order values; the theory of blame enables modular verification and leads to the theorem that verified components can't be blamed ; and the run-time monitoring of contracts enables soft verification whereby verified and unverified components can safely interact. Conversely, symbolic execution aids contracts by providing compile-time verification and automated test case generation from counter-examples to verification. This relation between symbolic exuection and contracts engenders a virtuous cycle encouraging the gradual use of contracts. Our approach is able to analyze first-class contracts, recursive data structures, unknown functions, and control-flow-sensitive refinements of values, which are all idiomatic in dynamic languages. It makes effective use of off-the-shelf solvers to decide problems without heavy encodings. Counterexample search is sound and relatively complete with respect to a first-order solver for base type values and counter-examples are reported as concrete values, including functions. Therefore, it can form the basis of automated verification and bug-finding tools for higher-order programs. The approach is competitive with a range of existing tools—including type systems, flow analyzers, and model checkers—on their own benchmarks. We have built a prototype to analyze programs written in Racket and report on its effectiveness in verifying and refuting contracts.


title: A simple library implementation of binary sessions

abstract: Abstract Inspired by the continuation-passing encoding of binary sessions, we describe a simple approach to embed a hybrid form of session type checking into any programming language that supports parametric polymorphism. The approach combines static protocol analysis with dynamic linearity checks. To demonstrate the effectiveness of the technique, we implement a well-integrated OCaml module for session communications. For free, OCaml provides us with equirecursive session types, parametric behavioural polymorphism, complete session type inference, and session subtyping.


title: Backtracking with cut via a distributive law and left-zero monoids

authors:
Maciej Piróg
Sam Staton

abstract: Abstract We employ the framework of algebraic effects to augment the list monad with the pruning cut operator known from Prolog. We give two descriptions of the resulting monad: as the monad of free left-zero monoids, and as a composition via a distributive law of the list monad and the ‘unary idempotent operation’ monad. The scope delimiter of cut arises as a handler.


title: Notions of computation as monoids

authors:
Exequiel Rivas
Mauro Jaskelioff

abstract: Abstract There are different notions of computation, the most popular being monads, applicative functors, and arrows. In this article, we show that these three notions can be seen as instances of a unifying abstract concept: monoids in monoidal categories. We demonstrate that even when working at this high level of generality, one can obtain useful results. In particular, we give conditions under which one can obtain free monoids and Cayley representations at the level of monoidal categories, and we show that their concretisation results in useful constructions for monads, applicative functors, and arrows. Moreover, by taking advantage of the uniform presentation of the three notions of computation, we introduce a principled approach to the analysis of the relation between them.


title: Algebraic data integration

authors:
Patrick Schultz
Ryan Wisnesky

abstract: Abstract In this paper, we develop an algebraic approach to data integration by combining techniques from functional programming, category theory, and database theory. In our formalism, database schemas and instances are algebraic (multi-sorted equational) theories of a certain form. Schemas denote categories, and instances denote their initial (term) algebras. The instances on a schema S form a category, S – Inst , and a morphism of schemas F : S → T induces three adjoint data migration functors: Σ F : S – Inst → T – Inst , defined by substitution along F , which has a right adjoint Δ F : T – Inst → S – Inst , which in turn has a right adjoint Π F : S – Inst → T – Inst . We present a query language based on for/where/return syntax where each query denotes a sequence of data migration functors; a pushout-based design pattern for performing data integration using our formalism; and describe the implementation of our formalism in a tool we call AQL (Algebraic Query Language).


title: Capability-based localization of distributed and heterogeneous queries

authors:
João Costa Seco
Paulo Ferreira
Hugo Lourenço

abstract: Abstract One key aspect of data-centric applications is the manipulation of data stored in persistent repositories, which is moving fast from querying a centralized relational database to the ad-hoc combination of constellations of data sources. The extension of general purpose languages with query operations is increasingly popular, as a tool to improve reasoning and optimizing capabilities of interpreters and compilers. However, not much is being done to integrate and orchestrate different and separate sources of data. We present a data manipulation language that abstracts the nature and location of data-sources. We define its semantics and a type directed query localization mechanism to be used in development tools for heterogeneous environments to efficiently compile them into native queries. We introduce a localization procedure based on rewriting of query expressions that is confluent, terminating and provides the maximum mapping between site capabilities and the structure of the query. We provide formal type safety results that support the sound distribution of query fragments over remote sites. Our approach is also suitable for an interactive query construction environment by rich user interfaces that provide immediate feedback on data manipulation operations. This approach is currently the base for the data layer of a development platform for mobile and web applications.


title: Modular, higher order cardinality analysis in theory and practice

authors:
Ilya Sergey
Dimitrios Vytiniotis
Simon L. Peyton Jones
Joachim Breitner

abstract: Abstract Since the mid '80s, compiler writers for functional languages (especially lazy ones) have been writing papers about identifying and exploiting thunks and lambdas that are used only once. However, it has proved difficult to achieve both power and simplicity in practice. In this paper, we describe a new, modular analysis for a higher order language, which is both simple and effective. We prove the analysis sound with respect to a standard call-by-need semantics, and present measurements of its use in a full-scale, state-of-the-art optimising compiler. The analysis finds many single-entry thunks and one-shot lambdas and enables a number of program optimisations. This paper extends our preceding conference publication (Sergey et al. 2014 Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014) . ACM, pp. 335–348) with proofs, expanded report on evaluation and a detailed examination of the factors causing the loss of precision in the analysis.


title: Quick specifications for the busy programmer

authors:
Nicholas Smallbone
Moa Johansson
Koen Claessen
Maximilian Algehed

abstract: Abstract QuickSpec is a theory exploration system which tests a Haskell program to find equational properties of it, automatically. The equations can be used to help understand the program, or as lemmas to help prove the program correct. QuickSpec is largely automatic: the user just supplies the functions to be tested and QuickCheck data generators. Previous theory exploration systems, including earlier versions of QuickSpec itself, scaled poorly. This paper describes a new architecture for theory exploration with which we can find vastly more complex laws than before, and much faster. We demonstrate theory exploration in QuickSpec on problems both from functional programming and mathematics.


title: Flexible dynamic information flow control in the presence of exceptions

authors:
Deian Stefan
David Mazières
John C. Mitchell
Alejandro Russo

abstract: Abstract We describe a language-based, dynamic information flow control (IFC) system called LIO. Our system presents a new design point for IFC, influenced by the challenge of implementing IFC as a Haskell library, as opposed to the more typical approach of modifying the language runtime system. In particular, we take a coarse-grained, floating-label approach, previously used by IFC Operating Systems, and associate a single, mutable label—the current label —with all the data in a computation's context. This label is always raised to reflect the reading of sensitive information and it is used to restrict the underlying computation's effects. To preserve the flexibility of fine-grained systems, LIO also provides programmers with a means for associating an explicit label with a piece of data. Interestingly, these labeled values can be used to encapsulate the results of sensitive computations which would otherwise lead to the creeping of the current label. Unlike other language-based systems, LIO also bounds the current label with a current clearance , providing a form of discretionary access control that LIO programs can use to deal with covert channels. Moreover, LIO provides programmers with mutable references and exceptions. The latter, exceptions, are used in LIO to encode and recover from monitor failures, all while preserving data confidentiality and integrity—this addresses a longstanding concern that dynamic IFC is inherently prone to information leakage due to monitor failure.


title: The calculus of dependent lambda eliminations

abstract: Abstract Modern constructive type theory is based on pure dependently typed lambda calculus, augmented with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system. New typing constructs are defined that enable induction, as well as large eliminations with lambda encodings. These constructs are constructor-constrained recursive types, and a lifting operation to lift simply typed terms to the type level. Using a lattice-theoretic denotational semantics for types, the language is proved logically consistent. The power of CDLE is demonstrated through several examples, which have been checked with a prototype implementation called Cedille.


title: Special issue on Programming with Dependent Types Editorial

authors:
Wouter Swierstra
Peter Dybjer

abstract: There has been sustained interest in functional programming languages with dependent types in recent years. The foundations of dependently typed programming can be traced back to Martin–Löf's work in the 1970s. In the past decades, this vision has given rise to the development of proof assistants and functional programming languages based on dependent types. The increased popularity of systems such as Agda, Coq, Idris, and many others, reflects the growing momentum in this research area. After sending out our first call for papers in October 2015, we are happy to accept six articles in this special issue covering a wide spectrum of topics.


title: Finiteness and rational sequences, constructively

authors:
Tarmo Uustalu
Niccolò Veltri

abstract: Abstract Rational sequences are possibly infinite sequences with a finite number of distinct suffixes. In this paper, we present different implementations of rational sequences in Martin–Löf type theory. First, we literally translate the above definition of rational sequence into the language of type theory, i.e., we construct predicates on possibly infinite sequences expressing the finiteness of the set of suffixes. In type theory, there exist several inequivalent notions of finiteness. We consider two of them, listability and Noetherianness, and show that in the implementation of rational sequences the two notions are interchangeable. Then we introduce the type of lists with backpointers, which is an inductive implementation of rational sequences. Lists with backpointers can be unwound into rational sequences, and rational sequences can be truncated into lists with backpointers. As an example, we see how to convert the fractional representation of a rational number into its decimal representation and vice versa.


title: A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading

authors:
Beta Ziliani
Matthieu Sozeau

abstract: Abstract Unification is a core component of every proof assistant or programming language featuring dependent types. In many cases, it must deal with higher order problems up to conversion. Since unification in such conditions is undecidable, unification algorithms may include several heuristics to solve common problems. However, when the stack of heuristics grows large, the result and complexity of the algorithm can become unpredictable. Our contributions are twofold: (1) We present a full description of a new unification algorithm for the Calculus of Inductive Constructions (the base logic of C OQ ), building it up from a basic calculus to the full Calculus of Inductive Constructions as it is implemented in C OQ , including universe polymorphism, canonical structures (the overloading mechanism baked into C OQ 's unification), and a small set of useful heuristics. (2) We implemented our algorithm, and tested it on several libraries, providing evidence that the selected set of heuristics suffices for large developments.


title: Size-based termination of higher-order rewriting

abstract: Abstract We provide a general and modular criterion for the termination of simply typed λ-calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.


title: The adequacy of Launchbury's natural semantics for lazy evaluation

abstract: Abstract In his seminal paper “A Natural Semantics for Lazy Evaluation”, John Launchbury proves his semantics correct with respect to a denotational semantics, and outlines a proof of adequacy. Previous attempts to rigorize the adequacy proof, which involves an intermediate natural semantics and an intermediate resourced denotational semantics, have failed. We devised a new, direct proof that skips the intermediate natural semantics. It is the first rigorous adequacy proof of Launchbury's semantics. We have modeled our semantics in the interactive theorem prover Isabelle and machine-checked our proofs. This does not only provide a maximum level of rigor, but also serves as a tool for further work, such as a machine-checked correctness proof of a compiler transformation.


title: Systematic identification and communication of type errors

authors:
Sheng Chen
Martin Erwig

abstract: Abstract When type inference fails, it is often difficult to pinpoint the cause of the type error among many potential candidates. Generating informative messages to remove the type error is another difficult task due to the limited availability of type information. Over the last three decades many approaches have been developed to help debug type errors. However, most of these methods suffer from one or more of the following problems: (1) Being incomplete, they miss the real cause. (2) They cover many potential causes without distinguishing them. (3) They provide little or no information for how to remove the type error. Any one of this problems can turn the type-error debugging process into a tedious and ineffective endeavor. To address this issue, we have developed a method named counter-factual typing , which (1) finds a comprehensive set of error causes in AST leaves, (2) computes an informative message on how to get rid of the type error for each error cause, and (3) ranks all messages and iteratively presents the message for the most likely error cause. The biggest technical challenge is the efficient generation of all error messages, which seems to be exponential in the size of the expression. We address this challenge by employing the idea of variational typing that systematically reuses computations for shared parts and generates all messages by typing the whole ill-typed expression only once. We have evaluated our approach over a large set of examples collected from previous publications in the literature. The evaluation result shows that our approach outperforms previous approaches and is computationally feasible.


title: Special Issue on Programming Languages for Big Data Editorial

authors:
James Cheney
Torsten Grust

abstract: Ideas from programming languages play an important role in a range of advanced applications of databases, in database system implementation, distributed programming (MapReduce), streaming computation, and high-performance (GPU/multicore) computation. This creative research area is broadening into a subfield of data-centric computation. Although the interaction of databases and programming has a long history (the 16th biennial Database Programming Languages symposium was held in 2017), there has been a recent renewal of interest and broadening of programming language techniques for dealing with data from several quarters in the last few years, including workshops at Microsoft Research (RADICAL 2010), ICFP (XLDI 2012), POPL (DDFP 2013, DCM 2014) and a Dagstuhl Seminar on Programming Languages for Big Data (December 2014). This special issue recognises and encourages the publication of mature research contributions in this area.


title: Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory

authors:
Jesper Cockx
Dominique Devriese

abstract: Abstract Dependently typed languages such as Agda, Coq, and Idris use a syntactic first-order unification algorithm to check definitions by dependent pattern matching. However, standard unification algorithms implicitly rely on principles such as uniqueness of identity proofs and injectivity of type constructors . These principles are inadmissible in many type theories, particularly in the new and promising branch known as homotopy type theory. As a result, programs and proofs in these new theories cannot make use of dependent pattern matching or other techniques relying on unification, and are as a result much harder to write, modify, and understand. This paper proposes a proof-relevant framework for reasoning formally about unification in a dependently typed setting. In this framework, unification rules compute not just a unifier but also a corresponding soundness proof in the form of an equivalence between two sets of equations. By rephrasing the standard unification rules in a proof-relevant manner, they are guaranteed to preserve soundness of the theory. In addition, it enables us to safely add new rules that can exploit the dependencies between the types of equations, such as rules for eta-equality of record types and higher dimensional unification rules for solving equations between equality proofs. Using our framework, we implemented a complete overhaul of the unification algorithm used by Agda. As a result, we were able to replace previous ad-hoc restrictions with formally verified unification rules, fixing a substantial number of bugs in the process. In the future, we may also want to integrate new principles with pattern matching, for example, the higher inductive types introduced by homotopy type theory. Our framework also provides a solid basis for such extensions to be built on.


title: Foundations of dependent interoperability

authors:
Pierre-Évariste Dagand
Nicolas Tabareau
Éric Tanter

abstract: Abstract Full-spectrum dependent types promise to enable the development of correct-by-construction software. However, even certified software needs to interact with simply-typed or untyped programs, be it to perform system calls, or to use legacy libraries. Trading static guarantees for runtime checks, the dependent interoperability framework provides a mechanism by which simply-typed values can safely be coerced to dependent types and, conversely, dependently-typed programs can defensively be exported to a simply-typed application. In this article, we give a semantic account of dependent interoperability. Our presentation relies on and is guided by a pervading notion of type equivalence, whose importance has been emphasized in recent work on homotopy type theory. Specifically, we develop the notions of type-theoretic partial Galois connections as a key foundation for dependent interoperability, which accounts for the partiality of the coercions between types. We explore the applicability of both type-theoretic Galois connections and anticonnections in the setting of dependent interoperability. A partial Galois connection enforces a translation of dependent types to runtime checks that are both sound and complete with respect to the invariants encoded by dependent types. Conversely, picking an anticonnection instead lets us induce weaker, sound conditions that can amount to more efficient runtime checks. Our framework is developed in Coq; it is thus constructive and verified in the strictest sense of the terms. Using our library, users can specify domain-specific partial connections between data structures. Our library then takes care of the (sometimes, heavy) lifting that leads to interoperable programs. It thus becomes possible, as we shall illustrate, to internalize and hand-tune the extraction of dependently-typed programs to interoperable OCaml programs within Coq itself.


title: A tutorial on computational classical logic and the sequent calculus

authors:
Paul Downen
Zena M. Ariola

abstract: Abstract We present a model of computation that heavily emphasizes the concept of duality and the interaction between opposites–production interacts with consumption. The symmetry of this framework naturally explains more complicated features of programming languages through relatively familiar concepts. For example, binding a value to a variable is dual to manipulating the flow of control in a program. By looking at the computational interpretation of the sequent calculus, we find a language that lets us speak about duality, control flow, and evaluation order in programs as first-class concepts. We begin by reviewing Gentzen's LK sequent calculus and show how the Curry–Howard isomorphism still applies to give us a different basis for expressing computation. We then illustrate how the fundamental dilemma of computation in the sequent calculus gives rise to a duality between evaluation strategies : strict languages are dual to lazy languages. Finally, we discuss how the concept of focusing , developed in the setting of proof search, is related to the idea of type safety for computation expressed in the sequent calculus. In this regard, we compare and contrast two different methods of focusing that have appeared in the literature, static and dynamic focusing, and illustrate how they are two means to the same end.


title: Abstract allocation as a unified approach to polyvariance in control-flow analyses

authors:
Thomas Gilray
Michael D. Adams
Matthew Might

abstract: Abstract In higher order settings, control-flow analysis aims to model the propagation of both data and control by finitely approximating program behaviors across all possible executions. The polyvariance of an analysis describes the number of distinct abstract representations, or variants, for each syntactic entity (e.g., functions, variables, or intermediate expressions). Monovariance, one of the most basic forms of polyvariance, maintains only a single abstract representation for each variable or expression. Other polyvariant strategies allow a greater number of distinct abstractions and increase analysis complexity with the aim of increasing analysis precision. For example, k -call sensitivity distinguishes flows by the most recent k call sites, k -object sensitivity by a history of allocation points, and argument sensitivity by a tuple of dynamic argument types. From this perspective, even a concrete operational semantics may be thought of as an unboundedly polyvariant analysis. In this paper, we develop a unified methodology that fully captures this design space. It is easily tunable and guarantees soundness regardless of how tuned. We accomplish this by extending the method of abstracting abstract machines, a systematic approach to abstract interpretation of operational abstract-machine semantics. Our approach permits arbitrary instrumentation of the underlying analysis and arbitrary tuning of an abstract-allocation function. We show that the design space of abstract allocators both unifies and generalizes existing notions of polyvariance. Simple changes to the behavior of this function recapitulate classic styles of analysis and yield novel combinations and variants.


title: A programming model and foundation for lineage-based distributed computation

authors:
Philipp Haller
Heather Miller
Normen Müller

abstract: Abstract The most successful systems for “big data” processing have all adopted functional APIs. We present a new programming model, we call function passing , designed to provide a more principled substrate, or middleware, upon which to build data-centric distributed systems like Spark. A key idea is to build up a persistent functional data structure representing transformations on distributed immutable data by passing well-typed serializable functions over the wire and applying them to this distributed data. Thus, the function passing model can be thought of as a persistent functional data structure that is distributed , where transformations performed on distributed data are stored in its nodes rather than the distributed data itself. One advantage of this model is that failure recovery is simplified by design – data can be recovered by replaying function applications atop immutable data loaded from stable storage. Deferred evaluation is also central to our model; by incorporating deferred evaluation into our design only at the point of initiating network communication, the function passing model remains easy to reason about while remaining efficient in time and memory. Moreover, we provide a complete formalization of the programming model in order to study the foundations of lineage-based distributed computation. In particular, we develop a theory of safe, mobile lineages based on a subject reduction theorem for a typed core language. Furthermore, we formalize a progress theorem that guarantees the finite materialization of remote, lineage-based data. Thus, the formal model may serve as a basis for further developments of the theory of data-centric distributed programming, including aspects such as fault tolerance. We provide an open-source implementation of our model in and for the Scala programming language, along with a case study of several example frameworks and end-user programs written atop this model.


title: On constructing 2-3 trees

abstract: We consider the task of constructing 2-3 trees. Given a sequence of elements we seek to build a 2-3 tree–in linear time–that contains the elements in symmetric order. We discuss three approaches: top-down, bottom-up, and incremental. The incremental approach is more flexible than the other two in that it allows us to interleave the construction work with other operations, for example, queries.


title: Batcher's odd-even merging network revealed

authors:
Ralf Hinze
Clare Martin

abstract: Comparison networks offer an attractive framework for studying parallel sorting algorithms. The visual presentation of such hard-wired networks makes processes easy to conceptualize without the overhead of programming syntax or the semantic complications of concurrency. Though simple in appearance they have a surprisingly rich structure. In this pearl we delve a little into their theory.


title: Parberry's pairwise sorting network revealed

abstract: Batcher’s “merge exchange” sorting network, discussed in a previous pearl (Hinze & Martin, 2016), remains one of the best practical algorithms for oblivious sorting, even almost half a century after its inception. So it is surprising that an algorithm with exactly the same level of performance, devised two decades later by Parberry (1992), has been relatively overlooked. Perhaps a reason for its lack of celebrity is that Parberry’s design is not immediately recognizable, whereas the Batcher method has a familiar ring, as a hardwired implementation of merge sort. Here we hope to rectify this imbalance by unravelling Parberry’s algorithm and uncoupling its close relationship to Batcher’s. Interestingly, Parberry derives his network using the zero-one principle (Knuth, 1998). We abandon this traditional method, in favour of a feature of comparison networks that we consider to be more fundamental: monotonicity. We shall see that this property, used before to demystify Batcher’s merger (Hinze & Martin, 2016), also helps to shed some light on Parberry’s design. To keep the pearl reasonably self-contained we start with a quick recap of the notation and Batcher’s construction.


title: PhD Abstracts

abstract: Many students complete PhDs in functional programming each year. As a service to the community, the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.


title: Iris from the ground up: A modular foundation for higher-order concurrent separation logic

authors:
Ralf Jung
Robbert Krebbers
Jacques-Henri Jourdan
Ales Bizjak
Lars Birkedal
Derek Dreyer

abstract: Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.


title: Editorial for the Special Issue on Parallel and Concurrent Functional Programming

authors:
Gabriele Keller
Fritz Henglein

abstract: Functional languages are uniquely suited to providing programmers with a programming model for parallel and concurrent computing. This is reflected in the wide range of work that is currently underway, both on parallel and concurrent functional languages, as well as on bringing functional language features to other programming languages. This has resulted in a rapidly growing number of practical applications. The Journal of Functional Programming decided to dedicate a special issue to this field to showcase the state of the art in how functional languages and functional concepts currently assist programmers with the task of managing the challenges of creating parallel and concurrent systems.


title: Applicative bidirectional programming: Mixing lenses and semantic bidirectionalization

authors:
Kazutaka Matsuda
Meng Wang

abstract: Abstract A bidirectional transformation is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws. One way to reduce the development and maintenance effort of bidirectional transformations is to have specialized languages in which the resulting programs are bidirectional by construction—giving rise to the paradigm of bidirectional programming. In this paper, we develop a framework for applicative-style and higher-order bidirectional programming, in which we can write bidirectional transformations as unidirectional programs in standard functional languages, opening up access to the bundle of language features previously only available to conventional unidirectional languages. Our framework essentially bridges two very different approaches of bidirectional programming, namely the lens framework and Voigtländer's semantic bidirectionalization, creating a new programming style that is able to obtain benefits from both.


title: Infusing an HtDP-based CS1 with distributed programming using functional video games

abstract: Abstract A Computer Science introduction course ought to focus on exciting students about the subject matter and on problem solving through the methodical design of programs. An effective way to achieve both is through the development of functional video games. As most students are interested in video games, their development adds an exciting domain to any introduction to programming. This article advocates that an exciting crowning achievement for students in such a course is the design and implementation of a multiplayer distributed video game. By exploiting a domain that is popular with students, they are taught about design principles, communication protocols, and pitfalls in distributed programming. This article puts forth a successfully used design recipe that places distributed programming well within the reach of beginning students and outlines the use of this design recipe in the classroom. For those teaching beginners, this article presents a model for developing their own distributed programming module. The success of the presented methodology is measured through student feedback on their distributed programming experience. The empirical results suggest that the design and implementation of distributed functional video games is effective and well-received by students. Furthermore, the data suggests that the presented methodology fails to exhibit the gender gap common in Computer Science and is effective regardless of the programming experience CS1 students bring to the classroom.


title: 1ML - Core and modules united

abstract: Abstract ML is two languages in one: there is the core , with types and expressions, and there are modules , with signatures, structures, and functors. Modules form a separate, higher-order functional language on top of the core. There are both practical and technical reasons for this stratification; yet, it creates substantial duplication in syntax and semantics, and it imposes seemingly unnecessary limits on expressiveness because it makes modules second-class citizens of the language. For example, selecting one among several possible modules implementing a given interface cannot be made a dynamic decision. Language extensions allowing modules to be packaged up as first-class values have been proposed and implemented in different variations. However, they remedy expressiveness only to some extent and tend to be even more syntactically heavyweight than using second-class modules alone. We propose a redesign of ML in which modules are truly first-class values, and core and module layers are unified into one language. In this “1ML”, functions, functors, and even type constructors are one and the same construct; likewise, no distinction is needed between structures, records, or tuples. Or viewed the other way round, everything is just (“a mode of use of”) modules. Yet, 1ML does not require dependent types: its type structure is expressible in terms of plain System F ω , with a minor variation of our F-ing modules approach. We introduce both an explicitly typed version of 1ML and an extension with Damas–Milner-style implicit quantification. Type inference for this language is not complete, but, we argue, not substantially worse than for Standard ML.


title: Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong)

authors:
Eric L. Seidel
Ranjit Jhala
Westley Weimer

abstract: Abstract Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed function, we symbolically execute the body to synthesize witness values that make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend this procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate the coverage of our approach on two data sets comprising over 4,500 ill-typed student programs. Our technique is able to generate witnesses for around 85% of the programs, our reduction graph yields small counterexamples for over 80% of the witnesses, and a simple heuristic allows us to use witnesses to locate the source of type errors with around 70% accuracy. Finally, we evaluate whether our witnesses help students understand and fix type errors, and find that students presented with our witnesses show a greater understanding of type errors than those presented with a standard error message.


title: Push versus pull-based loop fusion in query engines

authors:
Amir Shaikhha
Mohammad Dashti
Christoph Koch

abstract: Abstract Database query engines use pull-based or push-based approaches to avoid the materialization of data across query operators. In this paper, we study these two types of query engines in depth and present the limitations and advantages of each engine. Similarly, the programming languages community has developed loop fusion techniques to remove intermediate collections in the context of collection programming. We draw parallels between databases (DB) and programming language (PL) research by demonstrating the connection between pipelined query engines and loop fusion techniques. Based on this connection, we propose a new type of pull-based engine, inspired by a loop fusion technique, which combines the benefits of both approaches. Then, we experimentally evaluate the various engines, in the context of query compilation, for the first time in a fair environment, eliminating the biasing impact of ancillary optimizations that have traditionally only been used with one of the approaches. We show that for realistic analytical workloads, there is no considerable advantage for either form of pipelined query engine, as opposed to what recent research suggests. Also, by using micro-benchmarks, which demonstrate certain edge cases on which one approach or the other performs better, we show that our proposed engine dominates the existing engines by combining the benefits of both.


title: An extended account of contract monitoring strategies as patterns of communication

authors:
Cameron Swords
Amr Sabry
Sam Tobin-Hochstadt

abstract: Abstract Contract systems have come to play a vital role in many aspects of software engineering. This has resulted in a wide variety of approaches to enforcing contracts—ranging from the straightforward pre-condition and post-condition checking of Eiffel to lazy, optional, and parallel enforcement strategies. Each of these approaches has its merits, but each has required ground-up development of an entire contract monitoring system. We present a unified approach to understanding this variety, while also opening the door to as-yet-undiscovered strategies. By observing that contracts are fundamentally about communication between a program and a monitor, we reframe contract checking as communication between concurrent processes. This brings out the underlying relations between widely studied enforcement strategies, including strict and lazy enforcement as well as concurrent approaches, including new contracts and strategies. We show how each of these can be embedded into a core calculus, and demonstrate a proof (via simulation) of correctness for one such encoding. Finally, we show that our approach suggests new monitoring approaches and contracts not previously expressible.


title: Ghostbuster: A tool for simplifying and converting GADTs

authors:
Timothy A. K. Zakian
Trevor L. McDonell
Matteo Cimini
Ryan R. Newton

abstract: Abstract Generalized Algebraic Data Types, or simply GADTs, can encode non-trivial properties in the types of the constructors. Once such properties are encoded in a datatype, however, all code manipulating that datatype must provide proof that it maintains these properties in order to typecheck. In this paper, we take a step toward gradualizing these obligations. We introduce a tool, Ghostbuster, that produces simplified versions of GADTs which elide selected type parameters, thereby weakening the guarantees of the simplified datatype in exchange for reducing the obligations necessary to manipulate it. Like ornaments , these simplified datatypes preserve the recursive structure of the original, but unlike ornaments, we focus on information-preserving bidirectional transformations. Ghostbuster generates type-safe conversion functions between the original and simplified datatypes, which we prove are the identity function when composed. We evaluate a prototype tool for Haskell against thousands of GADTs found on the Hackage package database, generating simpler Haskell'98 datatypes and round-trip conversion functions between the two.


title: On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control

authors:
Yannick Forster
Ohad Kammar
Sam Lindley
Matija Pretnar

abstract: Abstract We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features. We present three calculi, one per abstraction, extending Levy’s call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro expressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.


title: POPLMark reloaded: Mechanizing proofs by logical relations

authors:
Andreas Abel
Guillaume Allais
Aliya Hameer
Brigitte Pientka
Alberto Momigliano
Steven Schäfer
Kathrin Stark

abstract: Abstract We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks.


title: A relational logic for higher-order programs

authors:
Alejandro Aguirre
Gilles Barthe
Marco Gaboardi
Deepak Garg
Pierre-Yves Strub

abstract: Abstract Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for reasoning about a broad range of properties, including equivalence and refinement, and specialized notions such as continuity, information flow security, or relative cost. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures. We present a logic, called relational higher-order logic (RHOL), for proving relational properties of a simply typed λ-calculus with inductive types and recursive definitions. RHOL retains the type-directed flavor of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms. We show that RHOL has strong foundations, by proving an equivalence with higher-order logic, and leverage this equivalence to derive key meta-theoretical properties: subject reduction, admissibility of a transitivity rule, and set-theoretical soundness. Moreover, we define sound embeddings for several existing relational type systems such as relational refinement types and type systems for dependency analysis and relative cost, and we verify examples that were out of reach of prior work.


title: How to find a fake coin

abstract: There are n coins, all identical in appearance, one of which may be fake. The fake coin, if it exists, is either lighter or heavier than the fair coins, but it is not known which, nor by how much. Given is a balance with two pans but no weights. Equal number of coins can be placed on each pan and weighed. There are three possible outcomes: the left-hand pan may be lighter than the right-hand pan, or of equal weight, or heavier. Design a recipe for determining the minimum number of weighings guaranteed to determine the fake coin, if it exists, and whether it is lighter or heavier than the others.


title: A theory of RPC calculi for client-server model

authors:
Kwanghoon Choi
Byeong-Mo Chang

abstract: Abstract With multi-tier programming languages, programmers can specify the locations of code to run in order to reduce development efforts for the web-based client–server model where programmers write client and server programs separately and test the multiple programs together. The RPC calculus, one of the foundations of those languages by Cooper and Wadler, has the feature of symmetric communication in programmer’s writing arbitrarily deep nested client–server interactions. The feature of the calculus is fully implemented by asymmetric communication in trampolined style suitable for the client–server model. However, the existing research only considers a stateless server strategy in which all server states are encoded for transmission to the client so that server states do not need to be stored in the server. It cannot always correctly handle all stateful operations involving disks or databases. To resolve this problem, we first propose new stateful calculi that fully support both symmetric communication from the programmer’s viewpoint and asymmetric communication in its implementation using trampolined style. All the existing calculi either provide only the feature of asymmetric communication or propose only symmetric implementation suitable for the peer-to-peer model, rather than the client–server model. Second, the method used to design our stateful server strategy is based on a new locative type system which paves the way for a theory of RPC calculi for the client–server model. Besides proposing the new stateful calculi, this theory can improve the existing stateless server strategy to construct new state-encoding calculi that eliminate runtime checks on remote procedure calls present in the existing strategy, and it enables us to design a new mixed strategy that combines the benefits of both kinds of strategies. As far as we know, there are no typed multi-tier calculi that offer programmers the feature of symmetric communication with the implementation of asymmetric communication under the three strategies together.


title: Review of "The Haskell School of Music: from Signals to Symphonies, " by Paul Hudak and Donya Quick, Cambridge University Press, 2018

abstract: Computer languages for music have a long and interesting history.Music signal processing in particular inspired some early work on dataflow computers, and functional programming concepts are frequently associated with music because of the importance of event sequences and sample sequences in music representation.This book offers a particular approach to music computation using the Haskell programming language and two libraries written in Haskell: Euterpea for representing musical structures and Haskell School of Music for both music performance and simple graphical interfaces for control.This book is intended to teach computer music concepts along with Haskell.The many programming examples are almost exclusively drawn from music.For example, the first Haskell type expression that appears is PitchClass, the set of music note names.Similarly, functions are introduced for musical transposition, sequences are introduced through simple melodies, and so on.Some of the powerful features of Haskell are polymorphic and higher order functions, allowing music representations and operations on them to be parameterized by the details of music events.Music can be an organization of pitches, of chords, of sound qualities, etc., and abstraction can help to avoid being too rigid and limiting.On the other hand, readers are quickly forced to reckon with these abstractions.I expect beginners will struggle with recursive definitions and parametric types.For seasoned functional programmers, there is certainly some beauty in the terse yet flexible notation offered by Euterpea.One of the attractions of computers for musicians is the ability to describe music as a dynamic process or computation rather than a static score.After introducing Euterpea, this book offers examples of algorithmic composition based on recursion, combinatorics, self-similar sequences, phasing, L-systems, and Markov chains.These are interleaved with more advanced Haskell topics such as type classes, monads, and induction proofs.Most of this book is concerned with symbolic and parametric representations involving discrete notes with symbolic or numerical parameters such as pitch and loudness.Beginning with Chapter 18, this book turns to audio processing and music synthesis, which is also supported by the Euterpea library.Some basic synthesis methods are covered, including additive synthesis, subtractive synthesis, types of modulation, and simple physical models.These sound generation capabilities mean that one can write algorithms to compose music in terms of symbolic "note" events, describe the translation or "performance" of these events into detailed and nuanced control signals, and finally convert the parametric control into audio, all within one programming language framework.This is unusual, as most music programming systems focus on one representation or abstraction


title: Folding left and right over Peano numbers

abstract: For example, consider the standard powerset function that maps the representation of a set as the list of its elements (in any order and without repetition) to the representation of its powerset:Definition powerset (V : Type) (vs : list V)


title: Constructive Galois Connections

authors:
David Darais
David Van Horn

abstract: Abstract Galois connections are a foundational tool for structuring abstraction in semantics, and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of Galois connections using proof assistants remains limited to restricted modes of use, preventing their general application in mechanized metatheory and certified programming. This paper presents constructive Galois connections , a variant of Galois connections that is effective both on paper and in proof assistants; is complete with respect to a large subset of classical Galois connections; and enables more general reasoning principles, including the “calculational” style advocated by Cousot. To design constructive Galois connections, we identify a restricted mode of use of classical ones which is both general and amenable to mechanization in dependently typed functional programming languages. Crucial to our metatheory is the addition of monadic structure to Galois connections to control a “specification effect.” Effectful calculations may reason classically, while pure calculations have extractable computational content. Explicitly moving between the worlds of specification and implementation is enabled by our metatheory. To validate our approach, we provide two case studies in mechanizing existing proofs from the literature: the first uses calculational abstract interpretation to design a static analyzer, and the second forms a semantic basis for gradual typing. Both mechanized proofs closely follow their original paper-and-pencil counterparts, employ reasoning principles not captured by previous mechanization approaches, support the extraction of verified algorithms, and are novel.


title: The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus

authors:
Álvaro García-Pérez
Pablo Nogueira

abstract: Abstract We exploit the idea of proving properties of an abstract machine by using a corresponding semantic artefact better suited to their proof. The abstract machine is an improved version of Pierre Crégut’s full-reducing Krivine machine KN. The original version works with closed terms of the pure lambda calculus with de Bruijn indices. The improved version reduces in similar fashion but works on closures where terms may be open. The corresponding semantic artefact is a structural operational semantics of a calculus of closures whose reduction relation is purposely a reduction strategy. As shown in previous work, improved KN and the structural operational semantics ‘correspond’, i.e. both artefacts realise the same reduction strategy. In this paper, we prove in the calculus of closures that the reduction strategy simulates in lockstep (at every reduction step) the complete and standard normal-order strategy (i.e. leftmost reduction to normal form) of the pure lambda calculus. The simulation is witnessed by a substitution function from closures of the closure calculus to pure terms of the pure lambda calculus. Thus, KN also simulates normal-order in lockstep by the correspondence. This result is stronger than the known proof that KN is complete, for in the pure lambda calculus there are complete but non-standard strategies. The lockstep simulation proof consists of straightforward structural inductions, thanks to three properties of the closure calculus we call ‘index alignment’, ‘parameters-as-levels’ and ‘balanced derivations’. The first two come from KN. Thanks to these properties, a proof in a calculus of closures involving de Bruijn indices and de Bruijn levels is unproblematic. There is no lexical adjustment at binding lookup, on-the-fly alpha-conversion or recursive traversals of the term to deal with bound and free variables as in other calculi. This paper contributes to the framework for environment machines of Biernacka and Danvy a full-reducing open-terms closure calculus, its corresponding abstract machine, and a lockstep simulation proof via a substitution function.