Code is Engineering, Types are Science(tweag.io)
tweag.io
Code is Engineering, Types are Science
https://www.tweag.io/blog/2020-03-05-peirce/
69 comments
I could write a multi-paragraph comment explaining why statically typed languages are better, but I’ll just say that I always see projects that were written in dynamic languages being rewritten in static languages, and never the other way around, fwiw.
I never heard anyone say “let’s rewrite this in Node” unironically.
I never heard anyone say “let’s rewrite this in Node” unironically.
At my work we've rewritten a few things to Clojure from Java and Scala. So at least now you've got one known data-point to the contrary.
Thank you :) I’ve been meaning to try Clojure out.
You might be interested in reading about spec[0] and as always, a Rich Hickey video on it[1].
[0] https://clojure.org/guides/spec
[1] https://www.youtube.com/watch?v=oyLBGkS5ICk
[0] https://clojure.org/guides/spec
[1] https://www.youtube.com/watch?v=oyLBGkS5ICk
We do use Spec heavily, we use it to define our domain data model for all data which crosses the application boundary (data which we will persist to disk, database, or data which we send/receive from other services (over APIs), or data which we take from the user or return to the user.
What we've found happens to us, is that because Clojure is dynamically typed, we actually spend more time focusing on making sure we have well specified and properly designed our data model for data which enters/leaves the application boundary, and that we use runtime validation everytime the data is about to leave the app boundary or enter it from a non-trusted source.
When we used Java and Scala, we did not spend quite as much time here, because you've already got your internal types, and you kind of take them as your data model, and rely on them for validation and specification. The issue is the types only go so far to perform validation, and you've often designed them in terms of the implementation needs, and not the domain model. A dynamically typed language like Clojure teaches you to be extra careful with data to make sure you don't mess it up, and it gives you really powerful tools for it, such as Spec and the REPL.
This turns out to help I've found in an enterprise context, because even with a statically typed language, when data enters/leaves the boundary of the application it is no longer within the purview of the type checker.
So with Clojure, we end up spending way more time thinking through our domain model and validating it. Which worked pretty well for us.
You also need to learn how to properly design an app in Clojure, and it's very different than other languages, so it's possible to overcomplicate things and shoot yourself in the foot. But if you do it right, it makes for very simple code bases that are way smaller in LOC.
Generally, we have one module that specifies our data model for the bounded context of our app. Another module to construct, validate, convert, and manipulate entities from our data model. And then we have a main module with all our APIs, each API implementation lives in its own module. Shared logic exist in a shared module. And shared state exist in another shared module.
It takes a bit of a different mindset, like knowing to ski and then trying to learn to snowboard, but for me I ended up liking it much better, and the lack of static types didn't bother me, the strong functional immutable leaning of Clojure, along with the help of the interactive REPL development style makes up for it.
What we've found happens to us, is that because Clojure is dynamically typed, we actually spend more time focusing on making sure we have well specified and properly designed our data model for data which enters/leaves the application boundary, and that we use runtime validation everytime the data is about to leave the app boundary or enter it from a non-trusted source.
When we used Java and Scala, we did not spend quite as much time here, because you've already got your internal types, and you kind of take them as your data model, and rely on them for validation and specification. The issue is the types only go so far to perform validation, and you've often designed them in terms of the implementation needs, and not the domain model. A dynamically typed language like Clojure teaches you to be extra careful with data to make sure you don't mess it up, and it gives you really powerful tools for it, such as Spec and the REPL.
This turns out to help I've found in an enterprise context, because even with a statically typed language, when data enters/leaves the boundary of the application it is no longer within the purview of the type checker.
So with Clojure, we end up spending way more time thinking through our domain model and validating it. Which worked pretty well for us.
You also need to learn how to properly design an app in Clojure, and it's very different than other languages, so it's possible to overcomplicate things and shoot yourself in the foot. But if you do it right, it makes for very simple code bases that are way smaller in LOC.
Generally, we have one module that specifies our data model for the bounded context of our app. Another module to construct, validate, convert, and manipulate entities from our data model. And then we have a main module with all our APIs, each API implementation lives in its own module. Shared logic exist in a shared module. And shared state exist in another shared module.
It takes a bit of a different mindset, like knowing to ski and then trying to learn to snowboard, but for me I ended up liking it much better, and the lack of static types didn't bother me, the strong functional immutable leaning of Clojure, along with the help of the interactive REPL development style makes up for it.
This. And I would go so far as to argue that the up from cost of adding types is not as big as people make it out to be.
If I don't specify a type in the input, I have to check in the method body that what was passed in was something usable. Skip this is very bad, the best case scenario is something your code will error out on wrong input, the worst case is it computes the wrong result with no errors.
If I don't specify a type in the input, I have to check in the method body that what was passed in was something usable. Skip this is very bad, the best case scenario is something your code will error out on wrong input, the worst case is it computes the wrong result with no errors.
I can spend a day coding* in a typed language without compiling, and my code more often compile than not work first time with the tests all green.
The exact same thing happens with dynamic languages - as long as I skip the tests (or write bad tests).
The exact same thing happens with dynamic languages - as long as I skip the tests (or write bad tests).
have you ever seen a Java app log? you still got to check and handle on public facing functions.
When it comes time to rewrite, it's usually because you've got an application which was successful in satisfying the users/customers needs, and which most often reached that point going through lots of iterations, changes, trials and errors - accumulating technical debt in the process. At that point you've got pretty clear specs: what the original application does. Rewriting in a language which makes exploration slower, but long term maintainability easier, makes a lot of sense. This doesn't imply that using the latter language during the exploratory phase would have gotten better - or even the same - results.
I've seen it go both ways for various reasons. typically nothing to do with types.
I always see projects that were written in dynamic languages being rewritten in static languages, and never the other way around, fwiw.
Actually it was (and is) quite common to see crufty old (but statically typed) C++, Java, what-you-have-you re-written in Perl and/or Python (well before the introduction of type annotations, in the latter case).
Reason: there are multiple factors involved in choosing a suitable language, and static typing is just one of them (and by no means a universal deal-breaker).
I never heard anyone say “let’s rewrite this in Node” unironically.
Good for you (and I would never say that other than as a tired, old joke). But unfortunately "respect" for Node runs quite high in some circles, and not a few developers consider to be not just occasionally acceptable server-side language, but (from the way they talk about it) to be the bees knees basically.
Why? TypeScript of course.
Actually it was (and is) quite common to see crufty old (but statically typed) C++, Java, what-you-have-you re-written in Perl and/or Python (well before the introduction of type annotations, in the latter case).
Reason: there are multiple factors involved in choosing a suitable language, and static typing is just one of them (and by no means a universal deal-breaker).
I never heard anyone say “let’s rewrite this in Node” unironically.
Good for you (and I would never say that other than as a tired, old joke). But unfortunately "respect" for Node runs quite high in some circles, and not a few developers consider to be not just occasionally acceptable server-side language, but (from the way they talk about it) to be the bees knees basically.
Why? TypeScript of course.
Likewise, you never see anyone suggesting the removal of type annotations in Python. But you often see people comment that they should have been used in the production Python code.
I fully agree about static types, I just want to mention that TypeScript works well with Node, and can be quite nice.
> Are you going to actually get things done faster or better? Seems unlikely, especially in a world where requirements shift every five minutes and are ill-defined in the first place.
What is the value of tests?
If requirements are going to shift every five minutes then sure, tests hold you back. Tests in an inherited codebase defined how the system needed to work, not how the system will adapt to changing requirements. Often, particularly for small-enough and simple-enough systems, a human eye is much more flexible than any tests you could write in code.
But the fact of the matter is that the utter majority of software that runs in production (note that qualifier - excluding code that never makes it into production for a variety of reasons), stays in production. It's a corporate cash cow of one kind or another. Software in production needs to be maintained. Software vulnerabilities are reported, old versions hit end-of-life. Java 4 -> Java 5 -> Java 6 -> Java 8 -> Java 11 -> on and on and on. So the business case is very simple. You're forced to make changes and you want to make sure those changes don't kill your cash cow.
Tests check your application at run-time. Types check your application at compile-time. As a result they can provide both more dependable and quicker guarantees than waiting for a run-time test suite to finish running.
If you don't understand the value of tests, you haven't worked on a large enough, mature enough system, where the original engineers have all long left the company.
What is the value of tests?
If requirements are going to shift every five minutes then sure, tests hold you back. Tests in an inherited codebase defined how the system needed to work, not how the system will adapt to changing requirements. Often, particularly for small-enough and simple-enough systems, a human eye is much more flexible than any tests you could write in code.
But the fact of the matter is that the utter majority of software that runs in production (note that qualifier - excluding code that never makes it into production for a variety of reasons), stays in production. It's a corporate cash cow of one kind or another. Software in production needs to be maintained. Software vulnerabilities are reported, old versions hit end-of-life. Java 4 -> Java 5 -> Java 6 -> Java 8 -> Java 11 -> on and on and on. So the business case is very simple. You're forced to make changes and you want to make sure those changes don't kill your cash cow.
Tests check your application at run-time. Types check your application at compile-time. As a result they can provide both more dependable and quicker guarantees than waiting for a run-time test suite to finish running.
If you don't understand the value of tests, you haven't worked on a large enough, mature enough system, where the original engineers have all long left the company.
The comment you're replying to doesn't mention tests, but "a rigorous type system". So accusing OP of not understanding the value of tests seems pretty OT.
I think the parent is suggesting that by this logic, tests are also useless, but almost no engineers would argue against tests.
I'm not arguing against types either.
I'm specifically arguing against their fetishization and the way that some languages (and programmers) view everything as mathematical type transformation.
I guess i need to write my comments a bit more precisely.
I'm specifically arguing against their fetishization and the way that some languages (and programmers) view everything as mathematical type transformation.
I guess i need to write my comments a bit more precisely.
This static vs dynamic types stuff pops up in HN every two weeks with the same old arguments. After the twentieth time I decided that the people who argue about that just work on different types of projects and that's okay. Just remember, not everyone works in a monoproject with a million loc and not everyone does micro services where often you have the code in a few files following established conventions. Trying to force patterns in situations where they are suboptimal shows that some people value form much more than function and could be safely ignored.
Just to be clear, the actual article here is much more nuanced than its button-pushing title.
But like many things, I think type systems tend to encourage the thinking "if a little bit of medicine is good, it's best to drink the maximum possible amount of medicine". I think types make good handrails, it's crazy not to provide a little support from falling 16 stories because you tripped on your shoelace. But they don't necessarily need to keep people from intentionally jumping off the stairs, or walking up the stairs backwards, or taking two stairs at a time. Eventually you end up with something so contrived you don't even recognize it's a staircase at first sight.
But like many things, I think type systems tend to encourage the thinking "if a little bit of medicine is good, it's best to drink the maximum possible amount of medicine". I think types make good handrails, it's crazy not to provide a little support from falling 16 stories because you tripped on your shoelace. But they don't necessarily need to keep people from intentionally jumping off the stairs, or walking up the stairs backwards, or taking two stairs at a time. Eventually you end up with something so contrived you don't even recognize it's a staircase at first sight.
I don't understand why people still think static types makes programming slower. If anything they make me quite a bit faster. Especially if the problem domain is shifting. Without types I have to spend a lot of time hunting down forgotten parts of the code where I didn't apply a refactor. With types the compiler just tells me and I can fix those errors in record time.
As someone who works on a decently complex project (essentially a graph execution engine for multi-node, data-parallel+model-parallel deep learning models), writing it in python is not really ideal. Python is great for the end user, but I’d be far more efficient if the code base was in C++ with some Python bindings. I think my conclusion after about 10 years of programming is this: the larger and more complicated a project is, the more I as a maintainer/implementer benefit from constraints in the language itself (where by constraints I mean things like compiler type checking, or Rusts borrow checker, even if I haven’t had a reason to use Rust yet). The more work the compiler/interpreter does, the less I have to explicitly keep in my head.
I agree. The same people who argue that types make programs slower to write and harder to maintain also argue (incorrectly) that tests have all of the benefits of types and then some. But if you’re writing lots of tests to compensate for types (and indeed I hear many dynamic typing advocates argue for exactly this) then your code is far harder to change than it would be if you just used types in the first place (and for the same reasons that it’s easier to write typed code and a few tests rather than i typed code and lots of tests).
Not only does it not make sense in theory, but in my 15 years with Python and 10 years with Go, it bears out in practice. I’m much more productive in Go because of the tooling and confidence that follow from static types, and that delta only increases as the project grows in lines of code, contributors, and/or age.
Not only does it not make sense in theory, but in my 15 years with Python and 10 years with Go, it bears out in practice. I’m much more productive in Go because of the tooling and confidence that follow from static types, and that delta only increases as the project grows in lines of code, contributors, and/or age.
A really good talk on the myth of "testing makes static types unnecessary" from Gary Bernhardt (Wat Talk)
https://www.destroyallsoftware.com/talks/ideology
https://www.destroyallsoftware.com/talks/ideology
It's because when developers are handed an abstraction like static types, they will tend to go as far as possible to create overengineered solutions using that tool, creating complexity that becomes a problem in its own right.
TypeScript in particular has been adding features at far too fast a pace, creating wild amounts of complexity in the type system. This is from one popular type library. Type theorists may enjoy this. I personally would not if I am onboarding to a new codebase and trying to understand this at a glance.
TypeScript in particular has been adding features at far too fast a pace, creating wild amounts of complexity in the type system. This is from one popular type library. Type theorists may enjoy this. I personally would not if I am onboarding to a new codebase and trying to understand this at a glance.
export type CamelCasedPropertiesDeep<Value> = Value extends Function
? Value
: Value extends Array<infer U>
? Array<CamelCasedPropertiesDeep<U>>
: Value extends Set<infer U>
? Set<CamelCasedPropertiesDeep<U>> : {
[K in keyof Value as CamelCase<K>]: CamelCasedPropertiesDeep<Value[K]>;
};With a powerful type system, I think you tend to see examples of libraries that fall along a spectrum of how deep into the type system they're willing to go.
This is an example of the farther end, but "ideally" as a user of the library, the actual complexity would be hidden, and it "just works" for you.
This is an example of the farther end, but "ideally" as a user of the library, the actual complexity would be hidden, and it "just works" for you.
> Are you going to actually get things done faster or better?
Faster: depends on what you’re used to. Personally I find strongly typed languages faster to work with evolved code bases. Where you’re refactoring code or dealing with unfamiliar API you get very clear compiler warnings and that becomes as powerful an aid as code coverage in your test suites. When writing new code, it does take marginally longer. But so does many other best practices in software development that are skewed towards maintainability (like writing tests in the first place).
Better: my favourite example of this is when you need to store a serial like “012345”. Without telling the compiler/runtime that it’s a string you run the risk of all sorts of uncaptured bugs. So personally I think typed code is better code. You don’t need to be scientific with how you use type systems either. This specific bug is captured just using a string instead of an integer.
Faster: depends on what you’re used to. Personally I find strongly typed languages faster to work with evolved code bases. Where you’re refactoring code or dealing with unfamiliar API you get very clear compiler warnings and that becomes as powerful an aid as code coverage in your test suites. When writing new code, it does take marginally longer. But so does many other best practices in software development that are skewed towards maintainability (like writing tests in the first place).
Better: my favourite example of this is when you need to store a serial like “012345”. Without telling the compiler/runtime that it’s a string you run the risk of all sorts of uncaptured bugs. So personally I think typed code is better code. You don’t need to be scientific with how you use type systems either. This specific bug is captured just using a string instead of an integer.
I don't think static types significantly impede productivity, but let's say they do. They still increase safety significantly. They still help you keep a mental model of what code has what properties. Even if dynamic types allow you to write code faster, so what if the code is more dangerous, more likely to cause security exploits? If a delivery company said "we don't believe in airbags because they slow down deliveries", would you be okay with that? No, probably not. So why would any of us be okay with companies that handle billions of people's data using unsafe languages?
P.S. I'm not saying dynamic types are always bad. There's certainly a time and a place for them. But there's a reason demanding systems software like browsers, databases, networks are being written in Rust these days.
P.S. I'm not saying dynamic types are always bad. There's certainly a time and a place for them. But there's a reason demanding systems software like browsers, databases, networks are being written in Rust these days.
>rather than merely apply mathema^H^H^H^^H^H^H^H logical operations within constraints.
This is what all programming and software engineering is - logical operations within constraints. Types make those constraints more explicit, and make them work for you rather than against you.
They make refactoring of large-scale systems more tractable and less painful, which is invaluable when requirements are shifting. And they can eliminate entire classes of errors, bugs, and security vulnerabilities at compile time, which is invaluable in a day and age when everything is getting hacked.
As type systems become increasingly sophisticated, those benefits become even more true. And when you take into account all the man hours spent on a system, not just in building the quick and dirty initial prototype, but in debugging it for production, and then maintaining it over a long period of time with eventually 100% turnover of the initial dev team, then types reduce time and effort spent too.
You should read the famous paper Out of the Tarpit. Type systems are one of the best solutions to the tarpit of complexity that large systems inevitably incur.
http://curtclifton.net/papers/MoseleyMarks06a.pdf
This is what all programming and software engineering is - logical operations within constraints. Types make those constraints more explicit, and make them work for you rather than against you.
They make refactoring of large-scale systems more tractable and less painful, which is invaluable when requirements are shifting. And they can eliminate entire classes of errors, bugs, and security vulnerabilities at compile time, which is invaluable in a day and age when everything is getting hacked.
As type systems become increasingly sophisticated, those benefits become even more true. And when you take into account all the man hours spent on a system, not just in building the quick and dirty initial prototype, but in debugging it for production, and then maintaining it over a long period of time with eventually 100% turnover of the initial dev team, then types reduce time and effort spent too.
You should read the famous paper Out of the Tarpit. Type systems are one of the best solutions to the tarpit of complexity that large systems inevitably incur.
http://curtclifton.net/papers/MoseleyMarks06a.pdf
> Type systems are one of the best solutions to the tarpit of complexity that large systems inevitably incur.
(Disclaimer: I haven't read the paper you linked.) Also, type systems aren't the only game in town, but they're more approachable than the alternatives. Type systems are a walk in the park compared to formal verification frameworks, for instance. If you write your project in verified SPARK, the prover will take all the guess work out of the interactions between subsystems, but again, verified SPARK is no cakewalk.
If your ambitions are no higher than throwing together a giant ball of mud that's impossible to precisely reason about, then sure, stick with an anaemic static type system or a dynamically typed language. As a discipline though, we have the means to do better. (Are my biases showing?)
As I mentioned in my other comment, various modern statically typed languages have decisively eliminated null-dereference errors. That kind of thing can't be achieved if the programming environment is a free-for-all.
To quote an obscure novel, Nothing is an absolute reality; all is permitted. So it is in the dynamically typed world.
(Disclaimer: I haven't read the paper you linked.) Also, type systems aren't the only game in town, but they're more approachable than the alternatives. Type systems are a walk in the park compared to formal verification frameworks, for instance. If you write your project in verified SPARK, the prover will take all the guess work out of the interactions between subsystems, but again, verified SPARK is no cakewalk.
If your ambitions are no higher than throwing together a giant ball of mud that's impossible to precisely reason about, then sure, stick with an anaemic static type system or a dynamically typed language. As a discipline though, we have the means to do better. (Are my biases showing?)
As I mentioned in my other comment, various modern statically typed languages have decisively eliminated null-dereference errors. That kind of thing can't be achieved if the programming environment is a free-for-all.
To quote an obscure novel, Nothing is an absolute reality; all is permitted. So it is in the dynamically typed world.
Fetishization is the correct word for it.
Most people, especially the ones who think typing everything is a great idea, don't understand the difference between types and constraints.
Constraints, for some reason, are incredibly easy for humans to understand. Simple constraints and types match well enough that pretty much all tutorial examples can be done in either without too much difficulty. That gives people the misplaced confidence that everything that can be done in constraints can be done in types. Which is simply not the case.
For the simplest example: what is the type of the identity function? You get into polymorphic types and type variables to get a satisfactory answer, which is by no means obviously true, and fall down the rabbit hole of having your type system be Turing complete too. Which kind of defeats the purpose of types since now you have to deal with all the goodness of undecidability not only horizontally in your code, but vertically in your types.
That is not to say that types are useless, they aren't, but when you start really dealing with higher order functions they are not worth the hassle as defined in any language today.
Most people, especially the ones who think typing everything is a great idea, don't understand the difference between types and constraints.
Constraints, for some reason, are incredibly easy for humans to understand. Simple constraints and types match well enough that pretty much all tutorial examples can be done in either without too much difficulty. That gives people the misplaced confidence that everything that can be done in constraints can be done in types. Which is simply not the case.
For the simplest example: what is the type of the identity function? You get into polymorphic types and type variables to get a satisfactory answer, which is by no means obviously true, and fall down the rabbit hole of having your type system be Turing complete too. Which kind of defeats the purpose of types since now you have to deal with all the goodness of undecidability not only horizontally in your code, but vertically in your types.
That is not to say that types are useless, they aren't, but when you start really dealing with higher order functions they are not worth the hassle as defined in any language today.
Taking the opportunity to point out, with most inferred type languages (mypy python, go, TS, rust, scala), you often don't have to write variable types at all, only functions. Gone are the days of `Foobar foob = new Foobar`, heck C++ has had `auto` for a decade.
So have your dynamic language functions you have to document (you do document your code right?), why not just use types instead? I'd far rather see
So have your dynamic language functions you have to document (you do document your code right?), why not just use types instead? I'd far rather see
def frob(data: np.ndarray) -> float:
<code with no docstring>
def frob(data):
"""takes an array and frobs it to give the frobitude score"""
At least call it frob_score.
If we're talking about getting things done, there's nothing worse than banging out some work, and then later finding out it's utter nonsense, because of some incredibly silly mistake ... like types getting messed up: https://www.sciencemag.org/news/2016/08/one-five-genetics-pa...
In the practice of software engineering, I would really hope we move away from the attitude of 'move fast'/'get things done' and more towards 'do it right', because I sure am tired of seeing these silly avoidable type errors continue to mess with people's work and lives day after day.
In the practice of software engineering, I would really hope we move away from the attitude of 'move fast'/'get things done' and more towards 'do it right', because I sure am tired of seeing these silly avoidable type errors continue to mess with people's work and lives day after day.
> Are you going to actually get things done faster or better? Seems unlikely
A simple concrete example: a language can use a static type system to make it impossible to encounter a null-dereference error at runtime. That guarantee is a very practical benefit for any codebase.
A simple concrete example: a language can use a static type system to make it impossible to encounter a null-dereference error at runtime. That guarantee is a very practical benefit for any codebase.
First financial application where you accidentally assign a string to an int or NaN gets treated as 0 (implicit floating point when dealing with fixed point money = shudder) makes you enthusiastic about static typing real fast.
You are confusing static and dynamic and weak and strong typing.
For all practical discussions (i.e. top 10 languages used in real world production), when people say static they mean strong+static.
I am more productive using types. You apparently aren’t. Some developers love types. Some don’t. OK fine. So what? Use what works for you. In the real world almost all software you use is typed (your OS, your compiler, your browser etc. etc.) but hey that doesn’t mean you have to use a typed language. Why the need/insistence that everybody has to use the same tools?
It seems nobody actually got what I was trying to say, which is on me in the end.
Types are fine, they're really useful. I just think they can be taken too far, particularly in the realm of mathematically-focused languages like Haskell, where there appears to be an idea that everything is types and your program is merely a description of changes between them. I find this sort of thing overly abstract and at the same time brittle.
:shrug:
Types are fine, they're really useful. I just think they can be taken too far, particularly in the realm of mathematically-focused languages like Haskell, where there appears to be an idea that everything is types and your program is merely a description of changes between them. I find this sort of thing overly abstract and at the same time brittle.
:shrug:
I'm increasingly frustrated by industry trends of more types. After 20 years I like typing less and less. Even with c++ code bases tend toward various methods of eliminating strong typing. Javascript didn't need types. pythons type hint are close to ideal, but anything other than primitive almost isn't worth adding type hints. who doesn't just toss args in a dict?
> who doesn't just toss args in a dict?
Me? Args in a dict, or worse, `**kwargs` chained through multiple functions, are awful to deal with.
I'm really curious about your stance. If anything, typing has gotten easier and better over 20 years. Types used to be verbose, you had to type out all characters, compiler messages were terrible. Now, type systems are better, inferred, flexible and structural subtyping is great. Type checkers are almost real-time. Autocomplete saves me keystrokes. Errors are helpful.
I used to hate types, 10 years ago, writing Java in Notepad++. Now I write python w/ mypy, go, and rust in Intellij, with lots of plugins to speed up autocomplete, and lint in real time.
Me? Args in a dict, or worse, `**kwargs` chained through multiple functions, are awful to deal with.
I'm really curious about your stance. If anything, typing has gotten easier and better over 20 years. Types used to be verbose, you had to type out all characters, compiler messages were terrible. Now, type systems are better, inferred, flexible and structural subtyping is great. Type checkers are almost real-time. Autocomplete saves me keystrokes. Errors are helpful.
I used to hate types, 10 years ago, writing Java in Notepad++. Now I write python w/ mypy, go, and rust in Intellij, with lots of plugins to speed up autocomplete, and lint in real time.
I love your comment. I'm the complete opposite of you I thought python was stupid when I was younger and thought c++ was awesome and things should be well typed. now I'm crotchety and avoid typed languages. all you need is data and functions - I know not everyone thinks this way.
Thanks for the reply! I think it highlights the fact that much of the "typing wars" depends a huge amount on what you're working on and how you like to work.
I wager much strain comes simply from individuals working in environments that force them to lean on their weaknesses.
I was absolutely floundering in one department simply because the senior devs loved bash and python2 and dynamic runtime everything and my brain couldn't keep up with the lack of structure.
I wager much strain comes simply from individuals working in environments that force them to lean on their weaknesses.
I was absolutely floundering in one department simply because the senior devs loved bash and python2 and dynamic runtime everything and my brain couldn't keep up with the lack of structure.
Why call it "fetishization?" That seems like you're looking for a fight.
Because IMHO there's reasonable use of types and then there's "the type system is the code and the application is expressed merely as type transformations", which to me is fetishisation of types over getting things done.
I'm not trying to say all types are bad.
I'm not trying to say all types are bad.
To be fair, typed languages usually allow polymorphism, creating an opportunity for increased productivity.
Which typed languages are you familiar with?
C, C++, Java are the languages I've worked in most over my career, though lately there's been more Go. They have types, to a greater or lesser extent, and they're useful.
The sort of fetishisation I'm talking about tends to happen when we start talking about things like Haskell, AFAICT.
Types are useful. Offloading everything to types and thinking about everything in terms of type transformation, not so much.
The sort of fetishisation I'm talking about tends to happen when we start talking about things like Haskell, AFAICT.
Types are useful. Offloading everything to types and thinking about everything in terms of type transformation, not so much.
You should check out OCaml, Rust or Scala.
Funny that until yesterday,
I had never even heard the name Idris, and now I find it mentioned in two HN articles within 24 hours.
Will definitely check it out as I’m fond of types. But I also like to imagine Big Typecheck trying to manipulate HN readers into abandoning untyped languages.
Will definitely check it out as I’m fond of types. But I also like to imagine Big Typecheck trying to manipulate HN readers into abandoning untyped languages.
Here is my view on this.
In the beginning types were useless and hard.
Then we made typeless languages so we didn't need to bother with useless and hard types.
Then we figured out how to make types easier and useful.
1. C - types represent memory layout, which the programmer doesn't care about, are not useful for error handling and control flow and you have to type them out and remember which one is which.
2. Python - Yolo, nothing matters, everything goes. eZ. Shit, why does this code break after refactoring?
3. Rust - Types are inferred, IDEs and the compiler basically tell you what to do and the types are safeguards, rails and handle logic.
Best thing: most of this stuff goes back to the olde languages as well. I.e. IDEs make types in C easier, type hints in Python help with refactoring and so on.
So I think w won't even need to manipulate people out if untyped languages. The academic research that helps make programming better will reach all popular languages.
(Please don't every example to verbatim - it's just a rough outline of an idea not meant to be an in depth analysis. Of course types in C weren't usesless, Rust want the first to introduce all if these ideas, ...).
In the beginning types were useless and hard.
Then we made typeless languages so we didn't need to bother with useless and hard types.
Then we figured out how to make types easier and useful.
1. C - types represent memory layout, which the programmer doesn't care about, are not useful for error handling and control flow and you have to type them out and remember which one is which.
2. Python - Yolo, nothing matters, everything goes. eZ. Shit, why does this code break after refactoring?
3. Rust - Types are inferred, IDEs and the compiler basically tell you what to do and the types are safeguards, rails and handle logic.
Best thing: most of this stuff goes back to the olde languages as well. I.e. IDEs make types in C easier, type hints in Python help with refactoring and so on.
So I think w won't even need to manipulate people out if untyped languages. The academic research that helps make programming better will reach all popular languages.
(Please don't every example to verbatim - it's just a rough outline of an idea not meant to be an in depth analysis. Of course types in C weren't usesless, Rust want the first to introduce all if these ideas, ...).
I don’t think types were hard originally, but rather the popular typed languages for a very long time were C, C++, and Java and they were loaded with foot guns, or at least the popular advice encouraged you to use those languages in a very difficult to maintain way (e.g., shoehorning inheritance into every problem in C++ and Java) or else they were ergonomic problems (lack of type inference or good tooling). The dynamic languages didn’t share these foot guns, so people wrongly assumed they were type system problems.
That's a very good observation and I agree!
In the beginning, memory layout mattered a lot because computers were limited.
Then hardware got better, computers became more accessible and the barrier for programming got lower.
Now we have numerous domains of software development covered by numerous different programming languages. The choice is good but because we get drilled that computers are a science people will often squabble that their theory is the one true unified theory.
Then hardware got better, computers became more accessible and the barrier for programming got lower.
Now we have numerous domains of software development covered by numerous different programming languages. The choice is good but because we get drilled that computers are a science people will often squabble that their theory is the one true unified theory.
> Funny that until yesterday, I had never even heard the name Idris, and now I find it mentioned in two HN articles within 24 hours.
there's some sort of phenomenon for this, but I can’t recall the name atm.
there's some sort of phenomenon for this, but I can’t recall the name atm.
Baader–Meinhof phenomenon or Frequency illusion
It happens to me when I want to buy a specific car. I see it everywhere.
It happens to me when I want to buy a specific car. I see it everywhere.
It happens to me with the Baader–Meinhof phenomenon every time I hear about the Baader–Meinhof phenomenon
[deleted]
[deleted]
> Types are Science
I think the author should read up on the scientific method.
Mathematics and computer science are not science (despite the name).
I think the author should read up on the scientific method.
Mathematics and computer science are not science (despite the name).
we are losing our minds
Not that interesting. The gist of the blog is this:
"I know some code is wrong, and I want to avoid it in production.
Code that doesn’t typecheck doesn’t run.
Therefore, I write types so that this code does not typecheck."
This reasoning can be seen as instance of "abduction". If you are familiar with Philosophy of Sciences, it is seen as Inference to the Best Explanation. Put simply, if we remove the buzzwords, it is an instance of hypothesis generation.
How can one test a hypothesis that adding types will fix a set of bugs? Just by adding types, of course.
In Philosophy, there is another discussion between types and tokens. This is a variation of the problem of universals. The answer depends on one's ontological commitments, which depends on whether one subscribes to nominalism or to realism, etc.
"I know some code is wrong, and I want to avoid it in production.
Code that doesn’t typecheck doesn’t run.
Therefore, I write types so that this code does not typecheck."
This reasoning can be seen as instance of "abduction". If you are familiar with Philosophy of Sciences, it is seen as Inference to the Best Explanation. Put simply, if we remove the buzzwords, it is an instance of hypothesis generation.
How can one test a hypothesis that adding types will fix a set of bugs? Just by adding types, of course.
In Philosophy, there is another discussion between types and tokens. This is a variation of the problem of universals. The answer depends on one's ontological commitments, which depends on whether one subscribes to nominalism or to realism, etc.
Could you, in theory, do just as well and have a greater understanding that code is completely correct, by implementing a rigorous type system? Probably. Are you going to actually get things done faster or better? Seems unlikely, especially in a world where requirements shift every five minutes and are ill-defined in the first place.
In fact if we're talking about "getting things done", regardless of which of the three activities you're undertaking at the end there, you're engineering.
(To those below - I'm not saying types are all bad or all wrong, in fact my current favoured languages are Java and Go, which both make use of types, I'm also a big fan of using type hints in python. My reaction is against the idea of relying on types for more or less everything, and viewing programming entirely through the mathematical lens of type transformation. I view this paradigm as overly abstract and mathematical and removed from what I'm usually trying to achieve - an action, rather than a calculation)