29 ms·

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

> 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 not talking about the kinds of invariants that require an undecidable type system to formalize, but about the most simple things. "Any value passed to this function can be iterated over." "This sequence of checks is exhaustive." "Calling this function with these arguments won't throw an exception." Those tend to be the mistakes I make when programming interactively in Python. Forgetting to put a single value into a one-element list. Forgetting to check for None. Misspelling a key in a dictionary. Swapping the order of two arguments in a function call. Yes, in some cases those properties can only be verified by proving some invariant equivalent to the Collatz conjecture. I'd conjecture that most instances could still be solved by an appropriate type system. I'm not too worried if it can't prevent me from invalidating invariants, so long as it can prevent me from making simple mistakes that are obvious in retrospect.
- catnaroek 9y ago
  > Those tend to be the mistakes I make when programming interactively in Python. Those tend to be the mistakes that I take for granted any seasoned programmer can detect and fix almost instantaneously and effortlessly. (Of course, not because programmers are superhuman, but rather because Hindley-Milner is the bare minimum a high-level language should have.) It's pathetic that we're still discussing these in 2017. > Yes, in some cases those properties can only be verified by proving some invariant equivalent to the Collatz conjecture. I have yet to see a useful program whose correctness is contingent on the Collatz conjecture being true. But I have seen lots of programs that are much easier to verify by hand than using a type system. > I'm not too worried if it can't prevent me from invalidating invariants, so long as it can prevent me from making simple mistakes that are obvious in retrospect. I'm not worried either. I'm just saying that “allow anything to be modified anytime, anywhere” is counterproductive. But if you really want to do it, you can do that in ML and Haskell too: just stuff all your top-level definitions into mutable cells.
  - yorwba 9y ago
    > It's pathetic that we're still discussing these in 2017. Evidently most language creators find it difficult to integrate both interactive programming and static typing, which suggests to me that the problem is not easy. Or maybe there just isn't enough overlap between the groups who value one or the other. > just stuff all your top-level definitions into mutable cells That seems like it could be part of a potential solution, but it would require rewriting the program so that everything is implicitly wrapped in the IO monad. And it still doesn't handle the case were you want to add to an existing data type.
    - catnaroek 9y ago
      > Evidently most language creators find it difficult to integrate both interactive programming and static typing. Interactivity is one thing. Randomly redefining things is a-whole-nother thing. ML and Haskell are interactive. They just don't stuff absolutely everything in mutable cells like most dynamic languages do. > That seems like it could be part of a potential solution, but it would require rewriting the program so that everything is implicitly wrapped in the IO monad. You can't have it both ways: either you have effects and accept that you have effects, or don't have effects and accept that you don't have effects. (IOW, lying is bad.)

yorwba 9y ago

I'm not talking about the kinds of invariants that require an undecidable type system to formalize, but about the most simple things. "Any value passed to this function can be iterated over." "This sequence of checks is exhaustive." "Calling this function with these arguments won't throw an exception." Those tend to be the mistakes I make when programming interactively in Python. Forgetting to put a single value into a one-element list. Forgetting to check for None. Misspelling a key in a dictionary. Swapping the order of two arguments in a function call. Yes, in some cases those properties can only be verified by proving some invariant equivalent to the Collatz conjecture. I'd conjecture that most instances could still be solved by an appropriate type system. I'm not too worried if it can't prevent me from invalidating invariants, so long as it can prevent me from making simple mistakes that are obvious in retrospect.

catnaroek 9y ago
> Those tend to be the mistakes I make when programming interactively in Python. Those tend to be the mistakes that I take for granted any seasoned programmer can detect and fix almost instantaneously and effortlessly. (Of course, not because programmers are superhuman, but rather because Hindley-Milner is the bare minimum a high-level language should have.) It's pathetic that we're still discussing these in 2017. > Yes, in some cases those properties can only be verified by proving some invariant equivalent to the Collatz conjecture. I have yet to see a useful program whose correctness is contingent on the Collatz conjecture being true. But I have seen lots of programs that are much easier to verify by hand than using a type system. > I'm not too worried if it can't prevent me from invalidating invariants, so long as it can prevent me from making simple mistakes that are obvious in retrospect. I'm not worried either. I'm just saying that “allow anything to be modified anytime, anywhere” is counterproductive. But if you really want to do it, you can do that in ML and Haskell too: just stuff all your top-level definitions into mutable cells.
- yorwba 9y ago
  > It's pathetic that we're still discussing these in 2017. Evidently most language creators find it difficult to integrate both interactive programming and static typing, which suggests to me that the problem is not easy. Or maybe there just isn't enough overlap between the groups who value one or the other. > just stuff all your top-level definitions into mutable cells That seems like it could be part of a potential solution, but it would require rewriting the program so that everything is implicitly wrapped in the IO monad. And it still doesn't handle the case were you want to add to an existing data type.
  - catnaroek 9y ago
    > Evidently most language creators find it difficult to integrate both interactive programming and static typing. Interactivity is one thing. Randomly redefining things is a-whole-nother thing. ML and Haskell are interactive. They just don't stuff absolutely everything in mutable cells like most dynamic languages do. > That seems like it could be part of a potential solution, but it would require rewriting the program so that everything is implicitly wrapped in the IO monad. You can't have it both ways: either you have effects and accept that you have effects, or don't have effects and accept that you don't have effects. (IOW, lying is bad.)