5 ms·

Which part is effortless? Solving the type checker puzzle, or asking whether type verification is truly needed in a particular given instance?

pyrale 9y ago
Thinking in types. 95% of the time, the type checker silently validates my input and the remaining 5% of the time, the trouble I get is understanding valuable information. There is no such thing as type checker puzzle once you have learned types, just like you don't stop on each word once you're literate.
- wellpast 9y ago
  > There is no such thing as type checker puzzle once you have learned types, just like you don't stop on each word once you're literate. Your analogy doesn't apply. I can read a book in O(n) time, where n is the number of words in the book. I can read a single word in O(1) time. When I get a type error, that is not a O(1) fix. The type error is connected to my program in the large and I have to understand/process more than just the single line where the error is called out. The worst case, obviously, is O(n).
  - wellpast 9y ago
    The worst case for the number of places I have to go fix is O(n). I.e., the verification half is O(n). The solution search side ("solving the puzzle") may be worse, because I have to generate/find the code that fits the type checker.
  - pyrale 9y ago
    Using a static type checker means that an error doesn't creep across all my code. The worst case you describe pretty much never happens, and the smaller instances I get are reified to a generic form I am trained to analyze and solve quickly. > Your analogy doesn't apply. One would think I am well placed to describe my own experience of interacting with a type system.
- jernfrost 9y ago
  Lots of valid code, won't pass the type checker. That is the problem with static type checkers. You have to adapt your code to satisfy the type checker even when you know your logic is right. Static type checking also significantly complicated meta programming, macros and code generation. But hey I like statically typed languages too. A big fan of Swift which has borrowed many functional ideas. I just don't think static typing is the silver bullet that many of its proponents think. It works well for some problems, but not all. E.g. I can't think of any statically typed language which can compete with Julia for numerical work and data science. Haskell e.g. is just terrible at doing numerical work, as it poor at mutation. You can work effectively with lots of big matrices if you don't allow easy access to mutation.
  - pyrale 9y ago
    > Lots of valid code, won't pass the type checker. That is the problem with static type checkers. I fail to see this as a problem. It's pretty much a feature, just as you don't expect object oriented languages to tolerate any shit you throw at them when you use the OO model. > I just don't think static typing is the silver bullet that many of its proponents think. You're the one making the case here, before answering it. > Haskell e.g. is just terrible at doing numerical work I've had good experience with https://wiki.haskell.org/Numeric_Haskell:_A_Repa_Tutorial https://wiki.haskell.org/Numeric_Haskell:_A_Repa_Tutorial
  - tome 9y ago
    > Lots of valid code, won't pass the type checker Perhaps you could give us an example of code you want to write that doesn't pass the type checker. We already know about the case of maps, but it's been pointed out that is solved by row types. A different example would be good.

pyrale 9y ago

Thinking in types. 95% of the time, the type checker silently validates my input and the remaining 5% of the time, the trouble I get is understanding valuable information. There is no such thing as type checker puzzle once you have learned types, just like you don't stop on each word once you're literate.

wellpast 9y ago
> There is no such thing as type checker puzzle once you have learned types, just like you don't stop on each word once you're literate. Your analogy doesn't apply. I can read a book in O(n) time, where n is the number of words in the book. I can read a single word in O(1) time. When I get a type error, that is not a O(1) fix. The type error is connected to my program in the large and I have to understand/process more than just the single line where the error is called out. The worst case, obviously, is O(n).
- wellpast 9y ago
  The worst case for the number of places I have to go fix is O(n). I.e., the verification half is O(n). The solution search side ("solving the puzzle") may be worse, because I have to generate/find the code that fits the type checker.
- pyrale 9y ago
  Using a static type checker means that an error doesn't creep across all my code. The worst case you describe pretty much never happens, and the smaller instances I get are reified to a generic form I am trained to analyze and solve quickly. > Your analogy doesn't apply. One would think I am well placed to describe my own experience of interacting with a type system.
jernfrost 9y ago
Lots of valid code, won't pass the type checker. That is the problem with static type checkers. You have to adapt your code to satisfy the type checker even when you know your logic is right. Static type checking also significantly complicated meta programming, macros and code generation. But hey I like statically typed languages too. A big fan of Swift which has borrowed many functional ideas. I just don't think static typing is the silver bullet that many of its proponents think. It works well for some problems, but not all. E.g. I can't think of any statically typed language which can compete with Julia for numerical work and data science. Haskell e.g. is just terrible at doing numerical work, as it poor at mutation. You can work effectively with lots of big matrices if you don't allow easy access to mutation.
- pyrale 9y ago
  > Lots of valid code, won't pass the type checker. That is the problem with static type checkers. I fail to see this as a problem. It's pretty much a feature, just as you don't expect object oriented languages to tolerate any shit you throw at them when you use the OO model. > I just don't think static typing is the silver bullet that many of its proponents think. You're the one making the case here, before answering it. > Haskell e.g. is just terrible at doing numerical work I've had good experience with https://wiki.haskell.org/Numeric_Haskell:_A_Repa_Tutorial https://wiki.haskell.org/Numeric_Haskell:_A_Repa_Tutorial
- tome 9y ago
  > Lots of valid code, won't pass the type checker Perhaps you could give us an example of code you want to write that doesn't pass the type checker. We already know about the case of maps, but it's been pointed out that is solved by row types. A different example would be good.