Bidirectional programming languages are a practical approach to the view update problem. Programs in these languages, called lenses, define both a view and an update policy - i.e., every program can be read as a function mapping sources to views as well ...
Quotient lenses | Proceedings of the 13th ACM SIGPLAN international conference on Functional programming
Bidirectional programming languages are a practical approach to the view update problem. Programs in these languages, called lenses, define both a view and an update policy - i.e., every program can be read as a function mapping sources to views as well ...
Symmetric lenses | Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
A lens is a bidirectional transformation between a pair of connected data structures, capable of translating an edit on one structure into an appropriate edit on the other. Many varieties of lenses have been studied, but none, to date, has offered a ...
Resugaring | Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation
Syntactic sugar plays a crucial role in engineering programming languages. It offers convenient syntax and higher-level of abstractions, as witnessed by its pervasive use in both general-purpose and domain-specific contexts. Unfortunately, the ...
Bidirectionalization for free! (Pearl) | Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
A bidirectional transformation consists of a function get that takes a source (document or value) to a view and a function put that takes an updated view and the original source back to an updated source, governed by certain consistency conditions ...
Bidirectional Programming Languages
The need to edit source data through a view arises in a host of applications across many different areas of computing. Unfortunately, few existing systems provide support for updatable views. In practice, when they are needed, updatable views are usually implemented using two separate programs: one that computes the view from the source and another that handles updates. This rudimentary design is tedious for programmers, difficult to reason about, and a nightmare to maintain. This dissertation presents bidirectional programming languages, which provide an elegant and effective mechanism for describing updatable views. Unlike programs written in an ordinary language, which only work in one direction, programs in a bidirectional language can be run both forwards and backwards: from left to right, they describe functions that map sources to views, and from right to left, they describe functions that map updated views back to updated sources. Besides eliminating redundancy, these languages can be designed to ensure correctness, guaranteeing by construction that the two functions work well together. Starting from the foundations, we define a general semantic space of well-behaved bidirectional transformations called lenses. Then, building on this foundation, we describe a particular language for defining lenses on strings with syntax based on the familiar regular operators (union, concatenation, and Kleene star). We present extensions to the basic framework that address the subtle complications that arise when lenses are used to manipulate, data containing unimportant details, ordered data, and confidential data.
The mythical matched modules | Proceedings of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications
Certified compilers are complex software systems. Like other large systems, they demand modular, extensible designs. While there has been progress in extensible metatheory mechanization, scaling extensibility and reuse to meet the demands of full ...
Calculating with lenses | Proceedings of the 20th ACM SIGPLAN workshop on Partial evaluation and program manipulation
Functional programs are particularly well suited to formal manipulation by equational reasoning. In particular, it is straightforward to use calculational methods for program transformation. Well-known transformation techniques, like tupling or the ...
Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem: ACM Transactions on Programming Languages and Systems: Vol 29, No 3
We propose a novel approach to the view-update problem for tree-structured data: a domain-specific programming language in which all expressions denote bidirectional transformations on trees. In one direction, these transformations---dubbed lenses---map ...
Principal type-schemes for functional programs | Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
As part of the Digital Library's transition to Open Access, new features for researchers are available in the Premium Edition. Click here to learn more.
The Spoofax language workbench | Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion
As part of the Digital Library's transition to Open Access, new features for researchers are available in the Premium Edition. Click here to learn more.
Integrating functional and imperative programming | Proceedings of the 1986 ACM conference on LISP and functional programming
We present a new model, based on monads, for performing input/output in a non-strict, purely functional language. It is composable, extensible, efficient, requires no extensions to the type system, and extends smoothly to incorporate mixed-language ...
OCaml Programming: Correct + Efficient + Beautiful — OCaml Programming: Correct + Efficient + Beautiful
A textbook on functional programming and data structures in OCaml, with an emphasis on semantics and software engineering. This book is the textbook for CS 3110 Data Structures and Functional Programming at Cornell University. A past title of this book was “Functional Programming in OCaml”.
The Topos of Programming | Yon
A topos-oriented programming language. Native via MLIR and LLVM, with a content-addressed heap on the Leech lattice.
Programming Language Foundations in Agda – Table of Contents
This book is an introduction to programming language theory using the proof assistant Agda.
Profunctor Optics, a Categorical Update
Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. However, functional programming languages are arguably better described by enriched categories; and we have found that some structures in the literature are actually mixed optics, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.
