浅谈可逆编程与双向编程
可逆编程
可逆编程,如同其名,意思是程序可逆。
在日常编程中我们会接触到很多可逆的概念。例如说JSON格式的编码与解码,既可以从JSON解析到特定语言的特定数据结构,也可以反向序列化到JSON;例如说前缀和,例如[1, 2, 3]
到[1, 3, 5]
,双向来回都可以做到;例如说压缩解压缩,加密解密,等等等等。当然,逆向执行之后并不要求与原来的结果一模一样,只需要同构即可,比如JSON里每个逗号是否换行显然不影响它们代表同样的数据结构,虽然文件并不完全一样。
对于可逆编程,如果我们把两个方向的程序分开写是完全没有问题的,也是我们一直在做的。但是一般而言,程序越长越容易出错,而且我们也无法保证两个程序能够一一对应,除非用上定理证明,因此最好可以把这个可逆的保证融入在编程语言中。这也是当下编程语言研究中的一个领域。感兴趣的朋友可以读一下Wang教授和Matsuda教授的Sparcl语言。
双向编程
双向编程即是对于程序的输入与输出之间有着双向的联系,其根本意义在于保持两个数据源的数据同步。
假设我们有两个数据源,且它们具有一定关系,例如一个数字以及这个数字的两倍。当一个数据源发生改变,我们需要找出如何对另一个数据源进行更改,使得这两个数据源始终保持原有的关系,在我们的例子中即是要保证第二个数字是第一个数字的两倍,第一个数字是第二个数字的一半。
双向编程最初的起源来自于数据库。对于数据库的查询,我们有视图这一概念。视图相当于是一个已经聚合的数据,其中的数据始终是与数据库中的数据同步的,这便是这两个数据源之间的关系。例如一个表包含员工的个人信息,另一个表包含员工的上下级关系。如果我们需要根据特定员工查询其上司的个人信息,我们就需要聚合一些信息,产生了一个视图。但我们是否有可能通过修改视图,从而修改数据库呢?例如我们直接视图中上司的姓名,那么对应的源数据库应该作何变化?是根据这个新的姓名重新创建一个员工,还是修改上司的姓名呢?诸如此类的一系列问题,即为双向编程最初的View Update Problem,可以追溯到1981年的论文。
对于函数式编程而言,一个常见的概念是Lens,这可能也是双向编程最为人所熟知的应用。Lens,即透镜,会使源产生一个像。而在编程中,常见的目的则是产生数据结构的某一个局部的像,从而对局部进行修改。例如说如下代码:
case class Student(id: String, age: Int, address: String)
def getAge(s: Student) = s.age
def updateAge(s: Student, age: Int) = s.copy(age = age)
以上代码中我们定义了一个对应学生的数据结构,包含了学号、年龄、地址,以及获取地址的函数和更新地址的函数。这两个函数共同组成了一个透镜,允许我们生成一个像(年龄),并通过修改像来修改最初的对象(学生)。
如先前所述,两个数据源之间是有关系的。对于透镜而言,一般有两个定律,来保证源与像之间的对应关系:
- get(put(source, view)) = view,意即修改像后对应的源所产生的像应为修改后的像
- put(source, get(source)) = source,意即若像未发生改变,则源亦不发生改变
透镜是可以组合的。设想如果学生的地址不是一个简单的字符串,而是一个复杂的数据结构时,如果我们对于每个学生需要了解其居住地所在城市,通过组合从学生信息中获取学生地址的透镜与从地址中获取所在城市的透镜,我们便可以获取到一个新的透镜。更重要的是,只要这两个透镜定律,则通过特定组合子组合而成的透镜同样将会符合透镜所需满足的定律。至于哪些组合子符合这个条件,以及如何增强语言的支持,简化透镜组合的定义也是当下编程语言研究中的一个领域。感兴趣的朋友可以读一下Wang教授和Matsuda教授的HOBiT语言。