Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

elixir-lang.org

Post reply on HN
Print view View original

21–30 of 170 posts

Re: Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

#21

Post by weatherlight »

tiffanyh wrote: post #19

How does this compare to Gleam (strong) typing? https://gleam.run

Different type system with different goals.

Gleam uses a modified version of the Hindley-Milner Type system. (Which is a rock solid tested type system.)

A Set theoretical type system is more expressive(which suits the dynamic nature or Elixir better.) You can do Union and Intersection Types, and Negation Types, among other things, that you can't do with a HM type system. but it comes at the cost of how fast the program can be typed.

HM types systems have amazing type inference capabilities and do so at O(n). Im not sure what the time complexity of the algorithm they are using to do the type checking for Elixir programs, but I bet it's more expensive than that. (Which is probably why they are rolling out the type system slowly.)

Re: Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

#22

Post by weatherlight »

williamdclt wrote: post #18
bobwaycott wrote: post #14

Earlier quoted context omitted.

From the original paper[0]: > We present a gradual type system for Elixir, based on the framework of semantic subtyping ... [which] provides a type system centered on the use of set-theoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations. The system is a polymorphic type system with local type inference, that is, fun…

sounds like what typescript does, I'm not clear if the Elixir approach is different from "structural typing" (as TS calls it) or if they're rediscovering the same thing. Either way, I'm happy it's the way they're going

Typescript's type system isn't sound. The Set theoretical type system proposed for Elixir is.

Re: Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

#23

Post by josevalim »

williamdclt wrote: post #18
bobwaycott wrote: post #14

Earlier quoted context omitted.

From the original paper[0]: > We present a gradual type system for Elixir, based on the framework of semantic subtyping ... [which] provides a type system centered on the use of set-theoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations. The system is a polymorphic type system with local type inference, that is, fun…

sounds like what typescript does, I'm not clear if the Elixir approach is different from "structural typing" (as TS calls it) or if they're rediscovering the same thing. Either way, I'm happy it's the way they're going

While both Elixir and TypeScript are structural, they are different type systems. A set-theoretic type system is not one that has unions, intersections, negations, but rather one where the foundation of the type system is represented on top of unions, intersections, and negations. Even relations such as subtyping, compatibility, etc. are expressed as set-theoretic. We also have a very different approach to dynamic/gradual typing (which is sound): https://elixir-lang.org/blog/2023/09/20/strong-arrows-gradua...

I recommend reading Giuseppe Castagna's work for those who want to dig deeper: https://www.irif.fr/~gc/

Re: Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

#24

Post by lolinder »

weatherlight wrote: post #22
williamdclt wrote: post #18

Earlier quoted context omitted.

sounds like what typescript does, I'm not clear if the Elixir approach is different from "structural typing" (as TS calls it) or if they're rediscovering the same thing. Either way, I'm happy it's the way they're going

Typescript's type system isn't sound. The Set theoretical type system proposed for Elixir is.

For more information about what that means, see this playground [0] from the TypeScript docs. PL people often make a big deal about TypeScript's lack of soundness as though it was some kind of mistake, but it was very much an intentional choice given the trade-offs they were making at the time.

If Elixir can pull off soundness without compromising expressivity that will be a huge feat, and I'm excited to see it!

[0] https://www.typescriptlang.org/play/?strictFunctionTypes=fal...

Re: Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

#25

Post by tiffanyh »

weatherlight wrote: post #21
tiffanyh wrote: post #19

How does this compare to Gleam (strong) typing? https://gleam.run

Different type system with different goals. Gleam uses a modified version of the Hindley-Milner Type system. (Which is a rock solid tested type system.) A Set theoretical type system is more expressive(which suits the dynamic nature or Elixir better.) You can do Union and Intersection Types, and Negation Types, among other things, that you can't do with a HM type system. but it comes at the cost of how fast the progr…

Does Gleam check types at compile-time?

And Elixir check types at run-time?

(If at run-time, would that mean it would slow down your entire app as a result?)

Re: Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

#26

Post by freedomben »

gregors wrote: post #16
sapiogram wrote: post #9

Does anyone know what they mean by "set-theoretic types"? I'm a PL nerd, but I've never heard this term before.

If you're into watching talks, this will be well worth your time. ElixirConf 2023 - José Valim - The foundations of the Elixir type system https://www.youtube.com/watch?v=giYbq4HmfGA

Thanks, this is a fantastic talk. Long, but well worth it, especially if you work with Elixir

Re: Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

#28

Post by zarathustreal »

lolinder wrote: post #24
weatherlight wrote: post #22

Earlier quoted context omitted.

Typescript's type system isn't sound. The Set theoretical type system proposed for Elixir is.

For more information about what that means, see this playground [0] from the TypeScript docs. PL people often make a big deal about TypeScript's lack of soundness as though it was some kind of mistake, but it was very much an intentional choice given the trade-offs they were making at the time. If Elixir can pull off soundness without compromising expressivity that will be a huge feat, and I'm excited to see it! [0]…

Yea I never bought this assertion from the TS team, saying “given the trade-offs at the time” is the same as saying “we’re already backed into a corner by previous decisions” - the decision(s) may have been intentional at each step but the design itself probably was not. Given the choice of sound or unsound, considering that the purpose of a type system is to give certain guarantees, a type system design must always choose soundness to be considered reasonable.

That being said, I don’t think it’s possible to “pull off soundness without compromising expressivity” because the expressivity in this context is self-referential types which equate to non-terminating unification logic (and thus, unsoundness). Still, I’m excited to see what they do with this type system! Reminds me a bit of Shen’s type system.

Re: Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

#29

Post by mtndew4brkfst »

neillyons wrote: post #15

Nice feature in this release is the addition of `get_in/1` which works with structs. eg. `get_in(struct.foo.bar)` If `foo` returns `nil`, accessing `bar` won't raise.

It was still possible to do this in prior versions of Elixir, just syntactically noisy. Any layer which isn't a vanilla map needs Access.key, as in:

    get_in(struct, [Access.key(:foo), :bar])

Re: Elixir 1.17 released: set-theoretic types in patterns, durations, OTP 27

#30

Post by nerdponx »

weatherlight wrote: post #21
tiffanyh wrote: post #19

How does this compare to Gleam (strong) typing? https://gleam.run

Different type system with different goals. Gleam uses a modified version of the Hindley-Milner Type system. (Which is a rock solid tested type system.) A Set theoretical type system is more expressive(which suits the dynamic nature or Elixir better.) You can do Union and Intersection Types, and Negation Types, among other things, that you can't do with a HM type system. but it comes at the cost of how fast the progr…

> A Set theoretical type system is more expressive(which suits the dynamic nature or Elixir better.) You can do Union and Intersection Types, and Negation Types, among other things, that you can't do with a HM type system. but it comes at the cost of how fast the program can be typed.

I doubt that Python's static type hints existing within a formal mathematical framework, but it's interesting that intersection types have been under consideration for a long time now: https://github.com/python/typing/issues/213

Post reply on HN