But a grammar, excluding the attributes, is the same as the parser specification.
For example we take an EBNF grammar specification, and write it using parser combinators, or compile it into code. What else is there to check it against? Keean. On 12 Jun 2015 09:52, "Matt Oliveri" <atma...@gmail.com> wrote: > 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 >
_______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
