Set Theoretic Types in Elixir with José Valim
Summary
José Valim, creator of the Elixir programming language, joins hosts Dan Ivovich and Charles Suggs to discuss the ongoing development of Elixir’s new type system based on set theoretic types. He explains that the system is being built to provide static analysis and bug detection for existing Elixir code without requiring developers to add type annotations. The goal is to infer types automatically and catch potential errors during compilation.
Valim details the history of the project, including earlier attempts in 2018 that were abandoned due to performance issues and theoretical limitations. The current approach, developed in collaboration with researchers from CNRS and Giuseppe Castagna, has proven much more successful. The type system can now handle the vast majority of Elixir language constructs, with only a few features requiring adjustment or deprecation.
The discussion covers practical aspects of the implementation, including performance considerations (currently taking about 20 seconds to type 12,000 modules), the relationship with existing Dialyzer type specifications, and plans for future development. Valim emphasizes that the type system is designed to be backward compatible and won’t force developers to change their coding style unless they want to take advantage of more advanced typing features.
Looking ahead, Valim estimates that developer-facing type syntax and more advanced features like typed behaviors might be available around June 2026. For now, developers can benefit from the type system through compiler warnings that help catch bugs in existing code. The episode concludes with practical advice for developers testing Elixir 1.19 release candidates and reporting any confusing warnings or performance issues.
Recommendations
Projects
- NX — José mentions continuing some work on NX, Elixir’s numerical computing library.
- LiveView — Valim notes ongoing involvement with Phoenix LiveView for real-time web applications.
- LiveBook — He mentions working on LiveBook, Elixir’s interactive notebook system.
- TideWave — A project launched by Dashbit focusing on the AI side of things, mentioned as one of Valim’s recent projects.
Research
- CNRS collaboration — Valim discusses working with CNRS and researcher Giuseppe Castagna on developing the theoretical foundations for Elixir’s type system.
Topic Timeline
- 00:00:00 — Introduction and José Valim’s current work — The hosts introduce José Valim, creator of Elixir. Valim explains that most of his recent time has been devoted to working on Elixir’s type system, along with some involvement in NX, LiveView, LiveBook, and TideWave. He discusses what motivated him to pursue a type system for Elixir, citing both personal curiosity and community interest.
- 00:07:08 — Progress with set theoretic type approach — Valim discusses how the current set theoretic type approach is progressing much better than earlier attempts. He explains that the key metric is how much of the existing Elixir language the type system can support without requiring changes or deprecations. So far, only a few features have needed adjustment, with struct update syntax being a notable example that was initially deprecated but may be reinstated with improved semantics.
- 00:12:49 — Boundaries and capabilities of the type system — Valim explains the technical challenges of implementing a type system for Elixir, particularly around maps that serve both as records and dictionaries. He notes that the research team had to develop new theory to handle Elixir’s unique features. The type system currently handles most language constructs well, with behaviors being one area where they want to improve beyond current capabilities to provide more advanced interface definitions.
- 00:17:03 — Relationship with Dialyzer and tooling — The hosts ask about how the new type system interacts with Dialyzer. Valim explains that the goal is to eventually replace Dialyzer, as set theoretic types are more precise. He cautions against automatic conversion from Dialyzer type specs because they were written with different goals and precision levels. The new system aims for exact type definitions that capture full function behavior.
- 00:22:12 — Developer adoption and timeline — Valim advises developers that they don’t need to change their coding practices yet. The type system is currently focused on inference and will provide warnings automatically. He estimates that developer-facing type syntax and features might be available around June 2026. The system is designed so that developers who are happy with dynamic typing can continue without changes, while those who want stronger guarantees can opt in later.
- 00:33:42 — Current output and practical impact — Valim confirms that the current output from the type system is compiler warnings. Developers who use
--warnings-as-errorsin CI will see build failures when type issues are detected. He notes that the type system has already found bugs in projects like Phoenix, LiveView, and LiveBook, but emphasizes that types don’t replace the need for tests. - 00:41:37 — Developer requests and concluding advice — Valim provides practical advice for developers testing Elixir release candidates. He recommends using
mix compile --force --profile timeto measure compilation performance before and after upgrades. He asks developers to report any confusing warnings or performance issues, as these likely indicate bugs or areas where error messages need improvement.
Episode Info
- Podcast: Elixir Wizards
- Author: SmartLogic LLC
- Category: Technology Education How To
- Published: 2025-07-10T10:30:00Z
- Duration: 00:45:40
References
- URL PocketCasts: https://pocketcasts.com/podcast/722afb10-1b49-0137-f265-1d245fc5f9cf/episode/d4627034-96ea-41d2-9910-0fe93ef1c8f9/
- Episode UUID: d4627034-96ea-41d2-9910-0fe93ef1c8f9
Podcast Info
- Name: Elixir Wizards
- Type: episodic
- Site: http://podcast.smartlogic.io
- UUID: 722afb10-1b49-0137-f265-1d245fc5f9cf
Transcript
[00:00:00] Welcome to Elixir Wizards, a podcast brought to you by SmartLogic, a custom web and mobile
[00:00:16] development shop.
[00:00:17] This is season 14, enter the Elixirverse.
[00:00:21] Join us for conversations about Elixir’s interoperability with other languages, libraries, tools, and
[00:00:26] more.
[00:00:27] Hey, everyone.
[00:00:28] I’m Dan Ivovich, Director of Engineering at SmartLogic.
[00:00:31] And I’m Charles Suggs, Software Engineer at SmartLogic.
[00:00:35] And we’re your hosts today for season 14, episode 7.
[00:00:38] We’re joined by Jose Valin, the creator of Elixir Programming Language.
[00:00:43] Jose, welcome back to Elixir Wizards.
[00:00:45] It’s nice to have you.
[00:00:47] Thanks for having me.
[00:00:49] Great to have you back.
[00:00:51] Top of our mind out of the gate is types and where we are with that.
[00:00:54] I know we’re at 1.19 release candidate.
[00:00:56] But maybe before we dig into that, for anyone…
[00:00:58] For anyone who maybe doesn’t know who you are, which seems hard to believe, given the
[00:01:01] topic of the podcast.
[00:01:03] But, you know, what have you been up to recently and what’s new with you lately?
[00:01:07] Right.
[00:01:08] Yeah.
[00:01:08] So, you know, I am Jose, Brazilian, living in Poland, allegedly created Elixir.
[00:01:17] And what I’ve been doing for the last more than a year, for sure, I think most of my
[00:01:24] time actually goes towards the type system, working on the type system.
[00:01:28] Which is good.
[00:01:29] It’s going to be one of the topics of today.
[00:01:31] I am involved with a few other things, like a few other projects here and there.
[00:01:36] Right.
[00:01:37] In the last year, I did a little bit of NX, still do a little bit of LiveView and LiveBook as well.
[00:01:43] And recently, one of the projects that we launched as part of Dashbit, something called TideWave,
[00:01:49] looking more at the AI side of things.
[00:01:53] So there is a little bit of work, you know, machine learning, web and stuff, but the main focus is for sure
[00:01:58] the type system.
[00:02:00] What’s driving you to devote so much energy into introducing a type system into Elixir?
[00:02:06] Is this largely driven by people in the larger community?
[00:02:09] Is this something you always kind of were thinking you might want to introduce into the language?
[00:02:15] It’s a little bit of everything, to be honest.
[00:02:18] I would say I am like generally a curious person.
[00:02:21] That’s why I end up doing a little bit of NX, a little bit of Phoenix.
[00:02:27] Because for me, like, that’s the exciting part about being a programmer is, you know, being able to learn all those different things, the different domains.
[00:02:36] There’s always something new for you to learn and type systems is something that I, it’s always a topic that I was interested on.
[00:02:46] Right.
[00:02:46] But I think like similar to machine learning, it’s like, look, we can find machine learning interesting, but unless we know a good way of bringing machine learning to Elixir, that’s not going to happen.
[00:02:56] Right.
[00:02:57] That is going to be efficient.
[00:02:58] That is going to be part of the language.
[00:03:01] It doesn’t make sense to add, right?
[00:03:02] Like I’m not going to work on something that feels that is, it doesn’t, something that ultimately I would have to tell people, oh, you cannot use it because it’s too slow or because it’s too clunky.
[00:03:13] Right.
[00:03:14] So with the type system, I actually did like a proof of concept and I even have like this joke in Elixir Call, I think it was like around 2018 where I actually explored the
[00:03:26] building.
[00:03:27] Yeah.
[00:03:27] Type system, like reading papers, exploring the literature, like by myself for Elixir.
[00:03:33] And, you know, I worked on it, I think for about like six months.
[00:03:37] So this was before the current announcement.
[00:03:39] Right.
[00:03:40] And then, you know, I was running into some limitations and it was really funny because I was implementing something called intersection types, a very particular implementation of intersection types on the Hitler Mino type system.
[00:03:53] And, and then I was having, I was running into like very.
[00:03:57] Like bad performance.
[00:03:59] And then I went to talk to John Hughes, which is a very known professor in the field of functional programming.
[00:04:05] And then he’s like, oh, it’s very known that this particular implementation is very slow.
[00:04:10] Right.
[00:04:11] And then I was like, I mean, none of the papers said it is like, yeah, like the papers, they are on the theoretical part, but when it comes to the implementation, it’s kind of known.
[00:04:19] And then I went like to Elixir Call and then my joke was I have two news to tell everybody.
[00:04:25] Right.
[00:04:26] And then my.
[00:04:27] And the first new was we started working on a type system for Elixir and then like half of the room started clapping, like very excited.
[00:04:35] And then the second news is that we stopped working on a type system for Elixir exactly because we couldn’t figure out how to do it.
[00:04:43] And even before like the current iteration, even before we announced it to the community, we work on it for like almost a year, like just kind of trying to see, like, look, before we go and tell the community.
[00:04:56] Right.
[00:04:56] We are doing this.
[00:04:58] Are we sure that this is something that is going to feel a part of the language is not going to be like, you know, like a subset of Elixir or it’s not going to feel like you’re writing something completely different.
[00:05:12] So, so yeah, like the interest has always been there and this was a matter of like finding the right theory and the right people.
[00:05:19] So we have been working with the CNRS, with Giuseppe Castagna, which is a very known researcher in this area.
[00:05:26] We have a PhD.
[00:05:26] So the interest was there, but we had to find like the, the right background and the right people to work on it.
[00:05:34] And then we put that together with the fact that that’s something the community has, like there was a very vocal part of the community and even non-vocal, like say, look, this would be great for, this is something that we are looking, that we are looking for.
[00:05:48] I remember asking, I think, Electrical Europe, like 2021 or so, like who here would like.
[00:05:56] I remember asking, I think, Electrical Europe, like who here would like.
[00:05:57] I remember asking, I think, Electrical Europe, like who here would like.
[00:05:57] More like static analyzes on the Elixir code base.
[00:06:00] And it was more than half of the room for sure.
[00:06:04] So it was clear that that’s something the community was interested in.
[00:06:09] Right.
[00:06:09] But it’s also important to say it’s not because the community wanted, right.
[00:06:12] Because I think like when it comes to type system, I hear so many things that are just clearly not true and overblown expectations, be it for Elixir or even other languages.
[00:06:21] Like people saying like, hey, a type system would catch like 90% of my buzz.
[00:06:26] Right.
[00:06:26] Like, I think, I think those statistics, you know, like, I feel like the web should, you know, like on Wikipedia, you have like citation needed.
[00:06:37] I feel like this should be like a feature on all of the forums, discussion forums.
[00:06:42] It should just be able to say, hey, citation needed on this, right.
[00:06:45] Like, you know, I need a little bit more concrete evidence on this, but, but yeah, so it’s a balance of all those things.
[00:06:52] If the interest is the community asking is being able to find.
[00:06:56] The right people is being able to explain what it is and what we are going to get from it.
[00:07:01] So all those things, they have to go together.
[00:07:04] So then thinking about this, like set theoretic type approach, right.
[00:07:08] Where you’re pretty far into it now, I guess like kind of at a high level, how’s it going?
[00:07:12] You know, are you happy with this approach?
[00:07:15] Do you think maybe a different theory would have panned out better or is it going how you would have hoped?
[00:07:20] It’s going pretty well and way ahead of whatever I tried in 2018.
[00:07:26] Like 10 times ahead, citation needed, but sure, but yeah, we are quite ahead to the point that it’s part of the language, right.
[00:07:36] And I think the thing is that we have an existing language and we have the idioms, the thing, the code that we wrote.
[00:07:44] So the big question is how much of the language can this type system support?
[00:07:50] Because it’s the type system does not support it.
[00:07:53] We have two options.
[00:07:55] We will have to say, oh, this is dynamic code.
[00:07:58] We don’t really understand it, right.
[00:08:00] Or we say the type system then just slap dynamic on it.
[00:08:04] Then it’s always going to be dynamic or we have to say, oh, this is a feature that we no longer support.
[00:08:10] This can no longer be part of the language because it’s dynamic and we want to mostly have features that the type system can understand.
[00:08:18] So we have been working on it, like adding it to a leaflet.
[00:08:21] The theory has been happening before, but the process is still going on.
[00:08:25] So adding it to a leaflet is going to be three releases at this point, which is 18 months.
[00:08:30] And the amount of things where we say, look, this doesn’t work with the type system as well as we wanted.
[00:08:37] They are very few still, right.
[00:08:39] And with 1.19, we have basically type like the huge majority of the language constructs.
[00:08:48] So that’s good.
[00:08:49] That’s a very positive indicator.
[00:08:52] And for me, that’s like, it’s the biggest metric.
[00:08:55] that we should tackle right now.
[00:08:57] Because just to recap, like the type system,
[00:08:59] it’s behind the scenes.
[00:09:01] We users are not adding type signatures.
[00:09:04] The whole purpose of the work we’re doing right now
[00:09:06] is that we are typing the language.
[00:09:09] We are trying to find the bugs for you for free.
[00:09:12] You don’t have to change your code.
[00:09:13] We are just going to go there,
[00:09:14] type your program and find potential bugs.
[00:09:18] So that’s the metric.
[00:09:19] Like, are we going to have like false positives,
[00:09:22] warnings that should not be there?
[00:09:24] Are we going to have to remove things from the language?
[00:09:27] And I think the only notable thing that is kind of saying,
[00:09:32] oh, this does not really work with the type system.
[00:09:36] It’s a deprecation that we introduce in Elixir 1.19,
[00:09:41] which is struct update.
[00:09:44] So if you use the struct update syntax for update struct,
[00:09:49] in Elixir 1.19, the first release candidate, which is rc0,
[00:09:54] it emits a deprecation warning.
[00:09:56] But that, of course, that caused some discussion
[00:10:00] in the community.
[00:10:01] And through that discussions,
[00:10:02] we’re actually able to find a good semantic
[00:10:06] for that operation in the type system.
[00:10:08] So we are actually reverting the deprecation.
[00:10:11] We are converting to something more.
[00:10:13] But I think it’s a really interesting example of like,
[00:10:15] look, we have this construct.
[00:10:16] We have to tell what this construct means
[00:10:19] in a way that makes sense for everybody,
[00:10:21] that makes sense for existing Elixir developers,
[00:10:24] dynamic programmers, and static programs.
[00:10:27] And that was something that was very hard, but it was good.
[00:10:30] We put the deprecation out there.
[00:10:32] We got feedback.
[00:10:33] And they’re like, okay, now we have a semantic.
[00:10:35] So what we are doing is that the next Elixir rc,
[00:10:38] which I think is going to come next week,
[00:10:40] is not going to have the deprecation anymore.
[00:10:42] The deprecation is going to be slightly different.
[00:10:44] And then when 1.20, before we release the next version,
[00:10:51] I’m going to have another discussion with the community.
[00:10:53] Like, well,
[00:10:54] we upgraded our code bases.
[00:10:56] We see how this new feature looks like.
[00:10:59] Do we want to keep the struct update syntax or not?
[00:11:03] But I think it’s a very good example.
[00:11:05] And we are going,
[00:11:06] and I believe there is an issue in the Elixir repost story
[00:11:10] where we say features that will have to change
[00:11:13] because it’s not because they are incompatible with types.
[00:11:16] It’s just because they end up being poor.
[00:11:21] Like the way we implemented some things do not allow
[00:11:24] the type system to express the things we wanted clearly.
[00:11:27] But I think like right now we have two or three,
[00:11:30] three, two or three entries in the list, right?
[00:11:32] For all of the Elixir.
[00:11:34] So it’s going, it’s going pretty well.
[00:11:36] That’s I think that’s the digest for the metric
[00:11:39] that we set for ourselves.
[00:11:42] Yeah.
[00:11:42] I know like, you know, in our,
[00:11:45] however long we’ve been doing Elixir now a long time,
[00:11:47] the path of kind of upgrading version to version
[00:11:49] has always been, I think, delightfully not a big deal.
[00:11:52] right? Like years ago, I think when you were early on the podcast with us, we talked about like,
[00:11:56] well, you know, is there ever going to be a 2.0? Are we ever going to break anything in the
[00:11:59] language, right? And it’s like, you know, that list of things that could potentially break if
[00:12:03] you ever did that just has remained extremely short over, what, 12 years now? That’s really
[00:12:10] fantastic. And this idea, I think something that you said that I really want to maybe
[00:12:14] peel back a little bit more on is the idea of like, you’re not making a type system for the
[00:12:19] user to interact with, right? The developer isn’t typing their language out. You’re not
[00:12:23] adding, we’re not adding a lot, really anything, right? You’re inferring it. Yeah, sure. So maybe
[00:12:29] can we just talk a little bit more about like, okay, so set theoretic and the type system you’re
[00:12:34] doing, like, what can it do right now? What can’t it do? You know, because you mentioned a little
[00:12:40] abstractly, like, there are some things like the struct update. I don’t know, can you just talk a
[00:12:46] little bit more about like, where are the boundaries of the type system as it stands?
[00:12:49] Let me give you like, one example, I believe there were three or four things where the theory
[00:12:56] as it existed, did not support Elixir. So for example, in Elixir, we have maps. And we use
[00:13:04] those maps for like structs for like to have structured keys, well defined keys. And in other
[00:13:11] programming languages, and in type theory, we would call them records. So record is a cursor
[00:13:17] that has a well defined set of keys. And in other programming languages, and in type theory,
[00:13:19] we would call those set of keys. You usually, you can add and remove keys, but you usually don’t
[00:13:23] add and remove keys. And those set of keys are like known statically, that’s a record. And other
[00:13:30] programming languages, they have dictionaries, right, which is, you know, you can say, oh, I have
[00:13:34] or they call them hashes, something that is a key value store, you can say that the key value, the
[00:13:40] key is an integer, the value is going to be a string. And so those in most programming languages,
[00:13:47] those are true distinct data types.
[00:13:49] But in Elixir, we use maps for both, because maps changes behind the scenes, and can be efficient
[00:13:55] for both. So when we started doing this, there was no theory, there was no way we could we could
[00:14:02] implement this. So there was we actually, and by we, I mean, Guillaume and Beppe, they actually had
[00:14:09] to develop new theory, publish papers, prove that things are correct. Right. So that’s the kind of
[00:14:15] work that we have to do. And there is something for us to do. And we have to do it. And we have to
[00:14:19] do it. And we have to do it. And we have to do it. And we have to do it. And we have to do it. And we have to do it.
[00:14:19] For example, and, and again, like, we are being able to support the huge majority of the language,
[00:14:24] which means that set derived types is being able to do everything that we needed to do. So we don’t
[00:14:29] have a lot of things that, oh, we can’t do that yet. Right? Like all those things, the things that
[00:14:34] we found that we can’t do it, we actually did research and publish new research, so we can do
[00:14:41] those things. And it’s great, right?
[00:14:43] Yeah, it’s fantastic.
[00:14:44] The fact that we are being able to publish research, not only it’s great in itself,
[00:14:49] which means that we’re able to get a foundation and extend it. If we were stuck by the foundation,
[00:14:55] the foundation is like, ah, you can’t do it, right? That would, that could potentially be
[00:14:59] problematic. So that’s all we have. The one thing that we are working on right now that we don’t
[00:15:07] have is behaviors. So actually, I should clarify that. So behaviors, like when you, in Elixir,
[00:15:14] you can define a behavior, right? And you can implement those behaviors.
[00:15:19] Most of the times you’re implementing behaviors. So every time, so a general server, for example,
[00:15:22] is a behavior, it tells the callbacks that you should implement. Most of the times you’re
[00:15:26] implementing behaviors. And with the type system we have today, the theory that we have today
[00:15:31] allows us to do behaviors as well as we have them today. So you can define the interfaces,
[00:15:37] what it accepts. So we can do that. We can do the same thing that we do today. But one of the
[00:15:43] things that I really want the language to have, like, well, if we are rethinking types, I want to
[00:15:48] have like processes.
[00:15:49] So I want to have proper behaviors. And by proper behaviors, I mean, look, I want to say that I’m
[00:15:55] implementing a general server and this general server is going to have this state and everything is
[00:16:01] derived for us. All the types, the requests, the response, like it figures a lot out for us because
[00:16:08] the way we do type with the Elixir today on those things, it’s quite loose. So it’s one of the
[00:16:13] things that we can’t do. There is research going into this right now.
[00:16:18] And
[00:16:19] I believe we solve like the biggest problem to make this possible. But we can’t really do what
[00:16:24] we have today. It’s just that we are being picky and say, no, it should be better. We should bring
[00:16:30] the next level of features. So and make those interfaces look more like, you know, type classes
[00:16:36] in Haskell or more advanced type features or even interfaces in Java where you can parameterize
[00:16:41] the interface or things like that. So I’m not giving like very specific examples because
[00:16:47] when we are finding things, we’re not going to be able to do it. We’re not going to be able to do it.
[00:16:49] It’s just that we can’t do like we we are trying to solve them because that’s our goal for now, right?
[00:16:55] Is to solve all of those things.
[00:16:57] You mentioned Dialyzer. How does the introduction of set theoretic types interact with Dialyzer?
[00:17:03] And I guess some of the editor tooling that Elixir developers are used to today, does it
[00:17:08] is it going to make it moot? Will Dialyzer kind of go away or?
[00:17:13] Yes, that’s the hope, right? So the hope is so I’m treating them as completely different
[00:17:18] things.
[00:17:19] One of the things we I did explain other presentations, but the idea is like we have been
[00:17:24] writing so much. Let’s say, hey, I just wrote a bunch of type specifications. I want to use my
[00:17:29] type specifications and I’m pretty sure even the fact me asking like, don’t do it. Some people
[00:17:35] will write like an automatic converter from one to the other, right? But the thing is, the
[00:17:41] set theoretic types, they are more precise. They are more powerful than Dialyzer ones. And I think
[00:17:47] an automated translation can be harmful because your type specs, they’re not necessarily being checked for this level of precision.
[00:17:56] Right. So it can mean that you’re going to write your programs in a very imprecise way that is going to make our life harder later.
[00:18:06] Right. So one of the.
[00:18:08] So let me give an example. Let me try to give a more concrete example, which is imagine that you have a function that if it receives an integer.
[00:18:15] Like, okay, the
[00:18:17] unarrayed plus in Elixir, right? The unarrayed plus, if it receives an integer, it returns an
[00:18:24] integer. And if it receives a float, it returns a float, right? So what we can say is that, well,
[00:18:31] this is a function that is exactly that. If it receives an integer, it returns an integer.
[00:18:37] And if it receives a float, it returns a float, right? Like we can say, you can think of two
[00:18:42] arrows, integer to integer and float to float. That’s a very precise definition. So that’s what
[00:18:48] precision means. Like you are giving it a very precise definition on what it does. But you could
[00:18:54] go today, right? And say, well, the type of this thing is that it receives integer or float and
[00:19:01] returns integer or float. And that type is also correct because if you give an integer, it is
[00:19:07] going to return an integer or float. You know, it’s always integer, but it is integer or float.
[00:19:12] And then if you give it a float, it’s going to return an integer or float. Even for you know that
[00:19:16] you know it’s just going to be float. So those two definitions, we can use them to type the
[00:19:23] same function. But one is very precise. One tells you exactly that if you give it an integer,
[00:19:30] the only thing that it can return is it’s going to return. So that’s what I mean about precision.
[00:19:37] So when we wrote Dialyzer today, we were not worried about precision. That’s not something
[00:19:42] that we had to worry about, right? Because even in some cases, Dialyzer, when it sees like
[00:19:46] large type signatures, it actually collapses the types because the goal of Dialyzer is to find a
[00:19:54] possible error, right? While here we want an actual type system. That example, it’s kind of
[00:20:00] the main point. I want to have precise definitions that capture the full behavior of our call,
[00:20:07] the full behavior of our functions. And we have not been thinking about this. So we wrote,
[00:20:12] a lot of type specifications that do not adhere to that. And that’s why I think we should take
[00:20:19] this opportunity and start with a clean slate and say, look, we’re going to type using these
[00:20:24] new properties that we want. So in the future, assuming that all this works, you’ll be replacing
[00:20:30] one by the other, right? You’re not going to be using Dialyzer. We should be using Elixir type
[00:20:35] system. And the goal is that it’s going to have better messages. Error messages is going to catch
[00:20:42] up and it’s going to be faster. So just to give you an idea right now, like we have been working
[00:20:47] a lot with remote, remote.com. They have a large Elixir code base and on 1.19, typing their code
[00:20:55] base, which has more than 12,000 modules, which is a lot, right? It’s taking 20 seconds, which is
[00:21:03] pretty good. Like that’s when you compile the whole project. When you change just one file is
[00:21:09] going to be, well, you can do 20.
[00:21:12] seconds divided by, I think it’s like, it’s going to be very quick, right? And, and we look at that
[00:21:19] and like, okay, that’s too slow. And now we are optimizing it and bringing it down, hopefully
[00:21:24] bringing it down back to around 10 seconds. But that gives you kind of like where we’re going at
[00:21:30] in terms of performance as well and finding bugs and all those kinds of things.
[00:21:36] So right now, when a developer is writing Elixir code, the existing type system in within Elixir
[00:21:42] like it’s kind of transparent, I guess, or even opaque, like, it’s not something I’ve noticed
[00:21:48] personally working in the latest 1.18 release, you know, everything is just working, I’m still
[00:21:52] writing dialers or type specs and that sort of thing. But as, as more of this gets introduced
[00:21:58] to the language, at what point should we as developers start anticipating planning for and
[00:22:04] kind of changing our behaviors a little bit so that our code and our planning works well with
[00:22:10] the introduction of the type system?
[00:22:12] So for now, I still would say you don’t have to worry about or change anything. My goal was that
[00:22:19] for Elixir 1.19, we would be done with the inference things, we would have implemented
[00:22:26] everything that is inference. So we can focus on actually changing the language and allowing
[00:22:31] people to have like, typed struct, or maybe typed signatures. But we did not add. So the funny thing
[00:22:39] is that full inference is actually the only thing that we can do. So we don’t have to worry about
[00:22:42] like, the full inference. We can do it in a way that is fully implemented, almost fully implemented
[00:22:45] in the language, we do full inference for everything except for guard. But I like to say that we we got
[00:22:52] to the draw the owl, you know, the name draw the owl that we have on the internet. So like, like,
[00:22:58] oh, first you do a circle and I’m not sure if I’m promoting the name of the animal correctly.
[00:23:03] All right, like, so the view is like, yeah, draw the owl. So step one, draw a circle. And then step
[00:23:10] two, draw the rest of the bee.
[00:23:12] Oh, right, like, do everything else. And we are kind of pretty much in this stage. Because we added
[00:23:17] inference to everything in the language except guards. What happens that we started having so
[00:23:22] much type information flowing through the code, that we started finding places where it had in
[00:23:31] our backlog, like, oh, we have to implement this feature, we have to add this precision here. But
[00:23:36] because this information now is all flowing through all those things are showing up as false
[00:23:40] negatives, like weren’t or
[00:23:42] false, false is always getting confused. But warnings that we’re not supposed to see, they were
[00:23:46] showing. And then we’re like, okay, now we have to work on all those things, like we have to do the
[00:23:51] rest of the work, because because otherwise, we’re going to have imprecise information going through.
[00:23:57] So we have to constantly refine. And then when we did that, again, more type information going
[00:24:02] through, which means that we have larger types, which is going to bring some bottlenecks in our
[00:24:10] implementation, which is natural.
[00:24:12] So going back, right, so the goal is, it’s still we are working on being able to do things. So you
[00:24:20] don’t have to touch and do anything. That’s still our goal. I was hoping it would be done by 1.19.
[00:24:25] But now it’s most likely going to be done by 1.20, which is going to be end of this year.
[00:24:33] So there is a chance that by May, June next year, about a year from now, is when we’re going to see
[00:24:40] actual things that you need.
[00:24:42] change in your code if you want to have better support for those features so how exactly that
[00:24:49] is going to look like we don’t know yet so my goal here would be well we’ll have these features
[00:24:55] we are going to add them to elixir and then because there’s always a gap between me changing
[00:25:01] elixir and a new version being released so i’m going to add them to main i’m going to play with
[00:25:07] them and whoever wants to try me out can try me out and give feedback but there is a chance it’s
[00:25:14] very likely that you know whatever is in my head right now i’m going to implement it and we are
[00:25:19] going to try it and we’ll say well this is bad this is not good so we have you know we have to
[00:25:24] go back right so i would but basically what i’m saying is like the the the the short answer don’t
[00:25:33] expect anything before june 2026 june
[00:25:37] next year but even that can change right so i don’t think we should change the way we’re writing
[00:25:44] elixir code because again a lot of what we are doing is to be able to support the code you write
[00:25:49] today i don’t think we have to worry about that but if you’re like oh i finally want to type my
[00:25:54] things if the new types i think a year from now at least is a reasonable estimate i i really
[00:26:02] appreciate the level of thinking that’s gone into how to introduce the type system
[00:26:07] and how to implement it and how to implement it and how to implement it and how to implement it
[00:26:07] and how to implement it and how to implement it and how to implement it and how to implement it
[00:26:07] in a backwards compatible way i think maybe it was a blog post on dash bit that you wrote that
[00:26:13] laid out kind of under the hood what’s going on with unions and intersections and how you would
[00:26:19] type a function and you’re drawing on your example of the unary plus operator and how it returns
[00:26:25] a type based on the input type and how you would write that out and how that would
[00:26:31] how new types are more of a super type if i remember this correctly of what was already there
[00:26:37] so that what’s already there existing code will still function just fine and you can add the types
[00:26:44] as you go i really appreciate that and i certainly recommend listeners to check out that that blog
[00:26:49] post it was pretty informative to read and that’s very important right that’s something that we had
[00:26:54] so it’s actually it’s two things so at the beginning my approach into this was look we
[00:27:01] don’t have to worry about existing code because if you want a dynamic program
[00:27:07] then you don’t write the types which is basically how we have been writing all along oh somebody’s
[00:27:14] like oh i i you know i i don’t want i don’t want types i want a dynamic program yeah don’t write
[00:27:19] the types you already have it you’re good you’re covered right so when we started out i was like i
[00:27:25] don’t care about the dynamic things but after the work started it was when we realized that
[00:27:31] hey we can actually so like this idea of having full inference for elixir code base
[00:27:37] i think a year ago we did not have this idea it was like a very recent like realization that’s like
[00:27:44] wait what we can actually type we can have actually have full inference for everything
[00:27:48] so in a way like this schedule that i had for these actually got postponed because
[00:27:52] we added new features so there’s a scope creep happening there never happened before right
[00:27:58] first scope creep ever in the world of software development yeah yes so but it’s because we
[00:28:04] realize we can do that and then we are even bringing more features and we’re bringing more
[00:28:07] features but it was very important for us to be like look we don’t want to have like and that’s
[00:28:13] how a lot of other languages when they added the types that’s how it behaved like they would run
[00:28:20] the type checker and then the type checker would come up with a bunch of violations that weren’t
[00:28:26] they are not actual bugs it’s just the type checker being like yeah you know you you can’t
[00:28:32] write this so it goes back to what i will say like that’s something i wanted to avoid
[00:28:37] since the beginning right like the existing code we should only say it is a bug if we are
[00:28:44] 100 sure it’s a bug it’s not because i don’t quite understand this and then the type checker
[00:28:49] is like kind of giving up yeah what is the world of like kind of downstream impacts of
[00:28:55] what you’re doing ben right like we talked about for the developer the idea here is no
[00:28:59] change right you just get more useful warnings from the compiler about your types but what
[00:29:05] about like live book ci pipelines and whatever you want to call it something like that
[00:29:07] language servers have you started to see any kind of impact on that work at all i would say it’s
[00:29:13] still too early for us to see that i mean we are definitely seeing bugs being caught right so there
[00:29:20] are people when they upgrade like oh the type system found that code like we found that code
[00:29:24] on phoenix on live view on live book itself so even some bugs we we find in those projects as
[00:29:32] well so i think it was live book there was a place where we were doing a rescue and then
[00:29:39] e.message so we were kind of assuming that all exceptions have a message field and our types is
[00:29:44] like you can’t assume that so we’re definitely finding bugs but the thing is when you upgrade
[00:29:51] in our existing code base it is hopefully a code base with tests right because we need that
[00:30:01] types they are
[00:30:02] not going, I talked a lot about this, we can talk more, it’s a separate topic, but we can
[00:30:06] talk about it later.
[00:30:07] Types do not replace the need for tests, right?
[00:30:10] So what happens is that when you upgrade your Elixir version and we do find a bug, it’s
[00:30:19] because it is a bug that your tests are not catching, right?
[00:30:25] So that’s why I say it’s limited what we are getting and seeing because you already
[00:30:31] have the tests that are catching all those things, right?
[00:30:35] So the tests already caught many of the bugs that the type system would have caught.
[00:30:39] So I think like the limits of our work, it is still the impact, it’s limited given the
[00:30:45] nature of where we are in the implementation and where we are as a community, but the goal
[00:30:50] is for it to increase.
[00:30:52] And there are things that we don’t do yet, which is, for example, it’s implemented, but
[00:30:59] it’s not what should be 1.19.
[00:31:00] It goes back to the…
[00:31:01] The full inference thing is that if you call Ecto passing a bad argument, we are not considering
[00:31:09] the types that we inferred from Ecto.
[00:31:12] We consider just a little bit.
[00:31:14] We don’t consider it fully.
[00:31:16] So like the amount of information going through, it’s still limited.
[00:31:20] But yeah, so in other words, I don’t think we are seeing that now.
[00:31:23] I mean, you can get a warning, a warning OCI, for sure that can happen, but we are mostly
[00:31:29] fixing them where we find them in our…
[00:31:31] In our machines, and it is still too early for IDE integration, for example.
[00:31:37] So one of the questions people have like, oh, can you infer the type?
[00:31:40] If Elixir is inferring the types for my functions, can you show me?
[00:31:44] Can you go and add the type and show it to me?
[00:31:48] And I am like very skeptical about doing that for now, because I think those types, they
[00:31:54] can be huge, right?
[00:31:55] Like, because imagine like you have a function with many clauses that calls a function with
[00:32:00] other many clauses.
[00:32:01] And if you’re just getting those signatures and giving them to the user, they can look
[00:32:07] really bad.
[00:32:09] While what you should do is that, well, so imagine one of the examples I gave recently
[00:32:13] is imagine that you’re doing payment processing.
[00:32:16] When you’re doing payment processing, the thing can go into a couple of different statuses,
[00:32:20] right?
[00:32:21] It can be, you know, it can be overdue.
[00:32:24] It can be on trial.
[00:32:26] It can be okay, right?
[00:32:27] The user can have canceled, right?
[00:32:30] And all those things should…
[00:32:31] You can say, hey, there are patterns in our code base, in our function clauses, right?
[00:32:36] So if we just say, hey, infer this for me is going to bring, give you like a huge union
[00:32:41] with all those things, right?
[00:32:43] And the correct would be, well, I want to define a type called the status that define
[00:32:49] all the possible types.
[00:32:50] So you break those things into proper definitions, and then you start using that in your
[00:32:55] signatures.
[00:32:57] So, so basically we, yeah.
[00:32:59] I think short is…
[00:33:01] We don’t have anything right now, but I think I want to be very careful also with that part,
[00:33:07] right?
[00:33:07] I don’t want to say, hey, here’s the type that we inferred, right?
[00:33:10] I want to make sure that everything that we are doing is conscious.
[00:33:15] Nothing is like automatic.
[00:33:16] And I know that means work.
[00:33:18] And sometimes people are like, don’t make me think, don’t make me work.
[00:33:21] But, you know, I think it’s something that is important enough that it does deserve some
[00:33:29] thinking.
[00:33:29] It does deserve some work.
[00:33:31] Yeah.
[00:33:31] It does deserve some working.
[00:33:32] So right now, all of the output from the type system work is compiler warnings, effectively,
[00:33:39] where we’re at right now?
[00:33:41] Yes.
[00:33:42] Exactly.
[00:33:42] So if you’re doing the right thing, which is in CI, you’re doing dash dash warnings
[00:33:46] as errors, then your build will fail with your types?
[00:33:50] Yep.
[00:33:50] Awesome.
[00:33:51] That’s how you did.
[00:33:52] Okay.
[00:33:53] Perfect.
[00:33:54] Man, developer experience, that’s just, you know, it just happens, right?
[00:33:58] Your code is just more checked.
[00:34:00] Yeah, I could use more supervision.
[00:34:01] Awesome.
[00:34:03] So things are going well, things are going how you’d hoped.
[00:34:06] Maybe you wish you were a little further along, but yeah.
[00:34:10] I mean, I can tell you from the outside, it’s been like just easy, right?
[00:34:14] Like it, it just, it’s like, it’s not there, but we get the value on it without having to really
[00:34:18] think about it, which is probably the best case scenario.
[00:34:21] Right.
[00:34:22] For now.
[00:34:22] Yes.
[00:34:23] For now.
[00:34:24] Yes.
[00:34:24] Yeah.
[00:34:24] Right.
[00:34:25] Yeah.
[00:34:25] But that’s the thing.
[00:34:26] Like if you’re happy with the status quo, right.
[00:34:30] You can still stay with this.
[00:34:31] Status quo in the future, right.
[00:34:33] You can just say, I don’t care about types.
[00:34:35] I am happy with the amount of guarantee that Elixir inference gives me by default.
[00:34:41] Sure.
[00:34:42] You know, and if you are happy with that, then, then you’re good.
[00:34:46] You just continue doing whatever, do it as a set, just have dash dash warnings
[00:34:50] as ever, and you’re good.
[00:34:52] But if you want, look, I want proper type then.
[00:34:56] Yeah.
[00:34:56] Then you’ll have a full bank to enjoy.
[00:34:59] Right.
[00:34:59] In about a year, you’ll have some syntax.
[00:35:01] You can.
[00:35:01] Add to do something.
[00:35:03] Yeah.
[00:35:04] Potentially.
[00:35:04] Yes.
[00:35:05] Fantastic.
[00:35:07] I feel like I’ve seen the LSP tell me about type issues that I hadn’t noticed
[00:35:13] before, but I’m assuming it’s just passing through something it’s finding through
[00:35:17] recompiling the code as opposed to anything that’s built into the LSP specifically.
[00:35:23] Yeah.
[00:35:23] So the, yes.
[00:35:25] So the compiler emits diagnostic about what went wrong during compilation.
[00:35:31] So from the LSP point of view, a undefined variable warning is the same type of diagnostics as a type violation.
[00:35:40] So the LSP is just getting all of those.
[00:35:44] So whenever we improve Elixir, you get it as a warning on CI, and it also shows up in your LSP as a warning as well.
[00:35:53] Has this impacted any of the work on the Elixir LSP project?
[00:35:58] Are they interacting or is that entirely separate?
[00:36:01] Tracks of work?
[00:36:01] So I would say it’s, it’s a still entirely separate tracks of work.
[00:36:03] We have a shared communication channel.
[00:36:04] And one of the good things about establishing this channel is that we can give and receive feedback early on.
[00:36:05] So of course we are being very mindful of what is happening there.
[00:36:06] But I think given both are still highly in development, they are separate track.
[00:36:07] How is the LSP project working?
[00:36:08] Yeah.
[00:36:09] Is there anything you’re able to share at this point, or is that still, people are heads down and making it happen?
[00:36:16] Yeah, so I am, I am.
[00:36:17] I am doing the LSP project right now.
[00:36:19] I am not aware of the LSP project.
[00:36:20] So I’m just doing the LSP project.
[00:36:21] So I’m still working on it.
[00:36:22] I’m working on it.
[00:36:23] I have all the resources I need.
[00:36:24] I have the tools I need.
[00:36:25] I have the tools to do this.
[00:36:26] I have the tools to do this.
[00:36:27] But I have a shared communication channel.
[00:36:28] And one of the good things about establishing this channel is that we can give and receive feedback early on.
[00:36:29] So of course, we are being very mindful of what is happening there.
[00:36:30] But I think given both are still highly in development, they are separate tracks.
[00:36:31] How is the LSP project going?
[00:36:32] anything you’re able to share at this point or is that still people are heads down making it happen
[00:36:36] yeah so i am i am not involved on it directly to be honest so i know they are working on it i know
[00:36:44] they are companies sponsoring the work like fly and tall spades so those are two companies that
[00:36:52] are sponsoring people working on the project and the project continues to to develop but i really
[00:36:57] don’t know like the the exact details of where they are you know so that’s a that’s an episode
[00:37:03] to have with them yes yeah absolutely is is there anything else ongoing in the elixir universe
[00:37:11] that are part of day-to-day elixir developers work that ties into this or that you’d like to
[00:37:16] bring to the table today in particular with types i’m not sure if there is anything worth
[00:37:25] calling out i mean i think there are
[00:37:27] things so one of the things that i mentioned and in the topic of interrupt that i mentioned in the
[00:37:33] keynote was having types can also potentially mean having interrupt at the types level for example
[00:37:41] oh i what if i can get an elixir type a struct type and convert to typescript and use that to
[00:37:50] have better integration between front and the back end so that’s something that we actually
[00:37:56] built some proof of concept proof of concepts or proofs of concept anyway one of those options
[00:38:03] or maybe add or maybe proofs of concepts anyway but yeah so we we did build some exploring those
[00:38:13] ideas so i think that can be interesting but it’s too early of course there are like many things
[00:38:19] happening in the ecosystem in terms of interrupt and ai but i think like types related it’s too
[00:38:26] mostly still on core yeah i mean i think that’s a testament to the approach that you guys took
[00:38:31] here right is is how focused it can be how much you’ll be able to give the developer for really
[00:38:38] no effort from well from our part lots of effort from your part yeah but uh yeah i mean this has
[00:38:44] been fantastic it’s really great to hear kind of where things are with all of this and you know
[00:38:48] the experience i think at least for me has been so like like it’s not a big deal that i think it’s
[00:38:56] not a big deal that i think that it wasn’t really that it has that you haven’t gotten much but i
[00:38:59] think the reality is we’ve gotten a ton and the fact that we don’t know it is really just a benefit
[00:39:05] of you know how great this language is and how great the work that’s going on behind the scenes
[00:39:09] is our goal for for now it should be like conference wi-fi you know if it works everybody’s
[00:39:15] happy nobody complain right and if something is wrong somebody’s going to complain loudly so we
[00:39:22] can fix it sure uh but yeah we hope to stay
[00:39:26] like you know everything is going and another so there is like uh big big uh big companies they
[00:39:35] have there is a word for this they do i think it’s like let me tell what it is when they want to add
[00:39:40] a new feature they launch the feature like kind of disabled to see like the load on the service i
[00:39:48] think like facebook did that for example when they launched the messenger the first thing they did
[00:39:56] was they loaded the whole thing right had it send like the initial messages but without ever showing
[00:40:04] to the user so we they could exercise the performance the impact this would have on their
[00:40:09] servers there is a right this this thing has a particular name there is a this technique right
[00:40:15] and that’s also the other thing because we are talking a lot about well getting the warnings
[00:40:20] but it’s also very important the warnings if we go back the performance should also be really good
[00:40:26] right so if you’re talking about like that it’s the other benefit of this approach is that the
[00:40:29] type system gets more complex every release we add more features it’s doing more work and it should
[00:40:35] be fast right and when it’s not fast like it’s getting stuck in some case and then people do the
[00:40:40] report that’s when the conference wi-fi fails but people do the reports and then we fix them
[00:40:46] but that’s the other very important thing for this right because it will happen but it would be really
[00:40:51] hard like if you’re like oh i added this type signature and now like my program takes you know
[00:40:56] you know, 30 minutes to compile, which will happen because we are going to have
[00:41:00] like all type systems that have those things, they have those really corner
[00:41:04] cases where a lot of type systems, the algorithms, their theoretical
[00:41:08] complexity can be like very high.
[00:41:10] It’s just that we don’t keep those particular cases in practice.
[00:41:14] So that can be for everything.
[00:41:16] So that was the other thing.
[00:41:18] And it gives us confidence, the fact that we, we keep on adding features
[00:41:22] and the compilation times are good.
[00:41:24] And when they, they got bigger than you were expecting, we can do the
[00:41:29] work and bring them back down again.
[00:41:31] And yeah, that’s all very exciting.
[00:41:34] David Pérez- In terms of maybe like asks for developers who are trying out
[00:41:37] 118, 119, you know, the RISC planets, all of that, sounds like let you know
[00:41:42] if things take a long time, you know, if it takes a lot longer to build than it
[00:41:45] used to and developers should not be ignoring their warnings.
[00:41:48] David Pérez- Yes.
[00:41:49] David Pérez- Beyond that, are there any, any asks for the audience
[00:41:51] or any, any plugs you’d like to make?
[00:41:53] David Pérez- Yes.
[00:41:54] So.
[00:41:54] David Pérez- Very good.
[00:41:55] So I’m going to recap yours.
[00:41:57] So when you, before you upgrade Elixir, do a mix compile dash dash force, and
[00:42:06] there is a flag called profile time.
[00:42:08] So mix compile dash dash force dash dash profile space time that is going
[00:42:13] to compile your project, fully compile only your project, measuring the time
[00:42:18] it takes for compiling and the time it takes in particular for the type system,
[00:42:23] which we call group path.
[00:42:26] That’s the group path.
[00:42:27] So then you upgrade Elixir, you compile everything, you run your tests, see if
[00:42:31] you’re happy, if you’re happy, then you run it again, mix compile dash dash force
[00:42:35] profile time, and you should see large projects should see like a big difference
[00:42:41] in compilation times in 1.19, because we did some work on this area.
[00:42:46] So I was talking about remote, they are code-based compiling three times
[00:42:49] faster, which is just amazing.
[00:42:52] So that’s one thing you can do, right?
[00:42:53] So you do that and don’t do that on the release candidate zero that is out right
[00:42:59] now, so we are going to announce release candidate one, and then you can do that
[00:43:03] because we already know, we already got, we already got the reports of bad wifi.
[00:43:07] We already know that it’s failing in some cases.
[00:43:10] We fix those.
[00:43:11] We are working on the next release.
[00:43:12] Then when RC1 is out, please try it again.
[00:43:16] Let us know the time.
[00:43:17] Let us know if things are looking good as we expect them to look.
[00:43:22] Yeah.
[00:43:22] So report.
[00:43:23] So reporting the times, try out the RCs and yes, please don’t ignore the messages.
[00:43:29] Go for the messages.
[00:43:31] And if something is making you scratch your head, don’t say like, ah, you know,
[00:43:35] like, oh, I’m not too smart to understand this, you know, or this is confusing.
[00:43:41] If it can either be, I would say that most likely it’s a bug in both cases.
[00:43:46] So if you get a report, you don’t understand what it is.
[00:43:48] It’s most likely a bug in Elixir.
[00:43:50] We’re not supposed to be getting that report.
[00:43:52] Or it’s.
[00:43:53] Most likely.
[00:43:53] Most likely a bug in Elixir.
[00:43:54] We could be doing a better job in that particular report.
[00:43:59] So it’s less confusing for you.
[00:44:00] So if you are upgrading, you see a warning, you’re like, oh, I can’t, I can’t solve this.
[00:44:05] I don’t know what it wants me to do.
[00:44:07] Let us know because it should be clear.
[00:44:10] We shouldn’t be saying like, Hey, you know, you were expected to do this or, uh, you know, this is the change you need to do, or there is a bug in your code and here’s how you can spot it easier.
[00:44:22] So, yeah, awesome.
[00:44:25] Well, thank you so much for your time and this was just a great update on where we are with types and Elixir and yeah, hope to have you back again soon.
[00:44:33] Thanks for having me.
[00:44:34] See you next time.
[00:44:35] Yeah.
[00:44:35] Thanks for joining us.
[00:44:36] Jose Elixir wizards is a production of smart logic.
[00:44:41] You can find us online at smart logic.io.
[00:44:44] Don’t forget to like subscribe and leave a review.
[00:44:47] This episode was produced and edited by Paloma for smart logic.
[00:44:51] Thanks for joining us and we’ll see you next week for another episode as we enter the Elixir verse.
[00:44:56] Hey, this is your ear flicker president of smart logic.
[00:45:12] The company that brings you this podcast smart logic is a consulting company that helps our clients accelerate the pace of their product development.
[00:45:19] We build custom software applications.
[00:45:21] We build custom software applications.
[00:45:21] We build custom software applications.
[00:45:21] We build custom software applications for our clients, typically using Phoenix and Elixir, Rails, React and Flutter for mobile app development.
[00:45:28] We’re always happy to get acquainted, even if there isn’t an immediate need or opportunity.
[00:45:32] And of course, referrals are always greatly appreciated.
[00:45:35] Please email contact at smart logic.io to chat.
[00:45:38] Thanks and have a great day.