Publications
56 results found
Kidney DO, Yang Z, Wu N, 2024, Algebraic Effects Meet Hoare Logic in Cubical Agda, Proceedings of the ACM on Programming Languages, Vol: 8
This paper presents a novel formalisation of algebraic effects with equations in Cubical Agda. Unlike previous work in the literature that employed setoids to deal with equations, the library presented here uses quotient types to faithfully encode the type of terms quotiented by laws. Apart from tools for equational reasoning, the library also provides an effect-generic Hoare logic for algebraic effects, which enables reasoning about effectful programs in terms of their pre- and post- conditions. A particularly novel aspect is that equational reasoning and Hoare-style reasoning are related by an elimination principle of Hoare logic.
Van Bakel S, Wu N, Tye E, 2023, A Calculus of Delayed Reductions
We introduce the Calculus of Delayed Reduction (cdr), that expresses that redexes can only be contracted when brought to the right position in a term, and will show that Call by Name or Value (cbn, cbv) reduction for the λ -calculus can be modelled through reduction in cdr, and that the cbn fragment of the -calculus can model reduction in cdr. cdr is a Call by Push Value calculus (cbpv) in that it separates terms in computations and values, with their corresponding types. Some simulation results were already achieved by others for cbpv, but only up to equality for cbv; for cbn past results are rather weak. In order to achieve a single-step reduction respecting mapping for the cbn λ -calculus, we allow forcing only for variables, thunking only for computations that are not forced variables, and change the nature of term substitution, and abolish the U-reduction rule. We will show that, by changing the standard interpretation, we can achieve a reduction-respecting mapping for the cbv λ -calculus as well. Moreover, these changes make it possible to establish a strong relation between cdr and , allowing to simulate cdr reduction in , and preserving assignable types.
Gibbons J, Kidney DO, Schrijvers T, et al., 2023, Phases in Software Architecture, Pages: 29-33
The large-scale structure of executing a computation can often be thought of as being separated into distinct phases. But the most natural form in which to specify that computation may well have a different and conflicting structure. For example, the computation might consist of gathering data from some locations, processing it, then distributing the results back to the same locations; it may be executed in three phases - gather, process, distribute - but mostly conveniently specified orthogonally - by location. We have recently shown that this multi-phase structure can be expressed as a novel applicative functor (also known as an idiom, or lax monoidal functor). Here we summarize the idea from the perspective of software architecture. At the end, we speculate about applications to choreography and multi-tier architecture.
Matsuda K, Frohlich S, Wang M, et al., 2023, Embedding by Unembedding, PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, Vol: 7
Yang Z, Wu N, 2023, Modular Models of Monoids with Operations, PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, Vol: 7
Tahir O, Luk W, Wu N, 2023, Extensible Embedded Hardware Description Languages with Compilation, Simulation and Verification, The International Symposium on Highly Efficient Accelerators and Reconfigurable Technologies 2023
Typical hardware description languages, such as Verilog and VHDL, are low-level declarative languages with little room for flexibility. Extending, verifying, or reinterpreting programs in these languages is typically done with external tools and at great cost. This paper presents an implementation of a relational hardware description language, Ruby, in the programming language and proof assistant Agda. Using our system, an engineer can easily write, compile, simulate, and verify new designs. The language is modular, allowing for new constructs and libraries to be added easily, and supports formal reasoning about circuit transformations. Symbolic simulation and compilation to a netlist format are also provided. We demonstrate our tool by designing, compiling, and simulating a priority queue design, and showcase how equational reasoning can be used to prove properties of circuits.
Bernardy J-P, Eisenberg R, Kiss C, et al., 2022, Linear Constraints
A linear argument must be consumed exactly once in the body of its function.A linear type system can verify the correct usage of resources such as filehandles and manually managed memory. But this verification requiresbureaucracy. This paper presents linear constraints, a front-end feature forlinear typing that decreases the bureaucracy of working with linear types.Linear constraints are implicit linear arguments that are to be filled inautomatically by the compiler. Linear constraints are presented as a qualifiedtype system, together with an inference algorithm which extends OutsideIn,GHC's existing constraint solver algorithm. Soundness of linear constraints isensured by the fact that they desugar into Linear Haskell.
Nguyen M, Perera R, Wang M, et al., 2022, Modular Probabilistic Models via Algebraic Effects, PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, Vol: 6
Thomson P, Rix R, Wu N, et al., 2022, Fusing Industry and Academia at GitHub (Experience Report), PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, Vol: 6
Katsumata S-Y, McDermott D, Uustalu T, et al., 2022, Flexible Presentations of Graded Monads, PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, Vol: 6
- Author Web Link
- Cite
- Citations: 3
Willis J, Wu N, 2022, Design patterns for parser combinators in scala, Pages: 9-21
Parser combinators provide a parsing experience that balances flexibility and abstraction with writing parsers in a style that remains close to the grammar. Parser combinators can benefit from the design patterns and structure of an object-oriented world, however, and this paper showcases the implementation and implications of various design patterns tailored at parsers in an object-oriented and functional world. In particular, features of Scala, such as implicits and path-dependent types, along with general object-oriented design help make it easy to write and maintain such parsers.
Xie N, Pickering M, Loh A, et al., 2022, Staging with Class A Specification for Typed Template Haskell, PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, Vol: 6
- Author Web Link
- Cite
- Citations: 1
Yang Z, Paviotti M, Wu N, et al., 2022, Structured Handling of Scoped Effects, 31st European Symposium on Programming (ESOP) Held as Part of the 25th European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 462-491, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 2
Nguyen M, Wu N, 2022, Folding over Neural Networks, 14th International Conference on Mathematics of Program Construction (MPC), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 129-150, ISSN: 0302-9743
Gibbons J, Kidney DO, Schrijvers T, et al., 2022, Breadth-First Traversal via Staging, 14th International Conference on Mathematics of Program Construction (MPC), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 1-33, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 1
Yang Z, Wu N, 2022, Fantastic Morphisms and Where to Find Them A Guide to Recursion Schemes, MATHEMATICS OF PROGRAM CONSTRUCTION (MPC 2022, Vol: 13544, Pages: 222-267, ISSN: 0302-9743
Kidney DO, Wu N, 2021, Algebras for weighted search, Proceedings of the ACM on Programming Languages, Vol: 5, Pages: 1-30, ISSN: 2475-1421
Weighted search is an essential component of many fundamental and useful algorithms. Despite this, it is relatively under explored as a computational effect, receiving not nearly as much attention as either depth- or breadth-first search. This paper explores the algebraic underpinning of weighted search, and demonstrates how to implement it as a monad transformer. The development first explores breadth-first search, which can be expressed as a polynomial over semirings. These polynomials are generalised to the free semi module monad to capture a wide range of applications, including probability monads, polynomial monads, and monads for weighted search. Finally, a monad trans-former based on the free semi module monad is introduced. Applying optimisations to this type yields an implementation of pairing heaps, which is then used to implement Dijkstra’s algorithm and efficient probabilistic sampling. The construction is formalised in Cubical Agda and implemented in Haskell.
Punchihewa H, Wu N, 2021, Safe mutation with algebraic effects, ACM SIGPLAN Haskell Symposium 2021, Publisher: ACM, Pages: 122-135
It can be difficult to write safe concurrent programs whichuse shared mutable state. Subtle mistakes can lead to dataraces that manifest as unexpected program behaviour. Theprevailing approaches to solving this dilemma are to either eschew mutable state altogether, or design bespokelanguages that prevent data races by design. This article introduces a third approach by showing how safe mutation canbe integrated into a mainstream functional programminglanguage with algebraic effects. This article produces a framework that tracks the use of mutable state and guaranteesdata race freedom at compile time
Willis J, Wu N, 2021, Design patterns for parser combinators (functional pearl), ACM SIGPLAN Haskell Symposium 2021, Publisher: ACM, Pages: 71-84
Parser combinators are a popular and elegant approach for parsing in functional languages. The design and implementation of such libraries are well discussed, but having a well-designed library is only one-half of the story. In this paper we explore several reusable approaches to writing parsers in combinator style, focusing on easy to apply patterns to keep parsing code simple, separated, and maintainable.
Yang Z, Wu N, 2021, Reasoning about effect interaction by fusion, Proceedings of the ACM on Programming Languages, Vol: 5, Pages: 1-29, ISSN: 2475-1421
Effect handlers can be composed by applying them sequentially, each handling some operations and leaving other operations uninterpreted in the syntax tree. However, the semantics of composed handlers can be subtle—it is well known that different orders of composing handlers can lead to drastically different semantics. Determining the correct order of composition is a non-trivial task. To alleviate this problem, this paper presents a systematic way of deriving sufficient conditions on handlers for their composite to correctly handle combinations, such as the sum and the tensor, of the effect theories separately handled. These conditions are solely characterised by the clauses for relevant operations of the handlers, and are derived by fusing two handlers into one using a form of fold/build fusion and continuation-passing style transformation. As case studies, the technique is applied to commutative and distributive interaction of handlers to obtain a series of results about the interaction of common handlers: (a) equations respected by each handler are preserved after handler composition; (b) handling mutable state before any handler gives rise to a semantics in which state operations are commutative with any operations from the latter handler; (c) handling the writer effect and mutable state in either order gives rise to a correct handler of the commutative combination of these two theories.
Bird R, Gibbons J, Hinze R, et al., 2021, Algorithmics, IFIP Advances in Information and Communication Technology, Pages: 59-98
Algorithmics is the study and practice of taking a high-level description of a program’s purpose and, from it, producing an executable program of acceptable efficiency. Each step in that process is justified by rigorous, careful reasoning at the moment it is taken; and the repertoire of steps allowed by that rigour, at each stage, guides the development of the algorithm itself. IFIP’s Working Group 2.1 [i] has always been concerned with Algorithmics: both the design of its notations and the laws that enable its calculations. ALGOL 60 had already shown that orthogonality, simplicity and rigour in a programming language improves the quality of its programs. Our Group’s title “Algorithmic Languages and Calculi” describes our activities: the discovery of precise but more general rules of calculational reasoning for the many new styles of programming that have developed over the 60 years since IFIP’s founding. As our contribution to the birthday celebrations, we outline how we have tried to contribute during those decades to the rigorous and reliable design of computer programs of all kinds—to Algorithmics. (Roman-numbered references like [i] in this abstract refer to details given in Sect. 10.)
van den Berg B, Schrijvers T, Poulsen CB, et al., 2021, Latent Effects for Reusable Language Components, 19th Asian Symposium on Programming Languages and Systems (APLAS), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 182-201, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 2
Pickering M, Löh A, Wu N, 2020, Staged Sums of Products, Haskell Symposium
Willis J, Wu N, Pickering M, 2020, Staged selective parser combinators, Proceedings of the ACM on Programming Languages, Vol: 4, Pages: 1-30, ISSN: 2475-1421
Parser combinators are a middle ground between the fine control of hand-rolled parsers and the high-level almost grammar-like appearance of parsers created via parser generators. They also promote a cleaner, compositional design for parsers. Historically, however, they cannot match the performance of their counterparts.This paper describes how to compile parser combinators into parsers of hand-written quality. This is done by leveraging the static information present in the grammar by representing it as a tree. However, in order to exploit this information, it will be necessary to drop support for monadic computation since this generates dynamic structure. Selective functors can help recover lost functionality in the absence of monads, and the parser tree can be partially evaluated with staging. This is implemented in a library called Parsley.
Schrijvers T, Pirog M, Wu N, et al., 2019, Monad Transformers and Modular Algebraic Effects, 12th ACM SIGPLAN International Symposium on Haskell (Haskell), Publisher: ASSOC COMPUTING MACHINERY, Pages: 98-113
- Author Web Link
- Cite
- Citations: 11
Pickering M, Wu N, Nemeth B, 2019, Working with Source Plugins, 12th ACM SIGPLAN International Symposium on Haskell (Haskell), Publisher: ASSOC COMPUTING MACHINERY, Pages: 85-97
- Author Web Link
- Cite
- Citations: 4
Pickering M, Wu N, Kiss C, 2019, Multi-stage Programs in Context, 12th ACM SIGPLAN International Symposium on Haskell (Haskell), Publisher: ASSOC COMPUTING MACHINERY, Pages: 71-84
- Author Web Link
- Cite
- Citations: 3
Innes S, Wu N, 2019, Tic Tac Types A Gentle Introduction to Dependently Typed Programming (Functional Pearl), 4th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe), Publisher: ASSOC COMPUTING MACHINERY, Pages: 40-51
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.