4 ms·

There is a movement going on from weak typing back to strong typing which is the same idea approached from the opposite (practical) end. Have the computer do mo

by Joeri 9y ago

There is a movement going on from weak typing back to strong typing which is the same idea approached from the opposite (practical) end. Have the computer do more work to verify program correctness by rejecting invalid expressions. Maybe the two will meet at some point?

Joe-Z 9y ago
I never got the excitement that some of my college classmates had for JavaScript because they didn't have to 'deal with types'. I always much preferred a compiler telling me that this won't work instead of having to find some obscure type bug at runtime. Don't get me wrong, I still very much liked programming in JavaScript for other merits, especially the functional aspect or flexibility of extending your program simply in a browser command line window. EDIT: I kind of got distracted by my JavaScript-story here. What I originally wanted to post was: I always had an interest in philosophy and the logical thinking you can apply in software development (i.e. you can save yourself so much trouble by just thinking through your system thoroughly before writing even one line of code). However, the general sentinment that I also got from a lot of my classmates was that they didn't want have anything to do 'with any of this stuff' (this stuff being the humanities) but didn't have a problem with cracking hard math problems day in day out (which for me at least is pretty similar to using logical thinking / philosophy on a less abstract level). Sorry, if by my large edit I confused some people!
- supernintendo 9y ago
  You should look into TypeScript if you haven't already. It's not perfect, but I think it strikes a nice balance between those two approaches. It's my "go-to" for new frontend projects because I enjoy the compiler's flexibility in regards to type checking. I can explore alternate approaches to solving the same problem (and by proxy, tests) and gradually introduce stronger compile-time checks as the solution comes together.
  - Joe-Z 9y ago
    Thanks for the input. In my place of work, where I mainly use C#/.NET, we are in the process of planning to implement a new frontend for one of our services. I was totally looking forward to using this to get some experience with TypeScript!
- losteric 9y ago
  It's a question of balancing planning with acceptable ambiguity. Types add compile-time assertions but the cost is a constant mandatory overhead that still requires behavioral testing. For my space, I prefer well designed systems and TDD/dynamically typed code. However, I absolutely agree that "systems thinking" is seriously underemphasized in undergrad. Bad algorithms are replaceable, bad systems require deeply invasive refactors.
- buzzybee 9y ago
  You wouldn't be alone as a philosopher-developer, there are a decent number of us out there. However - shipping code is often very organic, cultivated stuff which foils attempts to establish a coherent philosophy, a through-line of "how it works" - it works because it worked the day before, all that changed was that a little bit more was added. Repeat till broken, then refactor back to sanity(else abandon ship). It's Sisyphean hill-climbing. This in turn plays into the falsity of "engineering" as a way to describe what's going on with a lot of code. You can do it in the small, but at any scale the codebase habitually becomes a living organism. And that tends to get puzzle-solver types excited, because if it's alive and keeps changing, then they will have endless problems to solve forever! So I believe the philosophers of the crowd ultimately tend to move away from the applications coalface and look for something relatively smaller that does allow some time for reflection and distillation of the problem.
  - Joe-Z 9y ago
    I find your last paragraph very interesting. May I ask, did you make that move yourself and, if so, where to? In my daily work I often refactor an old, organically grown, codebase and that's exactly what I do: I try to think of what the system actually is / should be and try to put this in code in as concise terms as possible (that's kind of a general description of software development, but I just wanted to contrast this to simply hammering in the quickest fix you can think of). A lot of times I wonder though, if that is really what is needed and a simple 'prototyper' kind-of-developer would get the job done faster, although maybe not as elegantly (slight humble-brag there).
no_wizard 9y ago
So....Medium typing? Would that just be all the inference of Python mixed with the literalness of Swift?
- Joeri 9y ago
  Actually I meant that the formal proof to code and the strongly typed code camps would eventually meet, as the type system grows richer it may approximate a proof.
  - SAI_Peregrinus 9y ago
    The Homotopy Type Theory folks are way ahead of you on that one.
watwut 9y ago
For me the biggest advantage of strong typing is ide quality that follows - refactoring support ans code completion are much much better for example. Makes work on larger project significantly easier.
jameslk 9y ago
Although you make no citations of your claim, I think you mean a trend towards static typing over dynamic typing. Strongly typed languages are already pretty common.
- Joeri 9y ago
  No, I meant what I said. I'm talking about mindshare, with e.g. typescript gaining ground on javascript, or php 7's strictly typed style gaining ground over php 5's loose style, which is all in the dynamically typed camp.
  - jameslk 9y ago
    TypeScript brings static type analysis to JavaScript, not strong typing. I'm not sure what you mean by PHP 7's "strictly typed style" but I assume you mean its type annotations, which it's had since PHP 5. Those are neither a case of strong typing (PHP is duck typed) nor static typing (since it's evaluated at runtime).
