46 ms·

> I see, it's an interesting line of thought but I think trying to move type checking into the grammar is fundamentally a bad idea. You don't want to mix gramma

> I see, it's an interesting line of thought but I think trying to move type checking into the grammar is fundamentally a bad idea. You don't want to mix grammar and semantics because that's not how people think about code. I know that it’s common to refer to type checking as “semantic analysis”, but the logician in me is not happy. There’s nothing inherently more “semantic” about types compared to grammars. As Benjamin Pierce says [1]: > A type system is a syntactic method for enforcing levels of abstraction in programs. (Emphasis mine). > That said I agree that it is interesting to see what the 'parse, don't validate' approach to type checking would be, but I think it should still take place on the type level. You can certainly write parsers at the type level, but that doesn’t change the fundamental fact that a type checker is a validator. To change a type checker into a parser it would have to output a representation which makes invalid states impossible to represent. From a programmer’s point of view (not the compiler writer), this means that the actual compiled object code would have to have this property. I can see a couple of possible ways you could do this: - the compiled object code enforces invariants using dynamic checks provided by the runtime/processor - the type-checker outputs something like proof-carrying code [2] that can be rigorously checked prior to execution to ensure the illegal states removed by the type system cannot be recreated. [1]: https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ [2]: https://en.wikipedia.org/wiki/Proof-carrying_code https://en.wikipedia.org/wiki/Proof-carrying_code

contravariant 6y ago
>I know that it’s common to refer to type checking as “semantic analysis”, but the logician in me is not happy. There’s nothing inherently more “semantic” about types compared to grammars. They can be semantic and in practice are used semantically, especially in nominal type systems. It depends on the programming language how much they enforce though, but even if you don't enforce anything names carry meaning, and to some extent meaning isn't even about what should be impossible but what you should expect (though some states should be impossible). For instance there's no restriction you can build in that would make 'DegreesFahrenheit' and 'DegreesCentigrade' any different, in fact you could argue that any place one of them can be used the other is also valid. The meaning however is very different. >To change a type checker into a parser it would have to output a representation which makes invalid states impossible to represent. Agreed. That doesn't require you to do anything on the level of the grammar of the language though, parsing the text a programmer wrote and parsing an object to a certain type are two very different operations. It doesn't matter how a programmer produced the AST what matters is whether it makes sense (which is a semantic matter as the parser already forces the AST to be grammatically correct).
- nmadden 6y ago
  > They can be semantic and in practice are used semantically, especially in nominal type systems. It depends on the programming language how much they enforce though, but even if you don't enforce anything names carry meaning [...] But grammar productions are also named and grammars are also designed to capture semantic notions. The syntax is after all intended to convey meaning.

contravariant 6y ago

>I know that it’s common to refer to type checking as “semantic analysis”, but the logician in me is not happy. There’s nothing inherently more “semantic” about types compared to grammars. They can be semantic and in practice are used semantically, especially in nominal type systems. It depends on the programming language how much they enforce though, but even if you don't enforce anything names carry meaning, and to some extent meaning isn't even about what should be impossible but what you should expect (though some states should be impossible). For instance there's no restriction you can build in that would make 'DegreesFahrenheit' and 'DegreesCentigrade' any different, in fact you could argue that any place one of them can be used the other is also valid. The meaning however is very different. >To change a type checker into a parser it would have to output a representation which makes invalid states impossible to represent. Agreed. That doesn't require you to do anything on the level of the grammar of the language though, parsing the text a programmer wrote and parsing an object to a certain type are two very different operations. It doesn't matter how a programmer produced the AST what matters is whether it makes sense (which is a semantic matter as the parser already forces the AST to be grammatically correct).

nmadden 6y ago
> They can be semantic and in practice are used semantically, especially in nominal type systems. It depends on the programming language how much they enforce though, but even if you don't enforce anything names carry meaning [...] But grammar productions are also named and grammars are also designed to capture semantic notions. The syntax is after all intended to convey meaning.