中央研究院 資訊科學研究所

Bidirectional programming is about writing special programs — called “lenses” — that can be executed in two directions. Lenses are designed for maintaining consistency between a data source and a view, the latter of which exposes a subset of information of interest in the former. Whenever the source or view is changed, the other side should be changed accordingly to restore consistency; such change propagation is thus bidirectional, and can be performed by the two directions of a lens. More interestingly, the two directions of a lens are required to be “well-behaved”, which roughly means that necessary changes, and only those, are made.

Surprisingly, despite having two directions, lenses are unidirectional in nature, in the sense that the behaviour of one particular direction determines that of the other direction. It was not clear how this unidirectionality could be exploited though, and the lens programmer had to explicitly specify the behaviour of both directions — until recently.

I will talk about our recent work on a Hoare-style logic that explains how the lens programmer can think unidirectionally but still maintain control over the whole bidirectional behaviour. More generally, this work serves as a bite-sized example of principled programming language design: programming languages should be designed to provide safety guarantees; moreover, they should be accompanied by reasoning principles that capture what the programmer should think about when using the languages, (preferably) formally and logically.

Hsiang-Shang ‘Josh’ Ko obtained his BSc in Computer Science and Information Engineering at National Taiwan University, Taiwan in 2009 and DPhil in Computer Science at the University of Oxford, UK in 2014, and is now an Assistant Professor by Special Appointment at the National Institute of Informatics, Japan.  His research interests include dependently typed programming, datatype-generic programming, bidirectional programming, program calculation, and functional programming & type theory.  He has published papers at renowned international conferences/workshops and journals in programming languages, recently including the Symposium on Principles of Programming Languages (POPL) and the Journal of Functional Programming (JFP).  Among other roles, he has served as a co-chair of the long-running Workshop on Partial Evaluation and Program Manipulation (PEPM) in 2018 and the cross-disciplinary International Workshop on Bidirectional Transformations (BX) in 2019.  (See his website 【Ko, Hsiang-Shang's Home Page】 for more information.)