6 ms·

I love Bob Harper's view that something like Type Theory will eventually become the one-true-language. His arguments arise from a POV pretty different from the

by tel 13y ago

I love Bob Harper's view that something like Type Theory will eventually become the one-true-language. His arguments arise from a POV pretty different from the standard argument here—it's not that some particular implementation will win, but instead that the entire design space of languages we will eventually gravitate to type theory because it's just right.

brudgers 13y ago
At the end of the day who wants dependently typed bash? It's a great intellectual position for happy hour at the campus pub. Yet from a practical standpoint, it's hard to see how programming languages requiring more attention to type system will facilitate banging out code for ordinary problems more quickly. There are times when it is really important to be able to prove code is correct and times when it is enough to just provide a plausible answer. The market for ML on Rails remains without validation.
- tel 13y ago
  Who says it has to feel much at all like DTLs of today? I probably do want to be at least warned when the compiler can't be sure my bash is terminating. And I'd love Bash embedded in a DT. Even if I never write the DT components being able to nicely map Bash -> DT is powerful. Finally, I'd love Bash with sum types.
- prodigal_erik 13y ago
  Pretty much every program humanity has produced is grossly defective. Certainly there's nothing I use heavily that hasn't failed. IMHO shipping more garbage more quickly is not a problem worth solving.
  - perturbation 13y ago
    <sarcasm>That seems to be the principle use case for Javascript, and that is (arguably) the lingua franca of our generation. </sarcasm>
- rtpg 13y ago
  With something like Haskell (very good type inference) the types will only bother you if you're writing wrong code (or writing particularly complex expressions, I'm not necessarily against compilers complaining about things that are complicated). It's not a free lunch, but damn is it cheap.
  - brudgers 13y ago
    The Haskell compiler will complain if I am writing wrong Haskell code, or more generally when the types are indeterminate and can't be inferred. This not the same as 'wrong code' in the abstract. The code will run fine if I don't pass in mismatched data, or more generally bad data. And if I am passing in bad data, static typing doesn't give me good answers, it just keeps the program from crashing. Don't get me wrong, there are times when crashing is bad. But there are times when the cost of a runtime error is nominal and the value of flexible code is high. Static typing trades one type of cognitive overhead for another. The Java program of 500 classes is its manifestation.
    - efnx 13y ago
      What is the cognitive overhead Haskell is introducing? Types? Because as far as I can tell we use types in all OOP, they're just implicit and not checked.
      - brudgers 13y ago
        Static type checking, regardless of language, requires thinking about programs in a particular way because one possible mode of failure is prioritized over all other modes. It does so regardless of whether absolute type safety deserves to be prioritized given the purpose of a particular program and it does so regardless of whether absolute type safety is an appropriate concern at a particular stage of the program's development. Static typing can make "how do I get this to compile?" a design criterion Consider year 2038 problem. In MySQL, various date types are coerced to the timestamp type by design. Otherwise the program would not compile. Compilation takes precedence over problem solving. http://dev.mysql.com/doc/refman/5.0/en/datetime.html http://dev.mysql.com/doc/refman/5.0/en/datetime.html
m0nastic 13y ago
I think type theory is supremely interesting, and I'm curious to see how far you can take it. I worry a little that at some point your type system needs its own type system, and then we've just moved the argument about typing one level of abstraction deeper. I'm not willing to concede that strong static typing is a universal truth though. Too many people much smarter than me seem to disagree.
- nmrm 13y ago
  This is a solved problem; they are called Universe Types.

by tel 13y ago

brudgers 13y ago

At the end of the day who wants dependently typed bash? It's a great intellectual position for happy hour at the campus pub. Yet from a practical standpoint, it's hard to see how programming languages requiring more attention to type system will facilitate banging out code for ordinary problems more quickly. There are times when it is really important to be able to prove code is correct and times when it is enough to just provide a plausible answer. The market for ML on Rails remains without validation.

tel 13y ago
Who says it has to feel much at all like DTLs of today? I probably do want to be at least warned when the compiler can't be sure my bash is terminating. And I'd love Bash embedded in a DT. Even if I never write the DT components being able to nicely map Bash -> DT is powerful. Finally, I'd love Bash with sum types.
prodigal_erik 13y ago
Pretty much every program humanity has produced is grossly defective. Certainly there's nothing I use heavily that hasn't failed. IMHO shipping more garbage more quickly is not a problem worth solving.
- perturbation 13y ago
  <sarcasm>That seems to be the principle use case for Javascript, and that is (arguably) the lingua franca of our generation. </sarcasm>
rtpg 13y ago
With something like Haskell (very good type inference) the types will only bother you if you're writing wrong code (or writing particularly complex expressions, I'm not necessarily against compilers complaining about things that are complicated). It's not a free lunch, but damn is it cheap.
- brudgers 13y ago
  The Haskell compiler will complain if I am writing wrong Haskell code, or more generally when the types are indeterminate and can't be inferred. This not the same as 'wrong code' in the abstract. The code will run fine if I don't pass in mismatched data, or more generally bad data. And if I am passing in bad data, static typing doesn't give me good answers, it just keeps the program from crashing. Don't get me wrong, there are times when crashing is bad. But there are times when the cost of a runtime error is nominal and the value of flexible code is high. Static typing trades one type of cognitive overhead for another. The Java program of 500 classes is its manifestation.
  - efnx 13y ago
    What is the cognitive overhead Haskell is introducing? Types? Because as far as I can tell we use types in all OOP, they're just implicit and not checked.
    - brudgers 13y ago
      Static type checking, regardless of language, requires thinking about programs in a particular way because one possible mode of failure is prioritized over all other modes. It does so regardless of whether absolute type safety deserves to be prioritized given the purpose of a particular program and it does so regardless of whether absolute type safety is an appropriate concern at a particular stage of the program's development. Static typing can make "how do I get this to compile?" a design criterion Consider year 2038 problem. In MySQL, various date types are coerced to the timestamp type by design. Otherwise the program would not compile. Compilation takes precedence over problem solving. http://dev.mysql.com/doc/refman/5.0/en/datetime.html http://dev.mysql.com/doc/refman/5.0/en/datetime.html

m0nastic 13y ago

I think type theory is supremely interesting, and I'm curious to see how far you can take it. I worry a little that at some point your type system needs its own type system, and then we've just moved the argument about typing one level of abstraction deeper. I'm not willing to concede that strong static typing is a universal truth though. Too many people much smarter than me seem to disagree.

nmrm 13y ago
This is a solved problem; they are called Universe Types.