4 ms·

The thing about static typing is that there's a lot of research behind it and it's getting better every day. Eventually it will get to the point where it's nea

The thing about static typing is that there's a lot of research behind it and it's getting better every day. Eventually it will get to the point where it's nearly almost the same as dynamically typed systems, but with type checking (but today is definitely not that day). Checkout liquid types [1]. It's a way to get type inference with nearly dependent types. Cool stuff. Dynamically typed languages, on the other hand, don't really have that much more research that can even be done with them. Can't do any more research on the type system because there isn't much of one. Really the only thing you can do is introduce language features that are difficult to type in a static system, but at that point you're just giving more theory CS phd students targets of things to find a novel way to type. That being said, the problem with static type systems is that there is a lot of details that you need to figure out to A) be able to use it and B) be able to avoid the edge cases. You'll eventually need to learn about type theory ... which isn't just one thing. Agda and Idris have incompatible definitions of equality and that has an impact. Are your dependent types intensional or extensional? It matters. And that's just the theory side. Two different type systems with the same theory might have different implementation details that impact the programmer. Are you using ML? Is that an applicative functor or a generative functor? Hey, you're using first class modules, cool. Btw you can't use that with applicative functors, don't ask why it has something to do with complicated type theory stuff that took people years to figure out. Using haskell? Is it GHC or is it some alternative ... because that impacts some type class definitions that are possible. Eventually the static types are going to win because we'll slowly figure out how to type everything (well, nearly everything) and we'll slowly figure out how to package that power in a way that everybody can understand. However, in the mean time there is a very real cost to having to learn any given static type system that doesn't exist if you live in a dynamically typed system. Additionally, if you do understand some type theory you can bring over the lessons learned to your dynamic system. You won't get type checks at compile time, but you will get a more disciplined way to produce code. [1] - http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=029D52B462162562BA423FE3B7A3A37B?doi=10.1.1.205.2089&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=029...

throwawayjava 9y ago
I'm not sure I agree that "eventually the static types are going to win". The problem is that a lot of program specifications are possible and even economical to write down, but not at all interesting from a research perspective. I do agree that "eventually statically checked specifications are going to win", but I'm not sold that those specifications will take the form of (something easily recognizable as) a type theory. (However, neither outcome would surprise me).
keymone 9y ago
regarding inference - where do you draw a line between "let's fail to infer with an error message because of rigidity of the type system" and "let's be flexible and construct a type that will pass all constrains implied by this part of program"? > the problem with static type systems is that there is a lot of details that you need to figure out to A) be able to use it and B) be able to avoid the edge cases. You'll eventually need to learn about type theory ... which isn't just one thing. Agda and Idris have incompatible definitions of equality and that has an impact. Are your dependent types intensional or extensional? It matters. And that's just the theory side. Two different type systems with the same theory might have different implementation details that impact the programmer. Are you using ML? Is that an applicative functor or a generative functor? Hey, you're using first class modules, cool. Btw you can't use that with applicative functors, don't ask why it has something to do with complicated type theory stuff that took people years to figure out. that in itself is one of the best arguments for strong dynamic systems with small set of ground types - if before solving your problem you have to solve the problem of how to type your problem and before that you have to learn man-years worth of category theory.. no thanks.
- Verdex_3 9y ago
  Ideally, the best way to approach a problem is going to be to find the right type to express it. However, sometimes problems in the real world can only be typed with types that are so complicated that you end up with no confidence that you're doing the right thing. Sure it checks at compile time, but you're not convinced that the program is doing the right thing. In these instances you might as well create a dynamically typed system and see what happens when it meets real life. Yeah it might fail, but the static version was going to fail too. You can save time by not having to worry about what the "proper" type is. The other side of this is: What do we really want our types to do for us? This isn't always the same thing for everyone. I've created DSLs in a dynamic system that failed in weird places and when I tracked down the reason it was because I was using two functions together that did not agree on the "type" they were passing between themselves. In this instance, type theory wasn't going to help solve my problem, but a quick "typecheck" of the code would have pointed me in the right direction to find a silly mistake. On the other hand, sometimes you can use types to solve your problem. I know it's a bit cliche, but rust is a good example of this. If you want to avoid GC but still want high level programming features and no memory corruption then linear types is one way to achieve that.

throwawayjava 9y ago

I'm not sure I agree that "eventually the static types are going to win". The problem is that a lot of program specifications are possible and even economical to write down, but not at all interesting from a research perspective. I do agree that "eventually statically checked specifications are going to win", but I'm not sold that those specifications will take the form of (something easily recognizable as) a type theory. (However, neither outcome would surprise me).

keymone 9y ago

regarding inference - where do you draw a line between "let's fail to infer with an error message because of rigidity of the type system" and "let's be flexible and construct a type that will pass all constrains implied by this part of program"? > the problem with static type systems is that there is a lot of details that you need to figure out to A) be able to use it and B) be able to avoid the edge cases. You'll eventually need to learn about type theory ... which isn't just one thing. Agda and Idris have incompatible definitions of equality and that has an impact. Are your dependent types intensional or extensional? It matters. And that's just the theory side. Two different type systems with the same theory might have different implementation details that impact the programmer. Are you using ML? Is that an applicative functor or a generative functor? Hey, you're using first class modules, cool. Btw you can't use that with applicative functors, don't ask why it has something to do with complicated type theory stuff that took people years to figure out. that in itself is one of the best arguments for strong dynamic systems with small set of ground types - if before solving your problem you have to solve the problem of how to type your problem and before that you have to learn man-years worth of category theory.. no thanks.

Verdex_3 9y ago
Ideally, the best way to approach a problem is going to be to find the right type to express it. However, sometimes problems in the real world can only be typed with types that are so complicated that you end up with no confidence that you're doing the right thing. Sure it checks at compile time, but you're not convinced that the program is doing the right thing. In these instances you might as well create a dynamically typed system and see what happens when it meets real life. Yeah it might fail, but the static version was going to fail too. You can save time by not having to worry about what the "proper" type is. The other side of this is: What do we really want our types to do for us? This isn't always the same thing for everyone. I've created DSLs in a dynamic system that failed in weird places and when I tracked down the reason it was because I was using two functions together that did not agree on the "type" they were passing between themselves. In this instance, type theory wasn't going to help solve my problem, but a quick "typecheck" of the code would have pointed me in the right direction to find a silly mistake. On the other hand, sometimes you can use types to solve your problem. I know it's a bit cliche, but rust is a good example of this. If you want to avoid GC but still want high level programming features and no memory corruption then linear types is one way to achieve that.