On Fri, Jun 12, 2015 at 4:18 AM, Keean Schupke <ke...@fry-it.com> wrote: > On 12 Jun 2015 08:57, "Matt Oliveri" <atma...@gmail.com> wrote: >> Keean, the goal here is not to improve performance over the >> one-big-tagged-union option. It is indeed clear that you can't do >> better, if you want AST nodes to be useful. The goal is to know, >> statically, that the parsed AST will always conform to the constrained >> structure allowed by the original CFG. > > Okay, I see. Can we always encode the CFG in the compiler host type-system?
Basically, yeah. CFGs are pretty simple. This is what my conversation with Shap was about on the "Threaded Types" thread. > What if well-typedness depends on intersection or linear types, or some > other sub-structural type system that is not expressible in the host > type-system? But we're not trying to capture well-typedness of the source language, just CFG structure. Like I said, we're in trouble if we try to statically capture well-typedness, because ordinary parsers can produce ASTs for ill-typed code. The type checking is usually a separate pass. That said, if you wanted to capture well-typedness for a substructural system, you'd want a judgements-as-types encoding. You'd need to reason about variable binding by hand. > Can we not rely on being well-typed by construction? So if the parser only > outputs well typed fragments, that's enough? Somewhere we need a > specification of the grammar, if you are using parser combinators we could > say the combinators are the grammar specification, so what they output is > always well typed. I don't think that's paranoid enough. How do we know the parser only outputs well-typed fragments? Even if we can agree on a set of combinators to use for defining the programming language in the first place, we still want some kind of evidence that the implementations of those combinators always produces the parser we think. And really, it doesn't seem like a good idea to use parser combinators instead of usual typing rules. This seems to _force_ us to combine parsing and type checking. Generally, for specification purposes, it's a good idea to split a complex thing into as many steps as possible, so that each step's meaning is maximally obvious. Implementations can be as yucky and clever and efficient as you please if you can verify it against the simple-minded spec. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
