8 ms·

showcase

167 points by weatherlight 3y ago

olafura 3y ago
https://elixirforum.com/t/any-update-on-the-set-theoretic-types/55553/4 https://elixirforum.com/t/any-update-on-the-set-theoretic-ty...
- bradrn 3y ago
  And a direct link to the paper: https://www.irif.fr/_media/users/gduboc/elixir-types.pdf https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
brainbag 3y ago
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.
- bhaney 3y ago
  Did you check out the example named "result/handle (precise intersection)"?
josevalim 3y ago
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
some_thoughts 3y ago
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?
- MartinMond 3y ago
  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-variables-dbb8efa86288 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?
  - laszlokorte 3y ago
    A simple syntax would be something like map :: forall a. ([a] -> [a]) or map :: <a> ([a] -> [a])
- masklinn 3y ago
  It’s how types have been specified in erlang for 20+ years: https://www.erlang.org/doc/reference_manual/typespec.html 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.
weatherlight 3y ago
A gradual inferred type system that is both sound and fast :) a dream come true honestly. I hope it works out.
commitpizza 3y ago
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.
- sodapopcan 3y ago
  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.
cubefox 3y ago
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.
- reuben364 3y ago
  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.
  - cubefox 3y ago
    > 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/ 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. Not sure what the difference is here.
    - deleted 3y ago
      [deleted]
    - reuben364 3y ago
      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.

167 points by weatherlight 3y ago

https://elixirforum.com/t/any-update-on-the-set-theoretic-types/55553/4 https://elixirforum.com/t/any-update-on-the-set-theoretic-ty...

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

brainbag 3y ago

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.

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

josevalim 3y ago

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

some_thoughts 3y ago

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?

MartinMond 3y ago
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-variables-dbb8efa86288 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?
- laszlokorte 3y ago
  A simple syntax would be something like map :: forall a. ([a] -> [a]) or map :: <a> ([a] -> [a])
masklinn 3y ago
It’s how types have been specified in erlang for 20+ years: https://www.erlang.org/doc/reference_manual/typespec.html 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.

weatherlight 3y ago

A gradual inferred type system that is both sound and fast :) a dream come true honestly. I hope it works out.

commitpizza 3y ago

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.

sodapopcan 3y ago
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.

cubefox 3y ago

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.

reuben364 3y ago
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.
- cubefox 3y ago
  > 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/ 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. Not sure what the difference is here.
  - deleted 3y ago
    [deleted]
  - reuben364 3y ago
    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.