luo*_*990 11 lazy-evaluation idris codata
我发现Lazy并Inf非常接近:
Lazy和Inf密切相关(事实上,底层实现使用相同的类型).实践中唯一的区别在于整体检查,其中Lazy被删除(即通常检查术语是否终止,忽略懒惰注释),Inf使用生产力检查器,其中任何延迟的使用必须是构造函数保护.
如所描述的以上,底层实现Lazy和Inf是同一个,唯一的区别是大约整体检查.
我认为总是使用Inf似乎更自然,这更接近我们在Haskell中使用的懒惰,并想知道我们必须使用的生产场景是什么Lazy- 它总是进行深度整体检查？