Type system updates: moving from research into development
elixir-lang.org
elixir-lang.org
Given that, I'm excited to see how this works out. Adding static types has the potential to be very disruptive but I trust the team to do it in a way that will work very well with existing Elixir apps and the BEAM VM.
Gleam from Day 1 is going to be statically typed using a Hindley-Milner type system/Algorithm W. It's battle tested. If you come from a lang like Rust, OCaml, Standard ML, etc its type system is going to be very familiar to you.
So I don't think this will have too much effect on Gleam.
> The type system will extract type information from patterns and guards to find the most obvious mistakes, such as typos in field names or type mismatches from attempting to add an integer to a string, without introducing any user-facing changes to the language.
> By propagating types from structs and their fields throughout the program, we will increase the type system’s ability to find errors while further straining our type system implementation.
Congrats to them.
I still wish it had been implemented 10 years ago, but, hey, that train has sailed a long while ago. (I know, trains dont sail. Or, as we say in Elixir-land, "** (MatchError) ...")
I got into Elixir because it is dynamically typed. I wouldn't have considered a statically typed one. Luckily I find enough customers with Ruby and Python. The last Elixir project was from a couple of years ago. I didn't have to use something statically typed since 2012, I think. Too tiring to write.
Ruby did influence the syntax and the names in the standard library, but the latter was also done in a more "democratic" fashion: I would look into Ruby, JavaScript, Clojure, Haskell, and choose a name that was common and closer reflected the semantics that would fit Elixir (for example, the term "protocol" come from Clojure).
The most curious case is the "Regex" module (which is named Regexp in Ruby). I quickly noticed that both "regex" and "regexp" were very common, Erlang simply used "re", so I had no clear direction to lean towards. The decision came by getting the top 50 languages at the time and using Rosetta Code to pick the most common term (which was regex).
He seems to have written a ton of interesting stuff on PL theory!
But I'm entirely unsure. Maybe it is completely unrelated to why set theory is used as a basis here. Just wondering.
https://twitter.com/BartoszMilewski/status/16743572724981104...
Having least structure is a soft/aesthetical statement, and the explanation is right after it (a correct definition).
I wish all the math looked like this, first a soft/aesthetical statement, then right after the correct math.
[1] https://mathstodon.xyz/@johncarlosbaez/110631013611448277
The category of sets is different from this lattice, since it allows arbitrary functions between sets for its morphisms rather than just inclusions.
"Set-theoretic types" have a meaningful notion of overlap. Usually types in other type system tend to be practically disjoint, like objects in a concrete category might be sets but the category itself doesn't give language to check whether the objects are disjoint sets.
A set cannot be part of itself in an axiomatic formulation of set theory. Naïve set theory, one that allows an unrestricted general comprehension, has been thoroughly rejected.
This isn't quite true. In practice, you're correct: "set theory", generally referring to ZF (or some closely related derivative thereof) with the Von Neumann Universe, doesn't allow sets to contain themselves. But it is possible to axiomatize set theory where sets can contain themselves [0].
This replaces the axiom of foundation with the axiom of anti-foundation [1], so it's not naive set theory but it is an axiomatized non-well-founded set theory.
[0]: https://plato.stanford.edu/entries/nonwellfounded-set-theory...
[1]: https://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axio...
In practice, you usually need either a definite sum.type (int | str | null), or the all-encompassing type, like Any. I think both cases should be adequately representable in a categorial language — am I wrong?
You may need to represent a sum type that includes Any (or a similar type) if you.allow type-based signature overloads for functions. I wonder if this may represent any obstacle to a caregorial approach.
Practically all other paradoxes can be reduced to one of these two.
This research paper by Giuseppe Castagna presents an in-depth exploration of programming with set-theoretic types, which include union, intersection, and negation type connectives. The author argues that these types are not just useful, but necessary for typing some common programming patterns, and they play a crucial role in precisely typing various language constructs, from branching and pattern matching to function overloading and type-cases.
What sets this work apart is the extension of the theory of types known as semantic subtyping to include polymorphic types. This is a significant step forward as it allows for a more expressive and precise type system. The paper also discusses the design of languages that use these types and presents a theoretical framework that covers all the examples given in the presentation.
one of the key takeaways from this paper is that current programming languages are unable to infer intersection types for functions without explicit annotations. This is a limitation that could impact the development and efficiency of certain programs. The author presents three effective restrictions of this system, each with its own trade-offs, which could potentially guide the design of future programming languages.
The paper concludes with an overview of other aspects of these languages, such as pattern matching, gradual typing, and denotational semantics. These insights could have far-reaching implications for the development of more expressive and precise programming languages.
this paper pushes the boundaries of what we understand about type systems in programming languages, Elixir is going to be the first general purpose language to implement such a type system.
Just out of curiosity. What other options?
As much as I appreciate the work the team has done, I think we have to be honest about the good and bad parts. ElixirLS has never worked quite right for me, or most other Elixir developers I know. It's often painfully slow to respond even in small project, it often gets stuck in obscure failures that require an editor reload to get it fully working again. If you run into any kind of issue with it, the boilerplate response it always: Try running `rm -rf .elixir_ls _build` which sometimes works, but usually not.
Javascript, Typescript have immaculate tooling in this regard, same goes for Java, C#, Go, even Python (on IDE side, the package management situation is of course a dumpster fire). I'd go as far as to say that any language supported by Jetbrains has better tooling than Elixir does.
Check out next-ls aims to replace ElixirLS.
https://www.elixir-tools.dev/next-ls/
There's a podcast/interview from its creator below.
macOS only, closed source, and VC funded :(
I don't work on a Mac, so it's a non-starter for me, but I'd be very reluctant to switch my workflow to an early stage VC funded product because I don't like having my rug pulled.
I had that problem with NeoVim's Mason plugin that manages language servers, then I just cloned `elixir-ls` and made a super small script to update it daily from GitHub and recompile it. I use that in NeoVim instead and it works near-instantly. Give it a try.
I don't disagree that IDE support can look subpar but I'd also venture a guess that proper IDE support is very first-world problem. You won't find yourself working on projects with millions of lines in Elixir ever, and thus not having e.g. full-blown IDE refactoring has never been a problem for me or any other Elixir dev I know.
All that being said, literally nothing I have ever saw was able to beat Golang's and OCaml's language servers. They just work and are amazingly fast to boot. It's simply a joy coding in those languages with their LS. Rust is trailing closely behind but it's also a fact that its LS is objectively slower -- still, they seem to have made a lot of strides on that front lately and it's much better compared to even one year ago.
Me too!
Have you learned any tricks for getting up to speed on large code bases with very limited static typing?
In recent years I've mostly worked on large, complex Python systems. The consequences of (undisciplined) dynamic typing not only sapped my joy in programming, it really burned me out.
Some people are really good at living with code bases like that. I'm not one of them, but I'm still hoping to find some way to bridge the mental gap.
For me it didn't go that far, fortunately, because I managed to jump ship on time... But it was getting _tiring_.
> Have you learned any tricks (...)?
My current apprach is: don't. These days I usually work in Rust, C# and sometimes Typescript. I'm only open to working with dynamically typed languages for short periods of time, as a side quest of the main task (e.g. for my last contract I had to read quite some C code, which somewhat resembled dynamically typed code, but I spent even more time writing Rust, so it was OK).
Eh, thanks. That's my approach as well. I was just hoping for some silver bullet I guess.
The drawbacks to statically typed languages have become way less significant since most of them have "var" or an equivalent which saves on typing.
Imagine if Typescript's type system if it were actually sound.
The research paper is here if anyone wants to read it. https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
#define let __auto_type
https://gcc.gnu.org/onlinedocs/gcc/Typeof.html
Having learned (old) C in college and taking a closer look at it lately, I was surprised how much you can make it look “modern”, what with _Generic, wchar_t, booleans and even this __auto_type.
It seems like with a couple #define macros and some discipline you can make it look and behave more ergonomic.
Typing has two meanings, the one intended here wasn't about types - it was about keyboards. The var keyword and similar syntax in modern languages is less typing where "typing" means pushing the little buttons on the keyboard, and the associated squiggles appearing on a display.
Do you mean type inference? Most typed-languages have that, even Haskell/Scala.
It gets iffy on dependent type systems like Agda/Idris.
Also, what is the novelty about this new type system?
We present a gradual type system for Elixir, based on the framework of semantic subtyping [10, 19]. This framework, developed for and implemented by the CDuce programming language [3, 15], provides a type system centered on the use of settheoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations [19]. The system is a polymorphic type system with local type inference, that is, functions are explicitly annotated with types that may contain type variables, but their applications do not require explicit instantiations: the system deduces the right instantiations of every type variable. It also features precise typing of pattern matching combined with type narrowing: the types of the capture variables of the pattern and of some variables of the matched expression are refined in the branches to take into account the results of pattern matching
A semi-mainstream BEAM language with static typing would be a huge boon. For those of us who have problems that BEAM fits really well, it's like saying Typescript doesn't matter because other statically typed languages exist. Which is really missing the point.
Type inference for set theoretic type systems is expensive and that has not changed. It is not surprising either: inference is harder or undecidable in more expressive type systems.
We address this by providing reconstruction based only on patterns, guards, and return types. Other than that, inference is not a major limitation to us, given you don’t need to declare types today anyway.