Wow, congrats to the Elixir team for all the work that went into this! There’s a paper that covers a lot of the theory that went into making this happen, as well as an accompanying blog post. I’m looking forward to trying out the type system.
From what I understand, they are using the same approach. The foundations of set-semantic type theory have been researched extensively prior to both papers (e.g. Castagna’s publications). Lanvin’s thesis contributes by providing a framework for gradual typing. The elixir paper then takes Lanvin’s research (along with the research of many others) and applies it to the elixir language.
From “Gradual Typing Guarantees” on page 18:
[… elixir uses] an approach known as sound gradual typing. This approach was developed for set-theoretic types in Lanvin’s PhD thesis
I’m not an expert here, so someone else might be able to provide better insight.
From what I know, elixir’s approach is a (reasonably) sound one right?
As in, if I say a function takes a number, I can’t get pass it a string at runtime calling from an untyped boundary?
I’m ok with an escape hatches in extreme cases, but in typescript you can just declare untyped variables as anything with no complaints - I have seen the horror in many people’s eyes when I informed them at unless you pull in a schema validation library there is no default runtime validation in typescript.
I am really excited to hear about how this works in practice, while typescript has been a huge success, it’s depressing to realize in practice it mostly just catches typos & making my editor much better to use.
From what I’ve heard of it, Elixir’s gradual typing approach is to combine 3 different features already in the language: typespecs, pattern matching in functional declarations, and guards.
typespecs are compile-time thing. They just say “this function should take in integers a and b, and produce a string c” there were tools for checking them, but they were optional, and… a bit lacking.
The other parts are checked at runtime, as you can use them for multiple dispatch:
def factorial(x) when x > 0 do
x*factorial(x-1)
end
def factorial(0) do
1
end
the “when” statement is a guard, and the 0 in factorial(0) is a pattern. Together, they decide which definition of factorial to use for a given call: factorial(5) would use the top one, since 5 is greater than 0, factorial(0) would use the bottom one, since 0 matches the pattern 0, and factorial(-1) would cause the calling process to crash, because there’s no valid function definition for factorial(-1).
Gradual typing is the best of both worlds IME outside of systems languages or other specialized usecases, as an early adopter of TypeScript after years with C# and Python. (edit: not with Python’s gradual type system, see the replies, this generalization doesn’t hold)
You can run any code you want, regardless of what the typechecker says, which is hugely beneficial for exploring ideas and APIs and moving fast. You can pull the typesafety lever as much or as little as makes sense for the context at hand. Pull the lever enough, and you can get language-maximal typesafety within the bounds you define. If you’re writing something quick and dirty, let the lever go if it’s ever inconvenient, but it’s still there to assist you for most things.
The arguments against it often make perfect the enemy of good, or express a distrust that developers can’t decide the right amount of safety for their problem.
Gradual typing is fantastic, I’m glad to see Elixir buy in.
I agree that gradual typing is conceptually an excellent approach. I’ve also observed that many developers who use gradually typed Python have become unable to choose the right amount of typing for each piece of code.
The way IDEs and language servers work make untyped code feel different, and worse in many cases, so there’s a natural push to apply types to everything — even to the detriment of clarity and succinctness. Ultimately the people who are maximalist typers win the arguments, analogous to the use of unsafe in Rust, perhaps?
So although I love the idea of gradual typing, I think as soon as you introduce type signatures to a dynamic language you start on a path to lose its essence and change the community’s philosophy. Sometimes that’s good (TypeScript), other times it’s bad (Python).
For Elixir I have no idea but I wish them luck and hope it brings their community more success.
So although I love the idea of gradual typing, I think as soon as you introduce type signatures to a dynamic language you start on a path to lose its essence and change the community’s philosophy. Sometimes that’s good (TypeScript), other times it’s bad (Python).
I agree it was good in JS, though I think we’d kind of moved away from being really dynamic already, but didn’t have the types system. What makes it bad for the same change to happen in Python?
I can see that, to clarify I have no experience with Python’s gradual typing, and I have heard a lot of negativity around it. Not every language and ecosystem will benefit the same, so gradual typing = good is a generalization that’s wrong in some cases. Agreed that TypeScript makes it shine.
I would love to better understand why exactly TypeScript shines, whereas Python’s gradual typing doesn’t. From my limited experience with Python, the type hints feel clunkier, whereas TypeScript is a joy to use. But I have no idea why they feel that way.
I have not seriously used either, but I got the impression from Python that it’s bolting on a ‘90s style nominal type system. A big part of the reason that languages like JavaScript, Ruby and Python became popular is that these are clunky and annoying to use. In contrast, TypeScript as a modern structural type system with algebraic types. If you’re encoding JSON, for example, then an algebraic type system lets you specify that every object is either an array, a dictionary, a string, or a number. That’s precisely the constraint that you want. If you’re serialising to JSON then you may want a guarantee that the object that you’re serialising has a toJSON method that returns one of these types. This is the kind of thing that’s easy to express with a structural type in an algebraic type system.
These are both pretty trivial examples but my (recent) experience working with structural and algebraic type systems is that they let me keep the loose coupling and generic behaviour that I love in dynamic languages, but are still amenable to efficient implementation in ahead-of-time compiled languages. The latter is not important for Python or TypeScript, but the former is.
This makes a lot of sense. One of my favorite things about TypeScript is that I can opt into degrees of nominal typing with “flavored” and “branded” types. I prefer flavored over branded in almost all cases and use it a lot.
Yup, the combination of nominal and algebraic types can be very powerful. In Verona, we are going a slightly different way that I hope will give you the properties that you want. We’ll see if it works:
Classes define concrete types. All concrete types are nominal. If you have a class C1 and you request a thing of type C1 then it will be an instance of that class. Any class implicitly implements any interface that defines a set of requirements that it.
Interfaces support subtyping but classes do not. If C2 inherits from C1 then it is not a subtype of C1. Inheritance is purely about code reuse. That said, if C1 implements interface I1 then, a subclass of it probably will as well. You can define an interface that people must comply with and you can also give them a class that they can choose to subclass (or not) to give them some bits of the implementation for free. You can inherit from multiple classes (making classes somewhat more like traits than traditional classes).
This means that you can write types like C1 | C2 | I3, which will either be an instance of class C1, an instance of class C2, or an instance of some class that implements interface I3. This also leaves us some useful space for optimisations in the implementation. If you write C1 | C2 then we can either:
Implicitly create an interface type for these two (with the common methods and methods for pattern machine to C1 or C2) and emit a vtable. We can use selector colouring to make that just the vtables of C1 and C2, so we get dispatch overheads comparable to C++ virtual functions.
Carry the pointer around with a discriminator bit and directly call the implementation from C1 or C2. This increases code size but also increases the set of potential optimisation opportunities and plays slightly better with modern branch predictors.
We can make this decision at any point in the compilation pipeline, so can can start with option 2 and then decide that there aren’t any big wins and transform to the other representation.
I’ve been wondering the same since posting this, I suspect it’s a mix of idiomatic Python being less friendly to types compared to JS, and TypeScript being extraordinarily well-designed.
I think it’s those two points and also that many people hated using JS before TypeScript came along. TS made it palettable for a wider audience. But people generally loved Python before typing came to the language. It wasn’t maligned in the same way. It wasn’t broken and in need of fixing. Adding types hasn’t broadened its appeal.
Oh yeah, “JS is lacking for ambitious software” should have been my first thought! And david_chisnall’s point about the structural/algebraic systems resonates.
Super excited for this! Always loved OTP and Elixir, but were missing the IDE support (proper autocomplete) and assurances of static typing (as in Java/Elm). Was tempted by Gleam.
If they roll this out and it works better than Sorbet that’d be another reason for me to try using Phoenix instead of Rails, especially because the creator of Elixir worked on Devise. For now the library and documentation situation for Rails is so much better, but Sorbet really sucked last time I tried it—random errors on a fresh project and an ugly syntax.
Wow, congrats to the Elixir team for all the work that went into this! There’s a paper that covers a lot of the theory that went into making this happen, as well as an accompanying blog post. I’m looking forward to trying out the type system.
There is also Victor Lanvin’s PhD thesis, which goes into far more detail: https://vlanvin.fr/papers/thesis.pdf.
Are they not using a different approach? I haven’t read either paper in detail, but it seems like the Castagna paper builds a new foundation?
From what I understand, they are using the same approach. The foundations of set-semantic type theory have been researched extensively prior to both papers (e.g. Castagna’s publications). Lanvin’s thesis contributes by providing a framework for gradual typing. The elixir paper then takes Lanvin’s research (along with the research of many others) and applies it to the elixir language.
From “Gradual Typing Guarantees” on page 18:
I’m not an expert here, so someone else might be able to provide better insight.
From what I know, elixir’s approach is a (reasonably) sound one right?
As in, if I say a function takes a number, I can’t get pass it a string at runtime calling from an untyped boundary?
I’m ok with an escape hatches in extreme cases, but in typescript you can just declare untyped variables as anything with no complaints - I have seen the horror in many people’s eyes when I informed them at unless you pull in a schema validation library there is no default runtime validation in typescript.
I am really excited to hear about how this works in practice, while typescript has been a huge success, it’s depressing to realize in practice it mostly just catches typos & making my editor much better to use.
From what I’ve heard of it, Elixir’s gradual typing approach is to combine 3 different features already in the language: typespecs, pattern matching in functional declarations, and guards.
typespecs are compile-time thing. They just say “this function should take in integers a and b, and produce a string c” there were tools for checking them, but they were optional, and… a bit lacking.
The other parts are checked at runtime, as you can use them for multiple dispatch:
the “when” statement is a guard, and the 0 in factorial(0) is a pattern. Together, they decide which definition of factorial to use for a given call: factorial(5) would use the top one, since 5 is greater than 0, factorial(0) would use the bottom one, since 0 matches the pattern 0, and factorial(-1) would cause the calling process to crash, because there’s no valid function definition for factorial(-1).
Gradual typing is the best of both worlds IME outside of systems languages or other specialized usecases, as an early adopter of TypeScript after years with C# and Python. (edit: not with Python’s gradual type system, see the replies, this generalization doesn’t hold)
You can run any code you want, regardless of what the typechecker says, which is hugely beneficial for exploring ideas and APIs and moving fast. You can pull the typesafety lever as much or as little as makes sense for the context at hand. Pull the lever enough, and you can get language-maximal typesafety within the bounds you define. If you’re writing something quick and dirty, let the lever go if it’s ever inconvenient, but it’s still there to assist you for most things.
The arguments against it often make perfect the enemy of good, or express a distrust that developers can’t decide the right amount of safety for their problem.
Gradual typing is fantastic, I’m glad to see Elixir buy in.
I agree that gradual typing is conceptually an excellent approach. I’ve also observed that many developers who use gradually typed Python have become unable to choose the right amount of typing for each piece of code.
The way IDEs and language servers work make untyped code feel different, and worse in many cases, so there’s a natural push to apply types to everything — even to the detriment of clarity and succinctness. Ultimately the people who are maximalist typers win the arguments, analogous to the use of unsafe in Rust, perhaps?
So although I love the idea of gradual typing, I think as soon as you introduce type signatures to a dynamic language you start on a path to lose its essence and change the community’s philosophy. Sometimes that’s good (TypeScript), other times it’s bad (Python).
For Elixir I have no idea but I wish them luck and hope it brings their community more success.
I agree it was good in JS, though I think we’d kind of moved away from being really dynamic already, but didn’t have the types system. What makes it bad for the same change to happen in Python?
Did you see this post last year? I think it captures it pretty well.
https://lucumr.pocoo.org/2023/12/1/the-python-that-was/
I can see that, to clarify I have no experience with Python’s gradual typing, and I have heard a lot of negativity around it. Not every language and ecosystem will benefit the same, so gradual typing = good is a generalization that’s wrong in some cases. Agreed that TypeScript makes it shine.
I would love to better understand why exactly TypeScript shines, whereas Python’s gradual typing doesn’t. From my limited experience with Python, the type hints feel clunkier, whereas TypeScript is a joy to use. But I have no idea why they feel that way.
I have not seriously used either, but I got the impression from Python that it’s bolting on a ‘90s style nominal type system. A big part of the reason that languages like JavaScript, Ruby and Python became popular is that these are clunky and annoying to use. In contrast, TypeScript as a modern structural type system with algebraic types. If you’re encoding JSON, for example, then an algebraic type system lets you specify that every object is either an array, a dictionary, a string, or a number. That’s precisely the constraint that you want. If you’re serialising to JSON then you may want a guarantee that the object that you’re serialising has a toJSON method that returns one of these types. This is the kind of thing that’s easy to express with a structural type in an algebraic type system.
These are both pretty trivial examples but my (recent) experience working with structural and algebraic type systems is that they let me keep the loose coupling and generic behaviour that I love in dynamic languages, but are still amenable to efficient implementation in ahead-of-time compiled languages. The latter is not important for Python or TypeScript, but the former is.
This makes a lot of sense. One of my favorite things about TypeScript is that I can opt into degrees of nominal typing with “flavored” and “branded” types. I prefer flavored over branded in almost all cases and use it a lot.
Yup, the combination of nominal and algebraic types can be very powerful. In Verona, we are going a slightly different way that I hope will give you the properties that you want. We’ll see if it works:
Classes define concrete types. All concrete types are nominal. If you have a class
C1and you request a thing of typeC1then it will be an instance of that class. Any class implicitly implements any interface that defines a set of requirements that it.Interfaces support subtyping but classes do not. If
C2inherits fromC1then it is not a subtype ofC1. Inheritance is purely about code reuse. That said, ifC1implements interfaceI1then, a subclass of it probably will as well. You can define an interface that people must comply with and you can also give them a class that they can choose to subclass (or not) to give them some bits of the implementation for free. You can inherit from multiple classes (making classes somewhat more like traits than traditional classes).This means that you can write types like
C1 | C2 | I3, which will either be an instance of classC1, an instance of classC2, or an instance of some class that implements interfaceI3. This also leaves us some useful space for optimisations in the implementation. If you writeC1 | C2then we can either:C1orC2) and emit a vtable. We can use selector colouring to make that just the vtables ofC1andC2, so we get dispatch overheads comparable to C++ virtual functions.C1orC2. This increases code size but also increases the set of potential optimisation opportunities and plays slightly better with modern branch predictors.We can make this decision at any point in the compilation pipeline, so can can start with option 2 and then decide that there aren’t any big wins and transform to the other representation.
I’ve been wondering the same since posting this, I suspect it’s a mix of idiomatic Python being less friendly to types compared to JS, and TypeScript being extraordinarily well-designed.
I think it’s those two points and also that many people hated using JS before TypeScript came along. TS made it palettable for a wider audience. But people generally loved Python before typing came to the language. It wasn’t maligned in the same way. It wasn’t broken and in need of fixing. Adding types hasn’t broadened its appeal.
Oh yeah, “JS is lacking for ambitious software” should have been my first thought! And david_chisnall’s point about the structural/algebraic systems resonates.
Super excited for this! Always loved OTP and Elixir, but were missing the IDE support (proper autocomplete) and assurances of static typing (as in Java/Elm). Was tempted by Gleam.
If they roll this out and it works better than Sorbet that’d be another reason for me to try using Phoenix instead of Rails, especially because the creator of Elixir worked on Devise. For now the library and documentation situation for Rails is so much better, but Sorbet really sucked last time I tried it—random errors on a fresh project and an ugly syntax.
There is a tracking issue for further development of this feature here: https://github.com/elixir-lang/elixir/issues/13227
Why did they announce the feature before finishing implementing?
They announced it a super long time ago. The featureset in place now is finished and will not be removed.
But the linked issue was made last week, and there are lots of essential items missing.
That tracking issue is for features beyond the MVP. The missing features aren’t considered essential, although I agree they are important.