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

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.

【Ko, Hsiang-Shang's Home Page】