From b4a403ebae956cf569c077cce550f77158f2c31a Mon Sep 17 00:00:00 2001 From: Adrian Sampson Date: Sat, 31 Aug 2024 12:10:21 -0400 Subject: [PATCH] TOC --- OpenTOC/erlang24.html | 2333 ++++++++++++++++++++++++++++++++++++++++ OpenTOC/farm24.html | 891 +++++++++++++++ OpenTOC/fproper24.html | 172 +++ OpenTOC/funarch24.html | 1216 +++++++++++++++++++++ OpenTOC/haskell24.html | 366 +++++++ OpenTOC/tyde24.html | 117 ++ _data/OpenTOC.yaml | 28 + 7 files changed, 5123 insertions(+) create mode 100644 OpenTOC/erlang24.html create mode 100644 OpenTOC/farm24.html create mode 100644 OpenTOC/fproper24.html create mode 100644 OpenTOC/funarch24.html create mode 100644 OpenTOC/haskell24.html create mode 100644 OpenTOC/tyde24.html diff --git a/OpenTOC/erlang24.html b/OpenTOC/erlang24.html new file mode 100644 index 0000000..606776f --- /dev/null +++ b/OpenTOC/erlang24.html @@ -0,0 +1,2333 @@ +Erlang 2024: Proceedings of the 23rd ACM SIGPLAN International Workshop on Erlang

Erlang 2024: Proceedings of the 23rd ACM SIGPLAN International Workshop on Erlang

+ Full Citation in the ACM Digital Library +

SESSION: Keynote

+

Environmentally Sustainable Software and Data Architectures (Keynote)

  • Madeleine Malmsten
+

The rising threat of climate change is leading countries to commit to ambitious carbon-reduction goals. Concurrently, a significant portion of Fortune 500 companies are targeting carbon emission cuts by 2030. + + + + + + + + + + + +As digital integration grows, Technology represents a huge opportunity, yet, the energy footprint of software is often overlooked. Each application transaction, interaction and new data asset adds to the energy demand, making sustainable software and data practices crucial. + + + + + + + + + + + +While improving sustainability in data and software alone won’t solve climate change, with an understanding of technology’s contribution to carbon emissions, a focus on tech’s foundational elements at multiple levels can pave the way for more substantial reductions in the future: (i) Software engineers can reduce the carbon emissions from their software and data by being aware of the effects of their choices. (ii) CTOs can make environmental sustainability a non-functional requirement for all software development. (iii) Companies can incorporate the environmental effects of software as a metric when gauging the quality of a solution. + + + + + + + + + + + +The goal is to cultivate a culture that embeds environmental sustainability into standard software and data engineering practices. Now is the perfect time to start!

+
+ +

SESSION: Papers

+

Same Same but Different: A Comparative Analysis of Static Type Checkers in Erlang

  • Florian Berger
  • Albert Schimpf
  • Annette Bieniusa
  • Stefan Wehr
+

Erlang is a dynamically typed language with support for optional type annotations. Though Erlang’s type annotations were originally intended for documentation, static analysis tools soon utilized them for semantic checks. The most advanced and mature of these tools is Dialyzer, a success typing-based tool widely used in current projects. Attempts to retrofit a static type system employing the type annotations have so far remained in the realm of research prototypes. Recently, three further tools have been developed: Gradualizer, eqWAlizer, and Etylizer. But, due to a need for more semantic agreement on Erlang’s type annotations, their results differ in ways that can be challenging for users to interpret. In this paper, we cross-compare the state-of-the-art static checkers regarding their expressivity and performance on the union of their respective test suites. Unsurprisingly, we find that the tools perform best on their own test suites. While Gradualizer, Etylizer, and eqWAlizer disagree on 25% - 45% of test cases across all test suites, Dialyzer’s success-typing approach sets it apart in its interpretation of the type annotations. Our analysis emphasizes that the nature of Erlang’s type language remains challenging when it comes to develop a correct and efficient static type checker.

+
+ + +

Erla⁺: Translating TLA⁺ Models into Executable Actor-Based Implementations

  • Marian Hristov
  • Annette Bieniusa
+

Distributed systems are notoriously difficult to design and implement correctly. Although formal methods provide rigorous approaches to verifying the adherence of a program to its specification, there still exists a gap between a formal model and implementation if the model and its implementation are only loosely coupled. Developers usually overcome this gap through manual effort, which may result in the introduction of unexpected bugs. In this paper, we present Erla+, a translator which automatically translates models written in a subset of the PlusCal language to TLA+ for formal reasoning and produces executable Erlang programs in one run. Erla+ additionally provides new PlusCal primitives for actor-style modeling, thus clearly separating the modeled system from its environment. We show the expressivity and strengths of Erla+ by applying it to representative use cases such as a Raft-based key-value store. Our evaluation shows that the implementations generated by Erla+ offer competitive performance against manually written and optimized state-of-the-art libraries.

+
+ + +

Nominal Types for Erlang

  • Isabell Huang
  • John Högberg
  • Kiko Fernandez-Reyes
  • Tobias Wrigstad
+

Erlang is a functional programming language with structural type-checking. Opaque types are the only types with a nominal component, where their names are used for type-checking. Using opaque types for nominal typing is possible, but it limits the use of pattern-matching and deconstruction to the module where it is defined. To distinguish types by names without imposing extra constraints, we introduce the new concept of nominal types for Erlang, together with a well-tested type-checking implementation in Dialyzer. We define a new syntax for declaring nominal types and a set of rules that specify how nominal types should be type-checked with respect to other nominal types and non-nominal types, which is designed to ensure backwards compatibility. Nominal type-checking is implemented on top of Dialyzer's structural type-checking logic. Through testing in the Erlang/OTP codebase, we show that nominal types can encode Erlang's opaque types, thereby improving Dialyzer's performance and maintainability.

+
+ + +

Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors

  • Jonah Pears
  • Laura Bocchi
  • Raymond Hu
+

