5 ms·

Thanks. For what it's worth, the flow of thought was the following: 1. The original "parse, don't validate" essay clearly describes why parsers are preferable

Thanks. For what it's worth, the flow of thought was the following: 1. The original "parse, don't validate" essay clearly describes why parsers are preferable to validators. 2. It uses a type system to make illegal states unrepresentable in a programming language - but a type system is a validator under its own terminology. 3. What would a parser-like approach to solving the problem look like? I believe that actually adjusting the programming language grammar (and thus the actual parser) is clearly a parser approach to solving the problem. Abstraction is also, to me, a parser-like approach to solving the problem - it transforms code that allows illegal states into code that enforces particular invariants. I probably didn't make those connections explicit enough in the blog. Perhaps the diversion into object-capabilities is a bit off the track, but I found it an interesting connection at least. (And frankly, I'm usually close to the sole audience of my blog so I better make it interesting for me!) Edit: formatting

contravariant 6y ago
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. 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. And I think this leads you towards interfaces, though perhaps we can improve interfaces by embracing the idea. Taking C# as an example interfaces basically ensure that if the type check succeeds then the function will be given an object that supports the methods of the interface and only the methods of that interface. Even further the methods and fields names of the interface can conflict with the fields and method names of the object but the type checker 'resolves' those conflicts and essentially returns a 'parsed' object with the right methods. Unfortunately this doesn't yet allow for arbitrary conditions (explicitly). Provability is always going to be an issue so let's say we fix that by dynamic type casts. Then I think the behaviour we want is essentially an interface defined by a function IMyInterface parse(MyObject: MyType) where the constructor of IMyInterface enforces some checks and an object implements the interface if it defines an implementation of 'parse'. Now we only need a language to support this. Maybe we can persuade the Julia guys? They seem to like this kind of type-polymorphism based aproach. Edit: Just checked, apparently they have implemented it, it's just called 'convert'.
- nmadden 6y ago
  > 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).
cannabis_sam 6y ago
> I believe that actually adjusting the programming language grammar (and thus the actual parser) is clearly a parser approach to solving the problem. How do you get the properties of type safety (progress and preservation) in this case?

contravariant 6y ago

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. 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. And I think this leads you towards interfaces, though perhaps we can improve interfaces by embracing the idea. Taking C# as an example interfaces basically ensure that if the type check succeeds then the function will be given an object that supports the methods of the interface and only the methods of that interface. Even further the methods and fields names of the interface can conflict with the fields and method names of the object but the type checker 'resolves' those conflicts and essentially returns a 'parsed' object with the right methods. Unfortunately this doesn't yet allow for arbitrary conditions (explicitly). Provability is always going to be an issue so let's say we fix that by dynamic type casts. Then I think the behaviour we want is essentially an interface defined by a function IMyInterface parse(MyObject: MyType) where the constructor of IMyInterface enforces some checks and an object implements the interface if it defines an implementation of 'parse'. Now we only need a language to support this. Maybe we can persuade the Julia guys? They seem to like this kind of type-polymorphism based aproach. Edit: Just checked, apparently they have implemented it, it's just called 'convert'.

nmadden 6y ago
> 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).

cannabis_sam 6y ago

> I believe that actually adjusting the programming language grammar (and thus the actual parser) is clearly a parser approach to solving the problem. How do you get the properties of type safety (progress and preservation) in this case?