4 ms·

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

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.
tome 9y ago
> you have to learn man-years worth of category theory No you don't. Most of the most prolific Haskell programmers (Don Stewart, Neil Mitchell, Lennart Augustsson, probably SPJ himself) would tell you they don't know any category theory.

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.

tome 9y ago

> you have to learn man-years worth of category theory No you don't. Most of the most prolific Haskell programmers (Don Stewart, Neil Mitchell, Lennart Augustsson, probably SPJ himself) would tell you they don't know any category theory.