5 ms·

Is there a Turing complete language suitable for writing a fast regex engine with a type system that can prevent all possible invalid states? And if so, how muc

Is there a Turing complete language suitable for writing a fast regex engine with a type system that can prevent all possible invalid states? And if so, how much overhead is associated with said process?

lmm 10y ago
> Is there a Turing complete language suitable for writing a fast regex engine with a type system that can prevent all possible invalid states? I suspect the only way to answer that for certain is to do it. I'd be vaguely interested in trying with Idris[1] or similar. Looking at the code from Reddit it seems like the important distinctions in this instance - between whitespace and not, between the raw input string and the input string with whitespace skipped, between a character that has been confirmed to lie between 0 and 7 and an unknown input character - ought to be trackable in Rust as well though. > And if so, how much overhead is associated with said process? In theory it should be zero overhead at runtime. In practice of course one should have to see how it turned out in benchmarks. [1] Which, sure, would require explicitly choosing possible nontermination when running the regex, if that's the desired behaviour. At one job my team deliberately added a step counter and limit to a regex matcher (abort after 10000 or so) as that was better behaviour than running indefinitely.
- burntsushi 10y ago
  Sorry, by overhead I meant developer overhead. But I think me and you have had this conversation before, and we fundamentally disagree. Putting a limit on the regex engine won't fly. How big should that limit be? I use this particular regex engine to search files that are many GB in size. Some people might search bigger files. What should the limit be? Limits only work when you can restrict your use cases significantly, which is not a luxury I can enjoy. The broader point I was trying to make with my question is that "invalid states aren't represented" isn't particularly interesting to me on its own. What's interesting to me is what it takes to achieve it. i.e., What do I have to give up to make it so? Developer time? Performance? Code complexity? Other practical things? Keep in mind that I'm after things that work, and not a hypothetically advanced-enough tool.
  - lmm 10y ago
    > Putting a limit on the regex engine won't fly. How big should that limit be? I use this particular regex engine to search files that are many GB in size. Some people might search bigger files. What should the limit be? Limits only work when you can restrict your use cases significantly, which is not a luxury I can enjoy. The limit just needs to be applied to backtracking (and other extended regex features that lead to turing completeness if there are any), not to input sizes or similar. I'm content to have a tool that errors if a given regex backtracks to the same point more than say 10000 times. I appreciate the principle of not restricting use cases, but in practice the overwhelming majority of the time that leads to the tool going into what's effectively a busy loop, which is not very user-friendly even if it's in some sense correct. (If I had control over the whole system I would say that perl-style extended regexes are fundamentally the wrong abstraction - the whole original point of regular expressions was that they were expressions for regular languages that were efficiently implementable, and the rare use cases that require turing-complete parsing/matching are better addressed through languages that are designed as turing-complete. But often in practice one doesn't have that freedom). > The broader point I was trying to make with my question is that "invalid states aren't represented" isn't particularly interesting to me on its own. What's interesting to me is what it takes to achieve it. i.e., What do I have to give up to make it so? Developer time? Performance? Code complexity? Other practical things? Keep in mind that I'm after things that work, and not a hypothetically advanced-enough tool. It's interesting in so far as it affects defect rates rather than in and of itself, sure. My sense is that it's natural to avoid this kind of problem in a language that encourages you to represent this kind of distinction, and that the shift of style shouldn't carry a cost beyond that. I mean in this example there was a big explanatory comment above the panic-ing line about why the unwraps were safe, which comes with its own cost (both for the initial developer and for anyone reading the code); to my mind expressing that comment in a type system rather than prose would not have been substantially more expensive, and would have caught the issue. But of course that's a lot to claim without a concrete implementation showing these advantages in practice; most of the experience I'm drawing on is unfortunately private, and skepticism is quite warranted.
    - burntsushi 10y ago
eru 10y ago
There are Turing-incomplete languages doing that kind of thing. Look up Coq and Idris etc. No runtime overhead necessary. (Turing incompleteness is not too much of a restriction for them in practice.)
- burntsushi 10y ago
  I know about them. That's why I added my criteria of Turing completeness. But perhaps I am wrong. Has anyone written a production grade regex engine in say, Coq or Agda? Can they prevent all possible invalid states? Can they support searching text of arbitrary length?
  - eru 10y ago
    Arbitrary length shouldn't be a problem. Agda and co are not restricted to programs of finite runtime. Not sure about production grade, but Google has plenty of results for "Agda regular expressions".

lmm 10y ago

> Is there a Turing complete language suitable for writing a fast regex engine with a type system that can prevent all possible invalid states? I suspect the only way to answer that for certain is to do it. I'd be vaguely interested in trying with Idris[1] or similar. Looking at the code from Reddit it seems like the important distinctions in this instance - between whitespace and not, between the raw input string and the input string with whitespace skipped, between a character that has been confirmed to lie between 0 and 7 and an unknown input character - ought to be trackable in Rust as well though. > And if so, how much overhead is associated with said process? In theory it should be zero overhead at runtime. In practice of course one should have to see how it turned out in benchmarks. [1] Which, sure, would require explicitly choosing possible nontermination when running the regex, if that's the desired behaviour. At one job my team deliberately added a step counter and limit to a regex matcher (abort after 10000 or so) as that was better behaviour than running indefinitely.

burntsushi 10y ago
Sorry, by overhead I meant developer overhead. But I think me and you have had this conversation before, and we fundamentally disagree. Putting a limit on the regex engine won't fly. How big should that limit be? I use this particular regex engine to search files that are many GB in size. Some people might search bigger files. What should the limit be? Limits only work when you can restrict your use cases significantly, which is not a luxury I can enjoy. The broader point I was trying to make with my question is that "invalid states aren't represented" isn't particularly interesting to me on its own. What's interesting to me is what it takes to achieve it. i.e., What do I have to give up to make it so? Developer time? Performance? Code complexity? Other practical things? Keep in mind that I'm after things that work, and not a hypothetically advanced-enough tool.
- lmm 10y ago
  > Putting a limit on the regex engine won't fly. How big should that limit be? I use this particular regex engine to search files that are many GB in size. Some people might search bigger files. What should the limit be? Limits only work when you can restrict your use cases significantly, which is not a luxury I can enjoy. The limit just needs to be applied to backtracking (and other extended regex features that lead to turing completeness if there are any), not to input sizes or similar. I'm content to have a tool that errors if a given regex backtracks to the same point more than say 10000 times. I appreciate the principle of not restricting use cases, but in practice the overwhelming majority of the time that leads to the tool going into what's effectively a busy loop, which is not very user-friendly even if it's in some sense correct. (If I had control over the whole system I would say that perl-style extended regexes are fundamentally the wrong abstraction - the whole original point of regular expressions was that they were expressions for regular languages that were efficiently implementable, and the rare use cases that require turing-complete parsing/matching are better addressed through languages that are designed as turing-complete. But often in practice one doesn't have that freedom). > The broader point I was trying to make with my question is that "invalid states aren't represented" isn't particularly interesting to me on its own. What's interesting to me is what it takes to achieve it. i.e., What do I have to give up to make it so? Developer time? Performance? Code complexity? Other practical things? Keep in mind that I'm after things that work, and not a hypothetically advanced-enough tool. It's interesting in so far as it affects defect rates rather than in and of itself, sure. My sense is that it's natural to avoid this kind of problem in a language that encourages you to represent this kind of distinction, and that the shift of style shouldn't carry a cost beyond that. I mean in this example there was a big explanatory comment above the panic-ing line about why the unwraps were safe, which comes with its own cost (both for the initial developer and for anyone reading the code); to my mind expressing that comment in a type system rather than prose would not have been substantially more expensive, and would have caught the issue. But of course that's a lot to claim without a concrete implementation showing these advantages in practice; most of the experience I'm drawing on is unfortunately private, and skepticism is quite warranted.
  - burntsushi 10y ago

eru 10y ago

There are Turing-incomplete languages doing that kind of thing. Look up Coq and Idris etc. No runtime overhead necessary. (Turing incompleteness is not too much of a restriction for them in practice.)

burntsushi 10y ago
I know about them. That's why I added my criteria of Turing completeness. But perhaps I am wrong. Has anyone written a production grade regex engine in say, Coq or Agda? Can they prevent all possible invalid states? Can they support searching text of arbitrary length?
- eru 10y ago
  Arbitrary length shouldn't be a problem. Agda and co are not restricted to programs of finite runtime. Not sure about production grade, but Google has plenty of results for "Agda regular expressions".