Is Sound Gradual Typing Dead? [pdf] | Hacker News Reader

Is Sound Gradual Typing Dead? [pdf]

ccs.neu.edu

74 pointsbshanks93 comments

> When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck.

Assertion without evidence.

Lack of static typing is awesome in evolving a system: you can convert a part of it to some new types as "proof of concept" and still load and run the code to get usefully far. You just avoid stepping on the parts which aren't converted/refactored yet.

Having something Working Now (tm) is a great motivator for some developers to keep going; it reduces the "activation potential barriers" against creativity.

The trick to using dynamic languages is to have a ton of static experience. The typing is in your head, where it doesn't get in the way. What we are seeing a lot of lately is a crop of developers who have never worked in anything but some dynamic language.

When I'm working in a dynamic language, my concept of type is consciously coming from all the static experience. That keeps me from doing totally scatter-brained things which are possible. I write code such that most of it could statically check, but with the freedom that some of it doesn't have to. Moreover, I am aware (hopefully!) of which code that is.

Lack of static typing is awesome in evolving a system

I really don't follow your logic, here. Few things change more frequently while evolving/hacking together software than the data structures and types. Changing a type in one place while forgetting to in N other places is an extremely common defect introduction method that is easily caught with static type systems. If anything, it's the evolving/hacking process that's MOST prone to accumulating runtime type errors than any other process.

> Few things change more frequently while evolving/hacking together software than the data structures and types.

I tend to agree; it is often correct. (Though sometimes we have solid data structures and types and are able to evolve things without changing them.)

Anyway, therefore it follows that if we calcify and ossify data structures and types, we kill the progress, not to mention fun.

> Changing a type in one place while forgetting to in N other places is an extremely common defect introduction method that is easily caught with static type systems.

This is blown out of reasonable proportion by static type advocates. In a dynamic system, type is de facto a few bits of value in an object. So the above situation is just another value that is wrong.

Static programs also have run-time values that can be wrong. A static program that is supposed to calculate 42 might calculate 43, which has the correct type.

To discover the cause, someone will have to sit down and think about the code.

Code which has never been exercised by a test case (coverage) should still be regarded as garbage, in spite of passing type checking. It is not known to be correct. Type checked is not the same thing as correct.

The graph of "type-value" in typical code is rather trivial. Take any moderately complex algorithm, and ignore what its operations are doing; just consider their input and output types. The resulting graph/tree is a lot simpler than what is going on with the values. Type problems are trivial. That is why it's even possible to move them to compile time and have static languages. Think about it: something that runs for hours or days in order to produce a result (and is not even known to terminate) can be entirely type-checked in a millisecond.

We do not know a whole lot about code just because it has type checked. It may feel like you do, but that's just a feeling. The name of the function might be `sort`, but it could actually fail to sort items, in spite of type checking. Or it could sort them in descending order when the expected order is ascending: some test was reversed and the reverse test type checks because the operator is commutative.

You still have to either prove your code if possible and feasible, else test it exhaustively if possible, or else test it imperfectly.

> We do not know a whole lot about code just because it has type checked. It may feel like you do, but that's just a feeling.

You can know a whole lot because it type-checked. What exactly you know depends on how you leveraged the type system.

For example, if you define a red black tree as is defined here: https://github.com/yairchu/red-black-tree/blob/master/RedBla...

You know code will never generate trees that break the red/black invariants. The tree is guaranteed to be balanced by the type checking process.

> The name of the function might be `sort`, but it could actually fail to sort items, in spite of type checking

Unless you use a dependently-typed language.

Consider this `sort` definition:

  sort : (in:List n a) -> (out:SortedList n a, IsPermutation in out)

"List n a" is a list of length "n" of values of type "a". "SortedList n a" is a sorted list of length "n" of values of type "a". "IsPermutation a b" is a proof that a is a permutation of b (returned from sort).

Here's how you can define a type like SortedList:

  type SortedList n a =
    exists min. SortedList' min n a
  data SortedList' min n a where
    Empty : SortedList' min 0 a
    Cons : LessOrEq x y -> (x:a) -> SortedList' y n a -> SortedList' x (1+n) a

SortedList thus embeds a proof alongside each element that it is less than or equal to the lower-bound of the remaining list (i.e: the next element).

Type-checking this guarantees that `sort` does the right thing, modulo resource-use/performance (or termination, depending on your type checker).

Resource use (bounding) can also be type-checked, but requires leveraging the type system even more.

These guarantees aren't free -- you have to write the types for them, and you have to prove them by instantiating values of these types. But you can opt in or out of each of these guarantees -- leverage the type system as much as you want.

With dynamic typing, you just don't have this tool at your disposal at all. No flexibility to guarantee anything. You're forced to opt out completely.

Please clarify something for me: Does that "proof" run a run time, or at compile time? If at compile time, how does it do so without running into something like the halting problem?

It does run at compile time, and it doesn't run afoul of Rice's theorem (a useful generalization of the theorem about the halting problem) because it's not implementing a general decision procedure that can decide for _all_ programs whether the property holds.

It's possible to solve halting-class problems for restricted subsets of programs, as well as to enlarge those subsets greatly by forcing the user to help. For example, I can trivially "solve" the halting problem for the subset of programs that contain no loops or recursion, by simply refusing to make a decision on programs that do. I can also solve it for the subset of all programs that do halt by simply running the program and reporting when it halts that it does, in fact, halt.

More usefully, the type systems in Peaker's examples rely on user-provided annotations to help the compiler "see" the truth of the user's claims (or equivalently, the compilers restrict the class of programs they operate on to those programs which contain sufficient user-provided annotations). The compiler doesn't have to prove everything itself - it only has to check that the proof is valid according to the rules of the relatively simple logic of the proof system.