In this work, we consider the formal framework TOAST for timed asynchronous interactions featuring mixed-choice states. + + + + + + + +TOAST extends the theory of timed asynchronous session types to support modelling of communication protocols featuring timeouts, which despite being commonplace in practice were previously out of reach for session type theory. + + + + + + + +We present ongoing work towards a practical toolchain that + + + + + + + +(a) automates the generation of correct-by-construction program stubs with timeouts in Erlang from TOAST processes that implement a TOAST protocol, + + + + + + + +and (b) provides an inline monitoring framework for TOAST protocols integrated with Erlang supervisors. + + + + + + + +Our toolchain generates Erlang code with a close correspondence to the source TOAST model by building on a formal correspondence between session types and Communicating Finite State Machines. + + + + + + + +The monitoring framework can be configured to perform either runtime verification or enforcement with respect to the source protocol, ensuring communication safety.

+
+ + +

Modeling Erlang Compiler IR as SMT Formulas

  • John Högberg
+

Erlang is an unorthodox language that has fault-tolerance and observability (tracing) baked into the language. This allows users to debug production systems without the maintenance overhead of adding these features manually, but comes at the cost of adding a side effect to almost every operation. + + + + + + + +Because the design choices around tracing err on the side of maximum observability, the compiler does not have much freedom to perform common optimizations, and requires sophisticated analysis to safely apply all but the simplest transformations. Each individual optimization also implements its own bespoke analysis, which is error-prone and difficult to maintain. + + + + + + + +This report describes an ongoing experiment on translating one of the compiler's intermediate representations (IR) to formulas, enabling the use of a satisfiability modulo theories (SMT) solver to drive analysis as well as prove the semantics-preserving nature of optimizations.

+
+ + +

Is This Really a Refactoring? Automated Equivalence Checking for Erlang Projects

  • Bendegúz Seres
  • Dániel Horpácsi
  • Simon Thompson
+

We present an automated approach to checking whether a change to a repository is a refactoring, that is, it makes no change to the behaviour of the system. This is implemented in the EquivcheckEr tool, which detects the places in which the code has changed, and compares the old and new versions of all functions that are affected by the change, applying the functions to randomly generated inputs. + + + +Our tool works for projects written in Erlang, and so needs to deal with effectful as well as pure functions. We aim only to report inequivalence when we have concrete evidence to that effect, avoiding any ``false positive'' counterexamples.

+
+ + +

Controlled Scheduling of Concurrent Elixir Programs

  • Luis Eduardo Bueso de Barrio
  • Lars-Åke Fredlund
  • Clara Benac Earle
  • Ángel Herranz
  • Julio Mariño
+

We describe the design and implementation of Scheduler, a new + +library for Elixir which provides + +a user-level scheduler. The goal is to improve the control over scheduling decisions, + +i.e., which process runs at which time, in order to obtain executions that are more random, + +but which are also repeatable and modifiable, + +and which moreover provide a detailed explanation of the scheduling decisions + +taken. This work is inspired by the Pulse user-level scheduler for Erlang programs, + +as well as other related tools. + +Our library is agnostic regarding what other testing/execution/formal + +verification tool uses the scheduler, and instruments + +Elixir code running under the scheduler through + +use of the Elixir macro facility. Moreover, the library + +provides a number of algorithms + +to explore the state space + +of the concurrent programs under study, including + +random search, depth-first search (potentially capable of exploring + +the whole state space of the program-under-study), and a novel + +search algorithm which selects schedules randomly. + + + +As an example the Scheduler library is applied to the task of checking + +whether a number of snapshot algorithms are correct.

+
+ + +

Unsafe Impedance: Safe Languages and Safe by Design Software

  • Lee Barney
  • Adolfo Neto
+

In December 2023, security agencies from five countries in North America, Europe, and the south Pacific produced a document encouraging senior executives in all software pro- ducing organizations to take responsibility for and oversight of the security of the software their organizations produce. In February 2024, the White House released a cybersecurity outline, highlighting the December document. In this work we review the safe languages listed in these documents, and compare the safety of those languages with Erlang and Elixir, two BEAM languages. + + + +These security agencies’ declaration of some languages as safe is necessary but insufficient to make wise decisions regarding what language to use when creating code. We propose an additional way of looking at languages and the ease with which unsafe code can be written and used. We call this new perspective unsafe impedance. We then go on to use unsafe impedance to examine nine languages that are considered to be safe. Finally, we suggest that business processes include what we refer to as an Unsafe Acceptance Process. This Unsafe Acceptance Process can be used as part of the memory safe roadmaps suggested by these agencies. Unsafe Acceptance Processes can aid organizations in their production of safe by design software.

+
+ + +

The Benefits of Tierless Elixir/Potato for Engineering IoT Systems

  • Solaris Li
  • Phil Trinder
  • Christophe De Troyer
  • Mart Lubbers
  • Adrian Ramsingh
+

IoT systems are increasingly pervasive, and developing, maintaining and ensuring the reliability of the software is challenging. IoT software is conventionally structured in multiple distributed tiers, where tiers use different programming languages and components that must interoperate. One way to minimise this complexity is to use a single tierless language to specify the entire IoT system. Tierless IoT languages require extremely sophisticated implementations, and are new and rare. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +A previous study compared two Clean-based tierless implementations of a smart campus IoT system (CRS and CWS) with two conventional tiered Python implementations (PRS and PWS). It showed that tierless languages dramatically reduce development effort. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +This paper describes a new implementation of the smart campus system in the Elixir/Potato tierless language (ERS), and compares ERS with the other implementations to show the following. (1) We provide further evidence that using a tierless IoT language reduces development effort. (2) We provide the first ever comparative study of two fundamentally different tierless IoT languages, i.e. we compare Elixir/Potato with Clean/iTask(mTask) using the ERS and CRS/CWS case studies. (3) We provide the first ever analysis of the software engineering costs of providing failure management in a tierless IoT language.

+
+ + +

Elixir-Powered Low-Income Animal Shelter Support: An Experience Report from Conception to Production

  • Carla Rodríguez Estévez
  • Laura M. Castro
