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).
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?
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.
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
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
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.
So I have very little experience with elixir, but I appreciate the effort to bring static typing. With that said, I find the use of parenthesis pretty hard to read. As in I need to spend more time than a quick glance to grok what's going on. Maybe it's because I'm not familiar with the ecosystem, but coming from a typescript, python, and go background mostly, I find this
negate :: ((integer() -> integer()) and
(true -> false) and (false -> true) and
(a -> a) when a: not(integer() or boolean()))
harder to reason about quickly than say this
negate :: (int -> int) & (true -> false) & (false -> true) & (a -> a)
when a: ~(int | boolean)
Is there a reason that syntax was chosen? Is it just for showcasing purposes or is that basically just how the language works?
For the paper, we have decided to go as precise as possible, since its goal is to discuss the type-system semantics and not its syntax, so parentheses are everywhere.
You will for sure be able to drop the outer parens in your case and you _may_ be able to drop them on the function types too (to be decided). Ending up with something like this:
$ (integer -> integer) and (true -> false) and (false -> true) and (a -> a) when a: not(integer or boolean)
def negate(arg)
We will also allow intersections to be broken across multiple declarations:
$ integer -> integer
$ true -> false
$ false -> true
$ a -> a when a: not(integer or boolean)
def negate(arg)
At least in the current system I think the parens are optional if it doesn't have arguments so if you really need to leave them off when writing the type you probably can. But like someone said it's erlang convention going back decades.
Anyway coming from ocaml I don't aesthetically like this but coming from ocaml I have no grounds to talk shit about any language's aesthetic choices. The parens make sense to me when I think of them as type constructors, rather than concrete expressions of the type itself.
If you look at any erlang api doc, you’ll see predicate-like type specs. Conveniently, it naturally supports generics by just adding “parameters” to the predicates, so a dict would have type.
It works fine, and makes things less ambiguous, as erlang “types” can contain enumerations of values, in the original spec it’s clear that `integer()` is a type and `false` is a value, in your version not so much.
I watch elixir from a distance and don't have that much practical experience in it but this looks like it's too hard to read in order to be that useful imo.
At least I wouldn't use it mostly because of the paranthesis and I really do hope that it's going to be optional if it were to be implemented. I do write code in typed languages on a daily basis but I do think it's overrated especially here on HN. I like that Elixir is dynamically typed and I think that it's just something that's not really in fashion at the moment but it will come around, eventually.
I like dynamic typing too which, contrary to popular belief, doesn't mean I don't care about types. I may start using this when it is released, though, we shall see. Otherwise, don't worry, it will definitely be optional. Elixir is all about backward compatibility and not changing too much. There's an often-uttered reminder when proposals come up on the Elixir forums that there is very little chance there will ever be a v2.0. Anything's possible, of course, but it would be years away.
The get_age example uses `dynamic()` to accept any type, but I'm wondering if there will be a way to structurally type it as `%{age: number()}` or equivalent. I didn't see anything comparable in the other examples.
I don't know anything about type systems in programming, but "Set Theoretical Type System" sounds wild from a historical perspective. Set theory was synonymous with being "type free". So in type theory you would have a hierarchy of types (e.g. distinguishing properties of things, like being red, from properties of properties of things, like being a color) while in set theory you can throw things and sets into a set without much restriction.
E.g. you could have a set which contains both colors and Joe Biden, while you couldn't have a property that both colors and Biden have, since Biden is an object but colors are properties of objects, i.e. they have different types.
ZFA (1908) had urelements. You can just partition your urelements if you want distinct "types". Union across those would be disjoint, but within would be standard set union. Even in type theory you have Church VS Curry style as to whether you consider terms as inheritly belonging to a type.
> You can just partition your urelements if you want distinct "types". Union across those would be disjoint, but within would be standard set union.
In which sense would partitioning urelements lead to something like types? This sounds somewhat like many sorted logic, which is only as expressive as first-order logic, not higher-order logic / simple type theory:
https://plato.stanford.edu/entries/logic-many-sorted/
> Even in type theory you have Church VS Curry style as to whether you consider terms as inheritly belonging to a type.
1. Haven't read too deeply, but aren't we working with FOL in this type system anyway (Well, Henkin semantics of HOL, I believe)
2. I guess the major semantic difference is that in one, you define a family of PERs for terms in a given type, giving each type separate notion of equality. In the other you define equality over all terms and types are just a predicates on terms. I honestly am not well versed enough in logic to understand what it means in that sense.
If you want a more expressive logic, use a language with dependant types. Although I wish to see more powerful type systems become more mainstream, I don't expect every language to aim for that.
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