Great link. Let’s break it down.

First of all, what is a gradual type system? A gradual type system is achieved by getting a static type system and adding the “dynamic” type to it. In other words, in a gradual type system, if you don’t use the dynamic type, you should be able to reap all benefits of a static type system.

So are gradual type systems more complex? Not in theory. But in practice, as they are applied to dynamic programming languages, type systems end-up being more complex because dynamic programming languages are more expressive. A static language, without gradual types, that wishes to incorporate all expressive power found in dynamic languages would end-up equally complex!

This is one of the points I mentioned in my keynote: often type systems are used to restrict the power of a programming language. However, do we really want to restrict the power of Elixir and Erlang? No, we don’t. Therefore I don’t agree with the implied causation from Richard’s talk. Even if Elixir was statically typed from day one, it would have a complex type system because we want all of the expressive power it offers.

The complexity of a type system therefore depends on the expressiveness and the guarantees it wants to provide. It is likely that the Rust type system is more complex than the one we are working on for Elixir, but it does provide a different set of guarantees and expressiveness.

Another point from the discussion is that gradually typed languages have reduced runtime performance but that doesn’t have to be the case. Remember, if you use a gradual type system, but not the dynamic type, it should behave as a static one. This could be an optimization path to be explored. The Static Python paper offer some explorations in this front. Our work on gradual type systems also introduces a novel approach to reduce the overhead between dynamic ↔ static while remaining sound. It is a pity though that the leading language for gradual types, which is TypeScript, cannot explore those routes as it transpiles to JS (otherwise we would likely have seen more advancements in this front).

Finally, it is worth remembering that gradual typing is a relative young discipline. For example, Richard mentions dynamic programming languages have features that were not meant to be statically typed. However, that’s a static (no pun intended) observation of the current status quo. There were features which were seen as dynamic or objected oriented in the past, until we were able to develop the theory necessary for them to become part of functional or statically typed languages. In fact, our work on the type system so far was exactly in researching and developing new theory to support all of existing Elixir features. It is not that Elixir is too dynamic, rather it takes on-going and exciting new work to type it. And it wouldn’t be surprising to see characteristics which are currently common to gradually typed languages (such as structural typing) to become more common on statically typed ones.

So overall: why dynamic languages? Because they are more expressive. Gradual type systems help formalize many of their features and provide red squiggly lines without affecting our expressive power. They are an argument in favor of dynamic languages, not against them.

Thank you for sharing @sundi and thank you for having us!

I have been live-streaming on Twitch and today livestream will be a Q&A session about types with myself and Guillaume Duboc (the PhD student working on a type system for Elixir). Join us today 22:00 CET / 16:00 ET / 13:00 PT at Twitch.

Bonus points if you listen to the episode and come back with additional questions! The stream will be recorded and available for 7 days.

Who knew a discussion about typing could be so fun? Thank you for joining us and for all of the hard work!