Elixir Wizards is an interview-format podcast, focused on engineers who use the Elixir programming language. Initially launched in early 2019, each season focuses on a specific topic or topics, with each interview focusing on the guest's experience and opinions on the topic. Elixir Wizards is hosted by Eric Oestrich and Sundi Myint of SmartLogic, a dev shop that’s been building custom software since 2005 and running Elixir applications in production since 2015. Learn more about how SmartLogic uses Phoenix and Elixir. (https://smartlogic.io/phoenix-and-elixir?utm_source=podcast)
José Valim, Guillaume Duboc, and Giuseppe Castagna on the Future of Types in Elixir
It’s the Season 10 finale of the Elixir Wizards podcast! José Valim, Guillaume Duboc, and Giuseppe Castagna join Wizards Owen Bickford and Dan Ivovich to dive into the prospect of types in the Elixir programming language! They break down their research on set-theoretical typing and highlight their goal of creating a type system that supports as many Elixir idioms as possible while balancing simplicity and pragmatism.
José, Guillaume, and Giuseppe talk about what initially sparked this project, the challenges in bringing types to Elixir, and the benefits that the Elixir community can expect from this exciting work. Guillaume's formalization and Giuseppe's "cutting-edge research" balance José's pragmatism and "Guardian of Orthodoxy" role. Decades of theory meet the needs of a living language, with open challenges like multi-process typing ahead. They come together with a shared joy of problem-solving that will accelerate Elixir's continued growth.
Key Topics Discussed in this Episode:
- Adding type safety to Elixir through set theoretical typing
- How the team chose a type system that supports as many Elixir idioms as possible
- Balancing simplicity and pragmatism in type system design
- Addressing challenges like typing maps, pattern matching, and guards
- The tradeoffs between Dialyzer and making types part of the core language
- Advantages of typing for catching bugs, documentation, and tooling
- The differences between typing in the Gleam programming language vs. Elixir
- The possibility of type inference in a set-theoretic type system
- The history and development of set-theoretic types over 20 years
- Gradual typing techniques for integrating typed and untyped code
- How José and Giuseppe initially connected through research papers
- Using types as a form of "mechanized documentation"
- The risks and tradeoffs of choosing syntax
- Cheers to another decade of Elixir!
- A big thanks to this season’s guests and all the listeners!
Links and Resources Mentioned in this Episode:
Bringing Types to Elixir | Guillaume Duboc & Giuseppe Castagna | ElixirConf EU 2023
Keynote: Celebrating the 10 Years of Elixir | José Valim | ElixirConf EU 2022
OCaml industrial-strength functional programming https://ocaml.org/
ℂDuce: a language for transformation of XML documents http://www.cduce.org/
Ballerina coding language https://ballerina.io/
Luau coding language https://luau-lang.org/
Gleam type language https://gleam.run/
"The Design Principles of the Elixir Type System" by G. Castagna, G. Duboc, and J. Valim
"A Gradual Type System for Elixir" by M. Cassola, A. Talagorria, A. Pardo, and M. Viera
Polymorphic Functions with Set-Theoretic Types https://www.irif.fr/~gc/papers/polydeuces-part1.pdf
"A reckless introduction to Hindley-Milner type inference"
Special Guest: José Valim.