I think the argumentation here is a bit a skewed towards 'what static types can and cannot do for the compiler' - i.e. how they can help the computer in constructing formal proofs. For me another almost as valuable thing is how static types help me think about and design the code. The static type information is always there to remind "this entity belongs to this set of objects" which frees me from the cognitive burden of maintaining this constantly in my working memory. With specific static types the function signatures now document the tranforms defined for those entities . This aspect of static types as a cognitive tool is highly personal, and not same for everyone, unlike the language and the compiler, though.
> It's also nothing to do with static checking—“type safety” holds in all “dynamically typed” languages.
This. Exactly true, and often forgotten.
It's useful here to distinguish between conversions and casts. Conversions use type information to ensure computations remain sensical; the canonical example is a conversion between integers and floating-point values which makes sure you never end up feeding invalid bit patterns into the relevant arithmetic hardware. An example of a cast is taking a bit pattern you had been treating as an integral value and then telling the language it's a floating-point value, and there not being an error at that point.
Conversions don't break the type system; they use the type system. Casts throw types away.
Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload.
> Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload.
This is true. A more interesting example might be a program which creates database queries from user input casting input strings to the type "unescaped string", and then converting them to type "escaped string" by performing a string-escaping process on them. (A cast from "unescaped string" to "escaped string", which is done implicitly very often in languages where those types are not machine-checkable, is often disastrous.)
Right, but I don't think this sort of type "conversion" (e.g. some function with type signature like this in Haskell)
escapeQueryString :: ByteString -> Query
is really adding or throwing away type information, it's just a function that accepts one type and returns another type. So it's not related to casting, except that it's the opposite of casting. But what that gives you is the ability to compose it with any other function that you define as accepting a `Query` type, and the program will refuse to compile if you ever accidentally try to pass it a ByteString. So it's about enforcing an invariant, in other words.
While I mostly agree, by this definition most things called "casts" aren't anything of the sort. In C++, static_cast (when called on value types) and dynamic_cast are both conversions, not casts--- static_cast<int>(5.5) returns exactly what you'd expect. Java and C# use C-style syntax, but their semantics are the same as those C++ casts. And of course the same is true of non-C-derived languages like Swift.
By your definition, most "casts" are actually conversions--- and while that's probably true, it feels pretty unhelpful, in the same way that it feels unhelpful to say "Python only has one type".
I agree that the terminology I used in my post isn't mainstream, and I won't claim it is. However, I couldn't think of a different word which would have the same familiarity with this audience which could plausibly carry that meaning. If anyone else can come up with better words, I'll use them.
To be clear, here's what I mean:
Conversion: The machine looks at the current type to figure out how to transform the value into a valid instance of the new type.
Casting: The machine ignores the current type and simply applies the new type.
Type safety also trivially holds in any dynamically typed language. You just call all values the same type---suddenly "preservation" and "progress" hold without actually meaning anything.
That's why its "type safety of a system which captures interesting invariants" which is actually interesting.
> Type safety also trivially holds in any dynamically typed language. You just call all values the same type
This isn't what most dynamically typed languages do and I suspect you know it. The reason "1" + 1 works in Perl (that is, produces a defined value rather than an undefined one or a program crash) is because the Perl runtime uses type information to deduce which conversion needs to be performed and then performs it.
The fact the type information is deduced as opposed to declared explicitly doesn't make it anything other than type information.
"The fact the type information is deduced as opposed to declared explicitly doesn't make it anything other than type information."
As I understand it, the fact that it is determined dynamically rather than declared or deduced statically makes it other than type information. Specifically, it makes it tags.
I think that's a valid point. A good example of this is Tcl, where "everything is a string". There are various ways you can treat a given string (as an integer, as a list, etc), but that doesn't make the value those types, it just means it can be used as one.
string is integer 1 ;# true
string is list 1 ;# true (list of length 1)
As the post I linked labors over, "type" and "type safety" have particular, well-defined technical definitions. There are other meanings, in particular the one you suggest "type as Perl means it" is one, but they don't have a consistent formal definition and don't have a consistent notion of "type safety" so it's difficult to use them except in the regime of a single language.
Now, if we take "type" to mean this formal meaning I suggest then dynamic languages have exactly one type. This is a meaningful, if degenerate, analysis. Within this analysis, Perl has one type and trivially satisfies type safety because type safety essentially means "things don't randomly change types" plus "programs continue to evaluate until they reach pre-defined evaluation stopping points". Both of these hold trivially in a language with one type.
The system you refer to, given again that we're sticking with the "formal type" terminology, is called a "tag system". It exists "below" or "after" the static system which ensures type safety and can indeed induce interesting behavior. But, in particular, it is not an analysis which can be considered complete (in any turing compete language) because it depends upon running the program which can lead to non-termination.
So really the distinction is not "deduction" versus "declaration" but instead "static" versus "dynamic". In general, static types are less powerful but more complete and dynamic tags are more powerful but highly incomplete. To confuse the two is to create a tremendous headache all around.
> There are other meanings, in particular the one you suggest "type as Perl means it" is one, but they don't have a consistent formal definition and don't have a consistent notion of "type safety"
Yes, they do: Type safety means "everything happens due to controlled conversion, as opposed to arbitrary behavior when conversions are not performed". For example, feeding an integer bit-pattern into an FPU is going to cause arbitrary behavior: It might work, it might cause a fault, it might crash the system.
> Now, if we take "type" to mean this formal meaning I suggest then dynamic languages have exactly one type.
Then the formal meaning is too weak (that is, not useful enough) to talk about dynamic languages. This has nothing to do with how type-safe dynamic languages actually are.
> "things don't randomly change types"
True in Perl and Python.
> "programs continue to evaluate until they reach pre-defined evaluation stopping points"
This is either true in Perl or meaningless in any language.
> The system you refer to, given again that we're sticking with the "formal type" terminology, is called a "tag system".
Right. The formal type terminology is so weak it has to make up terms to put dynamic languages off to one side, because it can't handle them. That's not really a property of the languages.
> It exists "below" or "after" the static system which ensures type safety and can indeed induce interesting behavior.
That's because it is a type system just the same.
> But, in particular, it is not an analysis which can be considered complete (in any turing compete language) because it depends upon running the program which can lead to non-termination.
Some static type system evaluators aren't guaranteed to terminate:
Of course C's type system evaluator is, but C isn't strongly typed. It's weakly typed, because it has a way to convince the compiler to ignore type information and, for example, verify a program which will feed an integer bit-pattern to the FPU.
Look, we're fighting about terminology not meaning. I have carefully defined my terms and made statements which live entirely within that world. I have also described terms of a larger world, noted that these two formal systems are distinct and also how they fit together.
If you want to talk about that which I called "tags" I'm fine with that. I'm even fine with calling them "types" if you insist---so long as it's also made clear that these "types" have nothing at all to with "static types" as they are different beasts that are essentially non-comparable. That is all fine.
I take argument to trying to smooth out the distinction, though. That is essentially wrong and unworkable.
Static type safety is far from meaningless or weak, but it is absolutely different from your definition of "type safety" as used here. I argue that static types have a precise and meaningful formal definition which extends far beyond what your attempt to define "dynamic type safety" encompasses. What you offer isn't meaningless or invalid---it's just vague and changes depending upon the language you're considering.
This topic of "what are static types good for" continued to bug me because I could not formulate a concrete answer to myself. I found the following Reddit discussion
Which had eventually the specific thing I was after in a comment by Rich Hickey which helped to nail the concept I was after
"Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the
scope of any type system."
Which is precisely why I enjoy types: Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism.
Which, I think tells exactly what static types are good for: For those sort of problems that benefit from having a formal specification. There are a lot of programs that have this quality.
So the argumentation is a bit skewed off. It should not be about whether static or dynamic types are better but more focus on what are those identifiable problem patterns where a dynamic type system helps programmer create more value than a static one and vice versa.
> Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism.
I think this is a valid point.
But I am less convinced about the second part. I feel that better type systems do help one model the world better (while retaining the consistency checking that you mentioned). In my mind at least having more/better "type tools" is like having differently shaped pieces in your lego tool box. You can create better models for yourself, because the pieces allow you to. And the more experience you have with them, your modeling abilities also improve.
The thing about "the outside world" is that it is just one form of interpretation of a chunk of code. Inarguably, it is the most important one, but once you recognize that it is not alone in that regard you get a very new appreciation for "internal consistency".
Ultimately, this becomes an issue of "minimize your interfaces" which is widely known to be close to vital for writing successful code. If you can "purify" most of your code base then use types to ensure that it has internal consistency then the remaining task is to write (at least) one valid, trusty "interpreter" from your pure/trusted codebase into the real world.
This is undoubtedly the most fragile piece of your application!
But it's also eminently library-able and it places the risk-burden over a tiny fraction of your code. It's also the place where you want to property/unit/integration test the hell out of the world.
So all of the standard CS adages apply again, but thanks to purity/type-checking you've reduced the risk exposure to a tiny fraction of what it is while using other tools.
I emphatically reject the many of the conclusions of this article.
>Let me say it simply. Type systems cannot be a one-stop solution for specification and verification.
Wrong! Any correctness property can be encoded into a sufficiently powerful type system. Which brings me to...
>Curry-Howard is an interesting mathematical equivalence, but it does not advance any argument about how to write software effectively.
This is absurd, of course. The isomorphism between type systems and proof systems allows us to build lots of impressive systems like Agda and Coq.
>No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments.
That's actually quite a reasonable desire.
>Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code.
To the author, this seems to mean "therefore, we shouldn't have types!". In reality, a sufficiently flexible programming language allows you to write type-level code in the same language as value-level code. See Agda.
>Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic.
> >Let me say it simply. Type systems cannot be a one-stop solution for specification and verification.
> Wrong! Any correctness property can be encoded into a sufficiently powerful type system.
I'm writing a factorial function. But, because the caffeine hasn't kicked in yet, at the recursion step, I add one instead of subtracting one. The result is that the program will run in an infinite loop until either the fixed-size Int rolls over to 0, or the bignum-style integer consumes all available memory. That's certainly incorrect behavior. But I'd like to see your "sufficiently powerful type system" that will handle that.
Then there's numerical accuracy. Here the results are not "wrong wrong", they're just "a little bit wrong" or "less accurate than they could have been". Again, I'd like to see your type system detect that.
In my world, embedded systems, you can get hard-real-time situations, which means that the right answer, too late, is wrong. I believe that there are formal verification tools, but they don't look anything like a type system. And even those tools depend on a very deep knowledge of the processor that the code will be running on (not compiled on). Once more, I'd like to see your type system that's going to handle this.
> > Curry-Howard is an interesting mathematical equivalence, but it does not advance any argument about how to write software effectively.
> This is absurd, of course. The isomorphism between type systems and proof systems allows us to build lots of impressive systems like Agda and Coq.
And if Agda and Coq were being used to write much software, you'd have a point. But if I understand correctly, they're mostly used for automated proofs. The point is that the program compiles, and therefore something is proven. The point isn't to get a runnable program.
> The result is that the program will run in an infinite loop until either the fixed-size Int rolls over to 0, or the bignum-style integer consumes all available memory. That's certainly incorrect behavior. But I'd like to see your "sufficiently powerful type system" that will handle that.
> To the author, this seems to mean "therefore, we shouldn't have types!".
This doesn't follow from the author's earlier statements about using and benefitting from languages with static type checkers. An ideal typed Lisp dialect would fit the author's requirements.
An ideally typed Lisp would be no different then a dependently typed language semantically.
Yes, you would use slightly different syntax but a key feature of most dependently typed languages is that they only have a single class of pseudo-terms that are used for both types and programs.
An example Idris program:
double : Nat -> Nat
double n = 2 * n
ourVectorType : Type
ourVectorType = Vect (double 1) Int
aVector : ourVectorType
aVector = [1, 2]
If you change everything above to an S-Exp you have a typed Lisp where both types and terms have the same language.
I have always gotten the impression there was a failure of communication when (without lose of generality) Haskell programmers would tell (also, without loss of generality) Python programmers that Python only has one type, 'object', which appears to violate the understanding of the Python programmer thoroughly enough that there isn't really even a conversation about what is meant by the comment.
The first point dissolves this conversation (because clearly neither the Haskell nor Python programmers are confused about the execution of actual programs). Notably, it dissolves it in a way where that pesky third issue doesn't pop up (which is perhaps the worst of them all, sans _maybe_ the last).
Well, that's an interesting comment. I have almost a decade experience in Python, and having recently picked up Haskell, I clearly see the value of having (or not) a static type system.
I have noticed that during all these years I would just "type-check" the various APIs in my mind, or with the aid of the REPL, but it's not as easy when programmers with less experience join the project. I would often have to explain tracebacks about type errors (e.g., tried to call a missing method on `None`, but the programmer didn't expect that API to return `None`). Strong typing avoids errors from propagating, but without static checking only gets you half-way there.
I would still use Python (or other dynamic language) to introduce someone to programming - not having to reason about types lowers some barriers - but nowadays I'm not sure it pays off for a project expected to be maintained.
I was always on the fence about static typing because I figured that it automatically led to more verbose code (clearly a significant down side), but after looking at Haskell and F# I'm not so sure that's true for them, even though it definitely is for C++ and Java.
I'm still unconvinced that additional testing is required to overcome bugs that a static type checker would catch, though. In my experience all of those "call a missing method on None" issues get caught relatively quickly by a test that you would have to write anyway even if you were using a language with static typing.
> In my experience all of those "call a missing method on None" issues get caught relatively quickly by a test that you would have to write anyway even if you were using a language with static typing.
There are lots of bugs that you still have to test for in a language with a typesystem like Haskell's. But it's not this class of bugs. Pattern matching (and completeness checks) should take care of that.
I know, but my point was that in my experience this class of bug is nearly always a problem at its heart in requirements anyway (i.e. an unspecified edge case), meaning you have to test it in whichever language you use to be confident of the program's correctness.
E.g. you'll still need to write a test for your haskell code to determine that the behavior is correct if the IP address is missing, and in your python code if you don't specify behavior it is the kind of thing that will likely lead to one of those nasty "cannot call a method on none" errors.
Since the act of testing which is necessary anyway catches it or confirms correct behavior, the additional benefit of a static type checker confirming the presence of such a bug is perhaps lower than it might appear at first glance.
This is clearly not true of weakly typed languages where you have to write a myriad number of extra tests just to achieve the same confidence in your code to cover all the unexpected use cases caused by weird type conversions you didn't even realize you were doing.
I believe eru's point was that those kinds of tests are not necessary in Haskell because if a function takes something of the type IpAddress, None simply isn't possible. So everywhere IpAddress is used, you don't have to do any of those tests.
It sounds like your point is that even in Haskell there will inevitably be boundaries where the None case is an issue. And that's true, namely the point where you call:
parseIpAddress :: String -> Maybe IpAddress
Somewhere your app will be sucking in a string and you need to have a test for the empty string case. That's true. But the surface area of the application that is susceptible to this problem is reduced (often dramatically). All code that works with IpAddress is free and clear. Whereas in most other languages, every function that takes an IpAddress probably needs to be tested with the None case. If you try to argue that you don't need to test every one, then you're plagued by the difficulty of knowing which need it and which don't. Haskell's types solve that for you completely.
Any typesystem that offers algebraic data types solve issues of this kind. As crdoconnor rightly puts it, handling these cases is ultimately a burden your spec has to bear. Haskell nudges you to handle them upfront.
What I hate most, is people using unusual but cromulent values as sentinels. Eg a function that takes a timeout will often interpret 0 as infinity. That's just wrong, and a symptom of working around an inadequate type system.
I get the point, but I still feel like the problem surface is not really reduced that much by static typing it away, and the bulk of the problem is simply moved elsewhere rather than solved outright since the root of these issues is incorrect specification anyhow.
As in, I take issue with the word "dramatic", not the word reduce.
Additionally - it might just be my python bias talking - but I tend to find that most useful "real-life" libraries need to have an opinion about what happens when a variable is None, because it is almost always meaningful. I guess if I were writing haskell my code would end up looking like a bad carly rae jephsen song :)
The key with Maybe/Option types is pattern matching ensures you don't forget to handle the case where it is none (it can be meaningful!). If you have a value of `Maybe a` you are required to pattern match on it.
case myMaybe of
Nothing -> foundNothing
Just v -> ...
In Python and Ruby any value can be None or nil at anytime.
In stark contrast languages like Rust and Haskell (that have no concept of None/nil/null) this is very useful as you know you always have a value in your variable and not a null.
This means when you do introduce an Option/Maybe type you are saying the null case should be treated with special semantics, exactly what you usually want in a dynamic language.
> I get the point, but I still feel like the problem surface is not really reduced that much by static typing it away
Ok, that's a valid point, which means that we need to precisely characterize what is meant by "problem surface". Let's continue with our IpAddress example. Imagine you are the author of the IpAddress package. Imagine we have an IpAddress type accompanied by an API of say 15 functions that take an IpAddress and do something with it. How many of those functions need to have tests that cover the case of passing None? I believe that number represents our problem surface.
If you agree that this is the problem surface, then I can confidently say the reduction is dramatic. (If you don' agree, then I refer you to the previous point about Maybe making it very clear what needs None tests.) The Python IpAddress package has to have None tests on every single function that takes an IpAddress. The Haskell package has to have None tests on zero. It only needs the equivalent of a None test on the functions that return a Maybe IpAddress. This is going to be a very small number. This brings us to your other point.
> Additionally - it might just be my python bias talking - but I tend to find that most useful "real-life" libraries need to have an opinion about what happens when a variable is None, because it is almost always meaningful. I guess if I were writing haskell my code would end up looking like a bad carly rae jephsen song :)
I'm pretty sure this is indeed largely caused by your Python bias. In my experience, Haskell code does not end up littered with Maybes. I think you don't appreciate the full weight of the statement that when you have an IpAddress, you never need to worry about the None case. Never ever. Period. There are cases where you need to deal with a Maybe IpAddress. Those cases don't end up polluting all your code, contrary to what you seem to think. In fact, it's the other way around. The pure cases tend to be the ones that are the most common, making the Maybe cases clearly visible.
Even in the situation where they do start to pollute some things, Haskell gives you dramatically better tools for dealing with the problem. Yes, you'll still have to have a test for it, but the code you're testing will have been much more concise and less prone to error. Furthermore, Haskell can make it so you don't even have to think about testing that case. You write an Arbitrary instance for IpAddress and the Arbitrary instance for "Maybe IpAddress" comes for free! This means that your QuickCheck test for the Maybe IpAddress function will automatically be sure to try it with Nothing.
From what you've said it is clear to me that your python bias is somehow making it hard for you to see/believe the benefits that we're talking about. I'm concerned that this gap seems to be so big and we seem to be having such a hard time crossing it. Give Haskell a try and see for yourself. But don't go off into a cave and play with it alone. There are abstractions and best practices for dealing with some of these things that took awhile to emerge. So you should be sure to talk to people who have experience using them while you're learning.
> I'm pretty sure this is indeed largely caused by your Python bias. In my experience, Haskell code does not end up littered with Maybes.
I think the Maybes and other optional/sum types tend to be limited to the boundaries, where you do IO or handle errors, while your internal functions can deal with the concrete type. A code base littered with Maybes is certainly a code smell.
> A code base littered with Maybes is certainly a code smell.
It's not because Maybe (and usually more practical Either) have functor instances. What this means is you can use fmap to apply pure functions to Maybes, Eithers, or any other type that has a Functor instance.
The 'uni-typed' argument is interesting, but seems to fall down under further examination. This is a comment from some guys at the University of Indiana, who are neither Python or Haskellers, but are working on advanced type systems:
... however Sam Tobin-Hochstadt argues the uni-typed classification is not very informative in practice.
The uni-typed theory reveals little about the nature of programming in a dynamically typed language; it's mainly useful for justifying the existence of "dynamic" types in type theory.
Projects like Typed Racket were invented precisely to discover and model the implicit type information utilised by programmers in such languages. Often types are quite accurate, and shows there's a lot more going on than meets the eye.
You bring up a very interesting point here. The "unityped" argument is a trivializing one, invented to try to draw bright lines between the worlds of static and dynamic typing.
But it's ultimately a minimal argument instead of an interesting one.
A dynamically typed fragment of code can be interpreted as a program in a statically typed world. From here we can attempt to use inference to partially recover real static information and use it during compilation. This is as old as dynamic languages---typed specialization! It's also a genuinely sophisticated static type system imposed on a genuinely dynamic language.
That's an interesting POV from the compiler's perspective, and it should not be ignored.
The other interesting perspective, though, and the one of more modern excitement, is that it's less about whether or not a program technically has a particular type but whether or not failure to be expressible at "good" types should be brought to the programmers attention immediately!
You can see a statically typed language as a gradually typed language which refuses to compile whenever `any` gets inferred, for instance.
To be fair, the type community makes a distinction between types (static entities) and tags (dynamic entities). From their perspective, Python is definitely "tagged" in the sense that tags are checked dynamically, and memory safety is preserved.
On the types mailing list, I think Bob Harper conceded the point that maybe it is more useful to use "type" to refer to dynamic tags when talking to practicing programmers; it is just that in the types community, type has a well defined specific meaning (I can't find a link right now since I'm behind the GFW, but can dig it up later if you are interested).
An alternate viewpoint is that static typing advocates invented a novel categorization that allows them to dismiss typing systems they disagree with. "Tag" doesn't have a consistent theory meaning "type determined at runtime"; on the other hand, "type determined at runtime" has been referred to simply as a "type" for decades.
In the academic literature of type theory, "type" has a very particular meaning and is a construct for reasoning about programs before execution. The community may use "tag" but mostly as a means of distinguishing between "types" in type theory, and a runtime tag. Often the term "dynamic type", or "runtime type" will be used as well all as means of differentiation.
The first type theories by Russell and Church were invented decades before practical computers allowed for programming languages high-level enough to even speak of their being typed or untyped. Type theory is primarily a constructive/computational foundation for mathematics, and secondarily a way of statically proving that programs will not exhibit undefined behavior.
(I find it tremendously amusing when people think that computer languages invented types instead of participated in a late-set convergent evolution with type theory.)
Type is such a generic word though. You can use the word just by its basic definition (a category of people or things having common characteristics) and everyone would mostly understand what you are talking about.
What Russell invented was a theory with types of a more formal definition.
So is "force" and its basic definition has been well-understood for far longer than its precise definition. But for anyone practicing anywhere near physics you ought to learn and recognize the formalization. People reinvent it all the time, to varying degrees of validity, but it's fairly clear how to draw all of this back to Newton and then connect it to the mainline formal development which has occurred since then.
"Patronising those outside the faith ... Please drop the condescending tone."
This is a great sentiment, but rather jarring to have it followed up by "No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments".
"Equivocating around “type-safety”"
Surely it's reasonable to use the terminology "type safety" to describe a range of properties that code may have beyond the (supposed) original meaning of "memory safety".
"If everyone would just use a modern language with a fancy type system, all our correctness problems would be over, right? ... Type systems cannot be a one-stop solution for specification and verification."
This is an enormous straw man. No fan of strongly typed languages claims that they solve all correctness problems. Furthermore, the fans of strongly typed programming are the most likely to appreciate the additional forms of verification that Stephen outlines.
> This is an enormous straw man. No fan of strongly typed languages claims that they solve all correctness problems.
I have read the claim "If it compiles, it works" (or minor wording variations), on this board, more than once (in reference to Haskell). Fans of strongly typed languages do in fact make claims that sure sound like they are saying that.
It's said semi-tongue-in-cheek. The original statement was filled with caveats. [0]
Sometimes it's said less tongue-in-cheek. Then it usually has to do with the facts that large refactorings can be handled by merely breaking things and rewiring until types check. This generally does work since types typically guard "wirings".
But taken out of contexts and as the meaning is extended bit by bit it becomes truly ridiculous and nobody would disagree.
So, don't just propagate the rumor. Nobody is claiming miracles. It just sounds like that at around the 8th iteration of the telephone game.
The origin is definitely further back. I recall hearing "it takes longer to get it compiling, but when it compiles it works" about OCaml more than a decade ago. When I mentioned this to my father at that point, he remarked that the sentiment goes back further.
I wouldn't be terribly surprised if he'd been thinking of Ada evangelists, though I think there are other candidates too. Unfortunately, I can't ask him to clarify...
You know, that's certainly correct. I feel like roconnor's post comes to mind for me because of it's audacity more than its primality. I'll make a note in my original comment if I can.
Huh, you know, that sounds just like how dimensional analysis affects people sometimes. I've certainly seen some take a pile of engineering inputs and whack them together until the units work (myself included); it's a shockingly powerful heuristic for linear systems, since you'll typically only be off by some logical scaling factor. Of course, there's a bajillion ways it can deceive, so it's wise to be thorough.
It has to do with how abstract and parametric the code was. There may very well be only one valid type-checking program which exists (so long as you do a cursory check against infinite loops and error throwing).
So, it's a gamble---do there exist any other non-trivial programs at this type?
If not, then I know my code written is correct without testing.
If there are, then I'm risking that I found the right one.
This is why Haskellers get so excited about "parametricity". It's the core tool that exacts this property of "there are only a small number of programs which could ever exist at this type" which drives correctness.
The claim "If it compiles, it works" taken literally is so trivially falsifiable that it cannot reasonably be interpreted as a serious claim that types "solve all correctness problems".
EDIT: I propose that next time you read "If it compiles, it works" you reply with "Are you suggesting that types solve all correctness problems?" I guarantee you that you will not get an affirmative response.
EDIT: I do however take the point that fans of strongly typed programming should act to moderate the excitement of some amongst their numbers in order to reduce the incidence of ambigous or misleading claims.
I've always taken it as meaning, "If it compiles, it must works, otherwise you're in trouble;" given that debuggers for Haskell are still relatively immature (especially for its age), your best bet is to lean heavily on the type system.
You can still run tests. Debuggers are great for figuring out why your program is wrong and how to fix it. But they seldom alert you to problems in the first place. Tests do.
OCaml and F# are also more conventional. Lazy evaluation is a pain during debugging; even using laziness in a language like C# can be troublesome when you hit the debugger. So if you are going to rely on a lot of it, might as well have a lot of static typing to avoid debugging it.
I can confirm that "If it compiles, it works" is tongue in cheek.
However, it's also true that I feel confident that a program in OCaml will be working correctly either the first time, or shortly afterwards, once it compiles (and, just as importantly, will keep working tomorrow or break at compile time). Knowing that the compiler eliminates for you a large amount of potential mistakes is a huge relief, and lets you focus on the parts of your program where the compiler cannot help you and where logic errors are lurking - especially where you are manipulating several values of the same type.
People get excited when they find out they can have types that are expressive, eliminate many useless bad programs almost for free, and be working in a language more expressive than most.
I don't think "people get excited when they encounter convenient sets of features" is a reasonable excuse for misleading claims like "if it compiles it works."
It is a reasonable explanation for why some people make these claims (over excitement), but they still shouldn't be misleading people like that.
I can't speak for lelandbatey. For myself, though, I picked that interpretation because that really seemed to be what they were trying to say. I'm not looking to take peoples' words in the least-charitable way possible, but I'm also not going to go out of my way to make excuses for them when they say something that is clearly wrong.
I cannot say that getting upset over people using jokey memes to communicate ideas (Haskell is more likely to be correct after a successful type-check than other langs) is likely to do you much good.
So let's see here: You asked why I was picking the interpretation I did. I answered. You respond about me getting upset, and commend Epictetus.
Where, exactly, did I say that I was getting upset? I was stating why I interpreted those guys as being serious rather than joking in their claims. What does Epictetus have to say to whether they were tongue-in-cheek or not? Are you just arguing to argue? Because you're sure not responding to what I said.
> Haskell is more likely to be correct after a successful type-check than (most) other langs
> "I cannot say that getting upset over people using jokey memes to communicate ideas (Haskell is more likely to be correct after a successful type-check than other langs) is likely to do you much good."
You have, evidently, taken the least-charitable interpretation of GP's post yourself. And, right in the context of a discussion where you were the person to introduce that phrase!
In this I prefer logical reasoning to empirical evidence. Consider a function that takes a list of things and returns the last one. Let's write that function in Haskell.
last :: [a] -> a
Without looking at an implementation, let's think of how many ways this function could possibly go wrong? It could return the first element of the list instead of the last one. It could return the second to last element of the list. More generally, it could return any one of the elements of the list that was passed in. But that's it (other than the empty list case which for simplicity we can ignore because it's a condition we can statically detect). There are no other possibilities, period.
Now think about implementing this function in any other language. What about Java?
public Object last(Object objs[])
This function can return any of the elements of the incoming array. It could also return null. It could also return the int 42, or the string "hello". It could delete files on your hard drive, open a network connection and phone home to the NSA. I could go on and on.
The point here is that you simply can't say as much about what this function could be doing as we could say about the Haskell version. This is the case for every mainstream language in wide use today. Some languages allow you to say a little more than others, but none of them come close to what Haskell gives you. Because of this, I don't really feel a pressing need for empirical evidence. Logical reasoning lets me make that claim quite confidently.
That's true! You have proved the original (deductive) claim "if it compiles, it works" for that one specific example, but that does not hold in general.
In general you may prefer the alternative (inductive) claim "more likely to be correct", but that claim requires empirical evidence.
The inductive claim "more likely to be correct" is strongly supported by the evidence gained from enumerating the number of ways the functions could go wrong. Now if we want to expand our domain out from just that function to programs in general, we need an idea of how applicable those ideas are to larger programs. The biggest source of reducing error cases in my example was purity.
Some parts of programs (namely the side effecting parts) can't be expressed as pure functions. So the next piece of evidence we need is an estimate of the percentage of large programs that can be expressed as pure functions. From my experience writing Haskell full-time for the last five years I can tell you that it is very substantial. Even in very impure code you can often factor out lots of small pure operations. I feel very safe in claiming that at least a third of Haskell code can be written with pure functions, and I think it's likely greater than half. (It could be a lot higher, but I'm trying to keep the confidence level fairly high.) You don't have to take my word for this. You can go off and browse through millions of lines of Haskell on [Hackage](http://hackage.haskell.org/packages/) and see for yourself. It probably wouldn't be too difficult to write an automated script to do this.
Now we've seen that pure functions have a small fraction of the error conditions that impure functions have. And we've seen that maybe half of all the code we write can be expressed that way. That's a pretty dramatic reduction in the number of potential error conditions we might encounter for even complex programs. That is why I think the claim "more likely to be correct" is strongly supported by evidence.
You are piecing a bunch of empirical facts together using reasoning, but there are lots of implicit assumptions in your reasoning.
One assumption is that reducing error cases, reduces errors. Maybe the other errors increase in prevalence when you reduce error cases?
You say that even in impure code you can factor out pure parts. You assume this refactoring doesn't introduce bugs.
You talk about the fraction of code that is pure in haskell repos. But we don't know how the amount of impure code compares to amount of impure code in other languages. Maybe it is the same? Just haskellers have some pure code in addition?
Finally, we are talking about the bug proneness of haskell, not just an idealized fp-language. Maybe something with haskell causes bugs. There are many candidates. Poor support for debugging has mentioned in another comment. Maybe the libraries are less mature. Maybe less IDE support. Maybe something about the syntax causes bugs. Etc etc.
For this reason I think it would be easier to just experimentally verify the hypothesis directly: Does Haskell cause less bugs?
> but there are lots of implicit assumptions in your reasoning.
Yes, there are assumptions, but now we're getting somewhere.
> One assumption is that reducing error cases, reduces errors. Maybe the other errors increase in prevalence when you reduce error cases?
I think this is pretty unlikely. If we switch from C to a programming language that makes buffer overflows impossible, we don't expect to see a corresponding increase in, for example, off-by-one errors. After working with a language like Haskell for awhile you start to see that when the compiler tells you about missing a case for Nothing, you don't just sweep it under the rug. You stop and think about that case. I think it's reasonable to assume that when a programmer stops and thinks about a case, he's more likely to get it right. Errors often happen because the programmer neglected to think about a case entirely.
> You say that even in impure code you can factor out pure parts. You assume this refactoring doesn't introduce bugs.
I'm not talking about refactoring here. I'm talking about writing your code that way from the start, so regressions aren't an issue. As for the question of how many bugs you might write to begin with, see the previous point.
> You talk about the fraction of code that is pure in haskell repos. But we don't know how the amount of impure code compares to amount of impure code in other languages. Maybe it is the same? Just haskellers have some pure code in addition?
In other languages ALL code is impure. There are no other pure languages in mainstream use today. So then the question becomes whether the pure code written in Haskell performs any useful function as opposed to being just meaningless fluff. It's obvious that this code performs tons of useful operations and every time it is used, we are avoiding the need to have to solve the same problem again. It's very clear what problems are solved by that code, and it's very clear that people are able to reuse it to avoid the work. Therefore, it's absolutely not simply additional cruft.
> Finally, we are talking about the bug proneness of haskell, not just an idealized fp-language. Maybe something with haskell causes bugs.
None of the points you mention cause bugs. Lack of debugging has nothing to do with causing a bug. It just means that you'll have to go about fixing your bug differently. You can look for counter-arguments all day long, but at some point you're just grasping at straws.
> For this reason I think it would be easier to just experimentally verify the hypothesis directly: Does Haskell cause less bugs?
It's not easier. Building software is hard and takes a long time. Furthermore, constructing a scientifically valid experiment is even more costly. Most people want to be productive, so they're not going to go to that effort. There is huge variation between people, so these kinds of experiments have to be undertaken like medical studies...i.e. with large n. If you're interested in building complex, real-world systems, you're simply not going to get a large n. Also, Haskell has only become commercially viable in the last 5 or so years, so there hasn't yet been enough time/effort spent to perform these experiments.
But even with all these caveats, we do have some experimental evidence. There was a CUFP report from a company that rewrote a substantial groovy app in Haskell [1]. And the result is that yes, Haskell did indeed result in fewer bugs.
Groovy was originally designed as a scripting language intended for manipulating and testing classes written in a statically-typed language, Java, in which substantial apps should be written. Only later did new managers of Groovy start promoting it for building systems even though it wasn't suitable for that. A better test would be rewriting a substantial Java app in Haskell.
Ok, so 50%, 95%--whatever your number is--of the code in Haskell we have established is susceptible to dramatically fewer bugs than any other language out there. How can you possibly claim it doesn't matter? Just because you can construct a situation where it seems to not matter doesn't mean that situation is representative.
And oh by the way, we can easily prevent your situation in Haskell as well.
safeRm :: SafeFilePath -> IO ()
Then we create the SafeFilePath data type (it can even be a newtype, which means it will have zero performance overhead) and we can write a smart constructor that makes it impossible to ever have dollar signs, stars, or anything else that might cause this kind of bug.
mkSafeRm :: String -> Maybe SafeFilePath
Then you hide that stuff away in a module and only expose a safe interface. Now, BOOM, safeRm cannot possibly ever have the bug you described. This is made possible by purity, strong static types, and the module system. Some mainstream languages allow you to partly achieve this, but it usually incurs lots of boilerplate and the lack of immutability means that there will be more holes in whatever solution you can come up with.
> 95% [...] of the code in Haskell we have established is susceptible to dramatically fewer bugs than any other language out there.
No! Haskell has about the same proportion of LOC performing IO as any language. In Haskell, it may be easier to find where the IO code is, using the type system, but that doesn't make any of the code correct.
> Then you hide that stuff away in a module and only expose a safe interface.
Now you're not even listening to what I said. In my topmost post in this thread I showed how pure code in Haskell is susceptible to dramatically fewer potential bugs than equivalent code in any other mainstream language.
I said:
> There are no other possibilities, period.
And you agreed:
> That's true!
Most of that bug reduction was made possible by Haskell's purity/immutability. Now you're completely ignoring that point that we already established.
> In Haskell, it may be easier to find where the IO code is, using the type system, but that doesn't make any of the code correct.
No, it doesn't deductively "make any of the code more correct". It makes the code inductively "more likely to be correct". You asked for empirical evidence for the inductive claim and I gave it to you.
> You could do that in any language.
No, you could not. Other languages have module systems with hiding, but they do not have purity, the ability to categorically eliminate things like null errors, etc. You're zooming in to one feature, but it's not just one feature that enables all this. It's the combination of several.
I did agree that you can prove some properties about your code. Specifically, you can prove which parts of the code do not perform IO, and in that limited sense "if it compiles, it works" for that example, but that does not hold in general.
I did not agree that your code is more likely to be correct in general. The non-IO code may still be wrong (as you said then: it could return the first element of the list instead of the last one) and the IO code may also be wrong. And you have no evidence that any of that code is more likely to be correct.
The Haskell compiler can enforce some organization on your code (IO code goes here, non-IO code goes there) but the bugs could still be anywhere. All you have done is to shift the deckchairs on the Titanic!
> Most of that bug reduction was made possible by Haskell's purity/immutability.
You have no evidence of any actual bug reduction.
> You asked for empirical evidence for the inductive claim and I gave it to you.
Working deductively from the definition of Haskell is not empirical evidence for the claim that Haskell programs are more likely to be correct.
> And you have no evidence that any of that code is more likely to be correct.
> You have no evidence of any actual bug reduction.
> Working deductively from the definition of Haskell is not empirical evidence for the claim that Haskell programs are more likely to be correct.
My deductive reasoning is not the evidence I'm citing here. We counted the total number of ways that a function could go wrong and saw that in pure Haskell code, the number is drastically reduced. We know that the bug types we eliminated actually occur in practice, so under the reasonable assumption that the distribution of bug types is relatively constant, those numbers do provide empirical evidence (observational, not experimental) that Haskell programs are more likely to be correct.
Yes, pure code can still be wrong, but it can be wrong in a lot less ways than the impure code that you're stuck with in other languages. That code is still doing useful work that is also bug-prone in other languages. Therefore we can be reasonably confident that it will reduce bugs.
> My deductive reasoning is not the evidence I'm citing here.
You have no evidence, only (invalid) deductions.
> We counted the total number of ways that a function could go wrong
If you did this it would be deduction.
> and saw that in pure Haskell code, the number is drastically reduced.
No.
Say you have an IO function with two parts, a non-IO part to compute a directory name using some input, and an IO part to remove that directory:
rmrf_steamroot some_input =
-- some code to compute a directory name using some_input
...
-- some code to remove that directory
...
Now, the first part does not perform IO, so let's extract that into a non-IO function:
compute_directory_name some_input =
-- some code to compute a directory name using some_input
...
rmrf_steamroot some_input =
let directory_name = compute_directory_name some_input
-- some code to remove that directory
...
How many bugs were removed by doing this? None. It's the same code, just moved about a bit.
Sure, the code in the non-IO function "compute_directory_name" does not perform IO (and therefore does not have IO bugs) but that code did not perform IO (and therefore did not have IO bugs) when it was in the original IO function "rmrf_steamroot"! So there is no bug reduction.
> those numbers do provide empirical evidence (observational, not experimental)
That is not empirical evidence. Perhaps it may help you to read this introduction to the topic:
https://en.wikipedia.org/wiki/Empirical_evidence
(And where it says "observation or experimentation" it may help if you follow those links.)
> If you absolutely insist on experimental evidence, we have that too
As you said earlier, they "rewrote a substantial groovy app in Haskell". There are too many confounding variables there.
We're not even arguing about the same thing. I wasn't talking about the rm function, I was talking about the "last" function in my original comment.
> If you did this it would be deduction.
I did enumerate every possible way that function can go wrong in Haskell. It is precisely n-1 where n is the length of the list (we can ignore the empty list case without loss of generality because it is easy to handle that case statically). In every other language in mainstream use today, the number of ways it could go wrong is infinite. And we actually do see those happen sometimes in practice.
The analysis in the above paragraph is the "active acquisition of information from a primary source", i.e. observational evidence for the inductive argument that code written in Haskell is "more likely to be correct".
> As you said earlier, they "rewrote a substantial groovy app in Haskell". There are too many confounding variables there.
I'm keenly aware of the confounding variables. But the fact is, you're never going to find a significant study that doesn't have a bunch of confounding variables. If that's your criteria for making a decision in this domain, then you won't be accomplishing much. In fact, I doubt we even have strong experimental evidence that C is more productive than assembly language. If you have different people write the different languages, the skill of the people is a confounding variable. If you have the same person write them all, then their knowledge of the languages and their mounting domain experience are confounding variables.
So we take whatever evidence we can get. If my bayesian prior was that all languages are equally likely to result in correct programs, then this evidence tips the scale slightly in Haskell's favor. We can't take it to the bank yet, but we've only looked at a couple pieces of evidence. (That's not the only evidence out there, but I'm constraining the discussion to this because of the bandwidth of this communication channel.) Point is, I think we're at the point where savvy forward-looking people should at least take note of Haskell's potential benefits. However much we know now, we will continue to learn more as we observe more and more people using Haskell to build real things.
> I was talking about the "last" function in my original comment.
Then let's say that "some_input" is a list and the non-IO function "compute_directory_name" should return the last element of that list. If that code were instead a part of the IO function "rmrf_steamroot" then the code would have just as many bugs. Conversely, extracting code from an IO function into a non-IO function proves only that the code did not perform IO (and therefore did not have IO bugs) in the first place. There is no bug reduction.
> I did enumerate every possible way that function can go wrong in Haskell.
This is deduction.
> "active acquisition of information from a primary source"
Did you read beyond the first sentence of that article? "In living beings, observation employs the senses." Which senses did you use to deduce the number of ways a function can return an element of a list?
> i.e. observational evidence
No, a mathematical "observation" is not an empirical observation.
It's more like "if the code were written like Haskell programmers write programs, taking full advantage of static types to encode information about function return values, then it would be correct. Forgetting to handle the 'null' option would be detected at compile time."
There is a big difference: "set -u" won't reject incorrect bash programs, it will merely stop some kinds of incorrect behaviors by stopping the program and preventing it from causing greater harm. However, the program won't have completed its intended task, therefore remaining incorrect.
In contrast, using Maybe to indicate "possibly no value" in Haskell (as it is standard practice; in fact there are no nulls in the language) prevents you from even writing some kinds of incorrect programs in the first place. In this sense, a program written in Haskell is a lot more likely to be correct than one written in bash, because the compiler will force you to consider cases you may have missed in a less safe language (like bash).
Of course, neither language guarantees correctness. It's just that one is safer than the other by design.
> No, but "set -u" does help the bash programmer to reject incorrect bash programs and to put "test" where necessary, just as the Haskell compiler helps the Haskell programmer.
> Perhaps the Haskell compiler helps more. Perhaps Haskell programs are more likely to be correct. Perhaps. There is only one way to find out.
I think you're being disingenuous. Haskell is designed to be safer (i.e. able to reject more incorrect programs) than bash. There is no "perhaps" here -- I've shown how the compiler helps more. In your example, bash simply fails to reject an incorrect program. The program will NOT run as intended, but instead will abort when it reaches an inconsistent state (such as attempting to access an uninstantiated variable). Do you see the difference between finding out at run-time that your program misbehaves, as opposed to entirely preventing the misbehavior at compile time? You simply cannot write a Haskell program that will attempt to reference an undeclared variable. That's a whole failure mode entirely gone! You don't even need to test for this, because Haskell is comparatively safer than bash.
If the Haskell programmer uses Maybe, but there is also a cost to doing that, and overall that approach may (or may not) help more in writing correct programs than using bash with a test suite using "set -u".
> The rest of your comment reads like a confused mess to me.
You have two options: 1. you can make deductive claims like "if it compiles then it works" which require proof; or 2. you can make inductive claims like "more likely to be correct (all else being equal)" which require empirical evidence.
You appear to be offering deductive arguments for an inductive claim.
> If the Haskell programmer uses Maybe, but there is also a cost to doing that
No, no ifs about it. Haskell uses Maybe to denote the absence of a value; this is a fact. There is no other possibility because the language doesn't have null values. If there to a cost in using Maybe, it's definitely not paid in safety/correctness, which is what we're discussing here.
You continue to write "may or may not" but I've shown you how the approach is better than bash. You can even forget the Maybe monad if you're less experienced with it, and instead focus on one simple fact: you can write and run a bash program that aborts after attempting to access an undeclared variable, but you cannot write and run such a program in Haskell because it's impossible. Haskell is safer.
Deductive/inductive is neither here nor there. I didn't make the ridiculous claim that "if it compiles then it works", and nobody else here did either. The claim I did make is that entire failure modes which are present in bash aren't possible in Haskell; I leave to you as an exercise to consider whether there exist failure modes in Haskell which are not in bash.
> Haskell uses Maybe to denote the absence of a value
A Haskell programmer could use an empty string for that, or given a Maybe could do this:
fromMaybe ""
But no true Haskell programmer would do that.
> you can write and run a bash program that aborts after attempting to access an undeclared variable
Yes, and perhaps the bash programmer could likely eliminate that fault through testing, perhaps about as likely as the Haskell programmer could get the Haskell compiler to accept a program at all!
> The claim I did make is that entire failure modes which are present in bash aren't possible in Haskell
And therefore Haskell programmers are more likely to write correct programs?
No, but "set -u" does help the bash programmer to reject incorrect bash programs and to put "test" where necessary, just as the Haskell compiler helps the Haskell programmer.
Perhaps the Haskell compiler helps more. Perhaps Haskell programs are more likely to be correct. Perhaps. There is only one way to find out.
> It's just that one is safer than the other by design.
What do you mean by this? Is this a deductive claim, contradicting the previous sentence, or an inductive claim that Haskell programs are "more likely to be correct" (all else being equal), which requires empirical evidence, as you cannot establish an inductive claim with deductive arguments.
> "set -u" does help the bash programmer to reject incorrect bash programs and to put "test" where necessary, just as the Haskell compiler helps the Haskell programmer.
Except the Haskell compiler (GHC here) doesn't just equivalently put test "where necessary", but it puts test everywhere and on everything which would be wildly impractical and tedious with bash.
I really wish static typing advocates would consider making inductive claims. The last few times I've asked for such evidence the response has been along the lines of "you just don't understand". It's indicative of a general intellectual orientation that I think has held back the introduction of valuable PLT concepts into mainstream languages.
> You have proved the original (deductive) claim "if it compiles, it works" for that one specific example, but that does not hold in general.
Are you sure it does not hold in general? Upon repeating mightybytes example with all Haskell functions vs another language I feel like you'd get similar results due to pervasive purity and the type system.
I chose that non-total function because it is easier to enumerate all the possible error cases than with the map function. And the error case is easily handled by the combination of incomplete pattern match and Safe Haskell. I was also trying to emphasize purity more than free theorems.
>What is the effect of programming languages on software quality? This question has been a topic of much debate for a very long time. In this study, we gather a very large data set from GitHub (729 projects, 80 Million SLOC, 29,000 authors, 1.5 million commits, in 17 languages) in an attempt to shed some empirical light on this question. This reasonably large sample size allows us to use a mixed-methods approach, combining multiple regression modeling with visualization and text analytics, to study the effect of language features such as static v.s. dynamic typing, strong v.s. weak typing on software quality. By triangulating findings from different methods, and controlling for confounding effects such as team size, project size, and project history, we report that language design does have a significant, but modest effect on software quality. Most notably, it does appear that strong typing is modestly better than weak typing, and among functional languages, static typing is also somewhat better than dynamic typing. We also find that functional languages are somewhat better than procedural languages. It is worth noting that these modest effects arising from language design are overwhelmingly dominated by the process factors such as project size, team size, and commit size. However, we hasten to caution the reader that even these modest effects might quite possibly be due to other, intangible process factors, e.g., the preference of certain personality types for functional, static and strongly typed languages.
Empirical evaluations break down quickly as the complexity of what is being measured increases, so your best bet in doing a study is to focus on one or a few features.
PLs are of course evaluated over time in the market place over time, like any other designed artifact.
I love that report and find it very inspiring (and it gives me an intuition that Haskell has an edge over the other languages), but the methodology is very disappointing:
- The requirements were mostly up to the interpretation of implementors, which more or less decided the scope of their programs.
- All results were self-reported. Even ruling out dishonesty, there are a lot of ways uncontrolled experimenters can report incorrect results.
- Many implementations weren't even runnable.
- No code was run by the reviewers, at all.
I really would love to see a more serious attempt at this experiment (probably with more modern languages).
The context I've read that remark in before is discounting the need for automated testing. At least one example has been provided in this thread of a Haskell developer claiming to have released code after it was verified by the type checker but without actually testing it. I don't think it's reasonable to take the phrase at anything but face value, considering that it's used as a promotional slogan by Haskellers.
"misleading claims like "if it compiles it works.""
ML family of languages contain powerful language features and libraries that, when programmed using particular style, can produce programs that actually do that (if they are brief). They are not magic, the point is just that the abstractions used there effectively remove large categories of typical bugs. Of course the language itself is not sufficient, one must study how programs are supposed to be written in the said languages to understand the utilization of those features.
If the program is a composed from trivial data conversion steps that are implementable using standard transforms (C++:s stl algorithms, ML:s folds, etc) then it is very likely that it works when it compiles. If there are various branches in the logic and I can encode those branches using types as invariants then that eliminates a particular category of bugs altogether which reduces logical errors. If I use immutable variables it helps even more. I'd say the 'compiles and works' means that if one can leverage existing operations on containers and use types as helpfull invariants then those two stylistic choices reduce the possible number of bugs in various categories.
I would not claim all errors are removed... e.g. numeric code that depends on the precision of arithmetic on floating points is as error prone with or without static types.
On the other hand, when working with dependent types, the specification is a type, and if the theorem giving that specification type-checks (ie: the "proof" is a program of the appropriate type), then the code is correct, period.
Of course, attempting to prove the theorem can be hair-pullingly frustrating and takes valuable time, but it will expose the assumptions and corner-case you weren't thinking clearly about.
The coda at the end is nice tool in general. Whenever you find yourself in a discussion, where it seems people talk past each other because some words have a fuzzy meaning, try to avoid the word completely. Works good for discussions about "free will", "love", "intelligence", "luck", "conciousness", and apparently "types".
With deference to Dr Kell, I think this is overwrought.
He has some good points, points made happily against a particular form of "type cultist" who oversimplifies argument toward making types out to be something magical. They're not, no sane person would think so, but they are a static, syntactic proof system pertaining to the meaning of your programs and there's a lot to be said for such technology.
I am happy to quibble exact points made in this rant, but I'm on my phone so for now I'll merely say that there's a large design space of programming languages and a similarly large (perhap today larger) space of type theories. Matching them up to hit all of your tradeoffs is hard, but there have been some great successes and I would happily contend that any professional programmer owes it to themselves to explore this design space "in anger".
I'm also happy to generally claim that faster, more complete feedback is better than the opposite. Static systems of all regards are faster than "dynamic" ones, and most of them are more complete. This is where you hear about comparisons of types (especially dependent ones) and tests. It's great stuff to think about and explore.
Further, I want to emphasize that SMT solvers are fascinating too and nobody thinks that they're not. The style of proof they provide is more expressive and less certain, though, so the right answer is to know how to combine all of these modes of evidence.
> Type checkers are one way to gain assurance about software in advance of running it. Wonderful as they can be, they're not the only one.
This is true, but in my experience they are far and away the most common and easily tooled automatic way. Tests may run automatically, but they must be manually written, and static analysis tools are not (yet?) very widespread.
No, I think a separate type-level language is a good thing, so long as my data-level language remains Turing complete (and thus undecidable). I would much rather be forced by the syntax -- by the construction of the language itself -- into a guaranteed decidable subset, rather than have to reason things out myself and get frustrated when the compiler doesn't agree with me (or when it used to agree with me and doesn't any longer!).
Now, there's no reason that the type-level language can't be exactly a subset of the data-level language. I'd just rather not play guess-and-check decidability with the compiler the same way I currently have to play guess-and-check optimizability.
Oh I totally agree. Unfortunately for many that's far too radical a notion, despite how unnecessary Turing-completeness is for 99.95% of programs written, and how desirable termination is. First you have to convince the Ruby/Python/JS/Elixir crowd of the frivolity of code mutability.
I think the author meant that you don't want two separate Turing-complete languages, one for values at runtime, and another for values at compile time.
> The Sniveley/Laucher talk included a comment that people like dynamic languages because their syntax is terse.
Sure. Trying to have a strongly-typed Java program, for instance, means a lot of boilerplate. As a consequence, it's often not done, or at least not done enough.
> To suggest that any distaste for types comes from annotation overhead is a way of dismissing it as a superficial issue.
On a large codebase, there is nothing superficial about it. The more boilerplate you have, the more difficult it becomes to understand the codebase and to find code which actually does something.
> If everyone would just use a modern language with a fancy type system, all our correctness problems would be over, right? If you believe this, you've drunk far too much Kool-Aid. Yet, apparently our profession is full of willing cult members. Let me say it simply. Type systems cannot be a one-stop solution for specification and verification. They are limited by definition. They reason only syntactically, and they specify only at the granularity of expressions. They're still useful, but let's be realistic.
Let's be realistic, and not pretend this is a widespread opinion.
> Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic. Usually they are captured only overapproximately, which, in turn, yields an inexpressive proof system. The end result is that some manifestly correct code does not type-check.
Possibly, but it's all a question of tradeoffs. There is a lot more incorrect than correct code which doesn't typecheck.
> On a large codebase, there is nothing superficial about it. The more boilerplate you have, the more difficult it becomes to understand the codebase and to find code which actually does something.
In case of types it's true for humans. IDE will be able to build a very precise model and ease navigation and code changes when it understands types.
Why should this be a property of the IDE and not the language itself?
No, seriously. If the language sucks but your interaction with the IDE is fine, why not have a language that is closer to your interaction with the IDE to begin with, and use a text editor?
It's the old "verbose getter and setters are not a problem because I can generate them in Eclipse" argument. To some extent, over-reliance on an IDE indicates issues with your language of choice, just like the overuse of design patterns.
It is property of the language - type annotations. Yes - maybe types can be infered, but I haven't seen any IDE with good refactorings for languages without types annotations (smalltalk doesn't count).
IDEs can help, but they're not a panacea. There is still a mental overhead when dealing with a more verbose codebase. Not to mention increased programmer time, especially when coding guidelines mandate the creation of builders.
Another point I wanted to address is that people will tend not to fight the language. Make types harder to create than necessary? You'll have less well-typed programs. Make types syntactically light? You'll have more well-typed programs.
Getters, setters, builders, special design patterns are not related to existence of type annotations. They are related to lack of different constructions or misusing existing ones.
They're very much related to the point I was addressing, namely "What does it cost to add a new type in a language like Java". You're going to have type annotations in your signature no matter what, but adding a new type is relatively expensive.
Things that also get my goat (from a less type theoretic point of view):
- Assuming that type checking is the only thing you might want to do with your program at compile time. There are, in fact, arbitrarily many things you might want to do at compile time. Textual preprocessing, expansion macros, type checking, C++ template metaprogramming, etc. are all obvious examples. The fact that most languages bolt all of these things on as one-off features is a sign that something deeper is being missed (perhaps the 3-Lisp[1] idea, for example, or just consider plain ol' Lisp macros).
- Assuming that totality, soundness, and lack of side effects are always type checking virtues. Sometimes I'd like a "typechecker" that isn't always guaranteed to terminate. Sometimes I'd like my typechecker to launch some missiles. This is really more about the previous point.
- Assuming that type checking is NOT desired at runtime. Sometimes it is. Clojure's core.typed has the property that it is "just code" and can therefore be run at anytime and used for things other than checking that your code is safe to ship. [2]
- Assuming that a program that fails type checking shouldn't be run. Maybe it should and the parts of the program that fail type checking should be run inside some monadic context. Maybe we want not only gradual typing, but gradual enforcement. Maybe if we had richer type data, then "failing type checking" wouldn't be binary. Perhaps a program that fails certain type checks has to add runtime support to enable certain features, but if the same program type checked to be about pure memory locations, the runtime would vanish and a "straight to the metal" program would remain. (In other words, maybe what we currently call a language's "runtime" should just be a residue of things that couldn't be checked at compile time, among other things.)
- Assuming that types and the type checker should be a fixed feature of the language. Perhaps type checking should be something that is built as a library from language primitives. Take this far enough and you get something like exotypes. [3] Which reminds me...
- Assuming that "type" is the only kind of metadata you might like to attach to a symbol, expression, or value. There are many other things I might like to express, and I might like to use the usual machinery of type checking to analyze or work with those things. Clojure's value-level metadata and Common Lisp's property lists are some good examples of generalizing this.
- Focusing on manifest typing for verifiability of programs and ignoring the extra information it gives tooling. Visual Studio's IntelliSense and F#'s type providers are examples. At least one person at Microsoft has trouble sleeping at night because he or she is worrying about when the rest of us are going to figure this one out. [4]
- Assuming that most programmers want one or the other. The article touched on this, but I wanted to expound a bit. I would like my original prototype to feel like play-doh and my finished product to feel like concrete. Why do I have to do this in two different languages? "Oh I'll prototype it in python and then switch to Haskell when I want it to be safe." What?
- In general, assuming that it is the job of the language designer to provide the safety nets, rather than the DSL or API designer. A suitably designed programming language is one that could prevent operation Foo in layer 3 while allowing it in layers 1 and 2. This is one reason why languages like Idris are so complicated. Dependent types HAVE to be complicated because the language designer feels that it is his or her job to make sure the part of your program that runs at compile time terminates and doesn't do anything "bad". Why do we rarely question this assumption?
Why do I have to do this in two different languages? "Oh I'll prototype it in python and then switch to Haskell when I want it to be safe." What?
This has always sounded a little crazy to me, too. I did recently have a successful experience at work where I prototyped something in Javascript and then built the production version in Java, but porting the code felt like a lot of wasted effort, compared to if I could just add typechecking to the JS version. A gradual typing library seems like a good way to achieve that.
Perl 6 elegantly blends static nominal typing and arbitrarily loose or tight dynamic constraints.
The following slides were published a week or so ago and should demolish most folks' overly simplistic view that one or other is best or indeed that they don't play well together:
> (It should also do so using a straightforward explanation, ideally featuring a counterexample or stripped-down unprovable proposition. I don't know any type checker that does this, currently.)
I guess the incomplete-pattern-matching warnings (in eg ghc) come closest. They usually give you an example of an example of a value you haven't matched. But that's a very restricted and simple domain.
> If somebody stays away from typed languages, it doesn't mean they're stupid, or lack education, or are afraid of maths. There are entirely valid practical reasons for staying away. Please drop the condescending tone.
The hardest objective problem in computer science may be P ?= NP, but the hardest subjective problem is whether it is better to have static vs. dynamic typing in languages. There are extremely intelligent, thoughtful people on both sides... and it's rare in software engineering that there is such an even divide. I'm quite familiar with Haskell, Scala, Clojure, and many other languages... and I still can't conclusively call one better. I prefer static, on a mix of practical grounds, but I realize that it's not a clear victory.
Take the concept of data frames from R, also seen in Python's Pandas library, and probably inspired by the APL family's (column-oriented) tables. It's not a complex concept. Yet it's very powerful for interactive data exploration. It's also a bitch to statically type (see: https://github.com/acowley/Frames). It's more of a leap than lenses (and probably, like lenses, extremely cool once you fully "get" it).
If we have to pull out some advanced Haskell extensions to do something basic in interactive data analysis then I consider that worrying. (This is not to say that Frames isn't a great piece of work. Bringing subtyping into a Hindley-Milner derived language and not having everything go to hell is really hard. See: Scala) And remember, this is coming from someone who's pretty invested in the "static" side.
Clojure also has a world-class aesthetic sense. Haskell is still using camelCase. OCaml uses under_scores; that's better than fuckingUglyCamelCase, but not ideal. Clojure (and the Lisp family in general) is run by people who realize that aesthetics are really important and that allowing hyphenated-tokens is far better than allowing people who hate their space bars to write "a-1" when they should be writing "a - 1". That's just one example. For another, maps. Clojure has {"five" 5, "ten" 10} but Haskell has fromList [("five", 5), ("ten", 10)]. My point is that (which I prefer Haskell, for its types) Clojure's aesthetic sense is arguably better, and I would say world-class, especially considering that it runs on a butt-ugly platform (JVM) and is still a beautiful language. We need to keep watching that community closely because they're doing some great work in a wide variety of fields, including front-end development (ClojureScript).
Type systems don't just make you write annotations; they force you to structure your code around type-checkability. This is inevitable, since type checking is by definition a specific kind of syntactic reasoning.
There is some truth around that. Just to get data frames, you need row types which means you have subtyping, and that complicates type checking considerably. Haskell (see Frames) uses multiple "experts only" language extensions to get something that "just works" for casual use but requires advanced knowledge to grok the types. It's great work, but its difficulty shows that we can't just ignore subtyping.
The counter-argument that I'd make is that 95+ percent (maybe more?) of all functions that are ever written ought to have simple static types. So much of code, when it is clean, is already well-typed, even in a dynlang. The difference is that, in a static language, the compiler yells any time someone fucks that up in refactoring. And, more generally, you learn about errors (not all errors, but a surprising percentage of them) sooner and that's a good thing. In a dynamically typed language, you see a lot of functions that evolve into multimethods that do different things per input type(s) and (although usually this won't happen if the code is maintained by decent designers) you can get O(n2) or worse complexity in the functionality. If you're programming defensively in a dynlang, you have to think about all the crap that might be passed into your functions. "What's a Matrix plus a Scalar? How about a RowVector plus a ColumnVector? How about a Sparse2DArray plus a DataFrame?"
On the whole, I'd rather be in a statically-typed language for a program of any size, and I'm stodgy and conservative and old (but efficient and concise) so, for me, "big code" starts around a couple thousand lines. I hate writing boilerplate unit tests that a compiler and a type system would knock out automatically. But I do have to give Clojure a lot of props for its community and its aesthetic sense, and I think that the above obviously derive from its ease-of-use and its Lisp heritage, both of which are tied to a feature (dynamic typing) that I otherwise wouldn't much like.
The main question that I've been pondering for a few years (and not coming to satisfactory answers) is whether it's possible to unify the cleanness-of-language and aesthetics of Clojure/Lisp with the static typing of Haskell... and not get some hyper-complex type system that results in compile-speed problems at scale (e.g. Scala under typical use). It's an open problem.
I found this wonderfully clear and refreshing and I felt hopeful for the future of programming. In the meantime, it's just nice to see that not everyone is a shambling cultist, repeating canned talking points they read on a wiki which affirm to them that their own choice is the very best choice possible.
It's fair to say that but it isn't the case that someone can have an worthwhile opinion of something they haven't tried and a lot of people working with say JavaScript or PHP just have never tried a decent ML-style language in anger.
I think Stephen is a tiny bit guilty (as we all are) of that which I'll use Kahneman wording's to put: "Nothing is as important as you think it is when you are thinking about it". There's what seems to be an exaggeration that whatever cost a type system has must be high... it isn't even true of dependently typed programming languages.
I also think product and sum types can be given a free pass to most complaints and while at it, you can throw in first-class function type as a minimum. And I will grant that you can stay away from ad hoc polymorphism and subtyping.
> It's fair to say that but it isn't the case that someone can have an worthwhile opinion of something they haven't tried
I disagree. I don't have to try hitting myself in the head with a hammer to have a reasonable basis to believe it would be a bad idea. There's not much point in having reasoning ability if you can't apply it to develop useful opinions on what is and isn't even worth trying.
Obviously, that's not to say that there aren't additional insights possible from direct experience, and that people sometimes apply prejudice rather than sound reasoning to present opinions on things they haven't tried, but its simply silly to say that people cannot have a worthwhile opinion on something they haven't tried.
There may be an "is -> isn't" or "can -> can't" issue in the line I quoted, but I don't think so -- the rest of the sentiment in that article seems to be a specific case where the poster believes that someone is making an error of offering an opinion without experience (which I agree is an error), which makes sense (though, I'd obviously argue, represents an overgeneralization from a valid example) if its supporting a generalization that opinions without experience are invalid, but, without some "but" or "on the other hand", etc., doesn't make a lot of sense if the thesis it goes with is that some such opinions are valid.
