4 ms·

> Ideally, it would support almost all modifications that work in a dynamically typed language, while still preventing anything that would take the program into

> Ideally, it would support almost all modifications that work in a dynamically typed language, while still preventing anything that would take the program into an inconsistent state. This is impossible. Data structures have these little things called “invariants” that require proof to be established. In statically typed languages, abstract data types are used to prevent users from breaking these invariants, by making the representation invisible to anyone but the implementor. If the data structure underlying an abstract data type can be modified anytime, then every time you patch your program, you would have to check two things: (0) That the new data structure respects every invariant relied upon by other code. (1) That either the new data structure is compatible with the old one (which is often not the case), or there are no reachable instances of the old data structure in memory. This is an even bigger pain in the ass than just stopping the program and fixing it.

yorwba 9y ago
I'm aware that a fully general invariant checker is impossible, but there are still type systems that can catch a lot of errors in practice. If dynamic modifications have to be taken into account, that makes the problem more difficult, but not necessarily impossible. Even though there are changes that can't be checked at all, those can't be too common, or humans wouldn't be able to handle them either. I'm not sure why you think that the checking will be painful, it almost sounds like you think that it would be done by the programmer. The whole point of type systems is that they can be checked automatically, so the programmer is prevented from doing something stupid. Dynamic languages already allow all kinds of modifications that might or might not break invariants or introduce subtle incompatibilities; a type system would only make it safer. It is also not just a matter of "stopping the program and fixing it". Suppose you are writing a game, and during playtesting you encounter a bug, where something is stuck in an endless respawn loop. In a dynamic language, you could look at the misbehaving code, develop a fix, and immediately observe its effects. This allows you to quickly iterate until you have found a solution that works. Compared to a "stop, fix, retry"-cycle, it's simply going to be faster, even assuming you can reproduce the bug reliably (maybe using some kind of input replay).
- branja 9y ago
  Look into success typing
  - yorwba 9y ago
    Thank you for the recommendation. I think I found the paper that introduced the idea: http://www.it.uu.se/research/group/hipe/papers/succ_types.pdf http://www.it.uu.se/research/group/hipe/papers/succ_types.pd... If I understand correctly, success typing rejects only programs that will lead to a type error at runtime, but allows all programs that it can't prove incorrect. I think that's an interesting idea and definitely better than no type checks at all, but I'd still like to have a type system that can prove some programs to be type safe, if possible.
    - branja 9y ago
      I agree. Yet I want as much inference as possible as you described upthread
- catnaroek 9y ago
  > but there are still type systems that can catch a lot of errors in practice. I have yet to see a type system that can take a putative implementation of a data structure with arbitrarily complicated invariants, and spits out whether the implementation is correct or not. (Note that Coq, Agda, etc. don't quite fit the bill, because they require the programmer to enter the proof himself, even if these tools can partially automate the process.) > I'm not sure why you think that the checking will be painful, it almost sounds like you think that it would be done by the programmer. The whole point of type systems is that they can be checked automatically, so the programmer is prevented from doing something stupid. My point is precisely that type systems aren't normally used to enforce data structure invariants directly. Instead, data abstraction (i.e., the inability to inspect the representation of abstract data types from client code) is used to confine the potential to break data structure invariants to a small fragment of a big program (namely, where the abstract data type is implemented). This is in furious contradiction with the idea of inspecting and modifying anything anytime from anywhere.

yorwba 9y ago

I'm aware that a fully general invariant checker is impossible, but there are still type systems that can catch a lot of errors in practice. If dynamic modifications have to be taken into account, that makes the problem more difficult, but not necessarily impossible. Even though there are changes that can't be checked at all, those can't be too common, or humans wouldn't be able to handle them either. I'm not sure why you think that the checking will be painful, it almost sounds like you think that it would be done by the programmer. The whole point of type systems is that they can be checked automatically, so the programmer is prevented from doing something stupid. Dynamic languages already allow all kinds of modifications that might or might not break invariants or introduce subtle incompatibilities; a type system would only make it safer. It is also not just a matter of "stopping the program and fixing it". Suppose you are writing a game, and during playtesting you encounter a bug, where something is stuck in an endless respawn loop. In a dynamic language, you could look at the misbehaving code, develop a fix, and immediately observe its effects. This allows you to quickly iterate until you have found a solution that works. Compared to a "stop, fix, retry"-cycle, it's simply going to be faster, even assuming you can reproduce the bug reliably (maybe using some kind of input replay).

branja 9y ago
Look into success typing
- yorwba 9y ago
  Thank you for the recommendation. I think I found the paper that introduced the idea: http://www.it.uu.se/research/group/hipe/papers/succ_types.pdf http://www.it.uu.se/research/group/hipe/papers/succ_types.pd... If I understand correctly, success typing rejects only programs that will lead to a type error at runtime, but allows all programs that it can't prove incorrect. I think that's an interesting idea and definitely better than no type checks at all, but I'd still like to have a type system that can prove some programs to be type safe, if possible.
  - branja 9y ago
    I agree. Yet I want as much inference as possible as you described upthread
catnaroek 9y ago
> but there are still type systems that can catch a lot of errors in practice. I have yet to see a type system that can take a putative implementation of a data structure with arbitrarily complicated invariants, and spits out whether the implementation is correct or not. (Note that Coq, Agda, etc. don't quite fit the bill, because they require the programmer to enter the proof himself, even if these tools can partially automate the process.) > I'm not sure why you think that the checking will be painful, it almost sounds like you think that it would be done by the programmer. The whole point of type systems is that they can be checked automatically, so the programmer is prevented from doing something stupid. My point is precisely that type systems aren't normally used to enforce data structure invariants directly. Instead, data abstraction (i.e., the inability to inspect the representation of abstract data types from client code) is used to confine the potential to break data structure invariants to a small fragment of a big program (namely, where the abstract data type is implemented). This is in furious contradiction with the idea of inspecting and modifying anything anytime from anywhere.