Separate scope from effects?

[mikeshulman]

This is the third time I've wanted to ask this. The first two times, I found another way to do what I wanted, and maybe I would be able to do that again; but since it keeps happening I thought I'd at least ask.

The module Scope does two things:

1. It defines a notion of "scope state" that stores a visible namespace, an export namespace, and an export prefix, and functions that manipulate scope states.
2. It exposes these functions through an interface of algebraic effects.

Why not separate these two things into two modules? Algebraic effects are great, but they don't do everything perfectly, and I think it's reasonable for a user to want to use scopes without them, managing the scope state themselves in a different way (e.g. explicitly or monadically).

Here are the three reasons I've wanted this so far:

1. Algebraic effects are great for combining with other algebraic effects, but not so great for combining with other kinds of monads, like a continuation monad, a nondeterministic choice monad, or a backtracking monad. In my case, the fmlib_parse library uses a monad for parsing combinators that I believe uses some kind of continuations for backtracking. It doesn't make sense to have algebraic effects be performed inside such monadic functions, so I wasn't able to write a parser that would parse a sequence of definitions, adding each of them to the scope as it went so that it would be available while parsing later definitions -- whereas the fmlib_parse monad does already include a monadic user state that is automatically backtracked across correctly. In this case, I was fortunately able to convince the author of fmlib to implement a partial parser so that I can parse a single definition and stop, perform an effect to add it to the scope, and then restart the parser where it left off. But combining with monads from other libraries seems like a general reason why one might want to use scopes without algebraic effects.
2. Especially in the absence of an effect system, it is easy to make mistakes regarding what effect handlers a given computation will be performed in the context of, and hence what scope it will be in. In my case, my functions for pretty-printing a term do a lookup into the scope to find in-scope names for defined constants, while the error messages I report with Asai use these pretty-printing functions to mention the terms relevant to the error. However, this led to Mutex errors when I started using scope sections. I believe the issue was that the Asai effects carry a function formatter -> unit rather than a string, which is then executed by the Asai handler -- and the Asai handler is outside the new Scope handler put in place by section, so the lookups were going instead to the parent scope, which is locked during section. I worked around this by refactoring my code so that the lookups, at least, happen before the data is packaged up into a formatter -> unit, but if I were managing scope state more explicitly I don't think such a bug could have happened in the first place.
3. Now I am thinking about how to support "undo" for an interactive ProofGeneral mode like Coq's that can make definitions and then retract them. Like other kinds of backtracking, this seems like one of those places where purely functional code is the way to go. If I could access the explicit scope state objects, I could store a (backwards) list of them, using the last one for lookups and adding an updated one onto the end every time a new definition is made, and then just peel a bunch off the end when I undo. I am not sure how to do something like this when the only way to access scope state is through algebraic effects. Maybe there is a way (and I'd be interested to hear suggestions), but I suspect that the non-effectual version will be more straightforward and less error-prone (for me, at least).

[favonia]

Ideally, the module containing the "pure" scopes should be called "Scope", and the module implementing lexical scoping should be called "Scoping". But the latter is taking the name "Scope" now. @mikeshulman Do you feel "ScopeData" is an acceptable name before we overhaul the whole thing? (I'm really bad at naming.)

[mikeshulman]

I'm fine with ScopeData. Thanks!

[mikeshulman]

The comment in January suggested you would be open to a change like this. If that's right, do you have a guess about when it might happen? As in, "next month" vs "next year" vs "maybe someday"? So I can decide whether I should come up with my own workaround when I'm ready to implement "undo".

[favonia]

@mikeshulman Thanks for the wake-up call. I was expecting "next month (Feb)" but something personal is dragging me all along. My personal issues are still not resolved but I should have more bandwidth after the semester ends (say, mid-May). My hope is that I can catch up with everything in June. There's really nothing difficult in implementing a pure "ScopeData" and then the current "Scope" on top of it. Once again I apologize for the huge delay in this project (and many other projects).

[mikeshulman]

I'm sorry to hear you're dealing with personal issues; I hope everything works out okay. Thanks for the update; I'll wait for the summer then.

[favonia]

@mikeshulman Hi, I'm getting back on track, and here's one question when I was trying to pin down the API:

The Scope module actually uses more than the scoping effects. It also incorporates the name-modifying effects (shadowing, etc.) from the Modifier module. Do you want a purely functional ScopeData module that uses none of these effects, or is it okay to use still the name-modifying effects?

[mikeshulman]

I think I don't completely understand what the name-modifying effects are for. It looks to me like they are basically a way for the programmer to tell yuujinchou what to do when a name is not found or tries to shadow another one. What is the reason for making these handled by effects rather than by ordinary functions in the module type Param that the programmer would specify when they implement it?

[favonia]

@mikeshulman Those can help implement the suppression of warnings about shadowing, such as OCaml's open!. But other than dynamic warning suppression, I guess we were just trying to use effects everywhere.

[mikeshulman]

Ok, so these effects are basically a Reader to avoid passing arguments around between functions. I don't think that should cause any problems with what I have in mind, if you want to keep them as effects.

[mikeshulman]

Thinking about this some more, and looking at the code again, I have an even simpler suggestion. What Scope does with a pair of namespaces is not complicated and I could easily do it myself by hand, and I might even prefer that so that I can see and control more clearly what is going on. Indeed, even if you implement a ScopeData, I might end up wanting to roll my own later anyway.

The one change on the Yuujinchou side that would make this a bit more natural would be for Modifier.Make to export versions of the Trie.union_* functions that automatically supply Perform.shadow as its merger argument, the way the Scope functions that call these functions do. I think it makes sense to do this at the level of Modifier since anyone using the modifier engine is likely to want this behavior for merging, whether or not they are using Scope on top of it.

[favonia]

The one change on the Yuujinchou side that would make this a bit more natural would be for Modifier.Make to export versions of the Trie.union_* functions that automatically supply Perform.shadow as its merger argument, the way the Scope functions that call these functions do. I think it makes sense to do this at the level of Modifier since anyone using the modifier engine is likely to want this behavior for merging, whether or not they are using Scope on top of it.

That makes sense. I have to say I was a bit troubled by explicitly passing every function (after removing algebraic effects) for two reasons:

1. I am not sure what the purpose of ScopeData anymore because it does almost nothing, and
2. The API looks very ugly with lots of repeated arguments.

[favonia]

@mikeshulman I am marking this as "done", and I look forward to the code you are going to write.

[mikeshulman]

I'll be sure to let you know when I write it!