+

Animal shelters are non-governmental organizations that have to face many difficulties in their management and carry out actions to help unprotected animals in the area. Apart from being small organizations and generally having limited resources, many of them also struggle with outdated tools or face challenges in centralizing their information and pro- cesses. However, the main problem faced by them is related to their economic situation and most of the time they need to use free online tools for their management. This work presents and explains a Phoenix web application solution to assist in the management of these groups, which leverages affordable development and easy maintenance with tailoring to meet their main needs. With this experience report, we aim to demonstrate that BEAM technologies, which have already proven their effectiveness in bigger corporate set- tings, such as WhatsApp or Discord, are also well-suited for smaller and more modest environments. Moreover, this aims to be an example of the use of Elixir/Phoenix in a non-profit environment, typical for social and community projects, with needs specific to the world in which they exist.

+
+ +
\ No newline at end of file diff --git a/OpenTOC/farm24.html b/OpenTOC/farm24.html new file mode 100644 index 0000000..0a272d5 --- /dev/null +++ b/OpenTOC/farm24.html @@ -0,0 +1,891 @@ +FARM 2024: Proceedings of the 12th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design

FARM 2024: Proceedings of the 12th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design

+ Full Citation in the ACM Digital Library +

SESSION: Keynote

+

Refactoring Musical Thought (Keynote)

  • Dmitri Tymoczko
+

My talk will introduce some twenty-first century music-theoretical ideas that I have found helpful musically, beginning with scales and macroharmony, proceeding through voice-leading geometry, and concluding with the idea of the “quadruple hierarchy”, a recursive nesting of collections supporting the same basic operations at each level. I will introduce Arca, a new musical programming language, and will make the case that musicians have made intelligent but tacit use of nonobvious mathematics. The core ideas will be illustrated with live improvisations that use the internet to transmit notation in real time, allowing for both spontaneity and coordination.

+
+ +

SESSION: SESSION 1

+

Using Functional Reactive Programming for Robotic Art: An Experience Report

  • Eliane Irène Schmidli
  • Farhad Mehta
+

The control software for robotics applications is usually written in a low-level imperative style, intertwining the program sequence and commands for motors and sensors. + + + + + + + + + + + + + + + +To describe the program's behavior, it is typically divided into different states, each representing a specific system condition. + + + + + + + + + + + + + + + +This way of programming complicates the comprehension of the code, making changes to the program flow a tedious task. + + + + + + + + + + + + + + + +Functional Reactive Programming (FRP) offers a composable, modular approach for developing reactive applications. + + + + + + + + + + + + + + + +To examine the strengths and limitations of FRP compared to the conventional imperative style, the control software for a robotic artwork was implemented using a form of FRP in the Haskell programming language. + + + + + + + + + + + + + + + +The resulting design separates the control of the hardware from the implementation of its behavior. + + + + + + + + + + + + + + + +In addition, state transitions are presented more clearly, resulting in code that is more understandable, especially for people with little programming experience.

+
+ + +

Demo: The Fun of Robotic Artwork

  • Eliane Irène Schmidli
  • Farhad Mehta
+

Developing software for robot control often is tedious, difficult and error prone. This is more so for people without a computer science background, such as artists. Functional Reactive Programming (FRP) aims to make reactive programs, such as those used for robotics control, more modular, composable, and aesthetically pleasing. We present the results of a collaboration with the art studio Pors & Rao, specializing in robotic artwork. The aim of this collaboration was to explore the use of FRP in this application area to allow artists to express their intentions for robot control in a more effective manner. We demonstrate the artworks that we jointly worked on, as well as our impressions of the acceptance and potential of FRP for artists without a computer science background.

+
+ + +

Bridging Art and Mathematics with Tessella: A Scala Functional Library for Regular Polygon Finite Tessellations of a Plane

  • Mario Càllisto
+

Tessellations of a plane surface by means of unit-sided regular polygons is a classical subject both in art, with examples dating back to the earliest human civilisations, and mathematics, where the complex patterns generated by a very simple set of rules have fascinated generations of inquisitive souls. + + + + + + + + While several taxonomies of the repeating patterns of a tessellation exist, the mathematical treatment of a particular finite tessellation is a quite recent field, greatly aided by computer algorithms. + + + + + + + + Introducing Tessella, a free software library of functional algorithms, written in Scala, where finite tessellations are described as immutable undirected planar graphs; thus providing the capabilities to experiment with manual and programmatic creation of finite tessellations, able in turn of inspiring new artistic insights. Abstract paintings are shown as an example, together with ideas on how this exploration journey might be taken further.

+
+ + +

Functional Curves and Surfaces: Algebraic Geometry Inspired Visuals in Hydra

  • Yoni Maltsman
+

We present FCS (Functional Curves and Surfaces), a framework for synthesizing visual patterns by composing functions for curves and surfaces, implemented as an extension to Hydra, a popular tool for live coding visuals. The extension consists of functions for dozens of implicit and parametric curves and surfaces, which can be chained together in numerous ways to create striking visuals. FCS can also serve as a tool for students and practitioners of math, art, and computer science to learn algebraic geometry in a fun, creative way.

+
+ +

SESSION: SESSION 2

+

Trane: Musical Janet on the Web

  • George Ash
+

Trane is a domain specific language and environment for livecoding music on the web. It gives the programmer control over instruments, effects, their connectivity, and the ability to sequence well-timed events. In this paper we explore the motivation behind the language, its design, and implementation.

+
+ + +

From Konnakol to Live Coding

  • Alex McLean
+

Konnakol is a South Indian, Carnatic musical practice involving the vocal recitation of algorithmic, geometric rhythmic patterns of non-lexical syllables. I reflect on the experience of learning konnakol rhythms, and of adapting the TidalCycles and Strudel live coding environments to better represent Konnakol-inspired rhythms, based on the concept of the metrical tactus. I share visualisations of examples, and the development of a hybrid practice that integrates vocal patterns with live coding. I conclude by considering the issue of cultural appropriation around this work.

+
+ + +

