Static typing is not at all bad; usual static typing mechanisms are, due to the fact that most of them force you into designing your types before you even have a working prototype.
(If you should first understand your problem before you write some code or if you should use code to help you understand the problem and then write more code is up to debate, of course. Typing is an invaluable
tool of thought to help you understand your problem, yes, but it is just one more tool in the toolbox.)
The sad thing I noticed though is that, having hacked a mostly untyped Python code base during the last few days, making sure that all typing annotations you add to the code base are sound is a big PITA, to put it bluntly, and I would pretty much prefer to work with a statically typed language in this particular case. If your typing discipline is uncoupled from the ability to run code, people simply remove that obstacle from their way. It starts to be treated pretty much like tests and documentation: indispensable in theory, relegated to second plan in practice.
So my impression is that gradual typing almost got it right, but it may do a great disservice to overall code quality as well. I am now inclined to think that some kind of barbell strategy on typing will render better results: use both a completely untyped dynamic language such as Tcl, where everything is a string, and a static, strongly typed programming language (ideally a proof assistant with dependent types). You prototype with the former and move into production after translating your solution to the latter. If you ever need to push untyped code into production, it will be obvious to everyone involved and, since it is so decoupled, it cannot affect the quality of the statically typed codebase by any chance.
> Static typing is not at all bad; usual static typing mechanisms are, due to the fact that most of them force you into designing your types before you even have a working prototype.
> Typing is an invaluable tool of thought to help you understand your problem, yes, but it is just one more tool in the toolbox
For me those two sentences contradict each others. Types force you to draw an outline of your solution. For any non trivial problem this will be a time saver even in the prototype phase.
> use both a completely untyped dynamic language such as Tcl, where everything is a string, and a static, strongly typed programming language (ideally a proof assistant with dependent types).
This is gradual typing. The real problem with gradual typing is that you largely forgo the performance advantages of static typing, since you spend a lot of compute time translating data in and out of "dynamically-typed" (i.e. tagged/runtime dispatched) representations. This is especially obvious in stringly-typed languages ala Tcl, but applies elsewhere as well.
Static typing isn't bad, but it's only as good as the type system is strong and detailed. Haskell's QuickCheck doesn't understand biases or infinite-typed values. The Hypothesis strategy of Strategies (the design pattern) is far more useful for producing serious test suites, as less time has to be spent fretting about which invariants can be hoisted to the type system.
So I use QuickCheck often and I'm a true believer, but the point this post is making is absolutely justified. Tying the test generation to the type is often requires some creative ways of writing `Arbitrary` instances (the specification of how test cases should be generated).
However, I don't think what the author is suggesting in its place better. The advantage of tying the test case generation to the type is that it's compositional. Lots of sub Arbitrary instances come together to generate the test case and in the long term I find this to be more maintainable. Whereas the author's approach discourages compositionally.
The real problem is that the types in vanilla Haskell are too loose, so there lots of inhabitants of a type that we are not interested in. The author mentions in passing, dependent-types might be a solution and that is exactly right. What is needed is to make the irrelevant terms illegal altogether. This is pretty achievable and is already somewhat used. For example, the program synthesis (proof search) mechanism of Idris 2[0] uses linear[1] dependent types[2] to heavily constrain which terms are possible candidates for a given type. The specificity of the type reduces the search space, hence increases the effectiveness of the proof search.
I find it rather disrespectful to summarise a 20 years old, very successful and at the time truly revolutionary tech like QuickCheck with a simple “this is a bad idea”. If you stand on the shoulder of giants at least pay some respect.
The title of this HN post is completely out of context, and the discussion here is unrelated to the article. The author is not at all arguing against types or Haskell, nor is he bashing QuickCheck (he’s developed a QuickCheck-like framework for Python). He’s merely complaining about some details of QuickCheck’s design.
I agree with your observation, except for the part where he not bashing on QuickCheck (he is, but you have to click the first link in the article in order to find it).
> One of the big differences between Hypothesis and Haskell QuickCheck is how shrinking is handled.
> Specifically, the way shrinking is handled in Haskell QuickCheck is bad and the way it works in Hypothesis (and also in test.check and EQC) is good. If you’re implementing a property based testing system, you should use the good way. If you’re using a property based testing system and it doesn’t use the good way, you need to know about this failure mode.
> The big difference is whether shrinking is integrated into generation.
> Integrating shrinking into generation has two large benefits...
> The first is mostly important from a convenience point of view...
> But the second is <i>really</i> important, because the lack of it makes your test failures potentially extremely confusing.
> In Haskell, traditionally we would fix this with a newtype declaration which wraps the type. We could find a newtype NonEmptyList and a newtype FiniteFloat and then say that we actually wanted a NonEmptyList[FiniteFloat] there.
> In Haskell, traditionally we would fix this with a newtype declaration which wraps the type. We could find a newtype NonEmptyList and a newtype FiniteFloat and then say that we actually wanted a NonEmptyList[FiniteFloat] there. […] But why should we bother? Especially if we’re only using these in one test, we’re not actually interested in these types at all, and it just adds a whole bunch of syntactic noise when you could just pass the data generators directly.
Did you know it's one function call to change your NonEmptyList FiniteFloat into [Float]? It's called coerce. There's very little extra syntactic baggage.
And you know what, carrying data generators around is a bad idea. It forces you to think about how you want the random data to be generated, and not what the random data should look like.
In order to understand "shrinking", an unfamiliar term to me, I read the linked blog post on test case reduction: https://blog.regehr.org/archives/1284
The primary assumption of whatever's in the first page is that types are sets of values right? Integrated shrinking assumes the rules that form the set while type based shrinking assumes subsetting. Am I right in reading this?
If so.. why are we still using the notion that types = sets of values?
Static typing (in any language) is just like training wheels on a bike. It's great to learn with them but eventually, as your skill increases, the training wheels become a problem and then they must come off.
Most things in the real world don't have a fixed set of attributes, attributes can change over time and as software developers we need to
model that. There is a reason why the largest package managers (with the most packages published) are for dynamically typed languages. It's simply more flexible; these packages can work with anything; no need to import type definitions that don't fit within your type system. They are unopinionated, they return only simple objects and therefore they are highly composable.
Early in my career, dynamically typed languages allowed me to push hard and fast and learn a lot in a short space of time via rapid prototyping.
If you don't care about error handling then you can wrangle hard with a dynamic language and it won't catch up with you for a long time. But eventually...
Now? I generally write even Python scripts over a few tens of lines with mypy running, because otherwise it becomes necessary to adopt some form of Hungarian notation anyway, and then you're just doing typing badly.
For the most part static typing prevents you from doing things you know you shouldn't anyway. Like tacking arbitrary attributes onto objects that get passed around.
APIs change indeed; and you want to know whether a type has changed, not simply be surprised.
> Static typing (in any language) is just like training wheels on a bike.
Well, no. It is more like a ABS once you switched from a bike to a car that can go way more than 100kph. In theory, you can take all corners without, but it will be dangerous, you have to do more, and you cannot go quite as fast. And while everyone thinks they understand how it works, its inner mechanism is only understood by specialists.
> Static typing (in any language) is just like training wheels on a bike. It's great to learn with them but eventually, as your skill increases, the training wheels become a problem and then they must come off.
LOL, what?
If anything, it's the opposite.
Dynamic typing is the lesser easy-to-start with machine (say, a toy bike), and as the needs grow (for both safety, performance, and guarantees for working with larger codebases/teams) you add types...
>Most things in the real world don't have a fixed set of attributes, attributes can change over time and as software developers we need to model that.
Which is irrelevant. Our programs (functions, custom types, etc) have a fixed set of attributes at any given time -- as the code must know about them to use them in the first place.
For things that we model and don't have fixed attributes, we can and do build ADTs and data structures to accommodate them.
This is nonsense. Static types can represent things with a non-fixed set of attributes just fine.
Also, note that the article isn't implying what you are: "Where stronger types are naturally present in the program, taking advantage of them to get better testing is certainly worth doing..."
[+] [-] tmcb|6 years ago|reply
(If you should first understand your problem before you write some code or if you should use code to help you understand the problem and then write more code is up to debate, of course. Typing is an invaluable tool of thought to help you understand your problem, yes, but it is just one more tool in the toolbox.)
The sad thing I noticed though is that, having hacked a mostly untyped Python code base during the last few days, making sure that all typing annotations you add to the code base are sound is a big PITA, to put it bluntly, and I would pretty much prefer to work with a statically typed language in this particular case. If your typing discipline is uncoupled from the ability to run code, people simply remove that obstacle from their way. It starts to be treated pretty much like tests and documentation: indispensable in theory, relegated to second plan in practice.
So my impression is that gradual typing almost got it right, but it may do a great disservice to overall code quality as well. I am now inclined to think that some kind of barbell strategy on typing will render better results: use both a completely untyped dynamic language such as Tcl, where everything is a string, and a static, strongly typed programming language (ideally a proof assistant with dependent types). You prototype with the former and move into production after translating your solution to the latter. If you ever need to push untyped code into production, it will be obvious to everyone involved and, since it is so decoupled, it cannot affect the quality of the statically typed codebase by any chance.
[+] [-] sbergot|6 years ago|reply
> Typing is an invaluable tool of thought to help you understand your problem, yes, but it is just one more tool in the toolbox
For me those two sentences contradict each others. Types force you to draw an outline of your solution. For any non trivial problem this will be a time saver even in the prototype phase.
[+] [-] zozbot234|6 years ago|reply
This is gradual typing. The real problem with gradual typing is that you largely forgo the performance advantages of static typing, since you spend a lot of compute time translating data in and out of "dynamically-typed" (i.e. tagged/runtime dispatched) representations. This is especially obvious in stringly-typed languages ala Tcl, but applies elsewhere as well.
[+] [-] lidHanteyk|6 years ago|reply
[+] [-] j88439h84|6 years ago|reply
[+] [-] mathetic|6 years ago|reply
However, I don't think what the author is suggesting in its place better. The advantage of tying the test case generation to the type is that it's compositional. Lots of sub Arbitrary instances come together to generate the test case and in the long term I find this to be more maintainable. Whereas the author's approach discourages compositionally.
The real problem is that the types in vanilla Haskell are too loose, so there lots of inhabitants of a type that we are not interested in. The author mentions in passing, dependent-types might be a solution and that is exactly right. What is needed is to make the irrelevant terms illegal altogether. This is pretty achievable and is already somewhat used. For example, the program synthesis (proof search) mechanism of Idris 2[0] uses linear[1] dependent types[2] to heavily constrain which terms are possible candidates for a given type. The specificity of the type reduces the search space, hence increases the effectiveness of the proof search.
[0] https://github.com/edwinb/Idris2
[1] https://en.wikipedia.org/wiki/Substructural_type_system#Line...
[2] https://en.wikipedia.org/wiki/Dependent_type
[+] [-] patrickmn|6 years ago|reply
https://ucsd-progsys.github.io/liquidhaskell-blog/
https://ucsd-progsys.github.io/liquidhaskell-tutorial/01-int...
The Python hypothesis package strikes me more like a dynamic version of Haskell/LiquidHaskell than Haskell/hedgehog.
[+] [-] pwm|6 years ago|reply
[+] [-] vfaronov|6 years ago|reply
[+] [-] thsealienbstrds|6 years ago|reply
> One of the big differences between Hypothesis and Haskell QuickCheck is how shrinking is handled.
> Specifically, the way shrinking is handled in Haskell QuickCheck is bad and the way it works in Hypothesis (and also in test.check and EQC) is good. If you’re implementing a property based testing system, you should use the good way. If you’re using a property based testing system and it doesn’t use the good way, you need to know about this failure mode.
> The big difference is whether shrinking is integrated into generation.
> Integrating shrinking into generation has two large benefits...
> The first is mostly important from a convenience point of view...
> But the second is <i>really</i> important, because the lack of it makes your test failures potentially extremely confusing.
[+] [-] mrkeen|6 years ago|reply
We sure would! What's the issue?
[+] [-] kccqzy|6 years ago|reply
Did you know it's one function call to change your NonEmptyList FiniteFloat into [Float]? It's called coerce. There's very little extra syntactic baggage.
And you know what, carrying data generators around is a bad idea. It forces you to think about how you want the random data to be generated, and not what the random data should look like.
[+] [-] pjc50|6 years ago|reply
[+] [-] chewxy|6 years ago|reply
If so.. why are we still using the notion that types = sets of values?
[+] [-] cryptica|6 years ago|reply
Most things in the real world don't have a fixed set of attributes, attributes can change over time and as software developers we need to model that. There is a reason why the largest package managers (with the most packages published) are for dynamically typed languages. It's simply more flexible; these packages can work with anything; no need to import type definitions that don't fit within your type system. They are unopinionated, they return only simple objects and therefore they are highly composable.
[+] [-] esotericn|6 years ago|reply
Early in my career, dynamically typed languages allowed me to push hard and fast and learn a lot in a short space of time via rapid prototyping.
If you don't care about error handling then you can wrangle hard with a dynamic language and it won't catch up with you for a long time. But eventually...
Now? I generally write even Python scripts over a few tens of lines with mypy running, because otherwise it becomes necessary to adopt some form of Hungarian notation anyway, and then you're just doing typing badly.
For the most part static typing prevents you from doing things you know you shouldn't anyway. Like tacking arbitrary attributes onto objects that get passed around.
APIs change indeed; and you want to know whether a type has changed, not simply be surprised.
[+] [-] choeger|6 years ago|reply
Well, no. It is more like a ABS once you switched from a bike to a car that can go way more than 100kph. In theory, you can take all corners without, but it will be dangerous, you have to do more, and you cannot go quite as fast. And while everyone thinks they understand how it works, its inner mechanism is only understood by specialists.
[+] [-] coldtea|6 years ago|reply
LOL, what?
If anything, it's the opposite.
Dynamic typing is the lesser easy-to-start with machine (say, a toy bike), and as the needs grow (for both safety, performance, and guarantees for working with larger codebases/teams) you add types...
>Most things in the real world don't have a fixed set of attributes, attributes can change over time and as software developers we need to model that.
Which is irrelevant. Our programs (functions, custom types, etc) have a fixed set of attributes at any given time -- as the code must know about them to use them in the first place.
For things that we model and don't have fixed attributes, we can and do build ADTs and data structures to accommodate them.
[+] [-] sicromoft|6 years ago|reply
Also, note that the article isn't implying what you are: "Where stronger types are naturally present in the program, taking advantage of them to get better testing is certainly worth doing..."
[+] [-] continuational|6 years ago|reply