Introduction

An article titled “What to Know Before Debating Type Systems” (capitalization fixed) appeared in one of my search results a while back, though I can’t remember what the search was.

Needless to say, as a programming language nerd, I was interested, but I will spare you the boring details.

What does matter, though is this quote near the end:

The battleground on which this is fought out is framed by eight questions, four for each side.

In the quote above, “this” means the debate between static type systems and dynamic type systems, and here are the eight questions:

1. For what interesting properties of programs can we build static type systems?
2. How close can we bring those type systems to the unattainable ideal of never rejecting a correct program?
3. How easy can it be made to program in a language with such a static type system?
4. What is the cost associated with accidentally rejecting a correct computer program?
5. For what interesting properties of programs can we build test suites via dynamic typing?
6. How close can we bring those test suites to the unattainable ideal of never accepting a broken program?
7. How easy can it be made to write and execute test suites for programs?
8. What is the cost associated with accidentally accepting an incorrect computer program?

I want to focus on those eight questions in the context of my programming language Yao, but let’s start with type systems in general.

Static vs Dynamic

Before I answer the questions, I would like to edit and reorder them:

1. For what interesting properties of programs can we build static type systems, and for what interesting properties of programs can we build test suites via dynamic typing? (What Can Be Checked?)
2. What is the cost associated with accidentally rejecting a correct computer program, and what is the cost associated with accidentally accepting an incorrect computer program? (Costs of Failures)
3. How easy can it be made to program in a language with such a static type system, and how easy can it be made to write and execute test suites for programs? (Ease of Use)
4. How close can we bring those type systems to the unattainable ideal of never rejecting a correct program, and how close can we bring test suites to the unattainable ideal of never accepting a broken program? (Approaching Ideals)

What Can Be Checked?

For what interesting properties of programs can we build static type systems, and for what interesting properties of programs can we build test suites via dynamic typing?

The answer to the first question for static typing is easy: we can build static type systems to check any and all interesting properties of programs that can be checked efficiently by computers.

For dynamic typing, it is also easy: we can build test suites to test anything about a program.

Those answers are a little too close, so we need to dive into details.

With the advent of “safe” languages, the number and types of interesting properties increased dramatically, though many of the checks are still at runtime. Static program analysis has likewise moved many of those properties into the realm that static type systems may be able to reach.

That said, there are bugs that you can test that you cannot use type systems to check for, such as a bug that causes bc to add two numbers incorrectly.

That said, while tests can test more things than static type systems, tests cannot prove the elimination of bugs like static typing can. As Edgar Dijkstra said,

Program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence.

— Edgar Dijkstra, The Humble Programmer (1972)

In other words, testing can test more, but prove less.

Subjectively, I think that static type systems and dynamic type systems are equal in this area, so I will give them each half a point.

Costs of Failures

What is the cost associated with accidentally rejecting a correct computer program, and what is the cost associated with accidentally accepting an incorrect computer program?

Now we know that both static typing and dynamic typing will fail, but in different ways. What are the costs of failures?

First of all, what is failure for each? For static typing, it is rejecting a correct program by not even letting compile or run. For dynamic typing, it is allowing an incorrect program to run.

Obviously, the cost of failures for dynamic typing, allowing a bad program to run, can be everything from benign to catastrophic and can have real world consequences. This is not good.

But for static typing, I would argue that the cost is within a rounding error of 0, for several reasons.

First, there can be more than one correct program that does a particular thing. That has actually been proven with the Structured Program Theorem, which says that every sequential program can be written in a structured programming style and still be equivalent to one that isn’t. I also believe that structured concurrency will do the same for concurrent programs.

But that fact alone doesn’t matter without the second import fact: structured sequential and concurrent programs are easier to prove properties about. This means that a static type checker can prove more about a program if it is written in a structured style.

Don’t believe me? Rust’s borrow checker is only possible because of structured programming, and it is technically a static type checker.

I firmly believe that as we work harder to structure our programs properly, static type checking will be able to prove more and more, and since any program for which static type checking cannot prove many interesting properties can be converted into a program which can, static type checking will not necessarily reject any correct programs, provided they are written well.

And we know how to write them well. For the most part.

