Hacker News Reader

Comment by josevalim | Hacker News Reader

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

The initial research announcement: 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

View on HN

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.

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

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.

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

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.

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.

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.

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

Reply on news.ycombinator.com