Hacker News Reader

Comment by AstralStorm | Hacker News Reader

And pray tell how do you verify that the parser is actually correct? How strict can you get?

Lax parsers are the bane of every web browser's existence.

Ultimately parsing does not get you to correctness, ensuring properties does, and a type system is the lamest way to do it. There are actual logic solvers/theorem provers that can handle properties and are as powerful as programming languages while also ensuring correctness and most importantly completeness.

Some of them were even available as extensions for Java, though constraint programming is not currently in the mainstream. (Besides a small variant called borrow checking, used in Rust for instance.)

View on HN

You should read Alexis King's articles on how this is achieved. One of the most imporant aspects of modern parser combinator libraries is that a very small composable core can be exhaustively tested (importantly: with both hand written and random cases) to provide a reliable kernel for parser combinators.

Given that those cited parsers were built from the ground up to mesh with an effective and expressive type system like Haskell's, this problem was significantly reduced. The downside, of course, is that it became quite opinionated.

There is no magic want to wave, but certainly it's easier to work on a common minimal core of components than work on custom ad hoc validators. Lax parsers are not an inevitable outcome; they're a decision propagated by decades of bad opinions being taken as gospel.

An expressive language should let programmers reason about code, including parsers, for their correctness.

You know it is correct when you see it, and you get more confidence in not making silly mistakes with unit tests. This is a different approach to formal verification using logic solvers or theorem provers.

For an example of parsing with Haskell, see this recent discussion: https://news.ycombinator.com/item?id=25212372

This approach, as hinted in Parse, Don’t Type-Check, is to raise the level of abstraction. The jargons are to create a domain-specific language (DSL) to model the problem, as in language-oriented programming.

With this approach, you understand what the code is trying to do and can change it easily because it reads like pseudo-code. (Pseudo-code is usually a synonym for code at the right level of abstraction.)

> And pray tell how do you verify that the parser is actually correct? How strict can you get?

The idea presented in the article is that the data type of the parser output ensures that your invariants are satisfied. It’s not a panacea for solving every possible problem with input validation, it’s more of an alternative technique that gives you much better assurances that some of the invariants you think should be satisfied, are satisfied.

The point of input validation is to fail early, not to ensure the function executes. Returning an empty list when the input is an invalid list sounds like a really bad idea.

What if the function is deleteWhereNotIn( list param )? That empty list just deleted everything.

> The point of input validation is to fail early, not to ensure the function executes.

> What if the function is deleteWhereNotIn( list param )?

  error: could not assign `param` = `mungeList foo`
  note: failed to match `List a` <= `Either SomeError (List b)`
  note: failed to match `List` <= `Either SomeError`

The original article was in a Haskell context, where you'd use a Maybe or Either to prevent that sort of mistake.

Lax parsers made the modern web possible. New web pages with image tags, forms, and scripts were possible without breaking that page's parsing in older browsers.

I think that at this point, folks have realized this is not in fact true. If anything, lax parsers made the evolution of the web more difficult and more subject to corporate cooption.

What's the argument for that? If HTML was strictly parsed the first page with an image tag would have been broken in all other browsers.

Ignoring for one second the specifics of <img> in relation to SGML's `O` option (which was rectified in XML), this doesn't really need to have been the case. HTML could easily have said "if you encounter an unknown tag, render its contents as PCDATA" and sites would have degraded at least as gracefully as they do today. (If less gracefully than they did in 2000.)

(Heck, it could've been a generic SGML feature! "Unknown elements' contents are CDATA, unless they have this attribute in which case they're PCDATA, or this attribute in which case they're ignored" as a rule the DTD...)

> HTML could easily have said...

But it didn't! The problem with being strict here is that every possible usage has to be pre-imagined and perfectly implemented. You're suggesting the original developers should have just made affordances for everything that will be added in the next 30 years. That's easy to say now. The first web browser was essentially just a hugely successful prototype.

And can you imagine having to type all your tags in upper-case? Yuck. :)

We never needed to parse tag soup. We only needed to say which DTD defines the new elements a document uses, and what a browser should do with valid but unknown elements. The latter could use #FIXED or default attribute values in the DTD, because some new elements have human-readable content and others don’t.

The looseness of html is usually in regards to automatically closing tags or unquoted attributes. You can keep strict syntax enforcement and still recognize and skip unknown tags or attributes.

> Lax parsers made the modern web possible.

that's the whole problem indeed

https://mcshowblog.files.wordpress.com/2019/08/dumpsterfire....

Yeah bad example if you wanted to convince me it’s any good :-D

This is not due to lax parsing though. It is due to the convention of how to process undefined tags and attribute:

User agents must treat elements and attributes that they do not understand as semantically neutral; leaving them in the DOM (for DOM processors), and styling them according to CSS (for CSS processors), but not inferring any meaning from them. https://html.spec.whatwg.org/multipage/infrastructure.html#e...

This is unrelated to parsing - for example a XHTML parser will be strict and draconian in its parsing, but still process undefined tags and attributes as above.

That's like saying sloppy programming makes software development possible. At best, it speeds things up (a temporary benefit) at the cost of quality (causing potentially permanent damage).

That’s not like what was said above. They said that a strict parser would choke on unrecognized tags, thus making experimentation non-viable.

Sloppy programming is not about enabling new syntax at all. That simile is not useful.

Reply on news.ycombinator.com