Numerical representation is a technique for modelling datastructures after number systems. Typically, the method has been used to derive one-dimensional datastructures. This paper explores utilizing the technique for modelling two-dimensional datastructures instead, with insights into multi-dimensional ones. The aim of this paper is to devise datastructures for modelling block matrices. We look into the different derivations and highlight some roadblocks that would otherwise not be an issue in the one-dimensional case. The points under consideration include dimensional bias, ease of defining functions and proving properties about them as well as the difficulty of understanding the derived datastructure.
A type- and control-flow analysis is a program analysis that yields both type-flow information, approximating the types that may instantiate type variables, and control-flow information, approximating the values (especially λ - and -expressions) that may be bound to variables. Moreover, each of the flows informs the other; control-flow establishes the types that may instantiate -bound type variables by determining the -expressions that flow to a type-application expression, while type-flow filters control-flow by rejecting the flow of values having static types that are incompatible (according to the type-flow information) with the static type of the receiving variable. In previous work [1, 13, 14], we introduced a (monovariant) type- and control-flow analysis for System F (with recursion). While System F has an expressive type system and has served as a useful core calculus in which to express interesting language features, it only allows abstraction over types and does not allow abstraction over type constructors. Increasingly, researchers are looking at System F _ω , with both term- and type-level abstraction over types of arbitrary kind, as a core calculus in which to explore advanced language features. Hence, we are motivated to define a type- and control-flow analysis for System F _ω that is able to analyze the rich structure of System F _ω types. In this work, we present a preliminary type- and control-flow analysis for System F _ω (with recursion). As in previous work, we give both a specification-based formulation of the analysis, used to prove soundness of the analysis, and a flow-graph-based formulation, used to guide the implementation of an algorithm. While the macro structure of the development for System F _ω follows that for System F, moving to System F _ω introduces subtle challenges that have left some unanswered questions about the meta-theory. In particular, the decidability of type compatibility defined in terms of System F _ω ’s definitional type equivalence remains an open question. In order to be computable, our flow-graph-based formulation uses a restricted form of definitional type equivalence and performs a 0CFA at the type-level, yielding an analysis result that is less precise than the “best” (but as of yet, uncomputable) analysis result accepted by the specification-based formulation. Our soundness results have been formalized in the Coq proof assistant. This work is based in part on the first author’s MS thesis [53].
Implementing communication between edge devices and their server in IoT systems is often a tedious and bug-prone task, since different programming languages with distinct underlying paradigms need to cooperate. The mTask system prevents this semantic friction by providing a single task-oriented framework for the whole system. Shared data sources provide flexible communication between tasks running on the server and tasks running on edge devices, however the current implementation has some drawbacks. We introduce an improved version of these shares with a clearer semantics. To improve the communication between edge devices and the server, we introduce the possibility to start parametrized server tasks from the edge device.
Functional Programming—–what is it good for? Programming is the writing of programs. Judging from the papers and most books on functional programming, functional programming excels as a tool for writing short programs—–up to a hundred lines maybe. We also know that there are large functional code bases at large companies, and folklore has it that this also works quite well. Yet there is precious little literature on how to go from a hundred lines to a million lines of functional code. This hinders the adoption of functional program by newcomers, who ask questions like: Successful practitioners rely on folklore and experience for the answers to these questions, but precious little is written down in findable places and accessible formats. This paper is a call to action: The functional programming community needs to do a better job at outreach—find the gaps in our published knowledge, write down what is undocumented and talk to other communities who deal with large-scale software development.
In recent years the energy-efficiency of software has become a key focus for both researchers and software developers, aiming to reduce greenhouse-gas emissions and operational costs. Despite this growing awareness, developers still lack effective strategies to improve the energyefficiency of their programs beyond the well-established approaches that optimize for runtime performance. In this paper we present a dynamic adaptation algorithm that uses energy consumption feedback to optimize the energy-efficiency of data-parallel applications, by steering the level of parallelism during runtime through external control. This approach is especially suited to functional languages, whose side-effect-free nature and strong semantic guarantees allow for easier code generation and straightforward scalability of the parallelism of programs. Through a series of experiments we evaluate the effectiveness of our approach. We measure how well the adaptation algorithm adapts to runtime changes, and we evaluate its effectiveness compared to a hypothesized oracle that knows the optimal level of parallelism, as well as a runtime-optimising-based approach. We show that in a fixed-workload scenario we approach the theoretical best energy-efficiency, and that in changing workload scenarios the adaptation algorithm converges towards an optimal level of parallelism that minimizes energy consumption.
Since their introduction, copatterns have promised to extend functional languages—with their familiar pattern matching facilities—to synthesize and work with infinite objects through a finite set of observations. Thus far, their adoption in practice has been limited and primarily associated with specific tools like proof assistants. With that in mind, we aim to make copattern matching usable for ordinary functional programmers by implementing them as macros in the Scheme and Racket programming languages. Our approach focuses on composable copatterns, which can be combined in multiple directions and offer a new solution to the expression problem through novel forms of extensibility. To check the correctness of the implementation and to reason equationally about copattern-matching code, we describe an equational theory for copatterns with a sound, selective translation into λ -calculus.
This paper presents two improvements to the compatibility and performance of stableKanren on monotonic programs. miniKanren supports monotonic reasoning, in which one program produces exactly one model. stableKanren extends miniKanren to nonmonotonic reasoning, where a program can have zero to multiple models. stableKanren handles loops and negations, the main elements of nonmonotonic reasoning, through an extended nonmonotonic resolution in its "run" interface. The current nonmonotonic resolution in the stableKanren also applies to monotonic programs and creates two issues. Firstly, a monotonic program with infinite answers could not produce an answer under stableKanren. Secondly, a monotonic program runs slower under stableKanren due to the additional nonmonotonic resolution. The nonmonotonic resolution is unnecessary for these monotonic programs. We construct a "run-partial" interface in stableKanren without nonmonotonic resolution. Using "run-partial" resolves the above two issues; however, expert knowledge is required to identify whether the program is monotonic or nonmonotonic and to choose the corresponding interface by the users. We further introduce two program analyses to the stableKanren "run" interface to identify the monotonic program implicitly. We use a macro to handle the first issue at the syntax level, so the "run" interface does not apply nonmonotonic resolution on monotonic programs without any negations. Furthermore, we present four syntax-level macros to construct two smaller twins of the input program. Each twin has different semantics on loops over negations, so we resolve the second issue by running these two twins. The twins of the monotonic programs produce identical outcomes, but the nonmonotonic programs do not. Our updated "run" interface can identify monotonic programs at the syntax level; there is still more work to identify such programs during execution.
This paper presents KappaMutor, a new graph reduction processor, along with its Haskell compiler. KappaMutor is based on structured combinators, a recently proposed combinator encoding, which is more flexible and efficient than fine-grained SKI combinators. The processor exploits parallel memories to enable single-cycle reduction of structured combinators while maintaining good compactness, utilising less than 1
Accumulative functions, such as tail-recursive functions, employ accumulation parameters to carry and update the intermediate results. Despite their ubiquity and importance for efficient implementations, the automatic synthesis of accumulative functions remains challenging. The presence of accumulative parameters not only expands the search space but also unfastens the input-output examples from the traces of recursive calls, leading existing program synthesis methods to either fail in generating nontrivial accumulative functions or rely on pre-provided skeletons of recursive calls with accumulations. In this paper, we investigate an alternative approach to synthesizing accumulative functions. Our strategy integrates an off-the-shelf synthesizer, which may not inherently produce accumulative functions, and a program transformation that derives accumulative functions from non-accumulative ones. We specifically focus on the transformation introduced by Kühnemann et al. (RTA 2001), which effectively derives accumulative functions if the non-accumulative ones consist of substitution operators. By guiding the synthesizer to use substitution operators, we aim to obtain functions suitable for the transformation. We demonstrate the ability of our approach with examples from existing benchmarks.
Historically, it has been challenging for students to get interested in and for instructors to teach Formal Languages and Automata Theory courses. The challenges stem from a multitude of reasons including the theoretical nature of the material, the use of formal notation, student lack of experience with problem solving and proof development, and the student perception that the material is not relevant to majoring in Computer Science. In this article, we illustrate our novel design- and programming-based approach to building state machines and developing constructive proofs. Student perceptions, both overall and by gender, are explored to determine if this approach effectively addresses some of the negative historical trends. Our empirical results suggest that the approach has a positive impact overall and by gender. In addition, the results reveal nuanced differences between female and male students and areas for future improvements.
Cross-stage persistence rules are commonly admitted in multi-stage programming languages. These rules codify the assumption that all module and package dependencies are available at all stages. However, in practice, only a small number of dependencies may be needed at each particular stage. This paper introduces Explicit Level Imports, a mechanism which gives programmers precise control about which dependencies are required at each stage. Imports are annotated with a modifier which brings identifiers into scope at a specific level. This precision means it is straightforward for the compiler to work out what is exactly needed at each stage, and only provide that. The result is faster compilation times and the potential for improved cross-compilation support. We have implemented these ideas in GHC Haskell, consider a wide variety of practical considerations in the design, and finally demonstrate that the feature solves a real-world issue in a pragmatic way.
Functional reactive programming (FRP) is a programming paradigm for implementing reactive systems, i.e. programs that continuously interact with their environments. While FRP allows for a functional, high-level programming style, FRP programs are prone to undesirable operational behaviours such as space leaks. To ensure favourable operational properties of FRP programs, modal type systems have been introduced, which – among other things – make it impossible to write FRP programs with implicit space leaks. In a recent development, several modal FRP languages have been introduced that are able to accommodate asynchronous events and behaviours – motivated by the goal to use such languages for GUI programming. This paper explores the suitability of one such asynchronous modal FRP language – called Async Rattus – for GUI programming in practice. To this end, we have implemented a mild extension of the Async Rattus language and used it to implement a small GUI framework. We demonstrate the language and its GUI framework by a number of case studies.
Typed functional programming languages like Haskell and OCaml make heavy use of the heap at run-time. This makes them largely unsuitable for systems programming, where resources are limited and programs are often expected to run on bare-metal. This paper demonstrates how a (slightly restricted) high-level, pure, functional language can be compiled to machine code which does not use the heap at all. Despite usually requiring a heap at run-time, features such as higher-order functions, polymorphism and typeclasses are all supported by the surface language. This is made possible through partial evaluation [12]: by carefully reducing the program at compile-time, we can eliminate these highlevel features entirely, resulting in a residual program which is trivial to compile to stack-based machine code. This paper describes the operation of this partial evaluator, justifies its design, and introduces a novel type system which guarantees that the partial evaluator will always succeed in removing all heap-using features.
The desire to comment is a human impulse, seen also in art forms from music and visual art to film and literature. Syntaxes for commentary appear almost at once in the history of programming. Comments lie in the zone of the inexpressible, saying what cannot be said in a programming language, and the need for them can never entirely be designed away by new languages. The most audacious case for commentary remains Donald Knuth’s radical proposal for “literate programming”, which recasts the programmer as essayist. Emerging from Knuth’s thinking about ideas of perfectibility, publication, and the sacred, this manifesto was in part a rebuttal of structured programming. Though it failed to achieve dominance, its ideas remain stimulating, and show an eerie convergence with today’s norms – GitHub being in some respects its triumph after all. Practical experience with large-scale LP is mixed, but it still has much to teach us.
Parsing is the process of recovering structure from strings, an essential part of implementing programming languages. Previous work has shown that formalizing languages and parsers using an idiomatic type theoretic approach can be simple and enlightening. Unfortunately, this approach has only been applied to regular languages, which are not expressive enough for many practical applications. We have extended the type theoretic formalization to context-free languages (without mutual recursion) which are substantially more expressive. We hope our formalization can serve as a foundation for reasoning about new disambiguation techniques and even more expressive formalisms such as data-dependent grammars.
WebAssembly is a popular low-level intermediate representation (IR) and compilation target. The official specification of WebAssembly provides a small-step reduction semantics. Unlike other common low-level IRs, WebAssembly provides structured control-flow constructs, whose reduction rules are complicated by additional administrative instructions in the reference semantics. This paper develops an alternative semantics in continuation-passing style (CPS), which can be implemented as a concise, compositional, and tail-recursive interpreter or CPS transformer. Using continuations from the meta-language eliminates the need for administrative instructions. We further demonstrate that the CPS semantics can be extended to support other forms of control abstractions, such as effect handlers.
Ask-Elle is an online tutor for solving small programming exercises in Haskell. It provides feedback by first determining whether a student's submission matches one of the teacher-provided model solutions. However, Haskell's rich syntax allows for semantically equivalent but syntactically different programs, making direct comparison challenging. To address this, Ask-Elle applies normalizing program transformations to reduce such syntactic differences. Despite this, some correct programs remain unrecognised. We have developed a new approach to feedback generation that leverages GHC's internal transformations and warning messages. This method improves the recognition of correct programs while also being much faster. Additionally, we share our experiences using GHC as a library.
Numerical representation is a technique for modelling datastructures after number systems. Typically, the method has been used to derive one-dimensional datastructures. This paper explores utilizing the technique for modelling two-dimensional datastructures instead, with insights into multi-dimensional ones. The aim of this paper is to devise datastructures for modelling block matrices. We look into the different derivations and highlight some roadblocks that would otherwise not be an issue in the one-dimensional case. The points under consideration include dimensional bias, ease of defining functions and proving properties about them as well as the difficulty of understanding the derived datastructure.
In distributed systems, nodes typically collaborate to perform tasks. Many distributed systems adopt groups or clusters as architectural units to improve the management and coordination of nodes. The group membership protocol serves a crucial role in ensuring a consistent understanding of member status across all nodes in the group. Group membership protocols are essential in various distributed real-world systems, such as IoT sensor networks, smart agriculture, environmental monitoring, satellite communications, remote infrastructure monitoring, smart buildings, industrial automation, intelligent transportation systems, and medical monitoring systems. Group membership protocols are traditionally classified as heartbeat-based or gossip-based. Both protocol categories require frequent heartbeat or ping messages, facing challenges in energy efficiency, especially in systems with low failure rates and high energy consumption requirements. This paper introduces a novel group membership protocol with two main algorithms that eliminate the need for periodic ping or heartbeat messages. This protocol is designed for Symmetric P2P Systems using the actor model and ensures strong consistency. We provide formal specifications and verifications using TLA+ to ensure the correctness of our algorithms. The safety and liveness properties of the specifications are verified with the TLC model checker. In addition, the implementation of the protocol in the functional programming language is provided.
