Should allow singleton sessions to carry a weighting function, e.g. lists can be weighted by their length, bytestrings by their length, trees by their size, etc. This can be used in loop to allow for a more refined notion of contraction map.

Currently, opening a file for writing causes it to be opened immediately, not on commit. This may cause a visible side-effect, e.g. creating or clearing an existing file. Perhaps the semantics should enforce that files are always opened as tmp files, and are copied to their destination when closed? We could save the filename in a ref to be opened on a later commit, but this would mean that Agda handles aren't Haskell handles, which complicates the FFI layer.

It'd be great if Everything.agda was included importing all the relevant code, allowing for easy type-checking. By proxy, it should of course work with recent (2.4.2) Agda ;)

IO should have universe-polymorphic type (requires compiler support).

Currently I'm claiming all kinds of categorical structure for processes, without proof. Proofs are good. We like proofs.

Currently the only primitive for reading from a handle reads all the data on commit. We should also provide support for parser combinators to parse from a handle, and leave the rest of the handle untouched.

Can we use Agda 2.2.8's syntax mechanism to define a binder similar to Haskell's do?

Looping is handled as an ad-hoc addition -- really it should be built using a fixed point or trace combinator.

Should we have a separate type for file paths, rather than just String? Can we give some static guarantees about file usage?

Currently there's an ad-hoc collection of inclusions such as (optional S) is included in (many S). Can we handle this via subtyping?

Currently the check for being a contraction map is dynamic rather than static. Dynamic checks are bad!

Should exceptions only be allowed in commit? Should actions be rolled back by an exception?

Currently the only codec is utf8, and it's hard-wired into putStr and getStr. There's also no handling of CR/NL issues.

Figure out a way to use a Haskell numeric type for weights, rather than Agda unary naturals.

Currently the inf postulate has no COMPILED pragma associated with it, as this requires Agda 2.2.8. When we decide not to support 2.2.6 any more we can add the pragma.

Are the commit actions per-process? per-thread? per-spark? Currently they're per-process but this may not be the desired semantics. We also need to think about how commit interacts with concurrency controls such as MVars.