[zozbot234]

> Gradual typing can offer us the benefits of both worlds.

Gradual typing has much the same overhead as other kinds of dynamic typing. It's broadly appropriate as part of the interface between separately-developed software components, and not very much otherwise.

[sparkie]

Gradual typing is static typing augmented with a known static type `dynamic`, and some rules by which conversions to/from `dynamic` are statically checked, called consistency.

A program in a gradually typed language which does not use `dynamic` is fully statically checked and has no overheads. The overheads only appear when `dynamic` is used.

This is why it offers the best of both worlds. We get static typing everywhere where we're not using dynamic, and when we do use dynamic, we can basically use it however we want and have the benefits of dynamic typing, because from the static perspective, dynamic ~ dynamic, regardless of what the runtime type is.

The important innovation is that consistency (~) is not transitive - so it doesn't allow us to implicitly convert one type to another - only conversions to/from dynamic are implicit, and other conversions must be done explicitly.

Obviously, this provides an "escape hatch" from static typing where we do use it - we can get around some static type check by casting to/from dynamic explicitly, but this works out well in practice.

C# is an example of a gradually typed language since v4 which introduced `dynamic`.

Haskell is close , in that it has the type `Data.Dynamic`, but it doesn't support implicit conversions to/from it, which would be possible if it had a consistency rule. We have to do the conversions explicitly.

https://jsiek.github.io/home/WhatIsGradualTyping.html