Demo: Composable Compositions with Tonart

  • Jared Gentner
+

This demo introduces Tonart, a language and metalanguage for practical music + + + + + + + +composition. The object language of Tonart is abstract syntax modeling a + + + + + + + +traditional musical score. It is extensible- composers choose or invent + + + + + + + +syntaxes which will most effectively express the music they intend to write. + + + + + + + +Composition proceeds by embedding terms of the chosen syntaxes into a coordinate + + + + + + + +system that corresponds to the structure of a physical score. Tonart can easily + + + + + + + +be written by hand, as existing scores are a concrete syntax for Tonart. The + + + + + + + +metalanguage of Tonart provides a means of compiling Tonart scores via sequences + + + + + + + +of rewrites. Tonart's rewrites leverage context-sensitivity and locality, + + + + + + + +modeling how notations interact on traditional scores. Using metaprogramming, a + + + + + + + +composer can compile a Tonart score with unfamiliar syntax into any number of + + + + + + + +performable scores. + + + + + + + + + + + + + + + +In this demo, we will make a small composition using Tonart. We will construct + + + + + + + +this composition by manipulating notations representing abstract music objects. + + + + + + + +These will eventually be compiled into a digital score representation, as well as a + + + + + + + +computer performance. We will add in an especially abstract object at the end, + + + + + + + +and use our creativity to compile it into something performable.

+
+ + +

The Maquette Monad

  • Carlos Agon
  • Karim Haddad
  • Gonzalo Romero-Garcia
+

This article defines the semantics of maquettes in the visual programming language OpenMusic (OM) using monads. A maquette can be seen as a sequencer of functions. Although maquettes have been widely used, their semantic have never been formalized. Formalizing maquettes has multiple benefits; primarily, we aim to provide a better understanding for composers through the use of a mathematical language rather than discursive semantics. In this work, we use a particular case of the state monad and show with examples how this monad is visualized in OpenMusic. The use of these advanced concepts in the field of music and their availability to composers aligns with our intention to bridge the gap between the theoretical and practical aspects of the intersection between mathematics and music.

+
+ +

SESSION: SESSION 3

+

Demo: A Geometric Approach to Generate Musical Rhythmic Patterns in Haskell

  • Xavier Góngora
+

We present work-in-progress on RTG, a domain specific language embedded in Haskell designed to explore the affordances of geometry as a means to generate and manipulate rhythmic patterns in live coded music. Examples of how simple geometry is capable of producing interesting rhythms are shown to support our use of binary lists as a pattern representation. We introduce Erlangen’s Program notion of geometry as encoded in groups, using such structure as the focus of a combinator interface based on an archetypal RhythmicPattern type implemented using a type class. Examples of the interface usage are provided. Future work targets the definition of Group instances for the rhythmic pattern types such that the group laws are fulfilled and its operations lift to the interface in a musically coherent and engaging way.

+
+ + +

Diffusion-Based Sound Synthesis in Music Production

  • Pierre-Louis Wolfgang Léon Suckrow
  • Christoph Johannes Weber
  • Sylvia Rothe
+

In this paper, we explore the usability of generative artificial intelligence in music production through the development of a digital instrument that incorporates diffusion-based sound synthesis in its sound generation. Current text-to-audio models offer a novel method of defining sounds, which we aim to render utilizable in a music-production environment. Selected pretrained latent diffusion models, enable the synthesis of playable sounds through textual descriptions, which we incorporated into a digital instrument that integrates with standard music production tools. The resultant user interface not only allows generating but also modifying the sounds by editing model and instrument-specific parameters. We evaluated the applicability of current diffusion models with their parameters as well as the fitness of possible prompts for music production scenarios. Adapting published diffusion model pipelines for integration into the instrument, we facilitate experimentation and exploration of this innovative sound synthesis method. Our findings show that despite facing some limitations in the models' responsiveness to specific music production contexts and the instrument's functionality, the tool allows the development of novel and intriguing soundscapes. The instrument and code is published under https://github.com/suckrowPierre/WaveGenSynth

+
+ + +

A Progressive-Adaptive Music Generator (PAMG): An Approach to Interactive Procedural Music for Videogames

  • Alvaro Eduardo Lopez Duarte
+

Procedural music generation in video game is rarely used in + + + + + + + + + + + + + + + +development despite its potential support for interactive narratives, + + + + + + + + + + + + + + + +and falls behind broadly-used procedural methods + + + + + + + + + + + + + + + +like graphic management. Currently, developers rely on preproduced + + + + + + + + + + + + + + + +audio sequences, focusing on sound quality while + + + + + + + + + + + + + + + +balancing storage and variety. Techniques like layering and + + + + + + + + + + + + + + + +re-sequencing are standard through sound design platforms + + + + + + + + + + + + + + + +like FMOD and Wwise, allowing adaptation and interactivity + + + + + + + + + + + + + + + +in gameplay. However, this can lead to repetitive audio, + + + + + + + + + + + + + + + +which becomes particularly noticeable in extended gaming + + + + + + + + + + + + + + + +sessions, diminishing the impact of musical storytelling. + + + + + + + + + + + + + + + +This study introduces the ProgressiveAdaptive Music Generator + + + + + + + + + + + + + + + +(PAMG), an algorithmic system that generates continuous + + + + + + + + + + + + + + + +music streams based on gameplay variables, seamlessly + + + + + + + + + + + + + + + +transitioning between moods, styles, and tension levels. It + + + + + + + + + + + + + + + +includes motivation, theoretical framework in the field of + + + + + + + + + + + + + + + +generative music, overview of the system structure, and a + + + + + + + + + + + + + + + +preliminary implementation test involving a Trial Game that + + + + + + + + + + + + + + + +compares conventional implementation with PAMG. In the + + + + + + + + + + + + + + + +discussion section, it addresses test results and issues, and future + + + + + + + + + + + + + + + +work. The study reveals a preference for PAMG’s music + + + + + + + + + + + + + + + +over traditional methods in certain aspects, although results + + + + + + + + + + + + + + + +are not conclusive.

