The many parser combinator falsely claims to be non-div

[AZMCode]

The std/text/parse/many parser combinator can diverge, along with its many1 variant.

This is pretty easily observable by passing in a parser which matches zero characters of a string yet succeeds, for example, whitespace0 on a string which contains non-whitespace characters.

Should the div effect be added to the effect annotation on the function?

[TimWhiting]

Good point. In general you cannot say anything about termination of the many parser without knowing whether the child parser makes progress on the input by consuming a few characters. So we have to err one way or the other. The "safe" way would to be assume nothing, and don't remove the div effect. However that would mean all parsers would have to be annotated as divergent, even if they do make progress. If the grammar is designed well, all parsers should make progress, or else they will not terminate on some inputs which would be very bad.

So the question is, do we go for the safe annotation, or for the annotation that reflects what grammars should be designed for. In this case Daan chose the second, which I'm inclined to agree with for a few reasons:

1. There is not really way for type checking to reason at this high of a level unless you get into dependent types (good in some application areas, but not what Koka is designed for).
2. Since all child parsers used with many should be designed to make progress or fail, no grammar should be divergent in practice (unless the underlying stream of characters is divergent - but that is not the case here, and is not the question).

So the intent of the claim that the many parser makes that it is non-div comes with the disclaimer that it should never be used with children parsers that don't consume input. (That probably should be more clearly stated in the documentation for many).

My suggested resolution to this issue (which definitely could lead to a real problem when working on a parser - though not a problem that wouldn't also exist in a language without effect types) would be to create an linter that checks for the more specific invariant that many expects. It is much easier to create a domain specific lint like this, than to try to enhance the type system, or develop a more sophisticated static analysis to fix this (it is essentially a conditional effect type depending upon a proof of progress on a inductive datatypes in the dynamic context - really complex proof, especially if something else also touches the list of characters!).

Koka's automatic divergence removal understands that basic structural recursion terminates, and recognizes where things could diverge through handlers or references in the heap, but doesn't try to do much more than that. It is then up to the user where to judiciously use pretend-decreasing to remove the divergence effect when it is not useful for helping to reason about where divergence actually practically happens in the program. In this case, many should converge if used properly. You could contend that all programs should converge if designed properly and so when would you ever not remove div, but there are reasonable programs that don't converge (such as web servers, UIs, operating systems, and other such programs).

Personally I think that the div effect becomes quite noisy in Koka, but it is useful to see where pretend-decreasing is used with some invariant in mind (such as many and the non-null parser), and this is where you can focus the effort for creating linters to prevent runtime issues. So in a way pretend-decreasing becomes something which flags parts of your code that you should try to write an argument or proof of termination (if truly convergent), or a proof of termination / progress under some conditions (if conditionally convergent). And any conditionally convergent function should be well documented what the conditions are that are required for convergence, and considered as a place where a linter or static analysis should be applied for strong guarantees of termination.

[AZMCode]

This feels a bit like the situation Rust has with unsafe functions, where breaking a contract (specified in documentation) results in unspecified behavior.

Interestingly, the "pretend-decreasing" function is declared as "unsafe", and specifies in documentation how to safely use it, and I'd argue, the many combinator would also need to be marked as "unsafe" in order to reflect the fact that it's possible to use it in a way where its effect annotation is innacurate.

Of course the notion of "unsafety" appears to not be well defined in Koka as strictly as it is in Rust AFAIK (At least I haven't found documentation that defines it, though i'd be glad to be proven wrong) and does not lead to memory unsafety, as it does in Rust.

Another interesting bit is that in Rust, the unsafety of a function is tracked in the type system, utilizing a limited effect system. Koka, having a generalized effect system, could easily track this unsafety in a more robust and composable way, by simply making it an effect that can be dismissed, same as div.

[AZMCode]

While it is true that any parser used with "many" obviously should make progress in order to not diverge, this would need to be tracked transitively for any parser combinator which uses many, and any parser combinator that uses those, and all the way up the call stack. After a few levels of indirection the unsafety of a function is not as clear, and I'd argue needs to be tracked and documented, which Koka's effect system would be great for.

[AZMCode]

As long as this doesn't happen, however, I'd argue that the many combinator should be marked div, and users of many should be able to use undiv in specific cases, where they can guarantee the parser given to many makes progress.

[TimWhiting]

Here are two alternate ideas.

1. Instead of div, dismiss the div effect and insert another abstract effect (no handlers) called div-no-progress or something, as well as a function to dismiss that. This way it is a bit more explicit than just dismissing div in general, so that if a use of many does make progress, but could diverge in a different way than you don't dismiss the other way it could diverge when you claim progress.

2. Create a no-progress effect, and make sure all parsers that could not make progress and still succeed are annotated no-progress and create an overloaded version of many that inserts the correct divergence when the parser doesn't make progress. The problem then is making sure that all the parsers are correctly documented, as well as a good way to dismiss no-progress when it doesn't apply (a sequence of two parsers one which doesn't, but the next one does or fails).

I think either of these ideas probably better documents the invariants and utilizes the strengths of Koka's effect system much better than a general unsafe keyword.

I'm not Daan so I don't know what he would prefer to do about this, but I do think that the parser library is not quite finished in it's current state anyways. I know he has mentioned that he would like an Alex like framework for lexing, and a Menhir like framework for parsing. Obviously there is a lot of design space to explore in general with effect handlers and lexing/parsing frameworks, so I don't think he is tied to any particular approach too strongly. It is probably something that we as a community need to try out a bunch of things, benchmark them and figure out what seems like the best approach might be to include in the standard library, or if there should be just a recommended set of packages outside the standard library. It really doesn't take much code to build your own library that is rather robust (I've made a few).

[chtenb]

On top of that, I think you could also turn div into exn or something similar, by checking if the parser state changed in between two frames of execution of the many parser. From a developers perspective, an error message is always more preferable than a hanging application.