Interesting @lambda_conf talk showing how Dialyzer ('discrepancy analyzer') offers gradual typing for Erlang and Elixir: https://youtu.be/FXCMiQWnWu0
It's a neat type system: it uses 'success typing', (it assumes you're correct) and exotic features like ranges and non-empty lists!
miniblog.
Related Posts
Most of the gradual type systems I've seen are targetting existing languages: you want to interact with existing libraries that don't have type annotations.
Are there many greenfield languages with gradual types? It's a useful technique in other cases, such as refactoring.
The tradeoffs of type system design, and thinking about a gradual type checker for Elixir:
Back from #POPL! The Saturday tracks were well worth attending.
Ronald's discussion of gradual type safety vs soundness was my highlight: https://popl20.sigplan.org/details/wgt-2020-papers/5/Gradual-Typing-as-if-Types-Mattered
When talking about soundness, it's important to say exactly what issues you're handling, and the talk explored this.