+
+ + +

Demo: Progressive-Adaptive Music Generator (PAMG) and the Trial Game

  • Alvaro Eduardo Lopez Duarte
+

The present Demo is submitted as a companion of the paper + + + + + + + +"A Progressive-Adaptive Music Generator: an Approach to + + + + + + + +Interactive Procedural music for Videogames". PAMG is a + + + + + + + +software able to generate music in real time adapting and + + + + + + + +progressing to game variables. The experience demonstrates + + + + + + + +PAMG through a gameplay session of the Trial Game, a + + + + + + + +first-person shooter (FPS) specifically designed to illustrate + + + + + + + +PAMG capabilities. It starts by a brief presentation of the + + + + + + + +model, its motivation, architecture, and interface. Then, a description of the Trial Game and the preliminary evaluation + + + + + + + +test with the main discussion points that stem from its + + + + + + + +results. After the introduction (5-7 minutes), a person from + + + + + + + +the audience will be invited to play in a table in front of a + + + + + + + +big screen using a conventional computer keyboard and a + + + + + + + +mouse. The audience will be able to see the gameplay, listen + + + + + + + +to the progressive-adaptive music, and compare the result + + + + + + + +with the clip-based implementation (CBI) that was used for + + + + + + + +the test. In an additional monitor screen, the PAMG’s development + + + + + + + +interface will display the parameters and activity in + + + + + + + +real time.

+
+ +
\ No newline at end of file diff --git a/OpenTOC/fproper24.html b/OpenTOC/fproper24.html new file mode 100644 index 0000000..9983a15 --- /dev/null +++ b/OpenTOC/fproper24.html @@ -0,0 +1,172 @@ +FProPer 2024: Proceedings of the 1st ACM SIGPLAN International Workshop on Functional Programming for Productivity and Performance

FProPer 2024: Proceedings of the 1st ACM SIGPLAN International Workshop on Functional Programming for Productivity and Performance

+ Full Citation in the ACM Digital Library +

SESSION: Papers

+

A Comparison of OpenCL, CUDA, and HIP as Compilation Targets for a Functional Array Language

  • Troels Henriksen
+

This paper compares OpenCL, CUDA, and HIP as compilation targets for + + + + + + + +Futhark, a functional array language. We compare the performance of + + + + + + + +OpenCL versus CUDA, and OpenCL versus HIP, on the code generated by + + + + + + + +the Futhark compiler on a collection of 48 application benchmarks on + + + + + + + +two different GPUs. Despite the generated code in most cases being + + + + + + + +equivalent, we observe significant performance differences on the + + + + + + + +same hardware, ranging from 0.42x to 1.72x in the most extreme + + + + + + + +cases. We identify the root causes of most of these differences, + + + + + + + +many of which are due to relatively superficial details such as + + + + + + + +inconsistent defaults regarding compiler optimisation and numerical + + + + + + + +accuracy, although a few remain mysterious.

+
+ + +

Fusing Gathers with Integer Linear Programming

  • David van Balen
  • Gabriele Keller
  • Ivo Gabe de Wolff
  • Trevor L. McDonell
+

We present an Integer Linear Programming based approach to finding the optimal fusion strategy for combinator-based parallel programs. While combinator-based languages or libraries provide a convenient interface for programming parallel hardware, fusing combinators to more complex operations is essential to achieve the desired performance. Our approach is not only suitable for languages with the usual map, fold, scan, indexing and scatter operations, but also gather operations, which access arrays in arbitrary order, and therefore goes beyond the traditional producer-consumer fusion. It can be parametrised with appropriate cost functions, and is fast enough to be suitable for just-in-time compilation.

+
+ +
\ No newline at end of file diff --git a/OpenTOC/funarch24.html b/OpenTOC/funarch24.html new file mode 100644 index 0000000..c7b6b40 --- /dev/null +++ b/OpenTOC/funarch24.html @@ -0,0 +1,1216 @@ +FUNARCH 2024: Proceedings of the 2nd ACM SIGPLAN International Workshop on Functional Software Architecture

FUNARCH 2024: Proceedings of the 2nd ACM SIGPLAN International Workshop on Functional Software Architecture

+ Full Citation in the ACM Digital Library +

SESSION: Functional Architecture in Practice

+

Architecting Functional Programs (Keynote)

  • Marco Sampellegrini
+

Functional programming in the small works great. Things start to get shaky when there are many services and teams involved, something that is becoming more and more common with large distributed systems.

+
+ + +

F3: A Compiler for Feature Engineering

  • Weixi Ma
  • Siyu Wang
  • Arnaud Venet
  • Junhua Gu
  • Subbu Subramanian
  • Rocky Liu
  • Yafei Yang
  • Daniel P. Friedman
+

In machine learning (ML), feature engineering is a crucial step that converts raw data to model inputs. This process traditionally relies on data processing languages (typically SQL), but now faces new challenges due to advancements in ML. We present the design of F3, a domain-specific language (DSL) and compiler developed at Meta. F3 leverages approaches developed in functional programming and type theory to support the ML engineers of a platform that serves billions of users

+
+ +

SESSION: Formal Methods

+

Design and Implementation of a Verified Interpreter for Additive Manufacturing Programs (Experience Report)

  • Matthew Sottile
  • Mohit Tekriwal
+

This paper describes the design of a verified tool for analyzing tool paths defined in the RS-274 language for 3D printing systems. We describe how the analyzer was designed to allow a mixture of verification and code-extraction techniques to be combined for constructing a correct toolpath analyzer written in the OCaml language. We show how we moved from a fully hand-written OCaml program to one incorporating verified components, highlighting architectural decisions that were made to facilitate this process. Finally, we share a set of architectural lessons that are generally applicable to other software with a similar goal of integration of verified components.

+
+ + +

Applying Continuous Formal Methods to Cardano (Experience Report)

  • James Chapman
  • Arnaud Bailly
  • Polina Vinogradova
+

