其他问题的答案解释了所有Agda程序都在终止.
我的理解是,任何有效的Adga程序的终止都是由Agda的高级依赖类型系统管理的要求.这个严格的要求似乎可以消除许多错误.但是,似乎禁止非终止程序会阻止语言表达一些有用的程序.例如,服务器是一种程序,其中非终止的可能性是其功能的关键方面.
是否可以在Agda中编写服务器？我认为在这种情况下,通过将服务器设置为最终终止于十亿年或其他东西,几乎可以绕过非终止限制.但我想知道是否有一些类型系统的技巧可以允许Agda表达一些这样的非终止程序,也许只有那些达到某种静态闭合循环的程序.如果没有,那么理论上可以发明这样的技巧吗？
没有这种可能性,似乎Agda概念在它可以表达的有用程序集中基本上受到限制.
所有Agda程序都需要全部.意思就是:
生产力意味着对过程的任何有限观察都需要在有限的时间内返回答案.服务器将是一个核心程序,为用户提供他们可以发出的一组命令,在有限时间内返回响应,并(如果适用)提供下一组命令.