[Agda] Value-recursive records?

[Joey Eremondi]

Disclaimer: X-posted on Stack Overflow:
https://stackoverflow.com/questions/61877871/agda-constructing-a-recursive-record-value

I'm wondering, is it possible to have records whose *values* depend on each
other, without being recursively defined in terms of types?

Basically, I have a record type that looks like this:

record SomeRec (a : Set) : Set where
   method1 : a -> a -> Foo
   method2 : a -> a -> Bar
  ...
  method n : a -> a -> Baz

where n is large enough that I want to actually bundle all of these up as
records, instead of just having a bunch of mutually recursive functions.
(Also, I'm using SomeRec as an instance argument).

Notably, SomeRec is not recursive: none of its fields types refer to
SomeRec.

Right now, I have a Description D, where FD : Set -> Set is the functor
described by D. What I'm trying to show is the following:

  muRec : ( FRec : (a : Set) -> SomeRec a -> SomeRec (FD a) ) -> SomeRec
(mu D)

That is, if I can take a (SomeRec a) to a (SomeRec (F a)), then I can tie
the knot recursively and show the instance for the whole thing.

In principle this can be done: each recursive call to a field of SomeRec
would happen with strictly smaller arguments. If I were to just have 10
mutually recursive methods, it would work. But if I try to build the
record, I end up passing muRec to FRec *without its arguments decreasing*.

So, what I'm wondering is: is there a way to show that this is
well-founded? Can induction or coinduction help, even though the record
type is not inductive or coinductive?

My current approach is to make a size-indexed version of D, and build
SomeRec for size n out of SomeRec for size < n. But this is dramatically
increasing the complexity of what I'm doing, and I'm having to use Brouwer
ordinals to get size bounds on what I'm doing. So I'm wondering if there's
a better way.

Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200518/c3891c1b/attachment.html>