[sparkie]

> I don’t understand why…

Because dynamic typing has its own advantages, which are worthy of experimentation even if you perceive absence of static typing as a weakness.

Gradual typing can offer us the benefits of both worlds.

> inferred typing is nearly as easy to use while being more robust.

Implementing type inference can be fairly trivial if your types are all disjoint. Hindley-Milner type inference is well studied and there's plenty of literature.

But as soon as you introduce subtyping, the traditional methods are not sufficient. It's only in the past decade that good solutions have been discovered, notably Dolan & Mycroft's MLsub[1], based on Dolan's Algebriac Subtyping thesis[2], and Parreaux & Chau's MLstruct[3], which uses a boolean algebra approach[4]. Type inference with subtyping is not a solved problem - these developments are big steps forward, but there are still open problems under research.

Subtyping doesn't imply object-oriented. Structural typing (ie "static duck typing") is a form of subtyping.

[1]:https://github.com/stedolan/mlsub

[2]:https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/the...

[3]:https://github.com/hkust-taco/mlstruct

[4]:https://dl.acm.org/doi/pdf/10.1145/3563304

[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