[HN Gopher] Elixir 1.17 released: set-theoretic types in pattern...
___________________________________________________________________
Elixir 1.17 released: set-theoretic types in patterns, durations,
OTP 27
Author : clessg
Score : 332 points
Date : 2024-06-12 11:13 UTC (11 hours ago)
(HTM) web link (elixir-lang.org)
(TXT) w3m dump (elixir-lang.org)
| notemaker wrote:
| Really impressed with how thoughtful _and_ fast they are
| delivering on their type system.
| widdershins wrote:
| I'm really curious to know if many people with large Elixir
| problems are finding any issues with the new type system. This
| is pure curiosity, I don't have a dog in the fight!
| krnsi wrote:
| Jose Valim already caught two bugs (one in Phoenix, one in
| Livebook) because of the type system:
| https://x.com/josevalim/status/1791409843888111667
| bhaney wrote:
| I'm excited about the type system so far, but I'm especially
| excited to hear about what else the type system is going to
| enable in the future. I remember Jose describing this as a
| "gradual gradual type system," where the gradual type system is
| going to be gradually added in stages, with this being the first
| stage. Any cool new type-system-related stuff coming up in the
| next few stages? I'm especially hoping for newly enabled compiler
| optimizations.
| neillyons wrote:
| Here is the roadmap https://hexdocs.pm/elixir/main/gradual-set-
| theoretic-types.h...
|
| The next milestone will include a mechanism for defining typed
| structs.
| pawelduda wrote:
| Doesn't gradual type system mean something else here? As in
| developers being able to iteratively add types while leaving
| untyped parts for later? At least this is how Ruby's Sorbet
| describes it
| mhanberg wrote:
| Correct, a gradual type system is a form of type system and
| not the method for rolling it out.
| arrowsmith wrote:
| It's a gradual type system that they're rolling out
| gradually.
| pjam wrote:
| Yes, but the discussion here was about it being a gradual,
| gradual type system, as in, the gradual type system being
| added gradually
| dub_gui wrote:
| You're right about what a gradual type system means! A
| gradual type system allows flexibility in how you approach
| typing a codebase. It also means that your system
| incorporates a dynamic type, making your types 'gradual'.
|
| Interestingly, gradual set-theoretic types are flexible
| enough to let you gradually implement type inference for that
| system. Hence, the gradual gradual type system. :-)
| GiorgioG wrote:
| Super-excited for this release. I wish someone would put some
| resources into the Elixir IntelliJ plugin. I've tried, but I just
| can't enjoy using VSCode (vs IntelliJ based IDEs, Visual Studio,
| etc.)
| azurelake wrote:
| Same. I would pay 50 / month for an Elixir plugin that had a
| comparable amount of polish to RubyMine.
| dimitrisnl wrote:
| I'm very happy for this release. I picked up Elixir recently, and
| the missing a type system was my only pet peeve.
| sapiogram wrote:
| Does anyone know what they mean by "set-theoretic types"? I'm a
| PL nerd, but I've never heard this term before.
| kylecazar wrote:
| The original post Jose wrote announcing the gradual typing
| project has a good summary of the goal specific to Elixir
| (2022)
|
| https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi...
| pjam wrote:
| There's a paper about it, linked from the blog post:
| https://arxiv.org/abs/2306.06391
| bobwaycott wrote:
| 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, functions are explicitly annotated
| with types that may contain type variables, but their
| applications do not require explicit instantiations: the system
| deduces the right instantiations of every type variable. It
| also features precise typing of pattern matching combined with
| type narrowing: the types of the capture variables of the
| pattern and of some variables of the matched expression are
| refined in the branches to take into account the results of
| pattern matching._
|
| [0]: https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
| williamdclt wrote:
| 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
| weatherlight wrote:
| Typescript's type system isn't sound. The Set theoretical
| type system proposed for Elixir is.
| lolinder wrote:
| 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/?strictFunctionTy
| pes=fal...
| zarathustreal wrote:
| 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.
| lolinder wrote:
| Is the TypeScript team correct in explaining that
| soundness would exclude functions accepting subtypes as
| laid out there? If so, it seems like any type system that
| was meant to be able to type common JavaScript idioms
| would _have_ to be unsound.
| zarathustreal wrote:
| Sub-types can be represented with algebraic types so I'm
| not sure that's necessarily true, for example an abstract
| class with subclasses can be represented as a sum type
| zem wrote:
| only if there is a fixed set of subclasses, which is not
| always or even mostly the case.
| josevalim wrote:
| 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/
| williamdclt wrote:
| I did read your article, and it's actually how I came out
| with the idea that Elixir had come up with the same idea
| as TS haha!
|
| I'm sure I'm missing something as I have no doubt you're
| by far more knowledgeable than I am, but TS also
| represents types as sets (semantically, dunno about
| internal implementation), structural typing seems to
| inherently map to set theory
|
| For example, about bounded polymorphism the article says
| "Of course, we can provide syntax sugar for those
| constraints": seems like this sugar could be 'a extends
| number' to me, like typescript does. I don't see how TS
| does _not_ map to set operations
| gregors wrote:
| If you're into watching talks, this will be well worth your
| time.
|
| ElixirConf 2023 - Jose Valim - The foundations of the Elixir
| type system
|
| https://www.youtube.com/watch?v=giYbq4HmfGA
| freedomben wrote:
| Thanks, this is a fantastic talk. Long, but well worth it,
| especially if you work with Elixir
| aatd86 wrote:
| It's the definition of types as set of values. Then you have
| set operations on these types that are lade available. That
| translates into subtyping considerations.
|
| Cf. Castagna's et.al. For semantic subtyping.
| pawelduda wrote:
| This is it, the final piece I wanted. Looking forward to the
| further stages. Apart from that, the language is 100% feature-
| complete as far as I am concerned.
| neillyons wrote:
| 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.
| mtndew4brkfst wrote:
| 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])
| gregors wrote:
| Elixir and Erlang teams are absolutely killing it over the last
| few years, not to mention all the work done by the library and
| book authors out there.
|
| I've never been more excited about a release. I've been watching
| commits to both Elixir and OTP for awhile now and I feel
| Elixir/Erlang has really picked up steam.
|
| Thanks to everyone involved for making my life easier!
| tiffanyh wrote:
| How does this compare to Gleam (strong) typing?
|
| https://gleam.run
| throwawaymaths wrote:
| Gleam's type system is (IIUC) basically h-m bolted onto the
| beam. elixir's is its own
| weatherlight wrote:
| 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.)
| tiffanyh wrote:
| 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?)
| arrowsmith wrote:
| Elixir checks at compile time.
| bo0tzz wrote:
| My understanding is that the BEAM vm already has some
| (optional) runtime typechecks in the form of guards, which
| this new typesystem will also add for you automatically.
| And that these guards are actually used to speed things up,
| for example by JITing more optimized code.
| davydog187 wrote:
| Both the Elixir and Gleam type systems run at compile time
| (and whenever you recompile during development)
|
| There are no plans for runtime checking AFAIK
| nerdponx wrote:
| > 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
| cobbal wrote:
| HM is worst-case exponential, but it just happens to have
| good performance in practice.
| aczerepinski wrote:
| For 10 years I've been reading about cool Elixir stuff here. Love
| the language. I gave up on finding a job in Elixir many years ago
| though after seeing salaries consistently lower than more
| mainstream languages. It may be the language I'd want to use
| most, but salary and cool product are more important to me than
| tech stack so it may never happen. Still fun to follow from afar.
| ch4s3 wrote:
| > seeing salaries consistently lower than more mainstream
| languages
|
| That seems surprising to me as an Elixir developer. Are you
| looking in the US, or elsewhere?
| davidw wrote:
| I keep an eye out in the US and there just aren't many of
| them out there.
|
| And you have to be careful because some of those are
|
| * "Bob wanted to try out Elixir, so now we use it for this
| one microservice, but we're mostly a
| PHP/Rails/Java/Python/whatever shop and we'd like to rewrite
| it one day, because Bob left a few years ago" - places where
| someone wanted to play with something shiny and new.
|
| * Early stage firms where someone is a true believer that
| BEAM is some kind of magic scaling bullet or secret sauce.
| acangiano wrote:
| Salaries are consistently above other mainstream stacks, partly
| because most Elixir jobs look for senior engineers.
| mike1o1 wrote:
| I've been using Elixir as a backend for a side project (with a
| Remix frontend) and it's been really pleasant and productive to
| work with on the backend. I appreciate how productive LiveView
| can be, but for my specific case I needed to handle poor network
| connections and LiveView was (as expected) a poor experience.
|
| I wish Elixir was able to decouple itself from LiveView in a
| sense in the minds of developers. Even without LiveView and
| realtime/channels, just using Elixir as a backend for a simple
| API has been really fun.
| manchmalscott wrote:
| You can use Phoenix without LiveView by running mix phx.new
| with the --no-live flag (or manually pull it out of an existing
| project).
| bnchrch wrote:
| But too the OPs point. This is not a technology that should
| be included by default. No matter how cool.
|
| Saying this as a die hard Elixir fan who's been using it
| since 2015.
| mike1o1 wrote:
| Yes, I totally get that (and have been doing that). My
| complaint/suggestion is more around the marketing and
| messaging. There is so much more to Elixir than LiveView!
| sbuttgereit wrote:
| There are a couple comments to you so far and both of them miss
| the point.
|
| > decouple itself from LiveView in a sense in the __minds of
| developers__
|
| This isn't a technical knowledge issue or if a given technology
| should be the default on install. Assuming I understand your
| original post correctly this is a mindset issue: too many
| people dismiss Elixir and the rest of the ecosystem because the
| first thing they think about is LiveView while ignoring the
| rest of the ecosystem and that's a shame, because it's much
| more than that... and I would agree with that point. Even
| Phoenix is more than LiveView.
|
| It's possible to have solidly productive, cost effective Elixir
| applications not involving LiveView or even Phoenix for that
| matter. The choice of Elixir in the backend should be more
| common than it is, though I understand some of the conventional
| wisdom and fears that motivate other choices.
| elbasti wrote:
| I love elixir. I use it for basically everything. And LiveBook
| has become my go-to place to start building toy software.
|
| I just can't do liveview. I have a very hard time grokking it,
| and it has a lot of footguns. (ex: if you need to remember to
| perform auth checks both doing a `pipe_through` in a router
| _and_ using the `on_mount` callback in a LiveView, see [0].)
|
| In fact, the fact that the above sentence has zero meaning to a
| new-to-phoenix-and-liveview dev is proof enough to me that
| liveview should _not_ be the default way of doing things.
|
| It creates a very steep learning curve where, crucially _none
| is required_. elixir /phoenix are _easy_.
|
| I would even say that the correct learning order for a new-to-
| elixir/phoenix dev should be:
|
| - Phoenix with deadviews (MVC style).
|
| - "Elixir in action" to learn the basics of OTP. This book is
| was both easy and utterly eye-opening to me and changed the way
| I code basically everything.
|
| - Then, and only then, LiveView.
|
| [0]: https://hexdocs.pm/phoenix_live_view/security-
| model.html#liv...
| arrowsmith wrote:
| Shameless self-promotion - if you're struggling to learn
| LiveView then you could try my tutorial:
| http://phoenixliveview.com/
| dankai wrote:
| I've been building my startup 100% fullstack in elixir, and it's
| been the most wonderful technology I've ever worked with. I'm
| evangelising all my serious tech friends about how great it is.
|
| Now it would be awesome if rabbitMQ and its client would run on
| OTP 27, would love to upgrade :(
| Joel_Mckay wrote:
| RabbitMQ is pretty solid, are you running into a performance
| leak or something?
|
| We've used the SSL cert client login method for years, and have
| been very happy with the reliability.
|
| Cheers, =)
| bglusman wrote:
| See announcement here
| https://www.rabbitmq.com/blog/2024/05/23/erlang27-support
| Joel_Mckay wrote:
| I guess we wait a bit more for a stable release. =)
| davidw wrote:
| If I may ask, what are you working on where Elixir hits the
| sweet spot compared to other technologies?
| dankai wrote:
| A news aggregator (and premium news chatbot) that indexes and
| analyses around ~150.000 new articles a day (http://im.fo)
|
| I'm absolutely certain the real time processing would be
| unfeasible in any other technology in terms of complexity and
| the minimal compute resources it's running on.
|
| Modules like broadway, ash, oban, phoenix liveview ... make
| it not just a pleasure to work with but insanely performant.
|
| With over 20 years of programming experience, I can say with
| certainty that there is no language that makes me as
| productive as elixir. It's at least 10x my python
| productivity (despite being at an expert level in python as
| well).
| sergiotapia wrote:
| Can't say enough good things about Elixir and Phoenix. Now with
| types coming, it'll get even better.
|
| By the way, you hear a lot about the BEAM and it's power - but in
| my experience you can go a LONG LONG LONG way before you ever
| have to even think about that part of your stack. Phoenix does
| such a tremendous job abstracting that for you. You just get the
| gainz with no effort. Other parts of the stack also just abstract
| that for you.
|
| Case in point: Oban. You get powerful, flexible and easy to use
| background jobs for essentially free. Right there in Postgres,
| with your Elixir code. It's crazy.
|
| Try it.
| nelsonic wrote:
| Awesome work Elixir & Erlang Devs! <3 Cannot _wait_ for the "no
| types" excuse to go away for mass adoption of Elixir! Keep up the
| great progress.
| mikl wrote:
| The introduction of set-theoretic types has truly been a
| technical tour-de-force. A huge improvement of the language, but
| in a backwards-compatible fashion.
___________________________________________________________________
(page generated 2024-06-12 23:00 UTC)