Typed Tagless Final Interpreters
Typed Tagless Final Interpreters
复制标题
类型化无标签最终解释器
DOI：
10.1007/978-3-642-32202-0_3
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
O. Kiselyov
中科院分区：
文献类型：
--
作者：
O. Kiselyov
文献[6]中所谓的“类型化无标记终结法”收集并完善了一些用类型化元语言表示类型化高阶语言的技术，以及类型保持的解释、编译和部分求值。该方法替代了将对象语言编码为(广义的)代数数据类型的传统编码或“初始”编码。这两种方法都允许对一个表达式进行多种解释、求值、美化等。最终的编码表示所有且只有类型化的对象项，而不求助于泛化的代数数据类型、依赖类型或其他花哨的类型。最终的编码允许我们添加新的语言形式和解释，而不会破坏现有的术语和解释器。
这些课堂讲稿缓慢而详细地介绍了最终的方法，重点介绍了可扩展性、表达式问题的解决方案以及看似不可能的模式匹配。我们将该方法进一步发展到类型安全强制转换、运行时类型表示、动态和类型重建。最后，我们给出了类型导向的部分求值、类型和效果系统的编码以及线性Lambda演算的例子。
The so-called ‘typed tagless final' approach of [6] has collected and polished a number of techniques for representing typed higher-order languages in a typed metalanguage, along with type-preserving interpretation, compilation and partial evaluation. The approach is an alternative to the traditional, or ‘initial' encoding of an object language as a (generalized) algebraic data type. Both approaches permit multiple interpretations of an expression, to evaluate it, pretty-print, etc. The final encoding represents all and only typed object terms without resorting to generalized algebraic data types, dependent or other fancy types. The final encoding lets us add new language forms and interpretations without breaking the existing terms and interpreters.
These lecture notes introduce the final approach slowly and in detail, highlighting extensibility, the solution to the expression problem, and the seemingly impossible pattern-matching. We develop the approach further, to type-safe cast, run-time-type representation, Dynamics, and type reconstruction. We finish with telling examples of type-directed partial evaluation and encodings of type-and-effect systems and linear lambda-calculus.