Cardano is a Proof-of-Stake cryptocurrency with a market + + + + + + + + + + + + + + + +capitalisation in the tens of billions of USD and a daily volume of + + + + + + + + + + + + + + + +hundreds of millions of USD. In this paper we reflect on applying + + + + + + + + + + + + + + + +formal methods, functional architecture and Haskell to building + + + + + + + + + + + + + + + +Cardano. We describe our strategy, projects, lessons + + + + + + + + + + + + + + + +learned, the challenges we face, and how we propose to meet them.

+
+ +

SESSION: From Programming to Architecture

+

Continuations: What Have They Ever Done for Us? (Experience Report)

  • Marc Kaufmann
  • Bogdan Popa
+

Surveys and experiments in economics involve stateful interactions: participants receive different messages based on earlier answers, choices, and performance, or trade across many rounds with other participants. In the design of Congame, a platform for running such economic studies, we decided to use delimited continuations to manage the common flow of participants through a study. Here we report on the positives of this approach, as well as some challenges of using continuations, such as persisting data across requests, working with dynamic variables, avoiding memory leaks, and the difficulty of debugging continuations.

+
+ + +

Bidirectional Data Transformations

  • Marcus Crestani
  • Markus Schlegel
  • Marco Schneider
+

Structured data is the foundation of software. Different + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + components of a system may need the same information but may have + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + different demands on its structure for reasons of performance, + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + resource efficiency, technical constraints, convenience, and so + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + on. For instance, transmitting data over a network requires a format + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + that is suitable for serialization, while persisting data requires a + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + format that is more suitable for storage. Thus, programmers need to + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + translate data between several data structures and formats all the + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + time. Authoring these translations manually is a lot of work because + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + programmers need to implement the logic twice, once for each + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + direction. This is redundant, tedious, and error-prone, and a case + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + of low coherence. We show how using bidirectional data + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + transformations that use functional optics like lenses and + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + projections simplify the conversions. These ideas and techniques + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + make converting data simple and straightforward and foster + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + understanding of the relationship between data structures by + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + explicitly describing their connections in a composable manner.

+
+ +
\ No newline at end of file diff --git a/OpenTOC/haskell24.html b/OpenTOC/haskell24.html new file mode 100644 index 0000000..4f38a08 --- /dev/null +++ b/OpenTOC/haskell24.html @@ -0,0 +1,366 @@ +Haskell 2024: Proceedings of the 17th ACM SIGPLAN International Haskell Symposium

Haskell 2024: Proceedings of the 17th ACM SIGPLAN International Haskell Symposium

+ Full Citation in the ACM Digital Library +

SESSION: Papers

+

Haskelite: A Tracing Interpreter Based on a Pattern-Matching Calculus

  • Pedro Vasconcelos
  • Rodrigo Marques
+

Many Haskell textbooks explain the evaluation of pure functional + + + + + + + + + + + + + + + + programs as a process of stepwise rewriting using equations. + + + + + + + + + + + + + + + + However, usual implementation techniques perform program + + + + + + + + + + + + + + + + transformations that make producing the corresponding tracing + + + + + + + + + + + + + + + + evaluations difficult. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + This paper presents a tracing interpreter for a subset of Haskell + + + + + + + + + + + + + + + + based on the pattern matching calculus of Kahl. We start from a + + + + + + + + + + + + + + + + big-step semantics in the style of Launchbury and develop a + + + + + + + + + + + + + + + + small-step semantics in the style of Sestoft's machines. This + + + + + + + + + + + + + + + + machine is used in the implementation of a step-by-step educational + + + + + + + + + + + + + + + + interpreter. We also discuss some implementation decisions and + + + + + + + + + + + + + + + + present illustrative examples.

+
+ + +

Higher Order Patterns for Rewrite Rules

  • Jaro Reinders
+

GHC’s rewrite rules enable programmers to write local program transformation rules for their own functions. The most notable use case are fusion optimizations, which merge multiple traversals of a data structure into one and avoids allocation of intermediate structures. However, GHC’s rewrite rules were too limited to express a rewrite rule that is necessary for proper fusion of the concatMap function in a variant of fusion called stream fusion. We introduce higher order patterns as a simple extension of GHC’s rewrite rules. Higher order patterns substantially broaden the expressiveness of rewrite rules that involve local variables. In particular, they enable the rewriting of concatMap such that it can be properly optimized. We implement a stream fusion framework to replace the existing fusion framework in GHC and evaluate it on GHC’s benchmark suite. Our stream fusion framework with higher order patterns shows an average speedup of 7% compared to our stream fusion framework without it. However, our stream fusion framework is not yet able to match the performance of GHC’s existing fusion framework. Additionally, we show that our higher order patterns can be used to simplify GHC’s existing mechanism for rolling back failed attempts at fusion and, at the same time, solve a problem that prevented proper optimization in one example program. However, evaluating it on GHC’s benchmark suite shows a small regression in performance overall.

+
+ + +

Welcome to the Parti(tioning) (Functional Pearl): Using Rewrite Rules and Specialisation to Partition Haskell Programs

  • Robert Krook
  • Samuel Hammersberg
+

Writing distributed applications is hard, as the programmer needs to describe the communication protocol between the different endpoints. If this is not done correctly, we can introduce bugs such as deadlocks and data races. Tierless and choreographic programming models aim to make this easier by describing the interactions of every endpoint in a single compilation unit. When such a program is compiled, ideally, a single endpoint is projected and the code for the other endpoints is removed. This leads to smaller binaries with fewer dependencies, and is called program partitioning. In this pearl, we show how we can use rewrite rules and specialisation to get GHC to partition our Haskell programs (almost) for free, if they are written using the Haste App or HasChor framework. As an example of why partitioning is useful, we show how an example application can be more easily built and deployed after being partitioned.

+
+ + +

Cloaca: A Concurrent Hardware Garbage Collector for Non-strict Functional Languages

  • Craig Ramsay
  • Robert Stewart
+

