Decomposition diversity with symmetric data and codata
Decomposition diversity with symmetric data and codata
复制标题
DOI：
10.1145/3371098
复制
发表时间：
2019-12
影响因子：
--
通讯作者：
D. Binder;Julian Jabs;Ingo Skupin;K. Ostermann
中科院分区：
文献类型：
--
作者：
D. Binder;Julian Jabs;Ingo Skupin;K. Ostermann
表达式问题描述了程序设计中的一个基本权衡：程序的主要分解应该由其域对象的构造方式（“功能”分解）还是由它们的析构方式（“面向对象”分解）来确定？我们认为，编程语言不应该强迫程序员的这些分解之一，相反，编程语言应该支持这两种方式的分解程序的对称方式，这些分解之间的一个简单的翻译。然而，当前的编程语言通常是不对称的，因此使得切换分解变得不必要的困难。我们提出了一种语言，在这方面是对称的，并允许“功能”和“面向对象”的分解之间的全自动翻译。我们提出了一种语言，代数数据类型和模式匹配的“功能”分解和codata类型和copattern匹配的“面向对象”的分解，连同双射翻译，把一个数据类型转换成codata类型（“析构”），反之亦然（“构造”）。我们提出了第一个对称编程语言，支持本地（共）模式匹配，其中包括本地匿名函数或对象定义，允许如上所述的自动翻译。我们还提出了这样一种语言的第一个机械形式化，并证明了i）类型系统是健全的，数据和codata类型之间的翻译是ii）类型保持，iii）行为保持和iv）彼此的逆。我们还从我们的形式化中提取了一个经过机械验证的实现，并实现了一个直接支持这些翻译的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.