F
François Pottier
gallium.inria.fr/~fpottier · Personal blog · on HN since 2014
François Pottier, a researcher at Inria, publishes papers and software on ML type inference, parser generators (Menhir) and the Mezzo language.
What HN saysCommenters bring it up in threads on OCaml parser generators, verified parsing, and type systems that track ownership or complexity.
18HN people shared it
16linked it in comments
2stories submitted
9story points
1 year agolast shared
2014people per year2026
Most-shared posts
- 1Menhir4 people · first shared 2016
- 2Manual.pdf2 people · first shared 2017
- 3A few lessons from the Mezzo project [pdf]1 people · 7 points · first shared 2015 · 1 comments on HN
- 4The Essence of ML Type Inference [pdf]1 people · 2 points · first shared 2019 · discussion on HN
- 5Fpottier 2015 11 oups.pdf1 people · first shared 2017
- 6Jourdan leroy pottier validating parsers.pdf1 people · first shared 2015
- 7Fpottier 2011 01 jfla.pdf1 people · first shared 2023
- 8Bpp mezzo journal.pdf1 people · first shared 2023
- 9Pottier abstracts1 people · first shared 2017
- 10Fpottier regis gianas typed lr.pdf1 people · first shared 2014
- 11Mezzo icfp2013 long.pdf1 people · first shared 2015
- 12Manual1 people · first shared 2025
- 13Fpottier reachability cc2016.pdf1 people · first shared 2018
- 14Fpottier 2007 05 linear bestiary.pdf1 people · first shared 2019
What HN people wrote when they linked it
jasperry · 2025-07-28
> If I was routinely working in a language that had a well respected de facto standard parser generator and lexer, and regularly building parsers for little languages for my programs, it would probably be worth mastering these tools.
In OCaml, a language highly suited for developing languages in, that de facto standard is the Menhir LR parser generator. It's a modern Yacc with many convenient features, including combinator-like library functions. I honestly enjoy the work of mastering Menhir, poring over the manual, which is all one page: https://gallium.inria.fr/~fpottier/menhir/manual.html
nickpsecurity · 2015-05-26
Getting parsing done correctly and efficiently is a requirement that pops up over and over. More work in the field is always good. Interesting paper, although I haven't heard of the parsers. I usually hear about yacc, GOLD parsing system, and so on. Like to see comparisons with most common ones for probable use cases in terms of productivity, safety, and performance.
Far as next project, Leroy's people at INRIA did excellent work in verified, LR parsers [1]. I'm not sure that anyone is building on it at the moment. Implementing that in or integrating with Rust might make for one heck of a parsing system. So long as correspondence was proven, it would be the safest one in a systems language.
[1] http://gallium.inria.fr/~fpottier/publis/jourdan-leroy-pottier-validat…
Ericson2314 · 2019-12-06
https://arxiv.org/abs/1803.02796 has a good intro referencing other work. The paper doesn't go into much detail on the borrow checking side of things, but that author is both thoroughly steeped in the linear types research tradition and knows Rust and mentions it a bunch.
The fact that that paper talks about the affine types far more than the lifetimes obliquely illustrates my point in my view, I'm not sure if it's been stated more directly.
https://gallium.inria.fr/~fpottier/slides/fpottier-2007-05-linear-best… has some nice history. It wish there is a newer version for things that have been published since, in case the issue is more resolved and I'm out of date.
So in Rust today type inference strategies are less the point this hinges on. It's more about abolishing the difference between intra-procedural control flow / data flow / whatever, and their inter-procedural equivalents. Similarly, if we had an annotated version of the MIR which was borrow-check correct under composition that would also be good. NLL is great, and starts to clarify what borrow checking is, but running it in "whole" functions makes it to what clear it is a compositional analysis.
hayley-patton · 2023-06-05
There are type systems which can track complexity (e.g. http://gallium.inria.fr/~fpottier/slides/fpottier-2011-01-jfla.pdf) but that's still different to performance; async/sync tells us things like "touches disk" or "touches network" but not "O(2^n) might take a really long time".
Alternately, an effect system can communicate "touches disk", can make functions which are polymorphic to effects (e.g. map touches the disk if the mapping function touches the disk), and can distinguish different effects, unlike async/sync being anything-or-nothing. IMO async is more of an implementation detail (as "may suspend/yield" is not a very precise or interesting effect), whereas effects would communicate the properties that ohgodplsno wants to know.
Rusky · 2023-02-09
I wouldn't say "absolutely no problem." Based on section 2.5 of [1], Mezzo needs some extra bookkeeping to handle reference cycles as well- the program needs to select a single owner for objects involved in cycles, and `give`/`take` them to/from that owner to access them, which can fail at runtime.
Section 2.6 describes a static variant of the same idea, named `focus`/`defocus`, which can't fail at runtime but has some limitations on how nodes can be used.
These don't exactly match the solutions Rust typically uses, but they are close to a few of them in several ways. This looks more like a question of defaults and API (including the choice to rely on garbage collection by default) than the design of the type/borrow checker.
[1] http://gallium.inria.fr/~fpottier/publis/bpp-mezzo-journal.pdf
nsajko · 2020-11-26
Maybe you should check out the Menhir parser generator instead.
Some links:
http://gallium.inria.fr/~fpottier/menhir/manual.pdf
https://semantic-domain.blogspot.com/2015/11/error-handling-in-menhir.…
https://baturin.org/blog/declarative-parse-error-reporting-with-menhir…
tom_mellior · 2018-05-15
> A hand-written parser can have better error recovery and more helpful error messages.
That depends on what you're comparing to. The Menhir parser generator can generate a file with all possible "error states" in the parser in which you can specify very nice and friendly error messages for each one.
I've posted this before: http://gallium.inria.fr/~fpottier/slides/fpottier-2015-11-oups.pdf (ignore the French title, the rest is in English). The examples for a C grammar in Menhir show much better error messages than the hand-written GCC ones.
fmap · 2017-08-15
Some people have mentioned parser generators, but so far nobody has mentioned Menhir (http://gallium.inria.fr/~fpottier/menhir/).
It's an LR(1) parser generator for OCaml and Coq with a lot of extremely interesting features, such as genuinely good debugging support for grammars and the ability of generating error messages by example.
What this means is that after you write down your grammar, Menhir will give you examples of all the possible syntax errors that could occur. You can then write error messages for each case and get a parser with built-in error reporting for syntax errors.
This works a lot better than you'd think and I really wonder why nobody else implements this feature. Or for that matter, why they're not advertising it on the webpage! If you want to know more, look in the manual, section 11.
Drup · 2017-03-20
While I agree with you those 3 points are extremely important, it turns out there is at least one parser generator that can do all of it: http://gallium.inria.fr/~fpottier/menhir/
It supports both incremental parsing and an API to inspect and recover incomplete ASTs (which powers Merlin, the IDE-like thing for OCaml). It provides stellar debugging features for ambiguous grammars and a way to have good error messages (which is used in compcert's C parser and facebook's reason).
So, it's not impossible. Most parser generators are not that good, though.
andrewcooke · 2015-07-03
http://gallium.inria.fr/~fpottier/publis/mezzo-icfp2013-long.pdf
http://lambda-the-ultimate.org/node/4960
thanks; these are all very interesting.
CHY872 · 2014-04-21
Ok, so in retrospect I didn't mean that for OCaml. Certainly it is true for Standard ML [1, 2, 3], or rather, the parts of the language that use the underlying native code (IO etc) are generally smaller pieces of code for which the correctness properties are hopefully more easily tested and verified. In any case, I believe my point still stands on the whole :)
[1] http://www.cl.cam.ac.uk/teaching/1314/FoundsCS/fcs-notes.pdf
[2] http://gallium.inria.fr/~fpottier/publis/fpottier-regis-gianas-typed-l…
[3] https://en.wikipedia.org/wiki/Type_safety#Standard_ML
ssize_t · 2020-02-03
I think the `#coding:` approach is promising. You have to fit your parsing/transpilation into a pretty small time budget (which is a fun challenge on its own) to keep the startup time hit negligible. The source code gets reparsed serval times in certain cases, e.g. when printing a stack trace, so its a good idea to have some sort of caching mechanism.
As far as parsing goes, if you want to stick with python I've had good success with pyparsing [1], otherwise I have a strong preference to do language-related things in OCaml with menhir [2]. I've toyed with wrapping the Python parser in an OCaml library with decent success [3]. But, of course, unless you're optimizing for fun, it's probably a good idea to stick with Python.
Another, weirder, approach is creating a language that happens to be able to be parsed by the same grammar as python, then using a decorator (or similar) to get the source code or the ast to reparse and transpile. As an example you could have something like `a <- b` be the syntax for an actor model message receive dsl (which is valid python).
[1] https://github.com/pyparsing/pyparsing
[2] http://gallium.inria.fr/~fpottier/menhir/
[3] https://github.com/georgek42/pyparser
cwzwarich · 2018-06-04
> The problem with bottom-up parsers of any flavor, LR included, is that when you encounter a syntax error there is no context information, or context is difficult to infer, which makes creating a sensible error message less fun than poking yourself in the eye repeatedly with a sharp stick.
Both LL and LR parsers share a fundamental flaw for error reporting; they are both prefix parsers. They will parse the input until it fails to be a valid prefix of the language represented by the grammar. However, it is rare that this coincides with the place where the actual error was made.
The difference in information available here at the end of the valid prefix is less about the difference between LL and LR parsing and more about the difference between LL and LR grammars. An LR parser parsing an LL grammar is able to recover the same information as an LL parser at the point of error. And for non-LL grammars, it is easy to extend an LR parser with additional context information by splitting states (see http://gallium.inria.fr/~fpottier/publis/fpottier-reachability-cc2016.…
Parsing algorithms that do not produce prefix parsers (e.g. precedence parsing) are often able to produce more logical error messages with less work, because they continue making actions after the input is no longer a valid prefix, and this can amount to gathering more information about the error. For the same reason, LR-family parsers that perform default reductions (e.g. LALR parsers, or any minimal state…
def-lkb · 2017-03-20
Hi,
I did a part of the incremental parsing in Menhir and the whole recovery aspect. I can try to explain a bit.
My goal was Merlin (https://github.com/ocaml/merlin/), not research so there is no paper covering the work I am about to describe. Also as of today only incrementality and error message generation are part of upstream version of Menhir, but the rest should come soon.
# Incrementality, part I
The notion of incrementality that comes builtin with Menhir is slightly weaker than what you are looking for.
With Menhir, the parser state is reified and control of the parsing is given back to the user. The important point here is the departure from a Bison-like interface. The user of the parser is handled a (pure) abstract object that represents the state of the parsing.
In regular parsing, this means we can store a snapshot of the parsing for each token, and resume from the first token that has changed (effectively sharing the prefix).
But on the side, we can also run arbitrary analysis on a parser (for error message generation, recovery, syntactic completion, or more incrementality...).
# Incrementality, part II
Sharing prefix was good enough for our use case (parsing is not a bottleneck in the pipeline). But it turns out that a trivial extension to the parser can also solve your case.
Using the token stream and the LR automaton, you can structure the tokens as a tree:
- starts with a root node annotated by the state of the automaton
- store each token consumed…
dsp1234 · 2017-03-20
Details about the "incremental" mode are listed in the documentation PDF[0] at section 9.2
Here are the first couple of paragraphs:
"In this API, control is inverted. The parser does not have access to the lexer. Instead, when the parser needs the next token, it stops and returns its current state to the user. The user is then responsible for obtaining this token (typically by invoking the lexer) and resuming the parser from that state. The directory demos/calc-incremental contains a demo that illustrates the use of the incremental API.
This API is “incremental” in the sense that the user has access to a sequence of the intermediate states of the parser. Assuming that semantic values are immutable, a parser state is a persistent data structure: it can be stored and used multiple times, if desired. This enables applications such as “live parsing”, where a buffer is continuously parsed while it is being edited. The parser can be re-started in the middle of the buffer whenever the user edits a character. Because two successive parser states share most of their data in memory, a list of n successive parser states occupies only O(n) space in memory."
There does not appear to be a specific mention of having the partial AST available.
[0] - linked from their front page and available at http://gallium.inria.fr/~fpottier/menhir/manual.pdf
x0re4x · 2022-02-15
@LeSUTHU:
* if you want to design and play around with your grammar (builtin interpreter is very nice to try things out):
https://www.antlr3.org/works/
* once you want to actually implement your language:
https://cs3110.github.io/textbook/chapters/interp/intro.html
* some older tutorials:
https://web.archive.org/web/20051220013748/http://pllab.kaist.ac.kr/~s…
https://web.archive.org/web/20051220043933/http://pllab.kaist.ac.kr/~s…
NOTE: modern replacement for ocamlyacc: http://gallium.inria.fr/~fpottier/menhir/