4 ms·

> Is this article against static type systems, or against runtime type checks? Or both... It's not "against" anything. It's pointing out that "make impossible

> Is this article against static type systems, or against runtime type checks? Or both... It's not "against" anything. It's pointing out that "make impossible states unrepresentable" is poorly satisfied by most typed languages themselves. The more of the language you lift into the parser (decidable! easily-analyzable memory bounds!), the less you need to worry about types. As a trivial case consider a language where `5 + ""` would fail typecheck. But why even get so far? Why does your parser accept `lit-term := lit '+' lit` and not `lit-term := [str '+' str] | [ num + num ]`, etc.

firethief 6y ago
Because the parser can't typecheck "ident '+' ident", so why make it vastly more complicated only to overlap with a later pass that is necessary anyway?
- morelisp 6y ago
  What constitutes "vastly more complicated"? "The type checker can't find all errors, why make the compiler vastly more complicated only to overlap with my unit tests later anyway?" is a pretty common argument. What differentiates your case aside from your personal aesthetics?
  - masklinn 6y ago
    > What constitutes "vastly more complicated"? You're duplicating special cases of the typechecker into the parser, completely unnecessarily (since the typechecker will handle it) and for no gain (since this is an approximately non-existent occurrence). Worse, by rejecting the program so early you're making it much harder to provide any sort of valuable feedback.
  - deleted 6y ago
    [deleted]
  - firethief 6y ago
    > The more of the language you lift into the parser (decidable! easily-analyzable memory bounds!), the less you need to worry about types. Doing the easy cases of type-checking at a different time doesn't allow you to worry about types less, because you are still doing that work; just at a different time. Making it necessary to pass type information between phases increases the amount of worrying about types. > As a trivial case consider a language where `5 + ""` would fail typecheck. But why even get so far? Why does your parser accept `lit-term := lit '+' lit` and not `lit-term := [str '+' str] | [ num + num ]`, etc. This approach increases the complexity of parsing so much that your trivial example is wrong. What good is `lit-term` in a language with different expression-trees for different value types? You need something like `maybe-str-expr := [maybe-str-expr '+' maybe-str-expr] | [function-call] | ...` -- where everything is `maybe-`, because enough type information is available to determine that certain things are wrong, but not enough is available to ensure everything is correctly-typed. We could strictly improve on this situation by increasing the scope of the parser, to include looking up the types of items so that it can fully type-check the tree and accept only validly-typed programs. We can further improve the situation by splitting the parser into two phases: one that just identifies the lexical structure of the input, and one that does the type-checking. Let's just not call that part a type-checker -- it's part of the "parser" now.
    - morelisp 6y ago
      Congratulations, you have demolished my trivial example made to clarify for someone who was having trouble understanding the point of the article. I would much rather you engage the ideas in the article directly, and not the deliberately trivial pedagogical case.
contravariant 6y ago
>parser (decidable! easily-analyzable memory bounds!), Hahaha, you wish. Sure there are languages that are simple to parse, but they are that way by construction. Parsing arbitrary grammars is hard to impossible depending on how general your class of grammars is.
- morelisp 6y ago
  I'm well aware of the limitations of some classes of parsers. > but they are that way by construction If I could summarize both this and the original "parse, don't validate" article, it would be "let's construct as much as possible this way."
  - contravariant 6y ago
    Fair enough but it wouldn't surprise me if you just get the exact same problems you get with type systems except phrased differently. You already hinted at this somewhat with your "num = num + num" example, surely that's just a type system in disguise? And well, personally I view types more like a way to denote pre- and post-conditions (with varying degrees of strictness). And a grammar just tells you what you are allowed to write, it doesn't dictate semantics. This becomes a problem when you get stuff like "daily_revenue + temperature", which grammatically makes perfect sense, but semantically does not. With types this can be fixed (admittedly in this case it might not be worth fixing), in a grammar this seem very hard to forbid.
