doge

Zirun Zhu's
Homepage

Education

2014 - present

PhD student,
Department of Informatics,
School of Multidisciplinary Sciences,
SOKENDAI (The Graduate University for Advanced Studies)

2010 - 2014

Bachelor of Engineering,
Computer Science and Technology,
University of Science and Technology of China


Research

My current research is to make practical use of putback-based bidirectional transformations (BX for short), which can serve as an elegant approach to synchronising data in different formats. In particular, I am focusing on the synchronisation problem between the program text and its abstract syntax representation. I am developing a declarative domain specific language – BiYacc – to help users easily write a single & simple program denoting both a parser and a reflective printer consistent with each other. BiYacc is based on BiGUL, a robust underlying system served for bidirectional programming formerly created in our lab.


Academic activities

[POPL 2019 (draft, rejected)]
“Retentive Lenses”
Zirun Zhu, Zhixuan Yang, Hsiang-Shang Ko, and Zhenjiang Hu

Research paper (draft) Rejected by POPL 2019

Based on Foster et al.'s [2007] lenses, various bidirectional programming languages and systems have been developed for helping the user to write correct data synchronisers. The two well-behavedness laws of lenses, namely Correctness and Hippocraticness, are usually adopted as the guarantee of these systems. While lenses are designed to retain information in the source when the view is modified, well-behavedness says very little about the retaining of information, since Hippocraticness only requires that the source be unchanged if the view is not modified. Thus nothing about retaining is guaranteed when the view is changed.

To address this problem, we propose an extension of the original lenses, called retentive lenses, satisfying a new Retentiveness law which can guarantee that if parts of the view are unchanged, then the corresponding parts of the source are retained as well. As a concrete example of retentive lenses, we present a domain-specific language for writing tree transformations. We prove that the pair of get and put functions generated from a program in our DSL forms a retentive lens. We study the practical use of retentive lenses by implementing in our DSL a synchroniser between concrete and abstract syntax trees for a small subset of Java, and demonstrate that Retentiveness helps to enforce the retaining of comments and syntactic sugar in code refactoring.

[ICFP 2018 (draft, rejected)]
“Retentive Lenses”
Zirun Zhu, Hsiang-Shang Ko, Zhixuan Yang, and Zhenjiang Hu

Research paper (draft) Rejected by ICFP 2018

Researchers in the field of bidirectional transformations have studied data synchronisation for a long time and proposed various properties, of which well-behavedness is the most fundamental. However, well-behavedness is not enough to characterise the result of an update (performed by put), regarding what information should be retained in the updated source. The root cause is that the property, Hippocraticness, for guaranteeing the retention of source information is too ‘global’, only requiring that the whole source should be unchanged if the whole view is.

In this paper we propose a new property retentiveness, which enables us to directly reason about the retention of source information locally. Central to our formulation of retentiveness is the notion of links, which are used to relate fragments of sources and views. These links are passed as additional input to the extended put function, which produces a new source in a way that preserves all the source fragments attached to the links. We validate the feasibility of retentiveness by designing a domain-specific language (DSL) supporting mutually recursive algebraic data types. We prove that any program written in our DSL gives rise to a pair of retentive get and put. We show the usefulness of retentiveness by presenting examples in two different research areas: resugaring and code refactoring.

[SLE 2016]
“Parsing and Reflective Printing, Bidirectionally”
Zirun Zhu, Yongzhe Zhang, Hsiang-Shang Ko, Pedro Martins, João Saraiva, and Zhenjiang Hu

Research paper SLE 2016

Language designers usually need to implement parsers and printers. Despite being two intimately related programs, in practice they are often designed separately, and then need to be revised and kept consistent as the language evolves. It will be more convenient if the parser and printer can be unified and developed in one single program, with their consistency guaranteed automatically.

Furthermore, in certain scenarios (like showing compiler optimisation results to the programmer), it is desirable to have a more powerful reflective printer that, when an abstract syntax tree corresponding to a piece of program text is modified, can reflect the modification to the program text while preserving layouts, comments, and syntactic sugar.

To address these needs, we propose a domain-specific language BiYacc, whose programs denote both a parser and a reflective printer for an unambiguous context-free grammar. BiYacc is based on the theory of bidirectional transformations, which helps to guarantee by construction that the pairs of parsers and reflective printers generated by BiYacc are consistent. We show that BiYacc is capable of facilitating many tasks such as Pombrio and Krishnamurthi’s “resugaring”, simple refactoring, and language evolution.

[FLOPS 2016 (poster presentation)]
“BiYacc: Roll Your Parser and Reflective Printer into One.”
Zirun Zhu, Yongzhe Zhang

Poster presentation FLOPS 2016

Language designers usually need to implement parsers and printers. Despite being two intimately related programs, in practice they are often designed separately. This leads to a maintenance problem: as a language evolves, both its parser and printer need to be revised and kept consistent, which is a routine but error-prone task.

To address the problem, we propose a new domain-specific language BiYacc, whose programs denote both a parser and a “reflective” printer for synchronising the concrete and abstract representations. BiYacc is based on the theory of bidirectional transformations, which guarantees that the pairs of parsers and printers generated by BiYacc are always consistent in a precise sense. The “reflective” printer generated from a BiYacc program is distinct from traditional printers: it takes not only an abstract syntax tree (AST) but also a concrete syntax tree (CST), and produces an updated CST into which information from the AST is properly embedded. Internally, BiYacc is implemented in terms of BiGUL, a core bidirectional programming language which has been formally proved correct and implemented as a Haskell library. The consistency of parsers and printers is thus derived from the correctness of BiGUL for free.

[BX 2015]
"BiYacc: Roll Your Parser and Reflective Printer into One."
Zirun Zhu, Hsiang-Shang Ko, Pedro Martins, João Saraiva, and Zhenjiang Hu

Tool paper BX 2015

Language designers usually need to implement parsers and printers. Despite being two related programs, in practice they are designed and implemented separately. This approach has an obvious disadvantage: as a language evolves, both its parser and printer need to be separately revised and kept synchronised. Such tasks are routine but complicated and error-prone. To facilitate these tasks, we propose a language called BiYacc, whose programs denote both a parser and a printer. In essence, BiYacc is a domain-specific language for writing putback-based bidirectional transformations — the printer is a putback transformation, and the parser is the corresponding get transformation. The pairs of parsers and printers generated by BiYacc are thus always guaranteed to satisfy the usual round-trip properties. The highlight that distinguishes this reflective printer from others is that the printer — being a putback transformation — accepts not only an abstract syntax tree but also a string, and produces an updated string consistent with the given abstract syntax tree. We can thus make use of the additional input string, with mechanisms such as simultaneous pattern matching on the view and the source, to provide users with full control over the printing-strategies.


Contact

Programming Research Lab, Room 1611,
National Institute of Informatics,
2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo, 101-8430, Japan

Email:


Reference

Prof Zhenjiang Hu (advisor)

Department of Informatics,
School of Multidisciplinary Sciences,
SOKENDAI (The Graduate University for Advanced Studies)