Most functional language runtime systems context switch between executing user + +code and a non-concurrent garbage collector (GC), exposing GC latency to overall + +wall-clock time. Recent concurrent software-based GCs reduce these latencies, + +but wall-clock times are instead increased due to their synchronisation and + +write barrier overheads, by as much as 21%. This GC overhead is exacerbated + +further for pure non-strict languages like Haskell, due to the abundance of + +allocations for storing immutable data structures and closures. This paper + +presents Cloaca, an FPGA-based hardware implementation of a concurrent, hybrid + +GC for a pure non-strict functional language. It combines mark-and-sweep tracing + +and one-bit reference counting. It traces live heap data using hardware-level + +synchronisation and write barriers, without damaging graph reduction + +performance. To ensure the correctness of Cloaca, three invariants of its + +Haskell-based implementation are verified with property-based testing. Despite + +GHC running on an Intel i7 CPU operating at a x25 higher clock + +frequency than Cloaca; Cloaca takes, on average, 4.1% of GHC's GC wall-clock + +time across 14 of 15 benchmarks.

+
+ + +

Functional Reactive Programming, Rearranged

  • Finnbar Keating
  • Michael B. Gale
+

At present, the most efficient implementations of Arrowized Functional Reactive Programming (AFRP), such as Scalable FRP (SFRP), do not support the loop combinator. This prevents us from expressing fundamental programs in such implementations, which limits AFRP’s use in domains where both performance and expressivity are required. We introduce Oxbow, which extends SFRP with support for the loop combinator by leveraging an improved variant of the rearrange technique. In benchmarks, Oxbow performs at least 2.2x better than Yampa, an AFRP implementation that supports the loop combinator.

+
+ + +

Making a Curry Interpreter using Effects and Handlers

  • Niels Bunkenburg
  • Nicolas Wu
+

Despite the intended use for prototyping or as a first step towards giving semantics to a new programming language, interpreters are often monolithic and difficult to extend. Higher-order effects and handlers promise modular composition of handlers and semantics; in practice, however, they have been mostly applied to toy examples. We present an approach that successfully combines algebraic, scoped, and latent effects into a handler pipeline for interpreting the functional logic programming language Curry. We show which effects make up Curry, discuss the infrastructure needed to combine effects of different classes and shed light on how these effects interact in order to lessen the barrier to entry for using effects in practical projects.

+
+ + +

Controlling Computation Granularity through Fusion in Improving Floating-Point Numbers

  • Momoka Saito
  • Hideya Iwasaki
  • Hideyuki Kawabata
  • Tsuneyasu Komiya
+

Improving Floating-Point Numbers (IFN) is a numerical computation library for Haskell. It allows the user to directly specify the accuracy of the result, making accurate computation easy. The library's computation process is based on adaptive control of accuracies, which propagates the demands for more accurate values from an expression to its appropriate subexpressions. However, despite its unique features, programs utilizing the IFN library often encounter efficiency issues regarding memory consumption and execution time due to its fine granularity of computations. This paper presents the computational granularity control mechanism through fusion transformation to resolve these problems and proposes two fusion strategies, the maximal fusion and chain fusion. We have successfully implemented a fusion system that automatically applies these strategies through program transformation. Its effectiveness was confirmed through numerical computation programs.

+
+ + +

Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl)

  • Jan van Brügge
+

Formal reasoning about the time complexity of algorithms and data structures is usually done in interactive theorem provers like Isabelle/HOL. This includes reasoning about amortized time complexity which looks at the worst case performance over a series of operations. However, most programs are not written within a theorem prover and thus use the data structures of the production language. To verify the correctness it is necessary to translate the data structures from the production language into the language of the prover. Such a translation step could introduce errors, for example due to a mismatch in features between the two languages. We show how to prove amortized complexity of data structures directly in Haskell using LiquidHaskell. Besides skipping the translation step, our approach can also provide a didactic advantage. Learners do not have to learn an additional language for proofs and can focus on the new concepts only. For this paper, we do not assume prior knowledge of amortized complexity as we explain the concepts and apply them in our first case study, a simple stack with multipop. Moving to more complicated (and useful) data structures, we show that the same technique works for binomial heaps which can be used to implement a priority queue. We also prove amortized complexity bounds for Claessen’s version of the finger tree, a sequence-like data structure with constant-time cons/uncons on either end. Finally we discuss the current limitations of LiquidHaskell that made certain versions of the data structures not feasible.

+
+ + +

Calculating Compilers Effectively (Functional Pearl)

  • Zac Garby
  • Graham Hutton
  • Patrick Bahr
+

Much work in the area of compiler calculation has focused on pure languages. + +While this simplifies the reasoning, it reduces the applicability. In this + +article, we show how an existing compiler calculation methodology can be + +naturally extended to languages with side effects. We achieve this by + +exploiting an algebraic approach to effects, which keeps the reasoning simple + +and provides flexibility in how effects are interpreted. To make the ideas + +accessible we only use elementary functional programming techniques.

+
+ +

SESSION: Talk Proposal

+

MicroHs: A Small Compiler for Haskell

  • Lennart Augustsson
+

MicroHs is a compiler for Haskell2010. It translates Haskell to SKI style combinators via λ-calculus. The runtime system is quite small with few dependencies.

+
+ +
\ No newline at end of file diff --git a/OpenTOC/tyde24.html b/OpenTOC/tyde24.html new file mode 100644 index 0000000..7917b23 --- /dev/null +++ b/OpenTOC/tyde24.html @@ -0,0 +1,117 @@ +TyDe 2024: Proceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development

TyDe 2024: Proceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development

+ Full Citation in the ACM Digital Library +

SESSION: Keynote

+

Types for Correctness, Convenience, and Performance (Keynote)

  • Gabriele Keller
+

Haskell offers a multitude of sophisticated type system extensions, from generics and generalised algebraic data types over type families to pattern synonyms. In the implementation of the embedded parallel language Accelerate, we make good use of these extensions, although they are often hidden from the user’s view. In this talk, I will illustrate how we exploit these features to improve the reliability of the compiler, provide stronger static checks for the user which eliminates many runtime errors. I also show how this approach improves the usability of the language and allows us to generate more efficient code.

