4 ms·

We were 100% not expecting this to show up on HN front page. :) In any case, the title is accurate in that it is only a prototype and it was built by Guillaume

We were 100% not expecting this to show up on HN front page. :) In any case, the title is accurate in that it is only a prototype and it was built by Guillaume to explore how Elixir idioms map to set-theoretic types. The UX and syntax do not reflect how the type system would look in Elixir itself (if we get a type system at all). You can find more context in Guillaume’s talk: https://m.youtube.com/watch?v=gJJH7a2J9O8 https://m.youtube.com/watch?v=gJJH7a2J9O8 The initial research announcement: https://elixir-lang.org/blog/2022/10/05/my-future-with-elixir-set-theoretic-types/ https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi... And the paper as an accurate and in-depth resource: https://www.irif.fr/_media/users/gduboc/elixir-types.pdf https://www.irif.fr/_media/users/gduboc/elixir-types.pdf

lambdasquirrel 3y ago
I took a quick glance at the paper. It sounds like initial efforts on a type system focused on trying to capture the whole space of programs that could be expressed? Whereas later efforts have focused more on how modern functional languages are meant to be used? (e.g. there’s an exhaustivity checker) This seems like really good news. It’s exciting to see where this goes.
- josevalim 3y ago
  Exactly. It was very important for us to figure out how well Elixir fits the type system, otherwise we would either get false positives or we would end-up relying too much on gradual typing. The other effort was to make sure we can lift as much information from pattern matching and guards.
bongobingo1 3y ago
My understanding is (from your twitch stream), that the type system will initially be obscured from developers. I guess this means it's going to hook into the existing `type` and `spec` features of elixir? Do you think we'll end up writing $ integer() -> integer() @spec inc(integer) :: integer() def inc(i), do: i + 1 or can the new type system be entirely expressed in `@spec` (perhaps with a slightly upgraded syntax), or perhaps we'll have the choice of @spec or $ (or @spec2.0, whatever). Additionally, do you feel there is any chance/desire/need of this bleeding up into Erlang? I can only assume the work done mapping the type system onto elixir would not require as much work to then map to Erlang if there were any interest.
- anne_biene 3y ago
  There is interest from the Erlang community. Etylizer is a set-theoretic type checker developed for Erlang. We have different objectives, though, as we try to remain backwards compatible with the existing type specs. https://arxiv.org/pdf/2302.12783.pdf https://arxiv.org/pdf/2302.12783.pdf
- manusachi 3y ago
  AFAIR, it should be possible to convert dialyzer specs to that new type system annotations. It would probably be not as precise, but could be a good enough starting point to then gradually make them more precise
- josevalim 3y ago
  Initially we will only leverage information from pattern matching and guards. There are no plans to leverage typespecs for now (as someone said below, they likely won't be as precise). And yes, the semantics should map 100% cleanly to Erlang.
asymmetric 3y ago
Just wanted to say that the paper is extremely readable and well-written. Congrats to the authors!
bullfightonmars 3y ago
This talk is great and Giuseppe delivers it well. I'm really impressed with the expressiveness of the type system they have designed. Describing types as sets with predicate logic reads very clearly. I was particularly impressed with the Exahustivity and redundancy in pattern matching, using the type to inform you when you have failed to fulfill the type contract across multiple expressions is _very_ clever and yet very easy to understand. This feels very much like the type of feedback I would expect from elixir when writing.

lambdasquirrel 3y ago

I took a quick glance at the paper. It sounds like initial efforts on a type system focused on trying to capture the whole space of programs that could be expressed? Whereas later efforts have focused more on how modern functional languages are meant to be used? (e.g. there’s an exhaustivity checker) This seems like really good news. It’s exciting to see where this goes.

josevalim 3y ago
Exactly. It was very important for us to figure out how well Elixir fits the type system, otherwise we would either get false positives or we would end-up relying too much on gradual typing. The other effort was to make sure we can lift as much information from pattern matching and guards.

bongobingo1 3y ago

My understanding is (from your twitch stream), that the type system will initially be obscured from developers. I guess this means it's going to hook into the existing `type` and `spec` features of elixir? Do you think we'll end up writing $ integer() -> integer() @spec inc(integer) :: integer() def inc(i), do: i + 1 or can the new type system be entirely expressed in `@spec` (perhaps with a slightly upgraded syntax), or perhaps we'll have the choice of @spec or $ (or @spec2.0, whatever). Additionally, do you feel there is any chance/desire/need of this bleeding up into Erlang? I can only assume the work done mapping the type system onto elixir would not require as much work to then map to Erlang if there were any interest.

anne_biene 3y ago
There is interest from the Erlang community. Etylizer is a set-theoretic type checker developed for Erlang. We have different objectives, though, as we try to remain backwards compatible with the existing type specs. https://arxiv.org/pdf/2302.12783.pdf https://arxiv.org/pdf/2302.12783.pdf
manusachi 3y ago
AFAIR, it should be possible to convert dialyzer specs to that new type system annotations. It would probably be not as precise, but could be a good enough starting point to then gradually make them more precise
josevalim 3y ago
Initially we will only leverage information from pattern matching and guards. There are no plans to leverage typespecs for now (as someone said below, they likely won't be as precise). And yes, the semantics should map 100% cleanly to Erlang.

asymmetric 3y ago

Just wanted to say that the paper is extremely readable and well-written. Congrats to the authors!

bullfightonmars 3y ago

This talk is great and Giuseppe delivers it well. I'm really impressed with the expressiveness of the type system they have designed. Describing types as sets with predicate logic reads very clearly. I was particularly impressed with the Exahustivity and redundancy in pattern matching, using the type to inform you when you have failed to fulfill the type contract across multiple expressions is _very_ clever and yet very easy to understand. This feels very much like the type of feedback I would expect from elixir when writing.