Productive Coprogramming with Guarded Recursion

作     者：Atkey, Robert McBride, Conor 

作者机构：Univ Strathclyde Glasgow G1 1XQ Lanark Scotland 

出 版 物：《ACM SIGPLAN NOTICES》 (ACM SIGPLAN Not.)

年 卷 期：2013年第48卷第9期

页      面：197-208页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：EPSRC [EP/J014591/1] Funding Source: UKRI 

主　　题：Languages Theory Types Recursion coalgebras corecursion guarded recursion total functional programming 

摘      要：Total functional programming offers the beguiling vision that, just by virtue of the compiler accepting a program, we are guaranteed that it will always terminate. In the case of programs that are not intended to terminate, e. g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a program generates an infinite amount of data, each piece will be generated in finite time. The theoretical underpinning for productive programming with infinite output is provided by the category theoretic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well-founded data like finite lists and trees. Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers, which ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compositional, and severely complicate coprogramming. Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to coprogramming. However, as we show, guarded recursion by itself is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano s guarded recursion. Clock variables allow us to close over the generation of infinite codata, and to make finite observations, something that is not possible with guarded recursion alone.