On Fri, Jun 12, 2015 at 2:54 AM, Keean Schupke <ke...@fry-it.com> wrote:
>
> On 12 Jun 2015 00:13, "Matt Oliveri" <atma...@gmail.com> wrote:
>> grammar. If, on the other hand, you tried to enforce well-typedness of
>> ASTs, you probably could _not_ have a type-safe parser, because the
>> parser is not going to reject ill-typed inputs, yet they are not
>> representable. In other words, with such a strongly-typed AST, you'd
>> actually need to parse and type check in the same pass. (I'm actually
>> interested in trying that some day.)
>
> This is what the compositional type inference link I posted above does,
> except that the type system can type any valid open fragment, which means a
> valid program must be the composition of valid fragments, but with the
> additional requirement of being closed. Every parser outputs a valid AST
> tree already annotated with its type.

Neat.

> The type annotations cannot of course be encoded into the C++ type system,
> which is always going to be the case when writing a compiler for a language
> with a more sophisticated type system than the compilers host language.

Well if you're just trying to enforce that ASTs are of well-typed
program fragments, this is not true. There's a certain point after
which you can encode any language's typing rules in the host type
system. This is analogous to how you only need predicate logic to
axiomatize any deductive system.

> Maybe you could 'borrow' the host languages type system when writing the
> self-hosted compiler, but this would make it harder to understand and
> maintain correctness in the compiler, as you would have to go back to the
> non self-hosted compiler to fix any type-system bugs or enhance the type
> system.

Yeah. Bootstrapping headaches.
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to