Agda: упрощение рекурсивных определений с использованием Thunk

Question

Я пытаюсь реализовать тип, который представляет (возможно) бесконечный путь в бесконечном двоичном дереве. Определение в настоящее время напоминает определение Conat в stdlib.

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

Поэтому я попытался обернуть в макрос, но я не могу найти, как построить термин branchL λ where .force → path когда path дается как Term, Следующее также не работает:

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 ∷ [])

Я поместил код в отдельную суть.