So when a static type checker rejects a program, it can be rewritten, or it was buggy anyway. This means that the program was poorly written, or it had bugs; static type checking will never allow a program with a bug that the static type checker can check for, which in turn means that the bugs never happen.

Therefore, the cost is within a rounding error of 0.

To score this one, it is obvious that static type checking gets a point. However, the consequences of incomplete testing makes me want to take a lot of points away from dynamic typing and give them all to static typing. That said, I will restrain myself by giving static typing a point and then taking a point away from dynamic typing and giving it to static typing.

Ease of Use

How easy can it be made to program in a language with such a static type system, and how easy can it be made to write and execute test suites for programs?

The answer for dynamic type systems is a bit complicated. On one hand, yes, it’s easy to write tests for a dynamic type system. On the other, you have to write a lot more tests just to cover the same things that you get from static typing, and when you already cannot test everything, it just means either you work more or you test less.

In one sentence, the answer for dynamic typing is that testing is easy but thorough testing is impossible.

For static type systems, the answer is that the static type system is as easy to use as it is flexible. By “flexible,” I do not mean weak or unsound; I mean adaptable.

The number one way static type systems are made adaptable is through statically checking behavior rather than types themselves. This is known as duck typing, and it is implemented best, in my opinion, in the Go programming language using interfaces.

The gist is that if something can do particular things, meaning that it has certain methods defined by an interface, it can be converted to that interface, and its new type is the interface. This means that several very distinct types can act like they are the same type.

With that in mind, let’s do a thought experiment.

In dynamic typing, we know that every type can be passed around everywhere that any other type can be passed around; the difference between the types comes when the program has to use the data in an object. When that happens, it has to check the type. When it does that, it raises an error if the type is wrong, but otherwise, it grabs the data and uses it.

Is there some way we could simulate that with interfaces?

Well, no, we can’t because we can’t just return types. We can’t just treat types as first-class values.

Why not?

Um…no idea. Because no programming language that we know of does that?

Doesn’t Python?

Oh, yeah, it does. So I guess we could.

So can we implement dynamic typing as an interface?

Sure, we can. The interface, which we will call Any, just needs two methods:

1. type(): returns the type of the object underneath.
2. data(): returns a generic pointer to the data of the object underneath.

The generic pointer would have to be casted to the proper pointer type, but this could work.

So now we have a way to implement the gist of dynamic typing using something that already exists, and we can do it in a static type system.

Does this result surprise you? It shouldn’t but it probably did, mostly because we are not taught the truth that dynamic languages are static languages. This thought experiment makes it easy to show that because it shows that every dynamic type is actually an instance of the Any interface.

However, wouldn’t that mean that dynamic typing and static typing are equivalent?

No. The reason for that is because dynamic typing puts off all type checking until runtime, and by the time the program is being run, if it is not free of bugs, there is a problem.

This means that static typing effectively can do what dynamic typing can do, but dynamic typing, while it technically can eliminate the same bugs that static typing can, it can only do so at the wrong time when the program is already running and such a bug will cause a crash.

This makes scoring easy: assuming a static type system with duck typing or some other method of flexibility, static typing is no doubt better. One point for static typing.

Approaching Ideals

How close can we bring those type systems to the unattainable ideal of never rejecting a correct program, and how close can we bring test suites to the unattainable ideal of never accepting a broken program?

Let’s look at dynamic typing first.

Do you remember when we said above that dynamic typing allows bugs through? That fact is made even worse by the fact that testing cannot eliminate bugs. A program can be well-tested, but it will still have bugs, which means that the bad consequences are not just possible, they are inevitable.

On the other hand, as shown above, static type checkers can allow for the exact same behavior that dynamic typing allows, when necessary.

So how close does static typing come to its ideal of never rejecting a correct program? It doesn’t come close either, but it doesn’t have to; remember that any unstructured program can be rewritten in a structured style, making it more amenable to static analysis, which means that, though static type checkers will reject many correct programs, we only care about ones that are written in a structured style.

But that’s not all. When a structured program would be rejected by a flexible static type checker, the part of the program that causes the rejection could be written in such a way to use the static type checker’s flexibility, and the problem effectively goes away.

