Agda：简化涉及 Thunk 的递归定义

Question

我正在尝试实现一种表示无限二叉树上的（可能）无限路径的类型。该定义目前类似于 stdlib 中 Conat 的定义。

open import Size
open import Codata.Thunk

data BinaryTreePath (i : Size) : Set where
  here : BinaryTreePath i
  branchL : Thunk BinaryTreePath i → BinaryTreePath i
  branchR : Thunk BinaryTreePath i → BinaryTreePath i

zero : ∀ {i} → BinaryTreePath i
zero = branchL λ where .force → zero

infinity : ∀ {i} → BinaryTreePath i
infinity = branchR λ where .force → infinity

现在我想定义一个重复部分较长的值，例如LRRL。我现在能写的最好的是以下内容（很快就会变得乏味）。

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 =
  branchL λ where .force → branchR λ where .force → branchR λ where .force → branchL λ where .force → sqrt2

-- or --

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 = branchL λ where
  .force → branchR λ where
    .force → branchR λ where
      .force → branchL λ where
        .force → sqrt2

目标

定义 branchL' 和 branchR' 以便以下通过类型检查和终止检查。

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 = branchL' (branchR' (branchR' (branchL' sqrt2)))

到目前为止我尝试过的东西

将零件包装在常规函数中不起作用：

branchL' : (∀ {i} → BinaryTreePath i) → (∀ {j} → BinaryTreePath j)
branchL' path = branchL λ where .force → path

zero' : ∀ {i} → BinaryTreePath i
zero' = branchL' zero'
--               ^^^^^ Termination checking failed

所以我试着包装成一个宏，但是当 path 作为 Term 给出时，我找不到如何构造术语 branchL λ where .force → path。以下也不起作用：

open import Agda.Builtin.Reflection
open import Data.Unit
open import Data.List

macro
  branchL' : Term → Term → TC ⊤
  branchL' v hole = do
    path ← unquoteTC v
    term ← quoteTC (branchL λ where .force → path)
    --                                       ^^^^ error
    unify hole term

{- error message:
Cannot instantiate the metavariable _32 to solution BinaryTreePath
.j since it contains the variable .j which is not in scope of the
metavariable or irrelevant in the metavariable but relevant in the
solution
when checking that the expression path' has type BinaryTreePath .j
-}

Answer 1

与其写成 branchL' 和 branchR'，我可以建议模仿我们所做的在Codata.Stream中定义一个循环的展开？

关键思想是我们可以定义辅助函数，在它们的函数中使用Thunk 类型，从而保证他们以谨慎的方式使用他们的论点。

第一步是定义一种 Choice 的小型语言，并提供给它根据 BinaryTreePath:

的语义

data Choice : Set where
  L R : Choice

choice : ∀ {i} → Choice → Thunk BinaryTreePath i → BinaryTreePath i
choice L t = branchL t
choice R t = branchR t

然后我们可以提升这种语义，使其不仅适用于个人选择，而且选择列表：

open import Data.List

_<|_ : ∀ {i} → List Choice → BinaryTreePath i → BinaryTreePath i
[]       <| t = t
(c ∷ cs) <| t = choice c (λ where .force → cs <| t)

现在到了关键点：如果我们有一个非空的选择列表，我们知道静态地说，它将通向的路径将受到保护。

open import Data.List.NonEmpty

_⁺<|_ : ∀ {i} → List⁺ Choice → Thunk BinaryTreePath i → BinaryTreePath i
(c ∷ cs) ⁺<| t = choice c (λ where .force → cs <| t .force)

使用这个组合子我们可以无缝定义cycle:

cycle : ∀ {i} → List⁺ Choice → BinaryTreePath i
cycle cs = cs ⁺<| (λ where .force → cycle cs)

然后你的例子直接用循环得到：

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 = cycle (L ∷ R ∷ R ∷ L ∷ [])

我把代码放在 self-contained gist.

Agda：简化涉及 Thunk 的递归定义

Agda: Simplifying recursive definitions involving Thunk

agda

codata

目标

到目前为止我尝试过的东西