我在前一个问题的答案中争论说,可以在Haskell中表示原始递归函数(PRF)和single或的单个额外值的并集undefined.这个论点是基于原始递归函数的公理结构的直接翻译; 它需要一些语言扩展和关于函数arity的类型级推理.是否有可能在更惯用的Haskell中表示一组等效的原始递归函数？
理想情况下,PRF的惯用语表示应能满足以下所有条件:
Category实例除了原始递归的要求
undefined输入功能都undefined适用于所有输入.这将PRF集限制为单个不可避免的额外值⊥,而不是包含多个部分递归函数.这意味着while循环或类似的部分递归函数的任何定义都应该是undefined.我注意到原始递归函数的公理就像Category法则一样,Arrow没有arr(实际上它与之相反arr),而且只有自然数才有效的有限形式的循环.