Thus, in a way, it can be argued that if the static type checker is flexible enough, static typing will not reject any correct program.

I will score this as one point to static type checking, and because dynamic typing still makes bugs inevitable, I will take a point away and give it to static type checking.

Winner: static type systems. In fact, dynamic type systems are in the negative, which can only mean one thing: dynamic type systems are so bad that they should never be used.

Refining the Design

By now, many of the dynamic typing enthusiasts are probably wishing there was a comment section on this blog so they could tear me to pieces. I will try to proactively address some of their arguments.

You’re biased!

Perhaps, but when I started really thinking about type systems, I tried to see both sides. It took me doing the same thought experiment I laid out above to come to the conclusion I did.

You are completely forgetting the fact that static type systems require you to write down the type! Dynamic typing does not! Therefore, it is easier!

Well, what do you mean by “easier”? Do you mean “quicker to write”? Or do you mean “easier to make correct”? I think you probably mean the former, but I meant the latter.

That said, who says static type systems require writing down types? Last time I heard, Haskell can get away without most of them, and I am sure there are others.

But…you have a point. Maybe we can take care of that problem? I think we can…

Eliminating Type Annotations

Let’s do another thought experiment.

What if we made type annotations optional?

We can do that. Type inference exists.

Okay, but inferring every type is equivalent to solving the Halting Problem. That is why Haskell still needs some type annotations. So how are you going to make every type annotation optional?

Maybe we do something specific when an annotation doesn’t exist. Maybe we have the compiler automatically generate code to wrap the unannotated value in our Any interface.

That was easy. The end result is that whenever a type annotation doesn’t exist, the unannotated value acts like a dynamic type.

Not only does it mean that type annotations are optional, it also means that it is easy to enable dynamic typing in the static type system when it is wanted.

Oh, did I just create gradual typing? Yes, I think I did.

Formal Analysis with Dependent Types

But let’s go one step further: what if our type system was powerful enough to prove programs are correct without testing?

Yes, we can. The key is dependent types. There are powerful theorem provers, the tools that prove correctness, that use dependent types. One such example is Coq, which is powerful enough to prove anything about programs, except anything equivalent to the Halting Problem because nothing can prove that unless they restrict the kinds of programs we can write.

But how can we implement dependent types in a general-purpose programming language?

Easy: since dependent types are just types that have programs inside of them, we just need to make that possible, and since programs are just code that returns values, we need to make types first-class values.

Oh wait, didn’t we already make types first-class in order to enable gradual typing? Yep.

So not only do we have the ultimate flexible type system, we can even prove our programs correct using it!

Above, when I said that “formal analysis…lies outside of what people normally think of as type systems,” I wasn’t lying, but it turns out that type systems can, in fact, be a part of formal analysis.

Bringing It Together

The post Dynamic Languages Are Static Languages, linked earlier, contains this quote:

[M]any statically typed languages, particularly the ones widely in commercial use, do not have a sufficiently expressive type system to make it feasible to work dynamically (that is, with multiple classes of values) within a statically typed framework. This is an argument against bad languages, not an argument against type systems. The goal of (static, there is no other kind) type systems is precisely to provide the expressive power to capture all computational phenonema, including dynamic dispatch and dynamically extensible classification, within the rich framework of a static type discipline.

I hope you can see that the type system we have here is, in fact, as expressive as possible, and it should be “sufficiently expressive…to make it feasible to work dynamically.”

On top of that, we were able to create a system that would eliminate the need for testing by enabling proofs of correctness.

Thus, when all is said and done, a good static type system can go far beyond what even testing is capable of.

Yao’s Type System

You may have caught on by now, but I have just described the type system in Yao.

As you can see from my comparison of static typing versus dynamic typing, I firmly believe that static typing is better. However, there are some things for which dynamic typing is a better choice, and that is why it will exist.

On the flip side, with dependent types, we can carefully define all of our types such that a theorem prover could actually prove that our programs are correct.

That is the kind of power I want in a language, along with the kind of tools I need to ensure my software is correct.

Conclusion

If there is anything to take away from this, it is that a good static type system is more capable than dynamic type systems. We just haven’t seen that because we don’t have any good type systems yet.

My hope is that Yao will.