[Agda] Value-recursive records?

[Andreas Abel]

 > 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.

Either this, or you can experiment with Agda's sized types, but I cannot 
foretell whether they will work for your case.

Best,
Andreas

On 2020-05-18 21:52, Joey Eremondi wrote:
> 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!
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>