zitterbewegung 9y ago
The two have already met. In Python you have optional typing [1] . Or in JavaScript you could use Flow [2] for static type checking. Also you could interface JavaScript with Typescript [3] [1] https://docs.python.org/3/library/typing.html https://docs.python.org/3/library/typing.html [2]https://flow.org https://flow.org [3] https://en.m.wikipedia.org/wiki/TypeScript#Compatibility_with_JavaScript https://en.m.wikipedia.org/wiki/TypeScript#Compatibility_wit...
- wozer 9y ago
  Python itself does not have optional typing, only optional type hints. You need additional tools for the type checking, and these tools are in experimental stage.
tunesmith 9y ago
My sense is that it won't really get close to meeting until dependent types are more mainstream. Idris is out there but not sure how usable it will end up being. Haskell and Dotty seem to getting closer even though I don't believe they entirely support dependent types.
Animats 9y ago
To some extent, they have. The big breakthrough was "auto" in C++. (I wanted to call it "let", but that involved introducing a new keyword.) The type of a local variable in C++ is quite verbose for iterators. This discouraged the use of iterators in FOR statements. With "auto", you can write for (auto p = thing.begin(); p != thing.end(); p++) { ... } for anything that uses an iterator. No need to write out the whole iterator declaration for p. Or to generate it in a template. Suddenly, iterators became far easier to use. Since then, Go and Rust have taken a similar approach of limited type inference. There seems to be a developing consensus that function parameters should have explicitly declared types, but within a function, type information should be inferred when possible. We're seeing convergence from the other direction, with Python and Javascript (via add-ons such as TypeScript) acquiring type declarations. So the two are meeting.
emmelaich 9y ago
This convergence (deliberate or not) has been noticed. I've seen a diagram like this http://wordaligned.org/articles/programming-nirvana-plan-b http://wordaligned.org/articles/programming-nirvana-plan-b but with more detail. ie. with C++, Java, Python placed in there somewhere. (probably in the linked paper, but I can't access it now)

by Joeri 9y ago

Joe-Z 9y ago

I never got the excitement that some of my college classmates had for JavaScript because they didn't have to 'deal with types'. I always much preferred a compiler telling me that this won't work instead of having to find some obscure type bug at runtime. Don't get me wrong, I still very much liked programming in JavaScript for other merits, especially the functional aspect or flexibility of extending your program simply in a browser command line window. EDIT: I kind of got distracted by my JavaScript-story here. What I originally wanted to post was: I always had an interest in philosophy and the logical thinking you can apply in software development (i.e. you can save yourself so much trouble by just thinking through your system thoroughly before writing even one line of code). However, the general sentinment that I also got from a lot of my classmates was that they didn't want have anything to do 'with any of this stuff' (this stuff being the humanities) but didn't have a problem with cracking hard math problems day in day out (which for me at least is pretty similar to using logical thinking / philosophy on a less abstract level). Sorry, if by my large edit I confused some people!

supernintendo 9y ago
You should look into TypeScript if you haven't already. It's not perfect, but I think it strikes a nice balance between those two approaches. It's my "go-to" for new frontend projects because I enjoy the compiler's flexibility in regards to type checking. I can explore alternate approaches to solving the same problem (and by proxy, tests) and gradually introduce stronger compile-time checks as the solution comes together.
- Joe-Z 9y ago
  Thanks for the input. In my place of work, where I mainly use C#/.NET, we are in the process of planning to implement a new frontend for one of our services. I was totally looking forward to using this to get some experience with TypeScript!
