Publications
35 results found
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.
Innes S, Wu N, 2019, Tic Tac types: A gentle introduction to dependently typed programming (Functional Pearl), Pages: 40-51
Tic-Tac-Toe is a simple, familiar, classic game enjoyed by many. This pearl is designed to give a favour of the world of dependent types to the uninitiated functional programmer. We cover a journey from Tic-Tac-Terrible implementations in the harsh world of virtually untyped Strings, through the safe haven of vectors that know their own length, and into a Tic-Tac-Titanium version that is too strongly typed for its own good. Along the way we discover something we knew all along; types are great, but in moderation. This lesson is quickly put to use in a more complex recursive version.
Schrijvers T, Piróg M, Wu N, et al., 2019, Monad transformers and modular algebraic effects:What binds them together, Pages: 98-113
For over two decades, monad transformers have been the main modular approach for expressing purely functional side-effects in Haskell. Yet, in recent years algebraic effects have emerged as an alternative whose popularity is growing. While the two approaches have been well-studied, there is still confusion about their relative merits and expressiveness, especially when it comes to their comparative modularity. This paper clarifies the connection between the two approaches-some of which is folklore-and spells out consequences that we believe should be better known. We characterise a class of algebraic effects that is modular, and show how these correspond to a specific class of monad transformers. In particular, we show that our modular algebraic effects gives rise to monad transformers. Moreover, every monad transformer for algebraic operations gives rise to a modular effect handler.
Pickering M, Wu N, Németh B, 2019, Working with source plugins, Pages: 85-97
A modern compiler calculates and constructs a large amount of information about the programs it compiles. Tooling authors want to take advantage of this information in order to extend the compiler in interesting ways. Source plugins are a mechanism implemented in the Glasgow Haskell Compiler (GHC) which allow inspection and modification of programs as they pass through the compilation pipeline. This paper is about how to write source plugins. Due to their nature-they are ways to extend the compiler-at least basic knowledge about how the compiler works is critical to designing and implementing a robust and therefore successful plugin. The goal of the paper is to equip would-be plugin authors with inspiration about what kinds of plugins they should write and most importantly with the basic techniques which should be used in order to write them.
Pickering M, Wu N, Kiss C, 2019, Multi-stage Programs in Context, Pages: 71-84
Cross-stage persistence is an essential aspect of multi-stage programming that allows a value defined in one stage to be available in another. However, difficulty arises when implicit information held in types, type classes and implicit parameters needs to be persisted. Without a careful treatment of such implicit information-which are pervasive in Haskell-subtle yet avoidable bugs lurk beneath the surface. This paper demonstrates that in multi-stage programming care must be taken when representing quoted terms so that important implicit information is kept in context and not discarded. The approach is formalised with a type-system, and an implementation in GHC is presented that fixes problems of the previous incarnation.
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
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
- Author Web Link
- Cite
- Citations: 1
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>
Pirog M, Wu N, 2016, String Diagrams for Free Monads (Functional Pearl), 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), Publisher: ASSOC COMPUTING MACHINERY, Pages: 490-501, ISSN: 0362-1340
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>
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: 6
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: 5
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: 18
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
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: 17
Schrijvers T, Wu N, Desouter B, et al., 2014, Heuristics Entwined with Handlers Combined From Functional Specification to Logic Programming Implementation, 16th International Symposium on Principles and Practice of Declarative Programming (PPDP), Publisher: ASSOC COMPUTING MACHINERY, Pages: 259-270
- Author Web Link
- Cite
- Citations: 6
Wu N, Magalhães JP, Bransen J, et al., 2013, Pure and lazy lambda mining: An experience report, Pages: 207-223, ISSN: 0302-9743
This paper discusses our entry to the 2012 ICFP Programming Contest, written entirely in Haskell. Our solution uses many features of Haskell: pure immutable data structures, laziness, higher-order functions, concurrency, and exception handling. Each of these features plays an essential part in our overall solution, and we demonstrate how these key elements can be composed together. In this exposition, we stress the importance of how the code was structured in such a way that made safely refactoring and extending the model a relatively easy task, and how Haskell's strong type system made it possible for our team to remain agile under changing specifications. © 2013 Springer-Verlag.
Hinze R, Wu N, 2013, Histo- and dynamorphisms revisited, Pages: 1-12
Dynamic programming algorithms embody a widely used programming technique that optimizes recursively defined equations that have repeating subproblems. The standard solution uses arrays to share common results between successive steps, and while effective, this fails to exploit the structural properties present in these problems. Histomorphisms and dynamorphisms have been introduced to expresses such algorithms in terms of structured recursion schemes that leverage this structure. In this paper, we revisit and relate these schemes and show how they can be expressed in terms of recursion schemes from comonads, as well as from recursive coalgebras. Our constructions rely on properties of bialgebras and dicoalgebras, and we are careful to consider optimizations and efficiency concerns. Throughout the paper we illustrate these techniques through several worked-out examples discussed in a tutorial style, and show how a recursive specification can be expressed both as an array-based algorithm as well as one that uses recursion schemes.
Hinze R, Wu N, Gibbons J, 2013, Unifying structured recursion schemes, ACM SIGPLAN Notices, Vol: 48, Pages: 209-220, ISSN: 0362-1340
<jats:p>Folds over inductive datatypes are well understood and widely used. In their plain form, they are quite restricted; but many disparate generalisations have been proposed that enjoy similar calculational benefits. There have also been attempts to unify the various generalisations: two prominent such unifications are the 'recursion schemes from comonads' of Uustalu, Vene and Pardo, and our own 'adjoint folds'. Until now, these two unified schemes have appeared incompatible. We show that this appearance is illusory: in fact, adjoint folds subsume recursion schemes from comonads. The proof of this claim involves standard constructions in category theory that are nevertheless not well known in functional programming: Eilenberg-Moore categories and bialgebras.</jats:p>
Hinze R, Wu N, Gibbons J, 2013, Unifying Structured Recursion Schemes, 18th ACM SIGPLAN International Conference on Functional Programming, Publisher: ASSOC COMPUTING MACHINERY, Pages: 209-220, ISSN: 0362-1340
- Author Web Link
- Cite
- Citations: 7
Hinze R, Magalhães JP, Wu N, 2013, A duality of sorts, Pages: 151-167, ISSN: 0302-9743
Sorting algorithms are one of the key pedagogical foundations of computer science, and their properties have been studied heavily. Perhaps less well known, however, is the fact that many of the basic sorting algorithms exist as a pair, and that these pairs arise naturally out of the duality between folds and unfolds. In this paper, we make this duality explicit, by showing how to define common sorting algorithms as folds of unfolds, or, dually, as unfolds of folds. This duality is preserved even when considering optimised sorting algorithms that require more exotic variations of folds and unfolds, and intermediary data structures. While all this material arises naturally from a categorical modelling of these recursion schemes, we endeavour to keep this presentation accessible to those not versed in abstract nonsense. © 2013 Springer-Verlag Berlin Heidelberg.
Hinze R, James DWH, Harper T, et al., 2012, Sorting with bialgebras and distributive laws, Pages: 69-80
Sorting algorithms are an intrinsic part of functional programming folklore as they exemplify algorithm design using folds and unfolds. This has given rise to an informal notion of duality among sorting algorithms: insertion sorts are dual to selection sorts. Using bialgebras and distributive laws, we formalise this notion within a categorical setting. We use types as a guiding force in exposing the recursive structure of bubble, insertion, selection, quick, tree, and heap sorts. Moreover, we show how to distill the computational essence of these algorithms down to one-step operations that are expressed as natural transformations. From this vantage point, the duality is clear, and one side of the algorithmic coin will neatly lead us to the other "for free". As an optimisation, the approach is also extended to paramorphisms and apomorphisms, which allow for more efficient implementations of these algorithms than the corresponding folds and unfolds. © 2012 ACM.
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.