The history of type systems has largely been a story of improving these logics and inference systems to reduce the amount of help needed from the user and enlarge the class of things that can be proven about programs. In this context, Rice's theorem amounts to saying that, no matter how complicated you make your type system, there will _always_ be programs that either (a) are valid but not accepted, or (b) are accepted but not valid.

So is it fair to say that you are proving to the compiler that your function will return a sorted list (rather than you handing an arbitrary function to the compiler, and the compiler decides whether it returns a sorted list)?

Yes, and in general it's pretty clear as you're doing it that that's what's happening. The ML family and Haskell type systems occupy a pretty nice place on the spectrum of expressiveness in that there's not much you can add to them without losing the ability to infer unique types. As long as your types are on the same level of complexity as a Haskell or ML type, you can typically get away with minimal type annotations - a bit more than ML or Haskell would've required, but not a lot more. When you introduce more complex quantifiers such as the "exists" in these examples, in practice you have to start thinking about "what the compiler knows" and how to help it know the things you want it to.

There are some systems such as Coq that use heuristics (and let you write your own new heuristics) to try to automatically find proofs, and interactive sessions in which you guide the system to the proof by suggesting tactics that move hypotheses toward goals or vice versa. This is one of the major factors that, in common speech, distinguishes between "typed languages" and "proof assistants" which otherwise are basically the same kind of thing. Even in proof assistants, though, you still need to be quite intentional about what lemmas need to be proven in order to move toward your ultimate goal, and often even in how you phrase your goals in order to improve the chances that the heuristics will find a proof.

These are the kinds of things i mean by "helping" the system in my previous comment. They are very powerful tools if assurance of correctness is a high priority, but definitely not a free lunch.

If you're ever interested in going down the rabbit hole, there's a pretty steep learning curve (though if you're comfortable with ML or Haskell you're already halfway up it) but an extensive and rewarding landscape of thought at the top. Unfortunately it's more of an academic or self-enrichment discipline than an industrial one these days, but if you look hard enough there are a few jobs where you can make use of these tools.

How the type checking proof avoids the halting problem is by lumping together "ill-formed" and "undecided" into one category: reject the program. Programs which cannot be shown not to be free a type inconsistency are rejected alongside those which are confirmed to have one.

(Actually before we even get to that, the type system has to be powerful enough to invoke the problem (i.e. be Turing complete: capable of expressing partial recursive functions).)

That would be useful if it could be applied to normal red-black trees and sorting. As in, respectively, the efficient, destructive algorithm which inserts into a tree, rendering it temporarily unbalanced and non-red-black, and then fixes it up; and an internal quicksort on an array.

Why is only destructive useful?

"...calcify and ossify data structures and types..."

What are you even talking about? This sounds like an assertion from someone who doesn't use statically-typed languages and is just guessing.

To change a data structure in a statically-typed language, you change the declaration then fix any compile errors. It is easy in most cases.

In a dynamically-typed system, data structures actually get way more ossified, because when you change a structure you don't really know what might be broken or when you are really done making the code correct again... Therefore programmers avoid this.

I feel we're getting into strawman assertion territory here.

I've worked with statically typed and dynamically typed languages, and the fact is that there's some overhead involved in static typing. You pay that overhead upfront in order to hopefully prevent some bugs (and possibly get a performance boost) later on.

If you haven't tried both, you probably won't notice the mental overhead.

I've also found that this difference sometimes result in people approaching things differently, with static typing leaning itself more to specifying things upfront compared to jumping straight into the code with dynamic typing.

Sometimes this surely means things end up being clearer with static typing, but I've also seen the reverse happen, more often than you'd think, because some kinds of code have a lot of messy little details - with a dynamic language like Python you can model, or perhaps rather avoid modeling, those little local details by just stuffing things onto something you're already passing along, while the static typer would have to think harder about how to fit them in without polluting the overall data structures.

When you're rewriting things a couple of times as your understanding of the problem evolves, it can certainly help to be able to not worry too much about those details.

Oh, I've tried both all right!

There is more mental overhead in dynamically-typed languages, actually .. it's just less visible because it's implicit! It's the overhead of having to "keep all the type information in your head", which dynamic type proponents sometimes seem to be saying is a good thing.

It's not good because it is a tax on everything you do! Whereas in a statically-typed language, sure, you have to do the little extra overhead of putting the types in the program text, but this is quite freeing in the long term, because you can then drop the burden of having to think about what type something needs to be, in most cases.

(It also serves as documentation / literate programming.)

My approach to programming tends to involve rewriting things several times, or heavily modifying them, and as someone who has been programming for 34 years, in a lot of different situations, I find that static typechecking is by far a superior framework when refactoring or rewriting code. It is not even close.

I'm firmly on the static typing side of the fence. But I think you're ignoring what others are saying about where dynamic typing shines: Where you don't know what you're doing to the point that you don't know what the proper types look like. You can try things faster in a dynamic language in that situation, because you can sweep the "don't know what the types look like" part under the rug, and experiment with algorithms, and let that experimentation show you what the types ought to be. In some situations, that can be faster/easier/better than trying, from first principles and analysis, to determine what the types must be.

I think the difference is that I (and, I suspect, you) spend little of our time in that mode, and much more in the mode where static types can save your behind. (Nothing like working on a million-line code base in its second decade to make you value static types.)

Sometimes you know what the types look like but not in detail. For instance, you know you need a structure with several named properties, but you don't commit to a type for some of them. You can have a fairly deep idea about the object model: what kinds of classes there are and how they connect, yet be loose about some of the lower level details.

You have types in the dynamic realm. Only, you're not restricted to executing nothing but consistently typed programs.

No, this is how I program all the time. Usually when I start typing I have only a rough idea of what I want to do.

