On Fri, Jun 12, 2015 at 7:21 AM, Keean Schupke <[email protected]> wrote:
> On 12 Jun 2015 11:04, "Matt Oliveri" <[email protected]> wrote:
>> Right. And the typing rules, which are stated in terms of ASTs, not
>> surface syntax, are the type checker spec. And they are separate.
>
> They need not be. In my Prolog type inference implementations I have
> combined grammar and type inference rules.
Right. They need not be. But for maximum clarity, they should be.
> I think the Prolog rules are
> about as close to a formal specification as you can get.
That's a weird thing to say. Either they are a formal specification or
they're not. I'd say Prolog rules would be a formal spec, if you
decide that they're a spec at all.
>> > 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?
>>
>> Since (I think) EBNF is generative, it's actually not a given that the
>> combinators parse the same language that the grammar generates. You'd
>> have to prove it. So that would be something to check even if you
>> consider a type-checking, combinator-based parser to be an acceptable
>> definition of a type system, which I don't.
>>
>> You can always take an implementation to be a spec, in which case it's
>> correct by definition. But most implementations have bugs, so taking
>> an implementation for a spec usually gets you a pretty stupid
>> definition of correctness.
>
> Actually the grammar and parsing are the same thing, its just the parser has
> an additional literal representation attached to leaf terms in the grammar.
I'm sure this is not literally true, so I'm not sure what you're really saying.
> So far I have been assuming we are discussing implementing a parser for our
> new language in some existing widely supported language (like C++).
Yes, to get back to the original point of this thread.
> But if we are taking about how our new language might better support
> compiler writing, then that's a different question. What would a proof look
> like?
I don't understand this question.
> If we can express the typed grammar as a logic program (see the example
> arity-aware inference algorithm I posted a while back), then we just need to
> statically assert that each parser implements a type transformation from the
> grammar. We might do this by naming the grammar rules and asserting which
> grammar rule a parser is implementing.
("Type transformation"?) Umm, yes? Basically? If you're trying to find
out what a parser correctness proof looks like, you should write one.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
