Publications
44 results found
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
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
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.
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.
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
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.
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: 2
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
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: 4
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: 2
Gibbons J, Henglein F, Hinze R, et al., 2018, Relational algebra by way of adjunctions, 23rd ACM SIGPLAN International Conference on Functional Programming (ICFP), Publisher: Association for Computing Machinery (ACM), Pages: 86.1-86.28, ISSN: 2475-1421
Bulk types such as sets, bags, and lists are monads, and therefore support a notation for database queries based on comprehensions. This fact is the basis of much work on database query languages. The monadic structure easily explains most of standard relational algebra---specifically, selections and projections---allowing for an elegant mathematical foundation for those aspects of database query language design. Most, but not all: monads do not immediately offer an explanation of relational join or grouping, and hence important foundations for those crucial aspects of relational algebra are missing. The best they can offer is cartesian product followed by selection. Adjunctions come to the rescue: like any monad, bulk types also arise from certain adjunctions; we show that by paying due attention to other important adjunctions, we can elegantly explain the rest of standard relational algebra. In particular, graded monads provide a mathematical foundation for indexing and grouping, which leads directly to an efficient implementation, even of joins.
Kiss C, Pickering M, Wu N, 2018, Generic deriving of generic traversals, Proceedings of the ACM on Programming Languages, Vol: 2, Pages: 1-32, ISSN: 2475-1421
Functional programmers have an established tradition of using traversals as a design pattern to work with recursive data structures. The technique is so prolific that a whole host of libraries have been designed to help in the task of automatically providing traversals by analysing the generic structure of data types. More recently, lenses have entered the functional scene and have proved themselves to be a simple and versatile mechanism for working with product types. They make it easy to focus on the salient parts of a data structure in a composable and reusable manner.This paper uses the combination of lenses and traversals to give rise to a library with unprecedented expressivity and flexibility for querying and modifying complex data structures. Furthermore, since lenses and traversals are based on the generic shape of data, this information is used to generate code that is as efficient as hand-optimised versions. The technique leverages the structure of data to produce generic abstractions that are then eliminated by the standard workhorses of modern functional compilers: inlining and specialisation.
Piróg M, Schrijvers T, Wu N, et al., 2018, Syntax and Semantics for Operations with Scopes, the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Publisher: ACM Press
Willis J, Wu N, 2018, Garnishing Parsec with Parsley, 9th ACM SIGPLAN International Symposium on Scala (Scala) as part of the ACM SIGPLAN International Conference on Functional Programming (ICFP), Publisher: ASSOC COMPUTING MACHINERY, Pages: 24-34
- Author Web Link
- Cite
- Citations: 2
Wong D, Wu N, Watkinson P, 2017, Quantitative metrics for evaluating the phased roll-out of clinical information systems, International Journal of Medical Informatics, Vol: 105, Pages: 130-135, ISSN: 1386-5056
ObjectivesWe introduce a novel quantitative approach for evaluating the order of roll-out during phased introduction of clinical information systems. Such roll-outs are associated with unavoidable risk due to patients transferring between clinical areas using both the old and new systems.MethodsWe proposed a simple graphical model of patient flow through a hospital. Using a simple instance of the model, we showed how a roll-out order can be generated by minimising the flow of patients from the new system to the old system.ResultsThe model was applied to admission and discharge data acquired from 37,080 patient journeys at the Churchill Hospital, Oxford between April 2013 and April 2014. The resulting order was evaluated empirically and produced acceptable orders.DiscussionThe development of data-driven approaches to clinical Information system roll-out provides insights that may not necessarily be ascertained through clinical judgment alone. Such methods could make a significant contribution to the smooth running of an organisation during the roll-out of a potentially disruptive technology.ConclusionUnlike previous approaches, which are based on clinical opinion, the approach described here quantitatively assesses the appropriateness of competing roll-out strategies. The data-driven approach was shown to produce strategies that matched clinical intuition and provides a flexible framework that may be used to plan and monitor Clinical Information System roll-out.
Pickering M, Gibbons J, Wu N, 2017, Profunctor optics: modular data accessors, The Art, Science, and Engineering of Programming, Vol: 1, Pages: 7-1-7-51, ISSN: 2473-7321
Data accessors allow one to read and write components of a data structure, such as the fields of arecord, the variants of a union, or the elements of a container. These data accessors are collectively known asoptics; they are fundamental to programs that manipulate complex data. Individual data accessors for simpledata structures are easy to write, for example as pairs of ‘getter’ and ‘setter’ methods. However, it is notobvious how to combine data accessors, in such a way that data accessors for a compound data structure arecomposed out of smaller data accessors for the parts of that structure. Generally, one has to write a sequenceof statements or declarations that navigate step by step through the data structure, accessing one level at atime—which is to say, data accessors are traditionally not first-class citizens, combinable in their own right.We present a framework for modular data access, in which individual data accessors for simple data structures may be freely combined to obtain more complex data accessors for compound data structures. Dataaccessors become first-class citizens. The framework is based around the notion of profunctors, a flexible generalization of functions. The language features required are higher-order functions (‘lambdas’ or ‘closures’),parametrized types (‘generics’ or ‘abstract types’) of higher kind, and some mechanism for separating interfaces from implementations (‘abstract classes’ or ‘modules’). We use Haskell as a vehicle in which to presentour constructions, but other languages such as Scala that provide the necessary features should work just aswell. We provide implementations of all our constructions, in the form of a literate program: the manuscriptfile for the paper is also the source code for the program, and the extracted code is available separately forevaluation. We also prove the essential properties, demonstrating that
Piróg M, Wu N, 2016, String diagrams for free monads (functional pearl), ACM SIGPLAN Notices, Vol: 51, Pages: 490-501, ISSN: 0362-1340
<jats:p>We show how one can reason about free monads using their universal properties rather than any concrete implementation. We introduce a graphical, two-dimensional calculus tailor-made to accommodate these properties.</jats:p>
Hinze R, Wu N, 2016, Unifying structured recursion schemes An Extended Study, JOURNAL OF FUNCTIONAL PROGRAMMING, Vol: 26, ISSN: 0956-7968
- Author Web Link
- Cite
- Citations: 2
Piróg M, Wu N, Gibbons J, 2015, Modules over monads and their algebras, Pages: 290-303, ISSN: 1868-8969
Modules over monads (or: actions of monads on endofunctors) are structures in which a monad interacts with an endofunctor, composed either on the left or on the right. Although usually not explicitly identified as such, modules appear in many contexts in programming and semantics. In this paper, we investigate the elementary theory of modules. In particular, we identify the monad freely generated by a right module as a generalisation of Moggi's resumption monad and characterise its algebras, extending previous results by Hyland, Plotkin and Power, and by Filinski and Støvring. Moreover, we discuss a connection between modules and algebraic effects: left modules have a similar feeling to Eilenberg-Moore algebras, and can be seen as handlers that are natural in the variables, while right modules can be seen as functions that run effectful computations in an appropriate context (such as an initial state for a stateful computation).
Hinze R, Wu N, Gibbons J, 2015, Conjugate Hylomorphisms -- Or, ACM SIGPLAN Notices, Vol: 50, Pages: 527-538, ISSN: 0362-1340
<jats:p>The past decades have witnessed an extensive study of structured recursion schemes. A general scheme is the hylomorphism, which captures the essence of divide-and-conquer: a problem is broken into sub-problems by a coalgebra; sub-problems are solved recursively; the sub-solutions are combined by an algebra to form a solution. In this paper we develop a simple toolbox for assembling recursive coalgebras, which by definition ensure that their hylo equations have unique solutions, whatever the algebra. Our main tool is the conjugate rule, a generic rule parametrized by an adjunction and a conjugate pair of natural transformations. We show that many basic adjunctions induce useful recursion schemes. In fact, almost every structured recursion scheme seems to arise as an instance of the conjugate rule. Further, we adapt our toolbox to the more expressive setting of parametrically recursive coalgebras, where the original input is also passed to the algebra. The formal development is complemented by a series of worked-out examples in Haskell.</jats:p>
Wu N, Schrijvers T, 2015, Fusion for Free Efficient Algebraic Effect Handlers, 12th International Conference on Mathematics of Program Construction (MPC), Publisher: SPRINGER-VERLAG BERLIN, Pages: 302-322, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 14
Hinze R, Wu N, Gibbons J, 2015, Conjugate Hylomorphisms Or: The Mother of All Structured Recursion Schemes, 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 15), Publisher: ASSOC COMPUTING MACHINERY, Pages: 527-538, ISSN: 0362-1340
- Author Web Link
- Cite
- Citations: 8
Wu N, Schrijvers T, Hinze R, 2014, Effect Handlers in Scope, ACM SIGPLAN NOTICES, Vol: 49, Pages: 1-12, ISSN: 0362-1340
- Author Web Link
- Cite
- Citations: 32
Wu N, Simpson A, 2014, Formal relational database design: an exercise in extending the formal template language, FORMAL ASPECTS OF COMPUTING, Vol: 26, Pages: 1231-1269, ISSN: 0934-5043
- Author Web Link
- Cite
- Citations: 1
Gibbons J, Wu N, 2014, Folding Domain-Specific Languages: Deep and Shallow Embeddings, 19th ACM SIGPLAN International Conference on Functional Programming (ICFP), Publisher: ASSOC COMPUTING MACHINERY, Pages: 339-347, ISSN: 0362-1340
- Author Web Link
- Cite
- Citations: 18
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.