But in practice this is not a problem. So what if I don't know exactly what type a particular thing will be in the end -- I know generally if it is a number, or an array/list, or a hash/index... that is all I need to know. I use one of those basic types. If I need to change it later I change it later, and the fact that I am in a statically-typed language is great for changes like this because it helps me make them with high confidence.

This is why I don't believe that anyone who makes this argument in favor of dynamic languages really has that much experience in static languages. The actual outcome in real life is the opposite of what is described.

You still have to keep type information in your head when working with static programs. Compiling isn't all that you do with programs.

Not every expression in a program is rife with explicitly visible type. Not even in a language with declarations for all storage locations. Type inference seeks to minimize that, because it's considered clutter.

However, the completely clutter-free static program looks much like a dynamic one! If I look at some snippet of OCaml or what have you, for all I know it could be dynamic.

The difference is that it's constrained in invisible ways. (If it is already correct in its current form) it cannot be changed in certain ways and still be accepted for execution.

That doesn't mean a thing to me when I'm just looking at it trying to understand it. I have to figure out what the types are, and connect all the pieces in my head.

In a statically-typed language with reasonable tools you can right-click on an expression and see what type it is. This whole thing you're describing is a non-issue.

> you change the declaration then fix any compile errors.

In all 3123 places in the code base; good luck.

This sounds like ... an assertion from someone who doesn't do actual software engineering.

Back at you!

> you don't really know what might be broken

Because you don't have a regression test suite, a test plan, and four developers to one QA person.

> Therefore programmers avoid this.

Programmers bravely avoid nothing. Historically, programmers have gotten themselves into every imaginable mess with every type of language.

> To change a data structure in a statically-typed language, you change the declaration then fix any compile errors. It is easy in most cases.

Right. This can become an overhead in a rapidly evolving design because every small type change has implications across the codebase. With dynamic typing, you only need to fix the code paths you are currently interested in and development is very focussed in a way - you don't have to shuffle all parts of the code through your mental caches. This way you can iterate over a few revisions to the types without having to 'fix everything' each time. Finally when you're happy, you go ahead and fix the other dependent code. Admittedly, dynamic languages may not help you find the code that needs fixing. This problem is somewhat mitigated by tests.

> We do not know a whole lot about code just because > it has type checked. It may feel like you do, but > that's just a feeling.

See also: The Safyness of Static Typing[1]

[1] http://blog.metaobject.com/2014/06/the-safyness-of-static-ty...

> Anyway, therefore it follows that if we calcify and ossify data structures and types, we kill the progress, not to mention fun.

I don't think it's fun to ship bugs to customers.

I think it's much more fun to have a pervasive, mandatory proof engine that shows that I don't create these bugs in my software. (since it's mandatory, I can also help my teammates use my code correctly even though they don't understand how it works!)

I make better progress when I'm not creating preventable bugs. My customers have more fun too.

> This is blown out of reasonable proportion by static type advocates. In a dynamic system, type is de facto a few bits of value in an object. So the above situation is just another value that is wrong.

It's wrong in a way that's totally preventable ahead of time. I'd rather take the proof engine and never suffer this class of bug. It certainly doesn't catch every bug, but I'll take what I can get.

> shows that I don't create these bugs in my software.

Unfortunately, it doesn't show you that you don't create other than these easy bugs in the code.

> It's wrong in a way totally preventable ahead of time.

That would be a more powerful argument if all else could be held equal, which it rarely is.

> I'll take what I can get.

Local greediness is not always rationally founded.

Anyway, dynamic typing doesn't preclude the proof engine. Dynamic programs can be analyzed to predict situations of inconsistent use of type, so that you can be informed. However, that doesn't prevent them from being executed, and still having the type representations at run time to resolve the situation. That is to say, programs for which the proof engine positively identifies one or more type error can be run anyway, as well as those for which it says "undecided" (not proven free of type errors, but no errors confirmed).

Dynamic typing doesn't mean "I don't want my program analyzed prior to it being run; do not inform me of any impending issue of type!".

A modern static type system allows this style of programming.

Not those aspects of that style of programming in which the developer consciously tries partially refactored, inconsistently typed (and thus ill-formed) programs.

>When I'm working in a dynamic language, my concept of type is consciously coming from all the static experience

Because it's fun to have to constantly lookup API docs for whatever API you're using right now to get the exact spelling or naming convention for the class that you're using. And naturally we're all writing unit tests with 100% code coverage so none of those typos ever get in to production.

Dynamic typing works great with simple APIs. Once you have to deal with complex data graphs with heterogeneous types it becomes tedious at best (eg. a simple and well designed GUI library) or a major pain in the ass (eg. Blender Python API)

Oh and let's not even get in to pants on head retarded stuff like monkey patching as a part of regular API (eg. see WAF build system)

Because it's fun to have to constantly lookup API docs for whatever API you're using right now to get the exact spelling or naming convention for the class that you're using.

Nope, I just let my editor show me the available methods for the class. It sounds like you haven't tried programming in a dynamic language with a modern editor?

I have - it heavily depends on the library you're using - it sounds to me like you haven't developed something like a GTK3 app with dynamically loaded bindings, blender extension or WAF build system plugin

No, I didn't, but your statements were general in nature ("whatever API you're using right now"). Certainly there are exceptions, but they are not relevant for most of the work being done in dynamic languages.

From my expirience those aren't the exceptions - it's pretty much half the time tools work and half the time they don't (anything involving native interop basically is a nogo, monkey patching or meta programming equally bad).

It's nowhere near the level of support you get from even rudimentary type systems such as Java which can always resolve names and can provide strong refactoring. Why do you think even Python added optional type information and type definitions ala typescript and guys like jetbrains are rushing to support it ?

