regex

host of trade offs at play given the actual choices available to me. (Even if those trade offs may be fundamentally orthogonal to the notion of type safety, they still exist and they are still things I must confront.) Sure; I've got my own agenda/narrative and I'm talking about this bug because it aligns with that. (My belief that greater use of type systems is the best way forward for the industry is genuine and good-faith, but that doesn't mean I'm right) > A long time ago, we had a discussion about ASTs and property based testing. I noted that my "AST" couldn't be round-tripped with the concrete syntax accurately, and you noted that it was therefore not an AST. I'm in the middle of making that happen, and I've tried a bit harder this time around to use the type system to avoid invalid states. I do still have one that I haven't been able to rule out though, which is related to an invariant on a sequence of operations applied to a stack: https://github.com/BurntSushi/regex/blob/syntax-rewrite/rege.... Glad to hear that. The invariant comes from only ever adding alternations to the stack via push_or_add_alternation, right? My first thought is to encapsulate the stack and the way alternations are added to / removed from it behind an opaque type. i.e. rather than Parser having direct access to the stack, it has a wrapped stack that it can push to (in a way that will always add alternations when necessary) and pop from (in a way that will provide it with the invariant - e.g. by returning an alternation-with-content or non-alternation). That doesn't offer any more proof, but practically it means the two halves of the invariant are in the same place and easier to review, and it's clear where the responsibility is. Going further and looking to actually eliminate the unreachable, it seems like a stack with an alternation on top is treated differently both on push and pop (not just at the end but also in pop_group)?. Maybe those should be different types. Or maybe the representation isn't quite right - maybe it would be better for each alternate to be its own stack entry (i.e. the AST looks like Alternate(case1, Alternate(case2, Alternate(case3, ...))). That way seems like a better separation of concerns - on encountering a '|' you just push an entry onto the stack rather than having to push-or-mutate, and then when you know the alternation has finished (because you hit ')' or the end) you peek and pop all the alternations that are currently at the top (possibly zero, which I think should actually simplify pop_group because there are no longer two different cases). In turn that suggests a representation where AstGroup always contains AstAlternation (possibly of only one alternate) and the root value is always AstAlternation too. I don't know whether that would work - maybe there're constraints I haven't thought of - but that's the kind of direction I'd be thinking in. Where there's a conditional, see if it can be moved into data (an enum or similar); where the representation has invalid states, look for a way to represent that avoids them. I think to a certain extent this awkwardness reflects a true awkwardness in the regex grammar - you can't tell whether what you're parsing is part of an alternation or not until you hit the | - but to the extent that it's possible to parse regexes it should be possible to come up with a representation that corresponds to what you do when parsing, and I feel like there's a correspondence/duality between operator precedence and deciding that the children of a certain node must be a particular type of node (e.g. if we wanted to parse arithmetic expressions consisting of +, *, () and variables/literals, we could say that both arguments to + are products (possibly of 1 element)). [1] Including at runtime; if you're looking to write a library that can be embedded into other languages then Rust is indeed probably still your best option. One of my very long-term projects is to extend Rust (or a Rust-like language) with Noether-like functionality, but that's purely theoretical at this point.

ial comment on the matter is that it neglects everything except for the "type system could have stopped it" part. But in reality, there are a host of trade offs at play given the actual choices available to me. (Even if those trade offs may be fundamentally orthogonal to the notion of type safety, they still exist and they are still things I must confront.) I feel like an Agda/Coq implementation would be dead in the water pretty quickly. How easy or hard is it to manipulate raw byte buffers in those languages? Or memory layout? That's why Rust is such a nice tool for a regex engine, because it gives you access to the hardware at the level of C without any fuss at all, while still remaining reasonably safe. A long time ago, we had a discussion about ASTs and property based testing. I noted that my "AST" couldn't be round-tripped with the concrete syntax accurately, and you noted that it was therefore not an AST. I'm in the middle of making that happen, and I've tried a bit harder this time around to use the type system to avoid invalid states. I do still have one that I haven't been able to rule out though, which is related to an invariant on a sequence of operations applied to a stack: https://github.com/BurntSushi/regex/blob/syntax-rewrite/rege...