Copatterns programming infinite structures by observations
Copatterns programming infinite structures by observations
复制标题
通过观察对无限结构进行共模式编程
DOI：
10.1145/2480359.2429075
复制
发表时间：
2013
影响因子：
--
通讯作者：
Abel A
中科院分区：
文献类型：
--
作者：
Abel A
归纳数据库提供了通过构造函数定义有限数据（如有限列表和树）的机制，并允许程序员通过模式匹配分析和操作有限数据。在本文中，我们开发了一个双重的方法来处理无限的数据结构，如流。无限数据存在于表示最大不动点的共归纳数据空间中。与由构造函数定义的有限数据不同，我们通过观测定义无限数据。对偶模式匹配，用于分析有限数据的工具，我们开发的概念copattern匹配，它允许我们合成无限的数据。这导致了一个对称的语言设计，有限和无限的数据模式匹配可以mixed.We提出了一个核心语言的无限结构的观察，其操作语义的基础上（共）模式匹配和描述覆盖copatteries。我们的语言自然支持按名称调用和按值调用解释，并且可以无缝集成到Haskell和ML等现有语言中。我们证明了我们的语言类型的合理性和草图copatteries如何打开新的方向，解决问题的相互作用，共归纳和依赖类型。
Inductive datatypes provide mechanisms to define finite data such as finite lists and trees via constructors and allow programmers to analyze and manipulate finite data via pattern matching. In this paper, we develop a dual approach for working with infinite data structures such as streams. Infinite data inhabits coinductive datatypes which denote greatest fixpoints. Unlike finite data which is defined by constructors we define infinite data by observations. Dual to pattern matching, a tool for analyzing finite data, we develop the concept of copattern matching, which allows us to synthesize infinite data. This leads to a symmetric language design where pattern matching on finite and infinite data can be mixed.We present a core language for programming with infinite structures by observations together with its operational semantics based on (co)pattern matching and describe coverage of copatterns. Our language naturally supports both call-by-name and call-by-value interpretations and can be seamlessly integrated into existing languages like Haskell and ML. We prove type soundness for our language and sketch how copatterns open new directions for solving problems in the interaction of coinductive and dependent types.