Fair enough; in my experience, direct native interop (not using a wrapper), monkey patching and meta programming are all exceptions in the Python world.

> The typing is in your head, where it doesn't get in the way.

If the typing's in your head, then why not write it down for the benefit of others? and for the personal benefit of automation provided by the compiler?

The answer is that for even the most basic systems, a model of its operation cannot be retained in a single person's working memory for even a moment, nevermind the duration of a incremental refactoring. People have trouble remembering phone numbers long enough to dial them. How are you supposed to remember the complex interactions of functions, libraries, and any state that they might be managing?

This is by far the greatest fallacy and self-delusion that is propagated by scripters. Talk about an assertion with a ton of evidence against it.

The same argument would say that it's impossible to write mathematics papers without proof assistants (Coq, etc).

Obviously that is bogus, mathematicians are not 'deluded' about their ability to check their work themselves. It's just a skill.

In the analogy between programming and theorem-proving, programs correspond to proofs. When mathematicians informally check a proof, they are usually judging whether a complete proof could be produced, not whether the presented proof is a complete correct proof. Programmers are not given the same affordance.

I feel like the analogy would be "writing mathematical proofs without writing down any of the propositions" (And indeed, the Curry-Howard correspondence lends credence to this). Writing down types for programs is not just useful because the computer can check them, but also because it commits what is in one's mind.

What's more, type-checkers offer a lot more help in checking types than Coq does at proving mathematical propositions (There is a reason, after all, that one is an assistant, whereas the other is a checker), so, relatively speaking, writing a proof without Coq is not as hard as typing a program without a type-checker.

Not the case. The same argument does not apply because of the nature of mathematical, and to a certain extent scientific. All three--mathematics, science, and computing (programming)--are similar in that their primary currency is knowledge that can be concisely described and embodied in instruments (tools), either of which can then be used by others without too much of a concern for where that knowledge or instrument came from as long as there's a good instruction manual nearby. The knowledge and instruments are used to create more knowledge, which is embodied in more instruments, and the cycle continues on and on etc.

The difference between computing and mathematics is the form that the knowledge and the instruments take. In mathematics, the concepts you're dealing with (or inventing, since I'm not a mathematical realist) are very clean and they stack well. You also have virtually no instruments to speak of. As a mathematician, it's not too common that you reduce your theories to practice. That's something that's left to the lesser sciences, such as computing.