+
+ +

SESSION: Papers

+

Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma

  • Hannes Saffrich
  • Peter Thiemann
  • Marius Weidner
+

Intrinsically typed syntax is an important and popular method for mechanized reasoning about programming languages. We explore the limits of this method in the setting of finitely-stratified System F using the Agda proof assistant. This system supports elegant definitions of denotational semantics as well as big-step operational semantics based on intrinsically typed syntax. While its syntactic metatheory (i.e., type soundness) works well, we demonstrate that its semantic metatheory poses technical challenges, by defining a logical relation and proving its fundamental lemma. Our logical relation connects a denotational semantics with an operational one, which exposes issues with transfer lemmas as well as minor issues with universe polymorphism.

+
+ + +

Modal μ-Calculus for Free in Agda

  • Ivan Todorov
  • Casper Bach Poulsen
+

Expressive logics, such as the modal μ-calculus, can be used to specify and verify functional requirements of program models. While such verification is useful, a key challenge is to guarantee that the model being verified actually corresponds to the (typically effectful) program it is supposed to. We explore an approach that bridges this gap between effectful programming and functional requirement verification. Using dependently-typed programming in Agda, we develop an embedding of the modal μ-calculus for defining and verifying functional properties of possibly-non-terminating effectful programs which we represent in Agda using the coinductive free monad.

+
+ + +

Normalizable Types

  • Stefan Monnier
+

In dependently typed programming languages, quotients can be introduced in two different ways: elements of each equivalence class can be made either propositionally equal, at the cost of having to manipulate those equality proofs, or definitionally equal, at the cost of requiring a normalization function. The convenience of definitional equality could make the requirement of a normalization function tolerable, if it were not for the fact that those quotients need to be normalized every time we look at them. In the context of proof assistants, this is sometimes acceptable since efficiency of the code is not always relevant, but for a programming language it means these kinds of quotient types (sometimes called normalized types) are usable only with normalization functions which are cheap, and in the end they do not offer very many benefits over the use of smart constructors which eagerly normalize their return value. We propose an adjustment to normalized types that allows manipulating values of such types without having to normalize them, thus offering much finer control over the code’s efficiency, as well as making those quotient types usable even when normalization functions are too costly or impractical at runtime.

+
+ + +

Type-Level Property Based Testing

  • Thomas Ekström Hansen
  • Edwin Brady
+

We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.

+
+ + +

Towards Type-Directed API Search for Mainstream Languages

  • Marc Etter
  • Farhad Mehta
+

Software developers spend a lot of their time finding and composing pre-existing functions from various libraries. Almost all developers today use general-purpose search engines for this search. Specialized search engines such as Hoogle for Haskell additionally use type information to improve this search, and have been successful for some typed functional programming languages. The options currently available for type-directed search for mainstream object-oriented languages is limited. Existing approaches for these languages do not have first-class support for subtyping or parametric polymorphism. The splitting and composition of a desired functionality into and from a number of pre-existing functions is also a task that needs to be done manually. In this paper we present a proof-search-based approach to type-directed search with first-class support for subtyping, parametric polymorphism, splitting, and composition. The approach is language agnostic, and can be specialized to simultaneously support multiple typed object-oriented languages. Given that most mainstream languages fall under this category, this approach would extend the benefits of type-directed search to the majority of programmers. As a proof of concept, we provide a running implementation of the core language-agnostic approach and extend it to support the Java programming language. Further extensions would allow the tool to simultaneously support multiple programming languages using the same query syntax.

+
+ + +

Term Search in Rust

  • Tavo Annus
  • Philipp Joram
+

The Rust programming language offers a rich type system, including sum- and product types. Developer experience is often similar to that of a high-level functional programming language. Yet, it lacks a tool for interactively synthesizing programs based on types; a feature of many functional languages. We devise a general term search algorithm, and integrate it with rust-analyzer, Rust’s official language server, making it usable from any client supporting standard LSP features. It suggests expressions for unfinished parts of a Rust program (as long as their type is known), or offers terms of matching type while typing via autocompletion. We develop the algorithm in three iterations. The first iteration is a backward search, inspired by Agsy, a similar tool for Agda proof assistant. The second iteration reverses the search direction, simplifying the caching of intermediate results. In the final iteration, we implement a tactic-based bidirectional search. This algorithm can synthesize terms in many more situations than the previous iterations, without a significant decrease in performance. To evaluate the performance of our algorithm, we run it on 155 popular open-source Rust libraries. We delete parts of their source code, creating holes, and let the algorithm re-synthesize the missing code. We measure how many holes the algorithm can fill and how often it suggests the original code. We have upstreamed our code, and term search is available as part of the official rust-analyzer distribution starting from v0.3.1850.

+
+ +
\ No newline at end of file diff --git a/_data/OpenTOC.yaml b/_data/OpenTOC.yaml index 49fe420..518f0ef 100644 --- a/_data/OpenTOC.yaml +++ b/_data/OpenTOC.yaml @@ -1405,3 +1405,31 @@ event: ICFP year: 2024 title: "Proceedings of the ACM on Programming Languages: Vol. 8, No. ICFP. 2024" +- + event: Haskell + year: 2024 + title: "Proceedings of the 17th ACM SIGPLAN International Haskell Symposium" +- + event: TyDe + year: 2024 + title: "Proceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development" +- + event: FARM + year: 2024 + title: "Proceedings of the 12th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design" +- + event: FUNARCH + year: 2024 + title: "Proceedings of the 2nd ACM SIGPLAN International Workshop on Functional Software Architecture" +- + event: FProPer + year: 2024 + title: "Proceedings of the 1st ACM SIGPLAN International Workshop on Functional Programming for Productivity and Performance" +- + event: Erlang + year: 2024 + title: "Proceedings of the 23rd ACM SIGPLAN International Workshop on Erlang" +- + event: Haskell + year: 2024 + title: "Proceedings of the 17th ACM SIGPLAN International Haskell Symposium"