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

[jonas.hoefer at stud.htwk-leipzig.de]

Hi Manuel,

thanks for your answer.

> Great that you're implementing scoped effects!

I'm glad you're interested! Scoped effects them self already work. Currently
I'm primarily trying to add effectful data structures to an implementation
without explicit scope delimiters, but this turned out to be quite difficult.

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

I already did some experiments with a level polymorphic implementation, but
things got complicated rather fast. As far as I can tell, parameterizing the
implementation just allows to push the problem up a level¹ (potentially
infinitely often; hence my original question about the practicality of
working
with increasing universe levels). Please correct me if I'm wrong about the
increasing levels. I did some more experiments and wrote up another sketch
using
universe polymorphism. It's probably not the cleanest implementation of
the idea,
but it demonstrates some consequences.

https://gist.github.com/JonasHoefer/0e3940b8c2a7264fde06aea5ddd967c0

It's now possible to pass data structures to scoped effects, but
implementation
comes with it's one set of problems thanks to the universe polymorphism. The
computation has to be lifted manually via up : Free ℓ C A →
Free (suc ℓ) C A
which has to be implemented per effect/via a type class to lift the shape
type.
Effects have to work on every level and therefore are of kind Setω.
Therefore
I'm not sure if this approach works when writing larger programs were
computations and data from different levels have to interact (especially
lifting
between two unrelated levels).

While writing the sketch I noticed another problem with this approach I'm not
sure how to deal with. When mapping a scoped effect over an effectful data
structure (a prime candidate would be sharing of nondeterminism) the level of
the outermost computation increases by the depth of the structure. This would
imply that the level of the result depends on data and that to find bounds
for
the level all branches of computation have to be traversed (but the
branches of
Free are described by positions functions i.e. the second element of
⟦ C ⟧ ...).
This seems impractical if not impossible.
At this point I unfortunately out of ideas on how to improve this approach.

Thanks,
Jonas

¹: See the last example. The Shape contains the captured computation
   (Free ...), but Free contains a Shape in the impure constructor.
   The second Free therefore has to be larger (which is now possible thanks
   to universe polymorphism).