Are there any additional resources on learning lean-par...

Stream: new members

[Joseph Junker]

I'm trying to parse some very basic data (a file with rows of numbers) and I thought that this would be a good time to learn how to use a parsing library in lean. The only one I found was https://github.com/fgdorais/lean4-parser/tree/main . Problem is... I can't make heads nor tails of how this works or how to use it. I've written combinator parsers before in TypeScript, in the sense of the old "a parser for things is a function from strings to lists of pairs of things and strings" sense but this is a whole different beast. Does anyone know of simple examples of how to use this, or where I might start?

Concrete questions:

• In the JSON example all of the parsers have Unit in their type signature. I would expect that the number function would have a number type in its signature. What am I missing?
• In the documentation I can see a function to parse numbers. However, this doesn't return a Parser, it returns a ParserT. Why? And to use this without additional effects, would I somehow apply it to the identity monad?
• I _mostly_ understand the implementation of roman numeral parsing but I could still use help understanding the type signatures and why ParserT is nowhere to be seen.

I really appreciate any and all help on any part of these.

[Aaron Liu]

Joseph Junker said:

• In the JSON example all of the parsers have Unit in their type signature. I would expect that the number function would have a number type in its signature. What am I missing?

This means that they don't return anything. The file you linked has "JSON validator" written at the top. The parser doesn't actually extract any information from the JSON, it just validates that it doesn't have any syntax errors.

[Joseph Junker]

:man_facepalming:

[Joseph Junker]

yeah that tracks. Thank you!

[Notification Bot]

Joseph Junker has marked this topic as resolved.

[Notification Bot]

François G. Dorais has marked this topic as unresolved.

[François G. Dorais]

I'm a bit late to the party, I've been busy.

Joseph Junker said:

• In the documentation I can see a function to parse numbers. However, this doesn't return a Parser, it returns a ParserT. Why? And to use this without additional effects, would I somehow apply it to the identity monad?

I'm (slowly) working on improving documentation. Many significant parts are still missing.

ParserT is a monad transformer, it takes a monad m and adds a parser layer to it. This is necessary to allow parsing external files, for example, which requires something like IO in an inner layer. However, if m has no side effects then the transformed monad will have no side effects either. In fact, the monad Parser is simply defined as ParserT applied to Id.

Many users will not need to use Parser or ParserT directly. For example, the specializations SimpleParser/SimpleParserT, BasicParser/BasicParserT, TrivialParser/TrivialParserT provide three different simple mechanisms for error reporting. The Trivial mechanism simply fails on error providing no additional info, use this when the parser cannot fail or is not expected to fail for your application. The Simple mechanism allows adding messages to explain the error. None of these provide tools for error recovery, this would be one reason to work with Parser/ParserT directly.