Agda: Simplifying recursive definitions involving Thunk

Question

I'm trying to implement a type that represents a (possibly) infinite path on an infinite binary tree. The definition currently resembles that of Conat in the 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

Now I want to define a value which has longer repeating parts, e.g. LRRL. The best I can write right now is the following (which gets tedious quickly).

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

The goal

Define branchL' and branchR' so that the following passes type check and termination check.

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

The things I tried so far

Wrapping the part in a regular function doesn't work:

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

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

So I tried wrapping into a macro, but I can't find how to construct the term branchL λ where .force → path when path is given as a Term. The following doesn't work either:

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

Rather than writing branchL' and branchR', may I suggest mimicking what we do in Codata.Stream to define the unfolding of a cycle?

The key idea is that we can define auxiliary functions which use Thunk in their type and thus guarantee that they are using their argument in a guarded manner.

The first step is to define a small language of Choices one can make and give it a semantics in terms of 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

We can then lift this semantics to not only work for individual choices but also lists of choices:

open import Data.List

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

Now comes the crucial bit: if we have a non-empty list of choices, we know statically that the path it will lead to will be guarded.

open import Data.List.NonEmpty

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

Using this combinator we can seamlessly define cycle:

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

And then your example is obtained directly by using cycle:

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

I've put the code in a self-contained gist.