In computing, the relationship between between knowledge and instruments is that of identity. At the very least, the two are conflated in casual discussion. More concretely, the "knowledge" of computing is typically a model of some problem domain and the the instruments are software, which in turn manipulate the physical world (that's what your JavaScript is doing) in order to perform some task or measurement in service of solving some problem in your domain.

So in mathematics, you have no correspondence between knowledge and instruments to do deal with. In computing, that's all you're dealing with except people are only really interested in the knowledge as its embodiment in the instruments. Static typing ensures that some sliver of that knowledge is explicit and checked. It doesn't mean it corresponds to the thing in your brain, but it does ensure that whatever's written down is embodied in your code. Mathematicians have no such constraints to deal with. They would if the proofs that they wrote were formal proofs, but they're not. Most, if not all, mathematicians know this. Most programmers, though, don't.

> Static typing ensures that some sliver of that knowledge is explicit and checked.

No. Testing ensures that the knowledge is checked. As in: run experiments. Empirical evidence. Static typing only checks one set of assumptions against another set of assumptions. Don't get me wrong, this is better than nothing. But the only real check is actually running the code, getting empirical evidence.

In every other engineering discipline, math is seen as a tool, simulations are cost saving measure because running experiments for everything is too expensive. Only in the discipline where gathering empirical evidence is actually generally cheaper than trying to prove things (with mostly dubious value) is there this odd notion that using math is superior to running the experiment.

If flying planes or running wind tunnel tests were as quick and cheap as running computer simulations, there would be no more computer simulations in aviation.

Compare Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."

First,

> some sliver

Second, I for the most part agree with you in the ways that are relevant to the point you're trying to make. However, the knowledge/tool distinction is a vague (in that they may fall on a spectrum) and ambiguous (both words tend to be moving targets), which is why I chose the term instrument instead. Mathematics is a tool only in the sense that it is knowledge that is applied towards some benefit, e.g., efficiency. Also,

> Compare Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."

This is again "proof" in the day-to-day mathematical sense of a convincing argument, not in the formal sense for writing down an expression per line such that each line can be logically deduced from some preceding lines through the the use of axioms. A type checker is literally a search procedure through the space of derivation trees to find a formal proof that this term has this type.

Type checking is a conservative analysis, and the type correctness of a program is undecidable. But you can still rely on the knowledge generated by your type checker without having to run your program. Among other things, this allows you to optimize your program automatically.

> "proof" in the day-to-day mathematical sense of a convincing argument

IIRC, that is the most that a so-called "proof" can ever be. I remember reading Carl Friedrich von Weizsäcker's "Aufbau der Physik"[1] in my younger years, and being somewhat flabbergasted when he starts by justifying classical logic, which he needs to do because later he talks about quantum logic, which is different.

Up to that point, it had never occurred to me to justify logic empirically, but now I can't imagine naively accepting it. That means that empirical evidence always trumps. Everything. If we find logical rules that we assume violated in the real world, we have to deal with it, not deny reality. Just like we had to accept that other aspects of the world we held as self-evident were not just theoretically contingent, but actually turned out not to be true.

> not in the formal sense for writing down an expression per line

> such that each line can be logically deduced from some preceding

> lines through the the use of axioms.

Hmm...that's how we always did (simple) mathematical proofs: line-by-line, with axioms or theorems justifying the transformation from line to line. Last time I checked, so-called "machine-proofs" are definitely seen as different by mathematicians, yes, but they are less well-respected, not more so. Has this changed?

[1] http://www.amazon.de/Aufbau-Physik-Carl-Friedrich-Weizsäcker...

Actually, empirical observation depends on the correctness of basic logic, which must therefore precede it. You can't do experiments without having a logical framework that allows you to interpret their results. You can certainly find people who've convinced themselves that they need to empirically check math. i.e. check that 30x100 = 3x1000 by rearranging beans on their kitchen floor. I wouldn't hire anyone who did that to paint my bathroom, though.

That's the fallacy of uncritical rationalism. See Popper.

I prove mathematical properties purely for the sake of proving them. The fact that they have any bearing on the real world is a mildly interesting diversion. Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof. Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite.

> I prove mathematical properties purely for the sake of proving them

Good for you. I also think pure maths can be a fun diversion.

> The fact that they have any bearing on the real world is a mildly interesting diversion.

Well, computer "science" is primarily an engineering discipline. It is therefore primarily, if not entirely, about having bearing on the real world. (And even if it were a "science", which it largely isn't, that would still be the case).

> Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof.

Given this frame of reference, your proof is of no relevance to software, which was exactly my point: yes, you can do these proofs, but they are largely irrelevant, and even if relevant always subsidiary to empirical evidence.

> Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite.

How do you know that while these proofs reference the infinite, they are actually applicable to the infinite? The answer is: you don't and you can't. You can only assume that the proof mechanisms you use actually do not break down. Now I am certainly convinced (= I believe) that induction will continue to work for all N if I prove 1 and N -> N+1, but I have only empirical evidence for small N to justify that belief. And if we found an M where it didn't, what then?

And of course, there always have been (and probably always will be) "proofs" that were later shown not to be correct, just like physical "laws" that turned out not to be laws. All knowledge is contingent, especially all-quantified knowledge.

And I have to admit that I find the naive/rigid belief (it is no more than that) in the absolute power of proofs...charming :-)

> Well, computer "science" is primarily an engineering discipline.

I would say that software engineering was the engineering discipline, and computer science a mathematical discipline.

My point was that the proof itself is not subsidiary to empirical evidence, only its application is, and in my eyes, there is merit in the proof, free from its application to the "real world", for example as a lemma to another proof. Consider it a form of separation of concerns: whilst I prove a theorem, I am not concerned with how it mirrors the observable world, but in order to apply it, of course I must ensure that its assumptions can be reliably observed. In this way, our "beliefs" are limited and do not taint the logic of the proof itself.

> How do you know that while these proofs reference the infinite, they are actually applicable to the infinite?

Which brings us to your next point: I do not know, I simply believe it to be true because it is convenient to do so. My point is that this belief or its refutation does not affect the worthiness of the proof, only that of its application.

I actually do not believe in the absolute power of proof, I don't think it is something you can get away with believing once presented with all the facts. I hope I've explained myself better in this comment though: I don't think our views are as antipodal as it first seemed.

But testing ensures no such thing, considering that comprehensive testing across the entire space of possible inputs for a unit is infeasible in most cases. Part of the usefulness of static typing is to prevent us from having to negotiate that state space explosion head on by a priori ruling out vast swaths of potential inputs.

I think static typing and testing are much more complementary than you're giving them credit for.

> But testing ensures no such thing

Yes it does. Empirically.

>considering that comprehensive testing across the entire space of possible inputs for a unit is infeasible in most cases

Fortunately, it is also not necessary, as numerous studies have found.

>I think static typing and testing are much more complementary than you're giving them credit for.

I totally agree that they are complementary. I find static typing to be most useful as checked documentation (for which, unlike the safety aspects, there is actual empirical evidence). Also, it makes various optimizations easy/cheap/predictable, which I find highly valuable.

Finally, it does help a little bit with correctness, though far less than what many people claim.

However, it also has costs that are not insignificant, in slowing down exploratory programming, compile-time costs, brittleness of designs and often code expansion / productivity.

More importantly, it appears to harm compositionality/reuse, at least at our current level of understanding. Both Unix Pipes and Filters and the Web, arguably the most successful reuse mechanisms in the history of software, are dynamically and somewhat loosely typed. In addition, personal computing was invented in around 20KLOC using Smalltalk, a dynamically typed OO language.

> > But testing ensures no such thing

> Yes it does. Empirically.

Your claim was "Testing ensures that the knowledge is checked." And, yes, testing ensures that the knowledge is checked - by the test.

mrbrowning's claim is that "Static typing ensures that some sliver of that knowledge is explicit and checked." That's also true (despite your reply of "No"). And note mrbrowning's use of the word "explicit". Type knowledge is more explicit than a test. It ensures that this data structure is an instance of the specified type. A test proves that in this set of circumstances this data structure behaves the way we expect, which is a weaker proof.

> It ensures that this data structure is an instance of the specified type.

But downcasts are unsafe.

> >considering that comprehensive testing across the entire space of possible inputs for a unit is infeasible in most cases > > Fortunately, it is also not necessary, as numerous studies have found.

If you know something about how some function or module works and you check the right corner cases, the only way a bug could be hiding in some of the other input combinations is if it were deliberately planted in the form of extra code, like "if the inputs are specifically x, y and z, then misbehave such and such".

For instance if we know that a 32 bit adder is made up of bunch of full adders, there are certain bit patterns we can use which tell us that the adders are working properly individually, and that they are hooked up together right. We don't have to test every A + B = C triplet, blackbox style.

> If the typing's in your head, then why not write

> it down for the benefit of others?

Because writing it down gets in the way while you are exploring.

To elaborate, some of the typing in your head is based on inaccurate domain assumptions that you're only going to find out about when you have some sort-of-working code to play with. It may not be worth writing down for others until you have something you know is going to last the week, or the day.

I like types, but jeez, the vast majority of web systems over the last decade were written in dynamic languages. You're trying to claim absolute proof for a very subjective choice, and it sounds silly.

They are not making a claim backed up by scientific evidence, but are rather stating a believable assumption that premises the work. PL is more about studying type theory than a it figuring out why it is useful (which dives into non science design anyways).

There is plenty of work in PL that covers why type theory is useful. Check out the classic paper by Philip Wadler called "Theorems for free" that covers some of the terrific benefits of parametric polymorphism.

There has also been a good amount of discussion generated by organizations such as Jane Street concerning the benefits of static typing and type inference in practice. Notably, the free documentation (that is completely coupled with the code) that you get when you design software that takes advantage of the type system.

Wadler's work is great, I've seen his talk on this many times (where he has the lambda shirt on), but it doesn't really cover "why it is useful" just "why it is inevitable".

Really, how would you scientifically show that parametric polymorphism is "useful?" "Useful" isn't a very empirical property, it isn't something you can reliably measure. In a scientific paper, you can't just say something like:

> When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck.

without justification! You have a citation, or perhaps it is something just accepted universally (which it isn't, of course). At the very least, you have to weaken the statement a bit...like:

> When it comes to maintaining and evolving these systems, the lack of explicit static typing is probably a bottleneck.

You can't talk in absolutes without evidence. But you know, the benefits of static typing are clear via anecdotal experience, we only really argue about whether or not the benefits balance out the disadvantages of static typing (and how those disadvantages can be mitigated, and if that is enough...). Again, in arguing about this we are firmly in the area of design and not science.

With regards to definitive benefit that's backed up by scientific study (rather than just anecdote)-- the UK's Ministry of Defense commissioned a study (IV&V) on the error rate of long-lived code comparing C code bases (static but not too strict) vs Ada (static and fairly strict). They presented their findings Ada-Europe 2001. There was about a 1 to 10 error ratio. They subset the Ada code into formally verified by SPARK code, and the error rate -- I kid you not -- dropped another order of magnitude. I'd assert based on that study static typing is definitively more reliable when your problem domain is set in stone [the operational semantics of flight, stock markets, power plants]. Of course that doesn't extend to any 'exploratory' computing where your domain isn't strictly (pardon the pun) defined.

RE: Parametric polymorphism being "useful" - a pedant like me would claim for it to be of use, one has to demonstrate one clear instance of PP being of use - trivial or not - after which PP gains the attribute "useful" ;)

Based on that study I would assert that tight static typing is more reliable than static typing that is full of holes.

It doesn't speak to strong dynamic versus strong static at all.

Speaking of holes, of course dynamic typing can have holes also: if an interpreter or compiler misses a type check, the consequences are that the wrong operation is applied to an object. The result is corruption, crashing.

The correctness and completeness of a type scheme is orthogonal to static versus dynamic.

This UK study is an anecdotal data point. It is not a controlled study, it is just comparing project A to project B that differ, among other thing in the languages they were written in (and probably much more!). It doesn't tell us very much for sure, but again adds to the anecdotes that can shape our judgement.

Of course, useful has a low bar, but it also has a magnitude (X is useful if it is used, it might not be very useful though).

Incidentally, stock markets have been big on Lisp and Smalltalk, two languages not known for static typing. It turns out that language X is always used in the stock market, where X is the latest hot language (Scala, Haskell, Clojure...).

Are these advanced theorem proving benefits obtainable with static typing alone, or does everything also have to be effect free ("purely funtional")?

Formally, everything has to be effect free; furthermore, everything has to be strict (the potential for any value to be "bottom" breaks things).

You can apply the same intuition and things mostly work, but there can be a few surprises.

These theorems are a huge part of the "if it compiles it must be correct" feeling that functional programming often provides.

The vast majority by count, perhaps, but if you took complexity of functionality into account I bet you'd find static languages (specifically Java and C#) take the win.

Google uses a lot C++.

They've done some Web things.

There can be an awful lot of dynamic typing hiding inside C++ code bases, by the way.

C++ has very good support for dynamic typing. You can make C++ look almost like Javascript, if you want.

C++ has polymorphism and templates.

If you have a lot of dynamic typing, you may want to look at C instead.

How on earth do you make C++ like JS? I'm no JavaScript programmer so correct me if I'm wrong, but I think this is legal: x = 5; x = "five"; How do you do that in C++? In C# they have the dynamic keyword, but C++? I guess boost has all sorts of magic, but... good support?

That can be easily made to work in C++95.

x can be of a smart pointer type (let's call it "var") which acts as reference to an anyobject class instance, which comes in varieties like string_anyobject, integer_anyobject and so on.

The smart pointer class can have a few assignment operators and conversion constructors for usage like var x = "lit"; or x = 5.

>I like types, but jeez, the vast majority of web systems over the last decade were written in dynamic languages

That's because the vast majority of web systems are glorified CRUD apps, the easiest kind of application one can make.

When it comes to the real hard backend parts (not just some queue handling of video conversion tasks for example, but things like search engines, social graph stores, programs for finding the cheapest air tickets, etc.), they're usually done in languages like Java, Scala, C++, Go, etc.

Heck, even as web front-ends got more evolved, people developed several typing systems to assist us (Flow, Typescript, etc) to solve that need, we got Go, Hack. Optional types are also landing in PHP and even in Python -- there's a consensus among many people about a need for such things. And Google wrote their more complex apps in a Java lib that could spat out Javascript IIRC (GWT).

As for the non CRUD apps, from PostgeSQL, Chrome, Office and Photoshop to Pixelmator, OmniPlan, Notepad++ and Scrivener, nobody writes those in dynamic languages (where nobody obviously means: some outliers being excepted). One might argue that those are few (they are not, they are merely "fewer" than web systems. Still millions of programmers work in that space), but the point remains: for developing harder apps, people opt to static languages.

> If the typing's in your head, then why not write it down for the benefit of others?

Because then it would be dumb typing with explicit declarations, not state-of-the-art inferred typing.

Also, you shouldn't write down or say everything that pops into your head. Doing so can have inconvenient consequences.

> > When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck.

> Assertion without evidence.

...

> The typing is in your head, where it doesn't get in the way.

That's fine, if it's you working on your code (and it hasn't been too long since you last worked on it). But if I wrote the code, now the types are in my head. Sure, it doesn't get in your way there, but it also gives you no protection against you doing something that completely violates the type assumptions of my code.

That's where the lack of static typing becomes a bottleneck to maintaining and evolving these systems - when the code was written multiple years ago by multiple parties other than yourself.

I heard the same argument from a certain breed of NoSQL fans (usually pushing MongoDB, in my experience...). "The datastore is schemaless! It's flexible! You can iterate quickly!"

I don't think those claims hold up in practice. In the real world, your data is never schemaless; it's just a question of how explicit you want to make the schema. With the added benefit that we have excellent tooling to help with, eg, migrating explicit schemas.

Old-style Java "double" type declarations suck. Stuff like this:

  BigNastyGenericThing<string,FooMonstrosityFactory<Tuple<int,string,double>>> _nastyFoobarObject = new BigNastyGenericThing<string,FooMonstrosityFactory<Tuple<int,string,double>>>();

That can die in a fire, for all kinds of reasons. I'm a huge fan of C#'s var keyword inference sugar, because it cuts the amount of type annotations in half. It also makes it a lot easier to mess around and iterate - there's less irrelevant syntax trash that's broken if you deliberately change the return type of a function or expression.

At least with a statically typed language, I can find all the things that I have to find if I break an interface - I have good tooling that uses the type system and can do semantic analysis and even track down when I'm hitting methods and properties through reflection. On dynamically-typed code, I have to grep the whole source-base, and filter out all the false positives.

I blame Javascript. If I could run C# in the browser and have real interfaces that understood the same assumptions instead of the hodge-podge of stringified data-binding and parsing...

It's interesting that "sound gradual typing" (i.e. static analysis with runtime type checks, AIUI) has supposedly caused large performance problems in some languages. Hack, Facebook's sound, gradually-typed dialect of PHP, doesn't seem to have this problem. And PHP itself, which doesn't do any static type checks itself (you must use a separate static analyser if you want that), only runtime ones, has had limited type checking for eleven years, without apparent performance problems.

Are these systems with performance issues doing something fundamentally different, or more complicated? Perhaps I am misunderstanding something.

The systems with performance issues are the sound ones!

Hack does not have a type soundness guarantee. The compiler statically checks your type annotations, but then generates untyped PHP code. If Hack-generated PHP interacts with PHP from 5 years ago, "type errors" are possible.

(I have to say "type errors" in quotes because a mismatch between originally-typed and originally-untyped PHP could result in any kind of error message, or no error at all!)

Systems like Typed Racket do type checking at runtime when interacting with untyped Racket code. These runtime checks are the performance problem, but they do accurately diagnose type errors.

> The compiler statically checks your type annotations, but then generates untyped PHP code. If Hack-generated PHP interacts with PHP from 5 years ago, "type errors" are possible.

That's not entirely true. Though some parts of Hack's annotations are not enforced by the runtime, if you say a function takes an int and pass it a float at runtime, it does throw an error from what I remember.

It's correct that Hack doesn't guarantee runtime soundness, though.

I love the work of the PLT group, and wish I had time to give this a better read right now. Barring that, I'll just waffle on related topics.

Having worked for about a decade in dynamically typed languages (mostly Racket, with a bit of Ruby and Python) and about the same in modern statically typed languages (mostly Scala, with a bit of O'Caml) I've come to believe that the use of types is more a cultural issue than a technology one at this point in time. Let me attempt to explain.

Working in Scala I've come to lean heavily on abstractions like applicatives and monads. When I design systems I now find I naturally break them down into these building blocks. For instance, a stream processing system I've been working on is an applicative functor (though I considered alternate designs that are Kleislis). Error handling is usually a monad. The meaning of the names doesn't matter. The important point I'm building systems by sticking together patterns. The patterns are different to OO design patterns as in the Gang-of-four book, but the core idea is the same.

When I was more into dynamic types I didn't lean on patterns so much. I tended to hand design the abstractions in each component, and they didn't always fit together so well as a result. Why the difference? I have a few thoughts.

Firstly, I've learned more with time. That's undeniable. But, more importantly, functional patterns have a different feel to OO patterns. They are much more precisely defined, with algebraic laws covering their interface. This makes interoperation easier as the interface and its properties are given. They are also a lot more general, in my experience, than OO patterns. Monads are famously general---so difficult to pin down that many people, including me at one time, struggle to see the point. This gives them great power, though.

Finally, FP patterns like monads are just about unusable without a (modern) static type system. I should know---I implemented a monadic library in Racket and debugging it was a total nightmare. I would find it easier now that I am more experienced with such things, but I believe the clarity enforced by the type checker was critical to building the mental model I now use.

This clarity of "thinking in types" is something I started to develop while using Racket, and I found as I went down that route more and more of my code became easily typeable with a classic ML style type system. I came to see a lot of my old code as rather goofy and ill thought out.

So this gets to what may the point (but I'm not sure; I'm kicking this from my head). Python, Ruby, and friends are culturally old languages. They were formed in a time (early 90s) when getting hold of PL research was hard. The look back to the OO languages of the 80s for inspiration, for the most part. It's also the case that statically typed FP wasn't really viable till about 2005 or so. That's when Scala came on the scene, and Haskell started to get enough libraries to make it usable. Also the techniques used in modern statically typed FP are surprisingly new. "The Essence of the Iterator Pattern" is 2009, for example, and techniques for monad composition is still an active area of research.

I think we're really seeing a cultural shift. I'm old enough to remember when OO was the new hotness. Java being fully OO was a big deal in 1997 when I first heard about it. The primarily OO languages now feel to me like they are the past. As FP knowledge becomes more widespread (and particularly as CS students graduate having learned about it) it's beginning to take the place of OO. When more people understand, say, algebraic data types I think we'll see less need for gradual typing. More people will have the mental model of statically typed FP and write code that doesn't need dynamic typing. On the flip side I don't know that a language community like Python's can ever entirely transition to a new paradigm.

Finally, I don't think FP is a silver bullet, though it does bring genuinely new and useful stuff to the table. Nor will we all switch to Haskell. It's the nature of the industry to build on the past, which is why languages like Scala with a strong backwards-compatibility story are successful. We're certain to take something from OO into the future, but I expect we'll be seeing more from statically typed FP and I'm not sure where gradual typing will find its home here.

I prefer mandatory static types + type inference. It is a productivity boost if you're allowed to skip entering type names for local vars. If you ever want to change anything meaningful in a large system, you better have meaningful compile-time checks. The only downside is longer build times, but tools are improving. Outside of legacy projects (Linus loves C! and fantastic library ecosystems for scripting languages) I don't see any future for languages without static typing + inference.

I smell a language problem when the cited problem is only the automatically added boolean checks.

Note that scheme (Racket) has explicit #true and #false values, and the type Boolean contains only those, while most other dynamic languages define booleans as nil or null or 0 as false (some even ""), and everything else as true. So you don't have to add type checks for a sound system, only a NULL/nil check, which is done in the op, and does not needed to be added for each argument or return value.

So it's only a problem for soundly typed scheme and some other obscure languages with explicit booleans, such as my potion, but not for most other dynamic languages, which have the NULL checks in the op already. Only very few specialized ops which permit no NULL args need this check.

I smell a typical Felleisen. He hates types.

"We find that Typed Racket’s cost of soundness is not tolerable. If applying our method to other gradual type system implementations yields similar results, then sound gradual typing is dead."

While some of the data is surprising (22x average slowdown for TypeScript dropping to 6.5% overhead when fully typed) the paper ignores the reason why people kicked and screamed for the functionality to begin with. It had nothing to do with run-time performance.

Obviously the tools will improve and you can always strip out the annotations if performance is an issue.

Reticulated Python is still an order of magnitude faster than Ruby, so obviously performance doesn't render a technology "dead."

> the paper ignores the reason why people kicked and screamed for the functionality to begin with

No it doesn't. The explicitly talk about this in section 7: "The acceptance of Typed Racket in the commercial and open-source Racket community suggests that (some) programmers find a way around the performance bottlenecks of sound gradual typing."

> Reticulated Python is still an order of magnitude faster than Ruby

Are you suggesting that a slower variant of Python is ten times faster than Ruby? That doesn't match my experience. For what it's worth, Ruby outperforms Python in some benchmarks: http://benchmarksgame.alioth.debian.org/u64q/ruby.html

Looking at the first benchmark in the list you gave, just in-lining eval_A in the Python code (as the Ruby code does) makes the Python code competitive with the Ruby.

As usual, don't trust the Benchmarks Game; it's not nearly well enough controlled to be a useful data point.

(I do agree with your main point, though. CPython ain't that fast.)

As usual, don't trust Joshua Landau: without in-lining eval-A the Ruby code only slows from 102secs to 137secs.

As usual, Joshua -- Do the ordinary thing and report specific programs that you think should not be allowed.

For those not aware, igouy maintains the Benchmarks Game.

Nothing hidden about that --

http://benchmarksgame.alioth.debian.org/sometimes-people-jus...

How to report specific programs that you think should not be allowed --

http://benchmarksgame.alioth.debian.org/play.html#invalid

Are you referring to this paper? http://wphomes.soic.indiana.edu/jsiek/files/2014/08/retic-py...

As referenced in the paper itself, section 6.1.

For those who have not looked at the referenced paper, the last section is -- "6. Conclusions"

"…Reticulated programs perform far worse than their unchecked Python implementation…"

p10 "Design and Evaluation of Gradual Typing for Python"

And I would argue that _use-site checking_ is the easiest and obviously the slowest method to attain the stated goal. Python is already slow, this is just going to make things silly.

Using the same inference methods as Shedskin [0] along with type annotations, functional tests and property based testing can get both correctness and performance in a gradual layered manner.

This paper doesn't prove that gradual typing is broken, it shows that _use-site checking_ happens to be slow for the version of Python that they used (PyPy could very well elide the checks).

[0]

Shedskin Thesis http://mark.dufour.googlepages.com/shedskin.pdf

Iterative Flow Analysis by Plevyak http://plevyak.com/ifa-submit.pdf

Agesen's Cartesian Product http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.88....

My point was simply that there is no section 6.1 in that paper, and what is in the paper does not support `tacos` claim ;-)

I'm referring to section 6.1 of the original paper which very much does exist (PDF page 11).

Not that the Ruby vs Python detour hasn't been amusing, but my core argument can and should have been better stated as: debug builds are slower than release builds and people still use them. Therefore this technology is not dead.

I see, by "in the paper itself" and "the original paper" you mean "Is Sound Gradual Typing Dead? [pdf] (neu.edu)" not the paper `sitkack` referenced.

Same problem in section 6.1 -- " “Reticulated programs perform far worse than their unchecked Python implementations” -- and nothing to support your claim that "Reticulated Python is still an order of magnitude faster than Ruby".

Reply on news.ycombinator.com