4 ms·

I don’t understand the idea here. Isn’t typechecking a means of making impossible states impossible? The article references ideas like non empty arrays or limit

I don’t understand the idea here. Isn’t typechecking a means of making impossible states impossible? The article references ideas like non empty arrays or limiting the input from all numbers to just integers between 1 and 5 inclusive. These are both ideas you can express in a type system (quite trivially in most as well). But instead we should use a function at runtime to parse the input and return an object of this type? Is this article against static type systems, or against runtime type checks? Or both... Personally I love having a type system and typescript (what I work with professionally) allows for making impossible states impossible just like many other type systems

morelisp 6y ago
> 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?
taeric 6y ago
Making impossible things impossible seems off. Type checking, by name, is just checking types. Akin to units checking. That said, some things may be impossible at a piecemeal, but correct as whole. Easiest is really any system. The parts usually do not stand on their own. A gear without the bike is effectively impossible to use, but still correct, after all.
- cylon13 6y ago
  Making incorrect states impossible to represent is exactly what type systems are about. If you're still thinking in terms of something that's basically checking units, I'd recommend experiencing a more advanced type system like Haskell, at least for a few hundred or thousand lines of code. C or Java are terrible examples of what a type system is capable of.
  - morelisp 6y ago
    It's extremely formalized, but at least for me the foundation I always come back to to try to explain type systems is the taxonomy in chapter 1 of Stepanov and McJones's Elements of Programming[0]. Type systems help ensure your binary data are well-formed value (and your bits are numbers, your numbers are temperatures, etc. up various hierarchies). I find this is more convincing initially for mechanically sympathetic programmers (including myself) than any taxonomy of endofunctors. [0] http://elementsofprogramming.com/ http://elementsofprogramming.com/
    - cylon13 6y ago
      This is awesome, thanks for the resource!
- wvenable 6y ago
  Pascal has subrange types -- you can declare a type that is 1..10 for example. Statically typed languages could be more strict and have more basic typing features. In most languages, it's not even as good as units checking because you can't say numeric type X is incompatible with numeric type Y (e.g. Celsius and Fahrenheit).
brundolf 6y ago
I think there were two main concepts: 1) When implementing a type system, you could have a separate representation for a typechecked AST than for a not-yet-typechecked AST, in the same way that you normally have a separate representation for a parsed AST than for a not-yet-parsed token stream. This would ensure against invalid states within a parser by making the type-checking pass another parsing pass instead of a validation pass. 2) The author then seemed to veer into applying this philosophy to application code. However, the author also seems like they've had a lot of experience with languages where the line between parser and application is blurred, so in that context this isn't such a big leap.

morelisp 6y ago

> 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?

taeric 6y ago

Making impossible things impossible seems off. Type checking, by name, is just checking types. Akin to units checking. That said, some things may be impossible at a piecemeal, but correct as whole. Easiest is really any system. The parts usually do not stand on their own. A gear without the bike is effectively impossible to use, but still correct, after all.

cylon13 6y ago
Making incorrect states impossible to represent is exactly what type systems are about. If you're still thinking in terms of something that's basically checking units, I'd recommend experiencing a more advanced type system like Haskell, at least for a few hundred or thousand lines of code. C or Java are terrible examples of what a type system is capable of.
- morelisp 6y ago
  It's extremely formalized, but at least for me the foundation I always come back to to try to explain type systems is the taxonomy in chapter 1 of Stepanov and McJones's Elements of Programming[0]. Type systems help ensure your binary data are well-formed value (and your bits are numbers, your numbers are temperatures, etc. up various hierarchies). I find this is more convincing initially for mechanically sympathetic programmers (including myself) than any taxonomy of endofunctors. [0] http://elementsofprogramming.com/ http://elementsofprogramming.com/
  - cylon13 6y ago
    This is awesome, thanks for the resource!
wvenable 6y ago
Pascal has subrange types -- you can declare a type that is 1..10 for example. Statically typed languages could be more strict and have more basic typing features. In most languages, it's not even as good as units checking because you can't say numeric type X is incompatible with numeric type Y (e.g. Celsius and Fahrenheit).

brundolf 6y ago

I think there were two main concepts: 1) When implementing a type system, you could have a separate representation for a typechecked AST than for a not-yet-typechecked AST, in the same way that you normally have a separate representation for a parsed AST than for a not-yet-parsed token stream. This would ensure against invalid states within a parser by making the type-checking pass another parsing pass instead of a validation pass. 2) The author then seemed to veer into applying this philosophy to application code. However, the author also seems like they've had a lot of experience with languages where the line between parser and application is blurred, so in that context this isn't such a big leap.