3 ms·

This might be a stupid question but anyway... Is there someone well-versed in a statically typed language who would still prefer python most of the time? Could

This might be a stupid question but anyway... Is there someone well-versed in a statically typed language who would still prefer python most of the time? Could you explain why? For me it's just the opposite. When I program I think about the types first. When I read code I care more about types than variable names. This is in my opinion the way to go even in C. Also most python programmers I know are engineers and for them it would be a waste of time to learn C++. I would like to know why an experienced developer might prefer python ...

mixmastamyk 6y ago
When I program I think of business problems to be solved. Types barely register. Yes, on a big project with lots of developers types become more of a priority. At that point I let an IDE worry about them.
- _jjkk 6y ago
  This is the reason for me as well. Many problems map very easily and readably to simple lists and dictionaries. The easiest example is web applications, especially internal ones, which are essentially shuffling JSON messages around from different SaaS and internal APIs. Adding (and testing!) a different ApiResultSerializer in between each of these points can become a huge headache when everything boils down to JSON string or number in your result anyway. Though I do use C / C++ (recently some Rust) where business problems are not the priority, and I can focus on technical efficiency / correctness.
ywei3410 6y ago
Sure — for context I’m very comfortable with Haskell, Typescript, Java and Scala, fairly comfortable with Agda, Coq, C and Rust. I don’t prefer Python (the reasons of which I can elaborate, if you’re interested), but I do prefer to do my programming in Lisp-like dynamic languages — even when not using meta-programming. The reason for this is quite simple. A static type-system, by design is meant to invalidate programs which are incorrect and accept the programs which are correct. All static type-systems which exist invalidate a certain number of programs which are correct — that is to say, you can write a perfectly valid program, but the type-system can reject it. What we term to be a more expressive type-system, is one which rejects more programs. The line which one draws in the sand as expressive enough is completely arbitrary and the type-systems we have currently heavily rely on the user constructing their programs in a certain way, so the type-system can prove certain properties about it. Here’s an example demonstrating what I mean. Consider a theoretical language which uses : as the type-ascription, has generics/kinds and all functions are total. A code-snippet taking the head of a list might look like this: > let num: Option<Number> = head(numberList) Note that the return type of the head will be Option<A>, if the function is total because the list can be empty. Now suppose I have the snippet — locally I can reason that the type of num should be Number — but I need to prove that to the type-system. In most current type-systems, proving this requires you restructure your code in a particular way. > let numberList = prependList(4, previousList) > let sortedList = sortList(numberList) > let num = head(sortedList) What I’m trying to drive at is that static type-systems are a spectrum and at some point you will run into a case which you’ll either need to use an escape-hatch or restructure your code in a non-trivial way to satisfy the compiler. The boundary of what you determine to be correct is also completely arbitrary — you can always encode more properties and restrict your code further; how far you go is ultimately determined by you.
- the5avage 6y ago
  Thanks for the lengthy reply ;) I'm aware of the fact that every type system will reject some valid programs. C evades this problem by letting you "escape" the type system. Many people criticize this without being aware that the language would be useless without this feature. I don't think that an expressive type system rejects more programs though. You don't have to escape the type system that often in C++ (compared to C). Nonetheless I probably should look up some design patterns you can do in lisp, to get a feel for what I'm missing

mixmastamyk 6y ago

When I program I think of business problems to be solved. Types barely register. Yes, on a big project with lots of developers types become more of a priority. At that point I let an IDE worry about them.

_jjkk 6y ago
This is the reason for me as well. Many problems map very easily and readably to simple lists and dictionaries. The easiest example is web applications, especially internal ones, which are essentially shuffling JSON messages around from different SaaS and internal APIs. Adding (and testing!) a different ApiResultSerializer in between each of these points can become a huge headache when everything boils down to JSON string or number in your result anyway. Though I do use C / C++ (recently some Rust) where business problems are not the priority, and I can focus on technical efficiency / correctness.

ywei3410 6y ago

Sure — for context I’m very comfortable with Haskell, Typescript, Java and Scala, fairly comfortable with Agda, Coq, C and Rust. I don’t prefer Python (the reasons of which I can elaborate, if you’re interested), but I do prefer to do my programming in Lisp-like dynamic languages — even when not using meta-programming. The reason for this is quite simple. A static type-system, by design is meant to invalidate programs which are incorrect and accept the programs which are correct. All static type-systems which exist invalidate a certain number of programs which are correct — that is to say, you can write a perfectly valid program, but the type-system can reject it. What we term to be a more expressive type-system, is one which rejects more programs. The line which one draws in the sand as expressive enough is completely arbitrary and the type-systems we have currently heavily rely on the user constructing their programs in a certain way, so the type-system can prove certain properties about it. Here’s an example demonstrating what I mean. Consider a theoretical language which uses : as the type-ascription, has generics/kinds and all functions are total. A code-snippet taking the head of a list might look like this: > let num: Option<Number> = head(numberList) Note that the return type of the head will be Option<A>, if the function is total because the list can be empty. Now suppose I have the snippet — locally I can reason that the type of num should be Number — but I need to prove that to the type-system. In most current type-systems, proving this requires you restructure your code in a particular way. > let numberList = prependList(4, previousList) > let sortedList = sortList(numberList) > let num = head(sortedList) What I’m trying to drive at is that static type-systems are a spectrum and at some point you will run into a case which you’ll either need to use an escape-hatch or restructure your code in a non-trivial way to satisfy the compiler. The boundary of what you determine to be correct is also completely arbitrary — you can always encode more properties and restrict your code further; how far you go is ultimately determined by you.

the5avage 6y ago
Thanks for the lengthy reply ;) I'm aware of the fact that every type system will reject some valid programs. C evades this problem by letting you "escape" the type system. Many people criticize this without being aware that the language would be useless without this feature. I don't think that an expressive type system rejects more programs though. You don't have to escape the type system that often in C++ (compared to C). Nonetheless I probably should look up some design patterns you can do in lisp, to get a feel for what I'm missing