masklinn 6y ago
> As a trivial case consider a language where `5 + ""` would fail typecheck. But why even get so far? Why does your parser accept `lit-term := lit '+' lit` and not `lit-term := [str '+' str] | [ num + num ]`, etc. Because it's an unnecessary complication to duplicate a few corners of the typesystem as special cases of the parser?

firethief 6y ago

Because the parser can't typecheck "ident '+' ident", so why make it vastly more complicated only to overlap with a later pass that is necessary anyway?

morelisp 6y ago
What constitutes "vastly more complicated"? "The type checker can't find all errors, why make the compiler vastly more complicated only to overlap with my unit tests later anyway?" is a pretty common argument. What differentiates your case aside from your personal aesthetics?
- masklinn 6y ago
  > What constitutes "vastly more complicated"? You're duplicating special cases of the typechecker into the parser, completely unnecessarily (since the typechecker will handle it) and for no gain (since this is an approximately non-existent occurrence). Worse, by rejecting the program so early you're making it much harder to provide any sort of valuable feedback.
- deleted 6y ago
  [deleted]
- firethief 6y ago
  > The more of the language you lift into the parser (decidable! easily-analyzable memory bounds!), the less you need to worry about types. Doing the easy cases of type-checking at a different time doesn't allow you to worry about types less, because you are still doing that work; just at a different time. Making it necessary to pass type information between phases increases the amount of worrying about types. > As a trivial case consider a language where `5 + ""` would fail typecheck. But why even get so far? Why does your parser accept `lit-term := lit '+' lit` and not `lit-term := [str '+' str] | [ num + num ]`, etc. This approach increases the complexity of parsing so much that your trivial example is wrong. What good is `lit-term` in a language with different expression-trees for different value types? You need something like `maybe-str-expr := [maybe-str-expr '+' maybe-str-expr] | [function-call] | ...` -- where everything is `maybe-`, because enough type information is available to determine that certain things are wrong, but not enough is available to ensure everything is correctly-typed. We could strictly improve on this situation by increasing the scope of the parser, to include looking up the types of items so that it can fully type-check the tree and accept only validly-typed programs. We can further improve the situation by splitting the parser into two phases: one that just identifies the lexical structure of the input, and one that does the type-checking. Let's just not call that part a type-checker -- it's part of the "parser" now.
  - morelisp 6y ago
    Congratulations, you have demolished my trivial example made to clarify for someone who was having trouble understanding the point of the article. I would much rather you engage the ideas in the article directly, and not the deliberately trivial pedagogical case.

contravariant 6y ago

>parser (decidable! easily-analyzable memory bounds!), Hahaha, you wish. Sure there are languages that are simple to parse, but they are that way by construction. Parsing arbitrary grammars is hard to impossible depending on how general your class of grammars is.

morelisp 6y ago
I'm well aware of the limitations of some classes of parsers. > but they are that way by construction If I could summarize both this and the original "parse, don't validate" article, it would be "let's construct as much as possible this way."
- contravariant 6y ago
  Fair enough but it wouldn't surprise me if you just get the exact same problems you get with type systems except phrased differently. You already hinted at this somewhat with your "num = num + num" example, surely that's just a type system in disguise? And well, personally I view types more like a way to denote pre- and post-conditions (with varying degrees of strictness). And a grammar just tells you what you are allowed to write, it doesn't dictate semantics. This becomes a problem when you get stuff like "daily_revenue + temperature", which grammatically makes perfect sense, but semantically does not. With types this can be fixed (admittedly in this case it might not be worth fixing), in a grammar this seem very hard to forbid.

masklinn 6y ago

> As a trivial case consider a language where `5 + ""` would fail typecheck. But why even get so far? Why does your parser accept `lit-term := lit '+' lit` and not `lit-term := [str '+' str] | [ num + num ]`, etc. Because it's an unnecessary complication to duplicate a few corners of the typesystem as special cases of the parser?