Skip to content
0:00 / 0:00

#elixir#gradual-typing#set-theoretic-types

ElixirConf 2023 - José Valim - The foundations of the Elixir type system

ElixirConf

13K subscribers • 28 videos on Hallway

YouTube
  • Recommended by 4 people: 3 on Hacker News and 1 in engineering communities.
  • Presented by José Valim, creator of Elixir

Advanced. Deep dive for people who know the field.

37K views3 years ago4 recommendations

Programming languagesElixir and ErlangLanguage design and type systemsFunctional programming

José Valim explains the design principles and mathematical foundations of Elixir's gradual type system, focusing on set-theoretic types.

Closing Keynote for ElixirConf US 2023. See related post and erratum: elixir-lang.org/blog/2023/09/20/strong-arrows-gradual-typing… Leave comments at: elixirforum.com/t/elixirconf-2023-jose-valim-the-foundations… ElixirConf.com

Why it's here

4 people recommend this

What people say. Recommended as a detailed and nuanced explanation of how Elixir's new gradual type system works.

Moments people linked to

u/arcanemachinedin r/elixir • Recommends

ElixirConf 2023 - José Valim - The foundations of the Elixir type system

gregorson Hacker News • Recommends

On “Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27”

If you're into watching talks, this will be well worth your time. ElixirConf 2023 - José Valim - The foundations of the Elixir type system link to this video

whalesaladon Hacker News • Recommends

On “Switching to Elixir”

static typing is a means to an end. if you can achieve the same end without static typing, good right? that is the goal of spec. the creator of the language has a fantastic talk on this link to this video

H12on Hacker News • Recommends

On “Elixir is now a gradually typed language”

My understanding is "yes, but only type errors that violate guards and pattern matching". Jose's elixirconf keynote this year did a great job providing details on how how this new type system works: link to this video

u/rogerfinin r/elixir • Mentions

On “Just started learning Elixir, with one sigh”

I picked it after years in C and Rust, so it was a different world to write even a single line of code without static typing. It was infact a similar feeling when I started Rust and fought its compiler in the beginning, and later fell in love. Similarly, it took me a while to get a hang of Elixir. Use specs, guards, doctests, to get a feel, this video helped me.

paweldudaon Hacker News • Mentions

On “Unpacking Elixir: Resilience”

Types in Elixir are on the roadmap 1 but I don't think there's concrete ETA For now you have typespecs and dialyzer that tries to infer types and detect incorrect assumptions in code but I found it cumbersome to work with. Testing in Elixir is first class so I prefer that for now. You get doctests (documentation that is also a runnable test), like in Python, which I find very useful when looking at some package source. 1 link to this video

rapindon Hacker News • Mentions

On “Koto Programming Language”

I'd keep an eye on Roc link Also, Elixir is working on gradual types, which is something I would keep an eye on. link link to this video

_accoon Hacker News • Mentions

On “Why Elixir? Common misconceptions”

It doesn't matter as much as you think. I believe this is in part due to how assertive most Elixir code tends to be. 1 These assertions not only aid the LSP and can cause compiler warnings/errors, they also help LLMs just like types do. Still, every release now contains new type system features. Next up is full type inference. 2 After that will be typed structs. 1 José Valim giving his balanced view on type systems: link to this video 2 link

aeonfoxon Hacker News • Mentions

On “Elixir v1.20 released: now a gradually typed language”

OP might be referring to Jose Valim's 2023 ElixirConf talk where he's explaining why Elixir should go down the path of types. He gives a lot more nuanced take than 'types are useless', which is more like 'types are less useful than people think in the context of Elixir development'. (Which makes sense because he's in the middle of implementing a type system for Elixir.) link to this video

mechanicumon Hacker News • Mentions

On “Elixir v1.20 released: now a gradually typed language”

Short answer: “a type system centered on the use of set-theoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations”. Long answer, well, there are blog posts0, the Design Principles of the Elixir Type System paper1 and related presentations2, 3, 4 that talk about it at length. Giuseppe Castagna’s site has many more related papers: link 0: link 1: link 2: link 3: link 4: link to this video

u/Sorc96in r/elixir • Mentions

On “Strong arrows: a new approach to gradual typing”

Jose explained this in his recent talk. Using `or` would be valid in this case, but less strict than possible. If A is the set of `integer() -> integer()` functions and B is the set of `float() -> float()` functions, then a function that can work with integers or floats has to be in the intersection of A and B.

u/pdgiddiein r/elixir • Mentions

On “What is the latest on static/gradual typing with Elixir?”

Here's a pretty in-depth presentation José made a few months ago: link to this video

u/lovebesin r/elixir • Mentions

On “Efficiency and speed in Elixir”

Type system will be coming real soon, and the fact that you're using a functional language with a robust pattern matching system negates for subsection of needs for types. Auto complete isn't as robust as the other languages, sure. But there's some enough to be helpful with language servers. Also it's erlang under the hood, which has been battle tested for the last 30+ years doing concurrency under the setting if network / telephone switching industry. If where you're getting at is that Elixir is a hobby language at best and not ready for production, or that developer happiness is gonna be hell because of lack of types or tooling, I'd have to say that is flat out an incorrect take.

u/bloodisbluein r/Clojure • Mentions

On “Why dynamic types though?”

I've found this talk by Jose Valim (creator of the Elixir programming language) about static types informative and just about everything he mentions applies just as much to Clojure. link to this video (timestamp is where he goes over the most common concerns he hears)
1View on Reddit