YT YouTube2Text

YouTube2Text → Transcripts → Static Types Finally Come to the BEAM | Annette Bieniusa & Guillaume Duboc

Static Types Finally Come to the BEAM | Annette Bieniusa & Guillaume Duboc — Transcript

by BEAM There, Done That · 9,655 words · 1,644 segments · language en · Watch on YouTube

Open in transcriber Summarize with AI Download SRT/VTT

Full transcript

0:00So, hello. Welcome to the episode of
0:02Beam There, Done That. I'm your host,
0:03Alan Wyman. Today, we have, of course,
0:06my other host, Francesco Cesarini.
0:09>> Hi, I'm Francesco. I'm also co-host.
0:11Welcome to the show. Today, we will be
0:13tackling the question of how we bring
0:16your static types
0:17to Erlang and Elixir. It's It's a quest
0:21which, you know, I tend to joke is
0:22almost as old as Erlang itself. And
0:25joining us are Annette Bieniusa and
0:28Guillaume Duboc. But, you know, before
0:30introducing me,
0:31let me go in and give you some some
0:33background of the topic. You know, when
0:35I was at the Computer Science Lab, you
0:36know, back in 1995,
0:38so, I can't believe it was over 30 years
0:40ago, I was working on my master thesis.
0:42Anders Lingren, who you know, studied
0:43computer science with me at Uppsala
0:45University, that as part of his thesis
0:47went in and proposed a soft type system
0:50you know, for Erlang. Simon Marlow, so,
0:52the Glasgow Haskell Compiler maintainer,
0:54was working on his PhD thesis at the
0:56University of Glasgow together with
0:59Philip Wadler.
1:00And they were looking at a subtyping
1:03based system. And what the system did is
1:05it trade did ex- expressive power, you
1:07know, for simplicity. So, they were
1:10going in and trying to understand, you
1:12know, how do we get stronger typing in
1:15in Erlang. Both Anders and you know,
1:17Simon met at conferences, you know, they
1:19shared a lot of notes and ideas, what
1:22worked and what didn't work, but you
1:24know, what they what what they achieved
1:27did not go far and and never really made
1:29it into production. You know, to quote
1:30Joe Armstrong at the time, you know,
1:32anyone can write a type system which
1:34covers 90% of Erlang, but the remaining
1:3610% is really, really hard. And even the
1:38brightest mind in computer science and
1:40here
1:41he was referring to Phil Wadler have
1:42struggled. And you know, as a side note,
1:46this is because of some of the design
1:47choices they made with the Erlang
1:49semantics very, very early on. So,
1:53the the the tension we were wrestling
1:55with, you know, back then is the same
1:57tension that we're wrestling with today.
1:59So, decades might have passed,
2:01but those challenges and tensions
2:03continued, you know, with Thomas Arts
2:05and Joe Armstrong's practical type
2:06system, you know, Sven Olof Nyström's
2:08polyvariance of typing, and Kostis
2:10Sagonas' Dialyzer. Dialyzer was a
2:13pragmatic compromise that admitted it
2:16couldn't prove your code was correct,
2:18but could reliably tell you when
2:20something was definitely wrong. It seems
2:22like today, we're reaching an inflection
2:24point. So, Elixir 1.
2:272 is is shipping with a gradual type
2:30with gradual set theoretic type system.
2:32It's built on the
2:34on years of research by Guillaume, who's
2:36on the show with us today.
2:38And our second guest, Annette, has been
2:40building, you know, the parallel
2:41Equalizer project for Erlang with her
2:44team and collaborators.
2:46And you know, between them and other
2:48projects such as WhatsApp Equalizer,
2:50it genuinely feels like the beam is is
2:53converging on an answer after nearly 30
2:56years. And yeah, and that's what we're
2:57here to dig into today. It's a bit of a
2:59long introduction,
3:00but you know, there's a lot of history
3:02behind us, and it's important to
3:03understand the history to understand
3:05where we're heading to. So, Annette,
3:06Guillaume, why don't you introduce
3:08yourselves? Welcome to the show.
3:10>> Hi Francesco. Great to have us, and
3:12we're very we are very happy to be here.
3:14Um my name is Annette Vinusa. I'm a
3:16professor for software technology at the
3:19uh RPTU in Southwest Germany, um
3:22university,
3:23and I've been doing research on
3:25programming languages, type systems,
3:27distributed systems for almost two
3:29decades now, and Erlang and Elixir and
3:33the beam is uh one of the core aspects
3:37that we uh that we deal with in our
3:39research, and we also introduce a lot of
3:41students to it. So, growing the
3:42community this way.
3:44>> Hi Francesco, Helen, uh
3:47Annette.
3:47I'm um
3:49Guillaume Duboc. I'm um
3:51a PhD currently at Dashbit. I did my PhD
3:56in Paris at the I Reef, Institute for
4:00research research in theoretical
4:03computer science. And I defended it in
4:06in January of this year. The name title
4:09is typing dynamic languages with set
4:12theoretic types the case of Elixir.
4:14And um
4:15I've been
4:17working on
4:18type systems since my masters. I did my
4:22internship with Jose Valim Castagna at I
4:25Reef
4:26on the theory of set theoretic types.
4:29So, this uh
4:30PhD was an
4:32occasion to apply them to
4:34real industrial language. And um
4:38I'm yeah, of course, I'm I'm really
4:40interested in to
4:42bringing research to to practice.
4:44And I was really charmed by this this
4:47theory of semantics of typing set
4:49theoretic types. And
4:50really pleased to really pleased to be
4:53able to
4:54to bring it
4:55into practice.
4:57>> Now, Guillaume, just to kind of start to
4:58break the ice and warm you up to the
5:00podcast. I'm kind of curious, right? I'm
5:02sure you've programmed before. Do you
5:04have a have has there ever been a bug
5:06that you've introduced to a production
5:08system that no type system would have
5:10caught?
5:11>> I I don't really have a crispy personal
5:14story of a bug, but type systems I'll
5:16I'll take the question the more general
5:18answer to that question is that type
5:20systems they catch a certain given class
5:24of bugs, but there are other class of
5:25bugs that they just have nothing to tell
5:28you about.
5:29Thinking about in most cases
5:33non-termination
5:34errors. Often the property that we can
5:38say after having typed the program is
5:40that
5:41it's not going to crash and you know
5:44what is the type of value that is going
5:47to compute, but the
5:50third second thing is that it may
5:52diverge, and in that case you cannot say
5:54anything. So,
5:57it's a bit of a of a
6:00an escape, but I've I've I've shipped
6:03some some program that looked because of
6:06badly evaluating the
6:08where where it was going to run out.
6:11And otherwise, uh
6:15the the
6:16to to take the the question more
6:19seriously, I think it boils down to how
6:22far you're able or willing to go with
6:25the complexity of the type system and uh
6:28amount of work that the programmer is
6:31going to have to do, because a lot of
6:34type errors that you don't catch are
6:35because the type system has limitations
6:39in the expressivity that uh
6:42that
6:43it is able to describe, or either that
6:46or uh
6:48uh
6:48the designers of the type system they
6:50want you to spend
6:52a lot of time
6:54writing a proof about why your uh uh
6:57functions are correct.
6:59So, um
7:01uh
7:03I would say that
7:05I don't wish that I had been able at I
7:08don't wish that I had been given the
7:10opportunity to prove that my program was
7:13correct every every time, because that
7:15that that means sometimes that I would
7:17have just spent a lot of time proving
7:20that something is correct when I just
7:21wanted to scrap up scrap it and do do
7:24things differently in a more simple way.
7:27>> Now, Annette,
7:28what was the first programming language
7:30with a type system that you know, made
7:33you either fall in love with or you
7:35know, have a real maybe disdain for?
7:37>> So, when I learned programming in in
7:40high school, we started with type
7:43languages and even the first university
7:46courses, you know, it was Java
7:48and Haskell. It was always kind of clear
7:50that these languages would have a type
7:52system and that types were something
7:54that you need to deal with somehow.
7:55First time I realized that type systems
7:57can actually bring something very very
7:59powerful to the to the table and help me
8:02refine my programs and make them better
8:04maintainable and so on was actually a
8:06master level seminar where I had to
8:10report on the new addition to Java 1.3,
8:14namely type variables and parametric
8:17polymorphism. And there was, you know,
8:20the wild cards and the the sub sub and
8:23supertype constraints, I realized that
8:25type systems can be actually very very
8:27expressive, but it took me a while to
8:29wrap my head around it and, yeah, make
8:31use of this expressivity in a in a good
8:34way.
8:34>> Now, coming back to to types, right? I
8:37want to start from the absolute bottom,
8:38Anette. If one of our listeners has only
8:40ever used a dynamic language such as
8:42Python or Elixir, of course Erlang,
8:45how do you explain what a type actually
8:46is to them?
8:47Uh without using the word class and
8:48without kind of getting deep and quoting
8:50what a textbook would say.
8:52And in in that in going on top of that,
8:55in Erlang, if you say that a function
8:58takes an integer,
8:59what is it actually promising uh when we
9:01talk about types within what you're
9:03working on?
9:04>> So, from my perspective, types
9:06characterize um values that are um given
9:10in a in a programming language. And uh
9:12if I know that some form of value has a
9:15specific type, I know what I can do with
9:18this value. So, and
9:20this this means that when in Elang
9:22Elixir, I have a function that takes an
9:24integer, I know that or I hope that the
9:27function will be well-behaving uh
9:29whenever I pass an integer to it. And I
9:31should not assume that it works
9:32correctly if I would pass a boolean
9:34value or another function or, you know,
9:36something of a different type.
9:39And depending on how the type checking
9:42is actually done and what the guarantees
9:44are that a specific type system gives
9:47you, there are certain things that you
9:49may assume and that you might not
9:51assume. So, types, in particular when it
9:53comes to functions, can be seen as
9:54contracts. As a
9:57caller of a function, I can assume a
10:00specific behavior if I pass the values
10:03according to the the type specification,
10:07and I can make assumptions again on the
10:09values that would be returned.
10:11>> Erlang and Elixir have always been
10:12dynamically typed. Java, Rust, Haskell
10:16are statically typed.
10:18And people say static catches the bugs
10:22before your program runs. Can you tell
10:25us what the difference is between your
10:27static and dynamic typing and what part
10:29of the sentence I just mentioned
10:32basically static catches the bug before
10:34they run
10:35is generally true and what part of that
10:37is oversold?
10:38>> So, static and dynamic first of all
10:40refer to the time when the type check
10:43happens, right? Static means it happens
10:46before the program gets compiled and
10:47before it's executed. Dynamic refers to
10:50type checks that happen at runtime while
10:53the program is executing. Both Both Both
10:56approaches catch bugs. For the dynamic,
10:59it feels different because very often
11:01the program resorts to aborting the
11:04execution if uh if the type check kind
11:06of fails, and most often this is very
11:08annoying, right? So, you run your
11:09program and then boom, it it kind of
11:11crashes and you're wondering what's
11:12happening and if the reason is where
11:14type kind of goes goes wrong,
11:17then that's that's really problematic,
11:19yeah? So, what you get with static
11:22typing is the is the bugs that actually
11:25are the bugs that that you can
11:26anticipate and yeah, prevent them from
11:29happening at runtime.
11:32What type of bugs can be can be checked
11:34really depends on the type system. So,
11:37even C that has has aspects of a So, so
11:41C has aspects of a static type system,
11:44of course. It doesn't do a lot of
11:45dynamic checks. Dynamic checks are
11:48somewhat more expensive, right? If
11:50you're If you're doing a lot of checks
11:52while your program is executing, this
11:53will will slow the program down. If you
11:56compare this to languages that try to
11:58provide better guarantees like Java,
12:01Java would still do checks at run time.
12:04Like also dynamically check for some
12:05aspects that it won't wouldn't be able
12:07to catch
12:08during during the the compilation phase
12:11as as part of the as part of the
12:12compilation phase. So, checks like null
12:16pointer exceptions are actually to some
12:18degree can also be considered type
12:20checks.
12:21And most languages actually use a mix of
12:24both. I would I would kind of claim in
12:26particular those that have static types
12:29will also make use of the types at run
12:30at run time somehow.
12:32>> And a a lot of developers think static
12:34and strong mean the same thing.
12:36And they don't. Yeah, can you untangle
12:38them? Where do Erlang and Elixir
12:41actually sit on both axes?
12:43>> With Erlang, right? Erlang is not
12:46statically typed unless you use an
12:48external tool like an additional tool
12:50like Dialyzer, say for example, then you
12:52don't get specific guarantees at compile
12:56time
12:57or prior to execution. It does checks at
13:00dynamically at at run time.
13:02Whether you consider the the type system
13:05strong or weak depends a bit on what
13:08your expectations are. Erlang actually
13:10has dynamic type checks and they give
13:12you some guarantees you can't
13:14accidentally wreck up your memory.
13:16>> And then a lot of developers think that
13:18static and strong mean the same thing
13:19when actually they don't. Can you
13:22actually start to kind of describe the
13:23the differences and maybe the positives
13:25and negatives of each one?
13:27>> So, static refers actually just to the
13:29to the point in time when the type check
13:31is happening. Whether the type system is
13:34strong or weak depends on the amount of
13:37guarantees or the type of guarantees
13:38that you would get with a with a type
13:40checker. All right? You can have very
13:42strong dynamic typing, you can have weak
13:45static typing, and everything in
13:46between. So, one thing is not per se
13:49better than the other. Even strong type
13:51systems can have aspects that
13:55make them not nice to use because a
13:58stronger guarantees typically mean that
14:00you need to be more careful in how you
14:02write types and how the types look look
14:04like. Like, be more precise, for
14:05example.
14:06>> Guillaume, the phrase that ties this
14:08whole episode together is gradual
14:09typing. You know, what is it?
14:12And why is it the thing that makes
14:14typing Elixir possible at all?
14:17>> I would say that gradual typing
14:20is allowing
14:22yourself or allowing the type checker to
14:25operate with uncertainty about the
14:28types. This is the dynamic type or any
14:32unknown that you have. And um in the
14:36case of Elixir, it's quite important
14:39because it has been a
14:41dynamic language, untyped language for
14:44its uh whole life. So, there are
14:47entire code bases that exist
14:50and that needed to work with the new
14:53system. You cannot just expect that
14:56those code bases are going to be to have
14:59to be entirely annotated with a static
15:02types before being used again after a
15:05version 1.21 of uh
15:08of Elixir. And uh so, gradual typing
15:11allows the type checker to function
15:13with the knowledge that, well,
15:16this function here, all that we know
15:19about it is that when you give it an
15:22integer,
15:23it returns you something dynamic.
15:26Value that you don't know about at
15:30compile time.
15:31So, from a very practical point of view,
15:35this is what makes the
15:39work possible in in the first place.
15:43Now, there's
15:43there's another um
15:46a theoretical reason why we also want a
15:49gradual system, which is and it is that
15:53in the type system that I've designed
15:55with BP and
15:56just to say BP and
15:58with Jose.
15:59Uh we are treating the functional aspect
16:03of Elixir. That is we are typing
16:06functions
16:08in a very precise way and uh
16:11case pattern matching
16:14all of this. And there are some aspects
16:16that we have not treated, for instance,
16:19typing the messages that are sent.
16:21And that means that we need an escape
16:25hatch when the type system is not going
16:29to be able to give static types to those
16:33um
16:34uh to those to those uh
16:36expressions. And this this escape hatch
16:40is baked into a gradual system in in the
16:43form of a the dynamic type.
16:45>> Why is Elixir team's version of gradual
16:48typing different from what TypeScript or
16:50Python does today?
16:51>> The difference is that it is part of its
16:56foundation. To design the type system of
17:01Elixir,
17:02uh we started from theory of types that
17:06are set theoretic,
17:08uh meaning that you can express union of
17:12types,
17:13intersection. An intersection of two
17:16types is going to be all the values that
17:18are both that are in both types.
17:21Negations as well. All the values that
17:23are not in a given static type. So, if
17:26you get the type the type not integer is
17:29every every double value, list value,
17:32etc. And the dynamic type is also part
17:36of that structure. If you do the union
17:39of a dynamic type and static type, what
17:42you have is a
17:44gradual type. So, for instance, you have
17:46the type integer or dynamic boolean.
17:49That that type is is interesting because
17:52it tells you how the type checker is
17:54going to treat that. It's it's going to
17:56consider that the integer part is a
17:59static, so it needs to you know, be
18:01handled by a
18:04function if if you pass this arg as
18:06argument to a function, but the dynamic
18:09boolean part is more is less strict less
18:14restrictive. So, if the function does
18:16not handle this boolean part, then the
18:19program
18:20may
18:22may accept this program. That allows
18:25that allows us to bake a lot of
18:27flexibility into the type system. And I
18:30think this is the difference with the
18:32way that
18:34TypeScript for instance was built is
18:37that at first they introduced
18:40the
18:41So, I I don't
18:43they they have they have two dynamic
18:45types. Uh
18:47I think it was any. At first they
18:49introduced any as this dynamic unsafe
18:53escape hatch. And then they realized
18:55that because of the way that they
18:57designed the system around it, it was um
19:01it was
19:02too too unsafe and
19:04disliked by the programmers who wanted a
19:06way to say, "Okay, I put an escape
19:08dynamic escape hatch, but I want you to
19:10remind me that I need to refine it and
19:13check in and this is why I have to
19:15introduce the unknown.
19:17And the the reason is the reason is that
19:20in those cases
19:21the dynamic type is
19:24an extra thing on top of type system and
19:28it it makes the things a difficult. I
19:30mean
19:32at least it it makes the design around
19:34the how it's going to be used
19:36non-trivial and
19:38I think
19:40that's that's the main difference.
19:41>> I mean the beam has has been around for
19:43quite some time, right? Why does it
19:45actually need a type system at all?
19:47Guillaume.
19:48>> The
19:49in our case the type system is not going
19:52to improve of on the run time
19:55cuz it's it's already a fantastic run
19:57time. What
20:00the
20:02what we bring I think to the table is an
20:05improvement on the process of writing a
20:09code base or of maintaining a code base.
20:12Elixir and Erlang scale to users but
20:16the does the
20:18code does Erlang and Elixir code scale
20:21to
20:23millions of lines of code?
20:25And
20:27I think that
20:28the type system helps helps with this
20:31this process because it's going to
20:34enable programmers senior programmers to
20:39define
20:40what the code base is about and have
20:42this
20:44mechanically checked documentation
20:47and it's going to improve collaboration
20:50around the code base. So, I would say
20:52this is
20:54there is there is an aspect of
20:58type system that
21:00maybe can
21:02improve the technical the technical
21:05aspect of the code like
21:06perhaps improve the quality of the code.
21:09Perhaps because the type system is going
21:11to to guide
21:13programmer towards um
21:15avoiding some
21:17some bad patterns or
21:20making sure that for instance um
21:24exceptions are completely
21:26handled in the in the whole code.
21:29Uh
21:29but
21:31like good software that has already been
21:33written in
21:35longer is not going to get better.
21:37However, maybe it's going to help
21:40writing um
21:42more of those.
21:44>> I'd love an X's view here because again,
21:46Erlang's run telecoms you know for 25
21:50years without static types. You know,
21:53we're talking GPRS, 3G, 4G, 5G.
21:56And Ericsson at Code Beam Stockholm
21:58announced you know that they're doing
22:00all of the 6G with Erlang.
22:03As you can actually work with Erlang,
22:05you know, you've got pattern matching,
22:06you've got supervision tree,
22:08embracing the whole let it crash
22:09approach, you know, and let it crash
22:11happens regardless
22:13of a
22:15of a type system. So,
22:18and so without
22:20static types, you know, the beam shipped
22:22some of the most reliable software ever
22:24written. And we're talking a few seconds
22:25of downtime per year including upgrades
22:29and maintenance. You know, I want to ask
22:31you the obvious question I think, what
22:33problems are we actually solving now
22:36that we weren't solving in 1995?
22:39>> So, one of the aspects here is that
22:42actually type systems catch bugs that
22:46are due to programmers uh
22:50and that that are that are introduced by
22:52programmers, not necessarily by
22:53situations that occur at runtime.
22:55So, let's assume you have a bug that
22:58could have been caught by a type system.
23:02It might be that you implemented all the
23:04supervision trees and everything kind of
23:05correctly. So, when you hit the specific
23:08path, the specific execution path, then
23:11your program will, you know,
23:14make use of the of the of the restart
23:15and everything, and it won't necessarily
23:18kind of go down immediately, but you
23:20have a lot of overhead, and you need to
23:22kind of keep in mind that you need to
23:23provide supervision trees, etc., and
23:26there might be parts in the code where
23:27this is not necessarily the case. You
23:29don't want to spawn a new process just
23:33for executing a function call, making
23:35sure that if this function call has a
23:37type error, that you can kind of catch
23:38it somehow. It's also not totally
23:40obvious how to deal with this problem at
23:43runtime, so you would need to kind of
23:44patch the code and so on. And this is
23:46all very expensive. And even if a type
23:49system just catches, say, 5% of all
23:52issues in your code base that happen
23:54over the course of of the runtime of a
23:56system, it's still 5%, right? And this
23:59directly reflects in in overheads, also
24:03on on latencies, and better machines
24:06that you need, and and so on, because
24:07you need to over-provision for these
24:09situations. And if it's just a bug that
24:12a type system could have caught, why not
24:14use a type system to prevent it?
24:16>> If you tried to build the type system
24:18you're building now, so this is for
24:20Guillaume, in 2005, what would have made
24:23it impossible
24:25or just not worth the effort?
24:27>> I think that
24:29the
24:30So,
24:32the
24:34immediate difficulty when typing uh
24:37Erlang
24:40is that
24:42because of the way it is structured
24:45around the pattern matching
24:47with no no need to
24:49satisfy a static type checker, you can
24:53have
24:54you can freely have a function that
24:55returns
24:57an integer or
24:59a boolean.
25:00And you don't want to build or rather
25:04you've not been asked to build special
25:07type
25:08that would
25:09encapsulate that like in the
25:12ML family of languages
25:15for instance where you're going to build
25:17some type saying
25:19or I can have a constructor with an
25:22integer under or another constructor
25:26boolean under.
25:27And so you need your type system to
25:30freely represent union of types.
25:35Integer or boolean.
25:37So you need
25:39fully developed type system that that
25:42has this property.
25:44Another thing is that because you have
25:47functions that
25:49are able to return those
25:51completely different
25:53type of values. Now it's possible that
25:56you're going to do overloading and that
25:58you're going to expect your function
26:00to return an integer when given an
26:03integer and return a boolean when given
26:05a boolean.
26:06And that's why you need overloading
26:09function overloading.
26:11And you want to bake it into your type
26:13theory as well because you want
26:14something that is that is
26:17that follows closely the the semantic of
26:20the language and the
26:22around the 2005 the
26:25there was the
26:26thesis of Anna Frisch on the
26:29on the CDuce which showed that you could
26:32do this in in a language have a
26:36function overloading via intersection
26:38types and the
26:40union of types
26:42and the
26:44other other very precise features. The
26:47theory called the semantics of typing
26:48but this theory was
26:51still missing a lot of things that were
26:53developed 10 years after. That is
26:56polymorphism.
26:58Being able to do
27:00parametric polymorphism
27:02in
27:03context in the context of sub 30 types
27:06was in
27:072015.
27:08And then the ability to integrate
27:12dynamic into that was from
27:162019.
27:18So the
27:21if you wanted to um
27:24have a theory that
27:26easily expresses those um
27:28those um
27:30free patterns that those
27:32this very free way of programming that
27:34Aaron uses, you couldn't use
27:38sub 30 types in 2005. So you would have
27:41to do some very complex
27:45inference, some so some very complex
27:49constraint solving. But the way that you
27:52present this to the programmer would
27:54maybe a bit difficult because
27:57I think that there are two
27:59there are two aspects to type system.
28:02There's the aspect is the type system
28:05able to
28:07represent
28:08all the types that you need. Like is its
28:11model
28:13complex enough?
28:15And is the type system
28:17adapted to
28:20the way the programmer thinks about the
28:23language. And then is the type system or
28:26maybe the type language sufficiently
28:30Is it is it easy to understand, right?
28:33And
28:34I think those are This is what the
28:37sub 30 types bring to the table there.
28:39Is that we have both way to technically
28:41solve the challenge and we have a way to
28:43present them
28:44in
28:45in an interesting
28:47in
28:48a sufficiently easy way for the
28:50programmers.
28:50>> And
28:51you were workshop chair when I believe
28:54this is pronounced Kostis Sagontas gave
28:56his 15 years of dialyzing retrospective.
28:59Now dialyzer has been a very good
29:01practical answer when we don't have
29:03types, right? That it can kind of run
29:04through and see if there's any kinds of
29:06type issues. I mean, it's it's really
29:08great. It's probably underutilized in
29:10terms of not many people using Elixir at
29:12least are using it. Even people who are
29:14using Erlang are probably I mean
29:15definitely not all using it. And it's
29:17air messages are
29:18you know, infamous in being very very
29:20cryptic. Do you think that dialyzer was
29:23definitely a great step forward in in
29:25working with a type system and in kind
29:27of like a good base to to to work at?
29:29Have you used it when you're working on
29:31the Elixir project? Or what do you kind
29:33of feel about the about dialyzer?
29:35>> I typically like to use use dialyzer in
29:39my projects and we always tell the
29:41students also to use dialyzer in their
29:42project projects. There is a catch with
29:45dialyzer. So from my experience, if you
29:48use it without knowing what it provides,
29:52um you get sometimes too high
29:53expectations. So being used to static
29:57types um in the in the way that say Java
30:00for example provides them, there is a
30:02certain class of type errors that I
30:03would expect a tool like dialyzer to
30:05catch, but just because dialyzer um has
30:08this specific approach of success
30:10typing, it will not flag these issues.
30:13So this is where people very often get
30:15get confused. Dialyzer did one decision
30:20very great, namely reducing the amount
30:23of false positives to zero. So when
30:26dialyzer is complaining, you can be
30:28pretty sure that actually there is
30:30something wrong with the code. It's not
30:32so easy to to debug once in a while if
30:34you get like several lines of debug
30:36output and need to compare very long
30:39type annotations or or type types for
30:42for function say to figure out in which
30:44of the parameter which option is
30:47actually the wrong one. There's been a
30:48lot of very nice work from the community
30:51and from the OTP team to highlight
30:53things and and make this more
30:54approachable. So this this is this is
30:56great. Then as the error messages are
30:59going into the right direction.
31:01If we can keep the idea of success
31:03typing only flagging not
31:05not flagging false positives, then we
31:07learn something from Dialyzer.
31:09>> From the Elixir side, is the new type
31:10system replacing like Dialyzer's
31:12philosophy or building on top of it? And
31:14also, where do success typing and
31:17gradual set theoretic typing actually
31:19agree and where do they actually start
31:20to diverge?
31:21>> Yeah, the Elixir type system is a
31:23replacement to Dialyzer. I would say
31:26that previously I was saying there are
31:28two aspects to type system. One is the
31:32technical ability of the system to find
31:34the bugs,
31:36all right. And
31:37Dialyzer does that
31:39very well. And
31:41this is
31:43something that
31:44we've we've done as well and I think we
31:47are on on par with the Dialyzer in in
31:49terms of bug finding.
31:51But the second aspect is the type
31:54language and the ability for the
31:55programmer to direct the
31:59the type the the type checker to to
32:03for the programmer to specify contracts
32:05on top of functions and for those
32:08contracts to be enforced in a strict
32:10way. And this is this is where Dialyzer
32:12is is not uh
32:16as a convenient as a as a normal type
32:18system because the way it has been
32:20designed is that it
32:23it sits in the middle of
32:25of
32:26of the programs and it builds this
32:29graph of
32:32dependency between between all the
32:34variables and then it looks at all the
32:36checks, the checks
32:38that are giving some type information
32:41like is integer is going to make
32:43variable integer and then it goes to
32:45look for in consti- inconsistencies
32:48between those.
32:50And
32:51with the
32:53with the system that we have designed,
32:55we are able to have
32:57also a top-down approach led by
33:00programmers that when they write a
33:02contract integer to integer on top of
33:04their function
33:06this this the body of this function is
33:09going to be um
33:11the type checker is going to go through
33:12it with the assumption that arguments
33:14are integers and it's going to enforce
33:17this
33:18in a more strict way. So, in in terms of
33:21um
33:22user of the design, it's um
33:25it's quite
33:27quite different.
33:28Uh
33:29I'd say that the the ability of Dialyzer
33:33to find bugs is something we've we've
33:36wanted to conserve. That
33:39and uh
33:41so, right now we haven't added the
33:44type annotations on top of functions, so
33:46we've been working on this type system
33:49in
33:51uh complete inference mode or dynamic
33:54mode.
33:55And
33:57so, that means that we've not we've not
34:00really allowed the type checker to
34:03reject programs uh instead we've made it
34:06give give out type warnings.
34:09And those type warnings they're
34:12the philosophy of
34:14of the current type warnings is that
34:16when you get a warning, 90% of the times
34:18it is because there is a bug that is
34:20definitely going to happen. In in the
34:23same same way that Dialyzer does. Um but
34:26yeah, in in the future we want to also
34:28have the the ability to for the type
34:32checker to say, well, this program
34:34doesn't uh compile or
34:36well, because you told me about its type
34:39and and those types are not are not
34:42working out.
34:42>> Anette, you've worked on CRDTs, you've
34:46worked actually we've worked on CRDTs
34:48together, you've worked on replication
34:50in distributed systems, formal
34:51verifications. Types are just one tool
34:54in your toolbox, not the whole answer,
34:56you know, so taking a step back from
34:58that broader vantage point,
35:01where do types sit in in this stack of
35:03things which make the beam software
35:06trust trustworthy, you know, are they a
35:08floor of a taller building or are they
35:10actually the foundation of that
35:11building? Doing much more than what it's
35:14daily users actually realize.
35:17>> I think there are two aspects to that.
35:18So, first of all,
35:21types help sometimes to restrict
35:24behaviors. So, if we assume for example
35:26that a function is only supposed to be
35:28working correctly if an integer is
35:29passed, then that's an assumption we can
35:31make and we can build arguments and
35:34verification tool chains based on these
35:37type of, yeah,
35:39guarantees that we get.
35:41So, my personal take is that we probably
35:45with with having with having the ability
35:47to type things, we will enable future
35:51verification works that can then build
35:54on top of that. And then there's a
35:56second aspect, namely that types are
35:58really not just for the programmer and
36:00for the documentation and so on, but
36:02they also have an effect on the runtime.
36:06Right now, the type annotations, if I if
36:09I recall correctly, that programmers add
36:12to their Erlang code will not and also
36:16for for the Elixir code, as far as I
36:17know, will not have influence on the on
36:20the execution engine, but in certain
36:23parts of the execution engine, types are
36:26actually derived and assumed to enable
36:29certain optimizations. So, these runtime
36:33optimizations could be done at a much
36:35more greater level if static type
36:38information was available because then
36:40we can kind of propagate this
36:41information from the code into the into
36:43the compiled version and then the
36:45runtime can make use of it, for example,
36:47when allocating space for things or when
36:50trying to parallelize things and so on.
36:51So, they might enable more than the
36:54community assumes.
36:57>> Uh Jose
36:58said it plainly at his Elixir Conf
37:00Europe talk in Malaga, the type systems
37:03do not mean error-free.
37:05But there's a real risk here. Developers
37:07see static types appearing their
37:09language, they get lulled into a false
37:11sense of confidence.
37:13They start writing less defensive code,
37:15fewer supervision trees, and less
37:18paranoia about failure. Even scarier,
37:21no recovery strategy. You know, these
37:24are the very things
37:26that make the programming model in the
37:28being reliable in the first place. Is
37:30there a concern that this could quietly
37:33erode? You know, how do you guard
37:35against that culturally and not just
37:38technically?
37:39>> I guess the fear is that programmers
37:41will start um
37:42writing a thousand line PRs and um
37:46uh accept that because it type checks
37:48that they can just send it or merge it
37:51and that but that's also the what what
37:54you want from a uh good good type
37:56system. You know, this sense of
37:58confidence that
37:59all the
38:01all the obvious errors have been have
38:03been tackled. But
38:05I think that
38:07this problem is
38:09in in in
38:11in the case of Elixir and Erlang,
38:13supervision trees, the the let it crash
38:16uh philosophy, and and all those
38:18recovery strategies that make give this
38:21fantastic up time. They they are not
38:24here to guard against type errors
38:27really. They are here to guard against
38:29the
38:30uh different kind of errors like
38:34conflicts or
38:36synchronization problems and um
38:39static types are are not going to
38:43are not going to make uh
38:45people get rid of these.
38:47I don't think so. So,
38:49I think per- perhaps it does not It's
38:51not the biggest
38:52the biggest danger there.
38:54>> We've basically established why, you
38:56know, this this can this why this work
38:58matters, what it's not trying to do, of
39:01course, what it's trying to do, but
39:03let's actually get into the the system
39:04that Guillaume and and his team is
39:06working on. What does it look like when
39:08it does work and where do you see like a
39:10lot of the strain when it's starting to
39:13work?
39:14>> When the type system starts working,
39:17you gain a level of control on your code
39:21which is
39:23very satisfying but but also has
39:27practical benefits because uh
39:30you become able to enforce those complex
39:33contracts over your code
39:35and
39:37it's going to um
39:39enable you to have uh uh
39:42for instance longer factoring, to have
39:45this this this power at your
39:47the tip of your fingers
39:49to know that actually you've
39:51successfully mutated the way a function
39:55call or function
39:58of
39:59of the logic of your program was working
40:01and
40:03that's uh
40:05that's on top of finding obvious bugs,
40:07right?
40:09Time where this can become
40:12a bit difficult is Uh,
40:15when the type system is not able to find
40:19uh
40:20why
40:21your program is
40:23actually correct. In a gradual
40:26type system, this is
40:28this is
40:29this is a problem. Or rather,
40:31when you're retrofitting a type system
40:33on top of dynamic language, it's um
40:36it's a danger because
40:38you're going to write, you know, good
40:40annotation on top of your function and
40:43uh unfortunately, the type system does
40:45not manage to find that in one branch of
40:49your program, one of your variables
40:52has a type integer instead and instead
40:55it thinks it has still has type integer
40:57or boolean.
40:59And so then you apply this you do I
41:02don't know plus one on this and it gives
41:04you a
41:06a warning. So this is the lack of
41:09precision of the system is that's why
41:12it's extremely important in what we're
41:15doing.
41:16Uh, because um
41:19if if this happens,
41:21then this means that
41:24the programmer
41:25is going to have to relax the safety
41:29that
41:29is expected of this function. For
41:32instance, you can wrap the input of your
41:35function in a dynamic. So you say
41:38okay, I was a
41:41uh writing the annotation that
41:44my function receives an integer or
41:46boolean and then does whatever. Instead,
41:49they can wrap it and say this is
41:52dynamic integer or boolean. Uh,
41:56both of those are dynamic. And this is
41:58going to relax the the system. So that
42:00now if this input is used as a list, you
42:03get an error, but
42:05now if it's used
42:07only as an
42:09as an integer, then uh
42:11the system is going to load this because
42:14it sees that it could be an integer at
42:16some point.
42:17So,
42:18I think when you start having to play
42:21with the
42:23limits of what the type system can
42:26express, this this is the difficulty.
42:28And
42:29in that case, um
42:31we're going to have to either provide
42:34clear warnings explaining, "Oh, well,
42:38this is a known um
42:40limitation of the system. You could
42:42perhaps try to
42:44rewrite this in this way, rewrite it in
42:46that way." But
42:48it's it's not obvious that we can think
42:50of all the possible cases in which this
42:52could fail. And otherwise, this is the
42:55reason why the the the way the type
42:57system works has to be uh well explained
43:00and understood by the programmer so that
43:03they can they can understand what's
43:05going wrong in a given situation. And it
43:08is better that
43:10the system is easy to understand so that
43:12they can think, "Oh, well, the system
43:15works that way and that way, so in this
43:16case it's not it's not going to be able
43:18to type my
43:20program, so
43:22I'm going to have to do it another way
43:24because
43:25because because of those those reasons.
43:28I I hope we've minimized those those
43:30instances, but they're they're going to
43:32they're going to exist."
43:33>> I'd like to go over one of the examples
43:35that Jose uses used in his talk before.
43:38It's a very simple function, basically
43:39it it's
43:40a function that takes in a string that
43:42splits on commas and then, you know,
43:44have basically a list with, you know,
43:46different size strings.
43:48And it returns the the largest string of
43:51those.
43:52Now,
43:53can we talk a little bit more about
43:54about this with regards to the type
43:55system? Because if you think about it,
43:57what happens when you pass in an empty
43:58list? What happens when you pass in,
44:00you know, like a string that doesn't
44:02have any commas? If you just pass in,
44:03you know, something that does have lots
44:05of commas, but maybe like nothing in
44:06between. How would the type system kind
44:09of help with this problem or
44:11do we have to kind of use your you
44:12talked about kind of like an escape
44:13hatch with dynamic, right? Would we need
44:15to rely on something like that?
44:17>> When it comes to very precise behavior,
44:21I don't know, for instance, imagine a
44:23program that works all lists except
44:26lists of size three.
44:29Uh and in that case it's going to crash.
44:32Well, there there are two two ways.
44:34Either you want your type system to be
44:37able to do this precise reasoning about
44:39the size of lists or you don't. And if
44:42you don't, then an easy way is that
44:46indeed you're going to work with dynamic
44:48lists.
44:49And all you're going to want from your
44:51type system is that you want it to check
44:53that, okay,
44:55I'm passing a list through my programs
44:57and not a
44:58tuple or and not a
45:01uh
45:02some not a
45:04struct
45:05And that's what you're expecting from
45:07your type system. You're
45:09You're not expecting your system to
45:10count the size of lists for you and uh
45:13uh
45:14you're not you're not expecting it to do
45:16all of this. And if you actually do want
45:20the type system to handle these kind of
45:22things, then sometimes it can mean that
45:25you're going to have to do a lot of lot
45:27of work. It's not necessarily that we
45:30can't express those things. We can
45:32actually uh
45:34in the theory of dependent types express
45:36a
45:38list of a given size
45:40or
45:42you know, express
45:44very precise integers uh
45:46the the the type of integers uh
45:49that are between two and five.
45:51Uh but the thing is that if you have
45:54this precision and you want to use it,
45:56then
45:58uh you
45:59you're starting not to write types,
46:01you're starting to write
46:03equations. Like you want to ensure that
46:07after this plus operation then your
46:10function is going to indeed have the the
46:12list of size of three and the
46:15type checker can help you but
46:18I think it stops at some point when you
46:21think that perhaps if you're doing this
46:24very precise thing you're not writing
46:27it's not
46:29it's not something that's important to
46:31the to the core logic of your program.
46:33>> Jose's talk laid out an argument that I
46:35want to test with both of you you know
46:37simple type systems are easy easy to
46:40learn
46:41easy to write signatures for they're
46:43fast to compile
46:45but they force you to push invariants to
46:48run time. Expressive type systems will
46:50catch more but the signatures explode in
46:53complexity error messages get worse and
46:56compile time suffer. He called it an
46:59inherent trade-off with no silver
47:01bullet. Dio, where did the Elixir team
47:04choose to sit on that spectrum and what
47:07and what made that the right point you
47:10have the right approach?
47:12>> I think that um
47:14the the big challenge in this work is
47:17that we're trying to answer the question
47:19is
47:21is a type system based on semantics of
47:23typing set the types or
47:27which is founded on that theory is it
47:30correct is it the right point in the
47:33design space for for programmers?
47:36And
47:37this is the the exact thing that is is a
47:40danger is that
47:42we are so precise that um
47:44the errors that are given or the
47:48the types that are inferred for
47:49functions
47:51they become too hard to handle. And I
47:53think we are sitting right at the
47:56at the
47:58right at the point where it it's it's
48:01good to understand. It's easy to
48:02understand. I think the notion that
48:05a type is either one or the other or
48:08both
48:10is
48:11is enough to present.
48:12And in order to reduce the complexity
48:15we've made some
48:16choices to limit
48:19representation of types.
48:22Those are choices that have been done
48:24for now. So they could
48:26potentially be changed. But for
48:28instance, we're we're not having a
48:30precise singleton integers
48:33because then you could express
48:35union of the integers between minus 10
48:38and minus five and
48:40five and 15 and have this whole
48:43machinery on on
48:45integers.
48:46And this may be not
48:49part of the language that
48:53that is required. You have we have atom
48:56singletons. So they are able to express
48:58the
48:59the way in which Elixir really uses
49:01those a lot to to have tagged tuples.
49:04So we we're trying to find
49:06the correct
49:09the simple enough place where we can we
49:11can say that the
49:13the system is both precise and still
49:15understandable by programmers. But this
49:17is a this is a constant effort, I think.
49:20There are some bug
49:22There there have been some bug
49:24bugs reported as issues in the
49:27in the type check in the in the compiler
49:29before that where it was just a giant
49:32union
49:34this was
49:36because we weren't
49:37simplifying of course, but
49:40seeing the type checker produce a giant
49:43giant type is is a
49:45is
49:47one of my personal fears, I would say.
49:49>> And you're building Dialyzer on
49:53for Erlang on the same theoretical
49:54foundation, but with different design
49:57priorities. Do you land at the same
49:59point on that spectrum or or somewhere
50:01different? And if different, why?
50:03>> We land at a slightly related point, but
50:05not exactly the same point. When
50:08designing Etilizer, we made a very
50:10conscious decision to keep the type
50:13specs as Erlang code and also Elixir
50:16code and still has, right? So, our
50:19assumption was that programmers can use
50:22with the type language with the type
50:25specification annotations that come with
50:27the Erlang standard. That these are the
50:29tools that allow them already nowadays
50:32to express what their functions, for
50:34example, are supposed to do. And we
50:37didn't want to have too many moving
50:38parts, so this was kind of the
50:39assumptions. Let's try to take code with
50:42its type annotations as it is and see
50:43how far we get. It turned out that
50:45unions, intersections are pretty
50:48important,
50:49but even numbers, like the the union uh
50:52the singleton types that Jim just
50:53mentioned, um do occur. So, like in the
50:56standard library, there are, I think, um
51:00something like a couple of hundred
51:02annotations where we rely on these
51:05singleton types. And the question is, do
51:07we want to uh deviate from that or not?
51:10Our decision was uh was to stay with it.
51:13Um other than that, the set theoretic
51:14types turned out to be, I think, the the
51:16the right theoretic foundation for
51:19approaching this type checking for the
51:21beam languages.
51:22>> Both type checkers have gradual typing
51:24on top.
51:25Why does set theoretic typing buy you
51:29You know, what what what does set
51:30theoretic typing buy you
51:33that you couldn't have gotten here from
51:35a more traditional type system?
51:37>> So, for me, it's really this this
51:38combination of these different this
51:40different expressiveness that you get
51:42with union type, with intersection
51:44types, and also with singleton types for
51:46for example for the atoms. Gradual
51:48typing is as as Guillaume mentioned is
51:51is required to help
51:54programmers and not require them to
51:57annotate every single line or every
52:00single function in a module with a type
52:02and be overly precise when it's not
52:05needed, right? So, gradual typing is is
52:08for practical reasons I think
52:09unavoidable. The combination of
52:11different aspects that you can have with
52:13set theoretic types makes makes them
52:15very, very powerful and they're also
52:16good mental model for describing values
52:19in the language.
52:20>> Intersection and unions they are the
52:21user-facing types, but there is also
52:24differences
52:26that are
52:28expressible using set theoretic types
52:30and they have
52:31particularly important value on the
52:33technical aspect of
52:36checking programs because they allow you
52:38to precisely analyze pattern matching.
52:42So, you have different clauses and they
52:45do pattern matching and uh
52:47you're able to compute the type of the
52:50first clause and in the second clause,
52:53you know that the type of values that
52:55enter this second clause, it's all the
52:57ones accepted by the pattern minus the
53:00ones accepted by the first clause. And
53:04this difference we're able to express it
53:06at the type level and this
53:09this gives us a lot of precision. It
53:11allows us to give exhaustiveness
53:13exhaustivity warning or it allows us to
53:16detect branches that are never going to
53:17run because all the values were already
53:20caught by previous clauses. And so it is
53:23not necessarily
53:25very present in annotations although
53:28although it can it can definitely, but
53:30from the technical
53:31point of thing it's it's really
53:33important
53:34and uh
53:35it's I think it's uh
53:38also one of the less uh,
53:41it's something that does not exist in
53:44other languages that have introduced
53:46ways to do unions and sometimes
53:49intersections in in in a bit of an ad
53:52hoc way.
53:53>> So, you both mentioned process
53:55boundaries as one of the hard problems.
53:57And and that's where I want to take the
53:58conversation next that's where Alan and
54:00I want to take the conversation next
54:02because the Beam's whole identity is
54:04built on process and message passing.
54:07And and and that yeah I suspect that is
54:09your territory.
54:11>> Everything we've talked about so far
54:13happens inside of a single process. Now,
54:15the moment that a message crosses a
54:16process boundary or worse a network
54:19boundary to another node, what changes
54:21for the type system and what does it
54:23stop being able to to tell you?
54:26>> So, this is for us typically the the
54:28boundary where you have to switch or
54:31where you typically would switch to
54:32dynamic because you don't exactly know
54:34what type of message to expect. There
54:36are type there are type systems that
54:38deal with these aspects that try to
54:41approach typing of
54:46line of work on on mailbox types that
54:48one of our students here is is is
54:50looking at. There are session types that
54:52help in dealing with understanding what
54:54type of messages are passed between
54:56processes in as part of a of a protocol.
54:59We started integrating some of the these
55:03ideas so kind of a poor man's approach
55:05for mailbox types if you want to wanted
55:07to say so. This is ongoing work and we
55:09are able to kind of make some progress
55:12on that but there are inherently some
55:15some limitations. Yeah, so if if your if
55:17your message can deal sorry if your
55:20receive can deal with a lot of different
55:21type of messages and you don't know what
55:24you get, you lose preciseness at some
55:26point.
55:27>> Let's set aside what's pragmatic to ship
55:29this year. You know, 10 years out, what
55:31do you personally hope the Beam looks
55:32like? So, effect session types,
55:35dependent types, you know, deeper
55:37verification or something new you which
55:40has not been named yet.
55:43Which of these if any do you actually
55:45expect to arrive?
55:46So let's start with Annette first.
55:48>> My personal guess is that we will see
55:50more work towards deeper verification
55:53approaches just because generating code
55:58becomes much simpler. We can have a
56:00large number of modules you know
56:02generated without completely
56:03understanding what they do. So
56:06programmer supporting programmers in
56:08getting confident about their code is I
56:11think the the most important thing that
56:13we need to address in programming
56:15languages in the in the next couple of
56:17years and verification is in its very
56:20many different forms
56:22will be exactly this. If we have good
56:24tools that help us verify behavior, we
56:27can be sure that the code actually does
56:31accordingly.
56:32>> My [snorts]
56:33answer is similar to
56:35Annette's. I think that um
56:38a fantastic uh
56:40uh state would be
56:42that uh the type system
56:45evolves
56:46and
56:48becomes able to be to serve as
56:50infrastructures for more complex
56:53techniques.
56:54So I could imagine for instance that you
56:58have a
56:59light
57:00typing mode for a program that finds a
57:04common type errors and then and that
57:07you can
57:09at some point mark that there is going
57:12to that the
57:14the proof for some function for instance
57:16that this function's logic is correct
57:18because it's implementing a sorting and
57:22you want to
57:23to know that the sorting is going to be
57:25correct that this is then delegated to
57:27to some other tool that provides deeper
57:30verification. Ideally, I think that um
57:34uh type system is made to be uh nice to
57:38deal with from the programmer's point of
57:41view. So, ideally, you would you would
57:43use the type system and then and then um
57:46delegate, but your main interface would
57:48be would be the type system for those
57:50for those deeper processes. I think
57:53also, one very interesting question for
57:56me is uh what is the good
58:00way to um
58:03bring these uh more complex
58:07uh ways
58:08to deal with um sending messages and and
58:11all of these. For instance, uh session
58:13types are a thing in the in the theory
58:16of typing concurrency. And the question
58:19is how
58:21what form would it take to bring these
58:23these verification techniques to to uh
58:26language as Elixir, which is which which
58:32like uh would it take the form of
58:34annotations? Would it be simple enough
58:36to understand? And would it bring would
58:39it cover the use case that that people
58:40need? Right?
58:41>> Very quickly, right? If we were to kind
58:43of sum up this whole conversation and
58:44what you've learned, what's one thing
58:46that you wished every Beam developer
58:48understood about types? And one thing
58:51you you wished every type system
58:53researcher could understand about the
58:54Beam. Uh let's go to Annette first.
58:57>> Uh types don't hurt. There is a certain
58:59learning curve, but there's a lot of
59:00things that you actually get from it.
59:02So, trying to hit the sweet spot between
59:05too much work on the type annotations
59:08and yeah, the nice guarantees and the
59:10confidence in the in the work that you
59:12get. I think this is something that I
59:13would hope for many programmers that are
59:16now refraining from use types from using
59:18types because they seem too complex or
59:21complicated. It's not as bad as it as it
59:23might seem might seem to be. Right?
59:25>> That uh
59:28the point of a static type system for
59:31for for the beam is to catch the
59:34the one path out of a hundred that is
59:38going to
59:39uh fail because the destruct at at this
59:42point or at this map at this point
59:45doesn't have does not have the given
59:47field anymore. And so, what we're
59:49helping with this the the the really
59:51edge cases those uh things that even a
59:55very well-designed library and a very
59:58well-designed
1:00:00project
1:00:01is going to have struggles with. And uh
1:00:05this is
1:00:06rather than
1:00:08promising a
1:00:09fight against a
1:00:10very complex logic design that to
1:00:14uh to make sure you don't write bad
1:00:15code. I think
1:00:17this
1:00:18this is a
1:00:20interest
1:00:21of types for the beam. And you said, I
1:00:23think, what should researchers
1:00:25understand about the beam? For me, what
1:00:27I understood is that the the beam is a
1:00:29is is stronger than me and uh the the
1:00:32runtime at
1:00:35uh
1:00:36the the importance of the
1:00:38of the quality of the runtime is a
1:00:40something that is
1:00:42that is a
1:00:44it's it's the first it's the main point
1:00:46of a of a language. And
1:00:48the role of a type system is to support
1:00:51that
1:00:52uh
1:00:53rather than
1:00:55restrict it. And if you have a
1:00:57runtime that is so excellent that you
1:01:00can afford to program in a dynamic way
1:01:03with a pattern matching
1:01:05or by um
1:01:07uh having message passing and or having
1:01:10all those extremely dynamic, very hard
1:01:13to type features that Elixir or Erlang
1:01:15have, then the role of the type system
1:01:17is going to get on their get on their
1:01:19level.
1:01:20>> The The beam ecosystem is actually great
1:01:22for research. Yeah, we have real world
1:01:24problems that have been high impact. We
1:01:26have a a long-standing community and the
1:01:30languages are very active, right? So,
1:01:32the community is active, the languages
1:01:34are evolving. There is no need to assume
1:01:37that the beam is obsolete in any way. I
1:01:40would I would rather claim it's getting
1:01:42more and more important with with every
1:01:45cloud server that runs some some Erlang
1:01:48or Elixir code, right? And there is a
1:01:50great opportunity to um make a point and
1:01:52have impact with the research that you
1:01:54do.
1:01:54>> So, Adnan and Guillaume, you know, thank
1:01:56you both. Yeah, this has been exactly
1:01:58the conversation I was hoping for. You
1:01:59know, we've got two amazing researchers
1:02:01from sister projects who spent years
1:02:03thinking hard about the same problem,
1:02:05but you know, from different angles. And
1:02:08what I'm personally taking away from the
1:02:11last hour, I hope the listeners too, is
1:02:13that the type system arriving in Elixir
1:02:161.2
1:02:17isn't the end of a 30-year argument
1:02:19about typing on the beam. It's actually
1:02:22the moment that argument finally has a
1:02:24theoretical foundations and the
1:02:25engineering pragmatism to move forward
1:02:28together. So,
1:02:30if you want to be part of where this
1:02:31goes next, the most useful thing you can
1:02:34do this week is to try Elixir 1.2
1:02:36release candidate, you know, read
1:02:37Adnan's, you know, same same but
1:02:39different paper to understand the
1:02:41broader landscape, and report back what
1:02:44works and what doesn't.
1:02:46You know, I think both teams generally
1:02:48want the feedback. So, yep, thank you
1:02:50for so much for listening. Don't forget
1:02:53to subscribe. And for the record, this
1:02:55podcast was recorded on May 28th, 2026.

About this transcript

This page contains the full transcript of Static Types Finally Come to the BEAM | Annette Bieniusa & Guillaume Duboc by BEAM There, Done That, generated from the public captions YouTube serves with the video. The transcript has 9,655 words across 1,644 segments, with the original timestamps preserved so you can click any line to jump to that moment in the embedded player.

What you can do with it

Use the transcript to take notes, quote the speaker, build a study guide, generate a summary with ChatGPT or Claude via the YouTube Summary tool, or export it as a timed subtitle file with YouTube to SRT. You can also re-open it in the transcriber to translate the transcript into 100+ languages.

Free YouTube transcript tool

YouTube2Text is a free YouTube transcript generator — no signup, no daily limit. Paste any YouTube link and get the full transcript instantly, with timestamps, click-to-jump, translation to 100+ languages, AI prompts for ChatGPT, Claude, and Gemini, and exports to TXT, SRT, VTT, or Markdown.