stream - 什么是 `where .force` ？

Question

我一直在尝试编写在 Streams 上运行的程序和它们的属性，但我觉得即使是最简单的事情我也被困住了。当我在标准库的 Codata/Streams 中查看 repeat 的定义时，我发现了一个我在 Agda 的任何地方都没有见过的结构:λ where .force →.

这里是用这个奇怪的特性定义的 Stream 的摘录:

repeat : ∀ {i} → A → Stream A i
repeat a = a ∷ λ where .force → repeat a

为什么 where 出现在 lambda 函数定义的中间？.force 如果从不使用它的目的是什么？

我可能会问文档中的内容，但我不知道如何搜索它。

此外，是否可以在某个地方找到使用“Codata”的文档和证明？谢谢!

Answer 1

Why does where appear in the middle of the lambda function definition?,

引用 the docs :

Anonymous pattern matching functions can be defined using one of thetwo following syntaxes:

\ { p11 .. p1n -> e1 ; … ; pm1 .. pmn -> em }

\ where p11 .. p1n -> e1 … pm1 .. pmn -> em

所以 λ where 是一个匿名模式匹配函数。 force 是Thunk 的字段.force 是一个 copattern在后缀表示法中(最初我在这里说了废话，但感谢@Cactus，它现在已修复，请参阅 his answer)。

Also, is there a place where I can find documentation to use "Codata" and proofs with it? Thanks!

查看这些论文

1. Normalization by Evaluation in the Delay MonadA Case Study for Coinduction via Copatterns and Sized Types
2. Equational Reasoning about Formal Languages in Coalgebraic Style
3. Guarded Recursion in Agda via Sized Types