[Agda] Size Issue when Modelling Effectful Data Structures and Computations

[Manuel Bärenz]

Hi Jonas,

Great that you're implementing scoped effects!

I'm not the greatest Agda expert, but I had a similar problem once and I
solved it by making all set levels as polymorphic as possible. You'd
have to index (or parametrise? I always confuse them) every record type
by set levels, e.g. record Container {l} : Set (lsuc l) or something
like that.

Manuel

On 11.09.20 15:08, jonas.hoefer at stud.htwk-leipzig.de wrote:
> Hello,
>
> I have a problem involving universe levels.
>
> I'm trying to implement scoped effects (based on "Effect Handlers in Scope"
> by Wu et al.) in Agda. I follow the the higher order approach from the paper.
> It models effects using a free monad over a higher order functor.
>
> The approach leads to a tree structure with an existential type in
> (potential) every node. I would like to store special data types which use
> the tree type itself in the existential type variable, but this obviously
> leads to size issues. I have outlined the problem and some ideas in the
> following gist. It contains a minimal example of the structure and a larger
> example for context.
>
> https://gist.github.com/JonasHoefer/f0a61744b1cb9cf1f649cfe3bcf414bb
>
> I'm not sure how to proceed at this point. Are there any standard approaches
> to deal with or transform this kind of size issues?
> Storing arbitrary types of the same level is of course not possible, but I'm
> dealing with just a limited set of "too large" data types (i.e. just those
> which continue the tree). This is not witnessed by the implementation but I
> don't know how to use this fact.
> Would it be possible (and practical) to work with always increasing universe
> levels?
>
> Thanks,
> Jonas
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>