Elixir's “Set Theoretical Type System” prototype/demo/showcase

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.

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.

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

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.

In your example, how can the compiler (or a human) know that int is a concrete type as opposed to an unconstrained type variable?

Consider these two function signatures:

map :: ([a] -> [a])

map :: ([int] -> [int])

Furthermore the syntax that Elixir uses here let's you do something like

map :: (list(a) -> list(b))

list_to_other_data_structure :: (list(a) -> other_data_structure(a))

It all reminds me a bit of how Haskell does it https://medium.com/functional/haskell-basic-types-and-type-v...

I'm now curious to know if/how the above 'generics' would be expressed in TypeScript/Python/Go without a similar 'type constructor' syntax construct?

It’s how types have been specified in erlang for 20+ years: https://www.erlang.org/doc/reference_manual/typespec.html

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.

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.

And a direct link to the paper: https://www.irif.fr/_media/users/gduboc/elixir-types.pdf

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.

Did you check out the example named "result/handle (precise intersection)"?

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.