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

【问题标题】：Agda: Simplifying recursive definitions involving ThunkAgda：简化涉及 Thunk 的递归定义
【发布时间】：2019-08-16 06:58:18
【问题描述】：

我正在尝试实现一种表示无限二叉树上（可能）无限路径的类型。目前的定义类似于标准库中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
-}

【问题讨论】：

标签： agda codata

【解决方案1】：

与其写branchL' 和branchR'，不如我建议模仿我们的工作在Codata.Stream 中定义循环的展开？

关键思想是我们可以定义使用Thunk的辅助函数类型，从而保证他们以一种受保护的方式使用他们的参数。

第一步是定义一个Choices的小语言，可以制作并给它 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。

【讨论】：