losteric 9y ago
It's a question of balancing planning with acceptable ambiguity. Types add compile-time assertions but the cost is a constant mandatory overhead that still requires behavioral testing. For my space, I prefer well designed systems and TDD/dynamically typed code. However, I absolutely agree that "systems thinking" is seriously underemphasized in undergrad. Bad algorithms are replaceable, bad systems require deeply invasive refactors.
buzzybee 9y ago
You wouldn't be alone as a philosopher-developer, there are a decent number of us out there. However - shipping code is often very organic, cultivated stuff which foils attempts to establish a coherent philosophy, a through-line of "how it works" - it works because it worked the day before, all that changed was that a little bit more was added. Repeat till broken, then refactor back to sanity(else abandon ship). It's Sisyphean hill-climbing. This in turn plays into the falsity of "engineering" as a way to describe what's going on with a lot of code. You can do it in the small, but at any scale the codebase habitually becomes a living organism. And that tends to get puzzle-solver types excited, because if it's alive and keeps changing, then they will have endless problems to solve forever! So I believe the philosophers of the crowd ultimately tend to move away from the applications coalface and look for something relatively smaller that does allow some time for reflection and distillation of the problem.
- Joe-Z 9y ago
  I find your last paragraph very interesting. May I ask, did you make that move yourself and, if so, where to? In my daily work I often refactor an old, organically grown, codebase and that's exactly what I do: I try to think of what the system actually is / should be and try to put this in code in as concise terms as possible (that's kind of a general description of software development, but I just wanted to contrast this to simply hammering in the quickest fix you can think of). A lot of times I wonder though, if that is really what is needed and a simple 'prototyper' kind-of-developer would get the job done faster, although maybe not as elegantly (slight humble-brag there).

no_wizard 9y ago

So....Medium typing? Would that just be all the inference of Python mixed with the literalness of Swift?

Joeri 9y ago
Actually I meant that the formal proof to code and the strongly typed code camps would eventually meet, as the type system grows richer it may approximate a proof.
- SAI_Peregrinus 9y ago
  The Homotopy Type Theory folks are way ahead of you on that one.

watwut 9y ago

For me the biggest advantage of strong typing is ide quality that follows - refactoring support ans code completion are much much better for example. Makes work on larger project significantly easier.

jameslk 9y ago

Although you make no citations of your claim, I think you mean a trend towards static typing over dynamic typing. Strongly typed languages are already pretty common.

Joeri 9y ago
No, I meant what I said. I'm talking about mindshare, with e.g. typescript gaining ground on javascript, or php 7's strictly typed style gaining ground over php 5's loose style, which is all in the dynamically typed camp.
- jameslk 9y ago
  TypeScript brings static type analysis to JavaScript, not strong typing. I'm not sure what you mean by PHP 7's "strictly typed style" but I assume you mean its type annotations, which it's had since PHP 5. Those are neither a case of strong typing (PHP is duck typed) nor static typing (since it's evaluated at runtime).

zitterbewegung 9y ago

The two have already met. In Python you have optional typing [1] . Or in JavaScript you could use Flow [2] for static type checking. Also you could interface JavaScript with Typescript [3] [1] https://docs.python.org/3/library/typing.html https://docs.python.org/3/library/typing.html [2]https://flow.org https://flow.org [3] https://en.m.wikipedia.org/wiki/TypeScript#Compatibility_with_JavaScript https://en.m.wikipedia.org/wiki/TypeScript#Compatibility_wit...

wozer 9y ago
Python itself does not have optional typing, only optional type hints. You need additional tools for the type checking, and these tools are in experimental stage.

tunesmith 9y ago

My sense is that it won't really get close to meeting until dependent types are more mainstream. Idris is out there but not sure how usable it will end up being. Haskell and Dotty seem to getting closer even though I don't believe they entirely support dependent types.

Animats 9y ago

To some extent, they have. The big breakthrough was "auto" in C++. (I wanted to call it "let", but that involved introducing a new keyword.) The type of a local variable in C++ is quite verbose for iterators. This discouraged the use of iterators in FOR statements. With "auto", you can write for (auto p = thing.begin(); p != thing.end(); p++) { ... } for anything that uses an iterator. No need to write out the whole iterator declaration for p. Or to generate it in a template. Suddenly, iterators became far easier to use. Since then, Go and Rust have taken a similar approach of limited type inference. There seems to be a developing consensus that function parameters should have explicitly declared types, but within a function, type information should be inferred when possible. We're seeing convergence from the other direction, with Python and Javascript (via add-ons such as TypeScript) acquiring type declarations. So the two are meeting.

emmelaich 9y ago

This convergence (deliberate or not) has been noticed. I've seen a diagram like this http://wordaligned.org/articles/programming-nirvana-plan-b http://wordaligned.org/articles/programming-nirvana-plan-b but with more detail. ie. with C++, Java, Python placed in there somewhere. (probably in the linked paper, but I can't access it now)