一句话：提出支持 data/codata 对称分解并可自动互译的语言，给出机器化验证与 IDE 实现。
表达式问题要求程序在按构造（函数式）或按析构（面向对象）分解之间取舍；现有语言通常不对称，切换分解困难。本文提出一种对称语言：用代数数据类型与模式匹配支持函数式分解，用 codata 类型与 copattern 匹配支持面向对象分解，并支持局部 (co)pattern matching（含局部匿名函数/对象定义）。其核心是可双向自动翻译：data 转 codata（destructorization）及反向（constructorization）。作者给出首个此类语言的机器化形式化，证明类型系统可靠、翻译保持类型与行为且互为逆；并从形式化中抽取经验证的实现，构造了直接支持这些翻译的 IDE。
The expression problem describes a fundamental trade-off in program design: Should a program's primary decomposition be determined by the way its domain objects are constructed ("functional" decomposition), or by the way they are destructed ("object-oriented" decomposition)? We argue that programming languages should not force one of these decompositions on the programmer; rather, a programming language should support both ways of decomposing a program in a symmetric way, with an easy translation between these decompositions. However, current programming languages are usually not symmetric and hence make it unnecessarily hard to switch the decomposition. We propose a language that is symmetric in this regard and allows a fully automatic translation between "functional" and "object-oriented" decomposition. We present a language with algebraic data types and pattern matching for "functional" decomposition and codata types and copattern matching for "object-oriented" decomposition, together with a bijective translation that turns a data type into a codata type ("destructorization") or vice versa ("constructorization"). We present the first symmetric programming language with support for local (co)pattern matching, which includes local anonymous function or object definitions, that allows an automatic translation as described above. We also present the first mechanical formalization of such a language and prove i) that the type system is sound, that the translations between data and codata types are ii) type-preserving, iii) behavior-preserving and iv) inverses of each other. We also extract a mechanically verified implementation from our formalization and have implemented an IDE with direct support for these translations.
@article{paperbot529,
title = {Decomposition diversity with symmetric data and codata},
author = {David Binder and Julian Jabs and Ingo Skupin and Klaus Ostermann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371098}
}