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

Elixir v1.20: Now a gradually typed language

elixir-lang.org

Post reply on HN
Print view View original

321–330 of 426 posts

Re: Elixir v1.20: Now a gradually typed language

#321

Post by williamdclt »

sph wrote: post #288
losvedir wrote: post #88

Oooh, here we go! As a professional Elixir developer for... 10-ish years now, I've been super excited about types coming. I'm very excited that the beginnings have started to land here. That said, I would love to know how the state of what's in v1.20 compares to un-spec'ed dialyzer. I was under the impression that dyalizer's "success typing" approach (not flagging a function if there are some combination of parameter…

I know this is blasphemy to the average HN reader, but as a professional Elixir developer for 10 years, never have I felt the need for stronger compile-time type guarantees. None of my production services have had downtime or crashes because of type errors. Sure, at times, for very data-intensive sections of the application I would have loved something a bit more complex than dialyzer, but the guarantees offered by O…

> people used to write server software in compiled languages feel the need for them because any runtime bug means downtime

I keep hearing that but I don't think it's been true in many years? Whether it's Go, Java, C#, Rust... a runtime bug will only fail the request, not the whole server.

FWIW, the main reason I like types isn't for the compile-time guarantees (although they're certainly nice). It's for documenting what are the data types I'm working with rather than having to guess them from the code, it's for knowing that something is a square hole therefore I should put a square piece in.

Re: Elixir v1.20: Now a gradually typed language

#322

Post by williamdclt »

elitehacker1337 wrote: post #202
teleforce wrote: post #163

Honest question, in the era of vibe and AI assisted coding is there any advantages of using untyped programming languages, apart from the fact that non-typed languages has more traning data for the LLM? This probably controversial, but personally I consider untyped languages as technical debts that need to be fixed sooner or later, and the OP article is partly addressing this very issue. Rewriting critical software i…

I’ve been using Ruby and Elixir for over a decade. Pre-AI I used them for aesthetic reasons. The code was beautiful, and I disliked dealing with types. People without experience in dynamic languages tend to overestimate the number of bugs their type system is saving them from. It’s pretty rare that I run into a bug in production that a type system would have caught. They also overstate how much types help their AI ag…

> It’s pretty rare that I run into a bug in production that a type system would have caught.

Wow, how different our experiences are. In Javascript/Typescript land, so so many bugs are null/undefined-related and really should have been caught at type level.

In fact, I'd say (without actually measuring it) that _most_ bugs I've ran into in Typescript are due to someone having bypassed the typing (casting, ts-ignore...), or a type mismatch at IO boundary.

Re: Elixir v1.20: Now a gradually typed language

#323

Post by mechanicum »

sa1 wrote: post #319

What do set-theoretic types mean? Aren’t types an alternative approach meant to avoid the paradoxes with sets? Is it just being used as a marketing term?

Short answer: “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”.

Long answer, well, there are blog posts[0], the Design Principles of the Elixir Type System paper[1] and related presentations[2, 3, 4] that talk about it at length. Giuseppe Castagna’s site has many more related papers: https://www.irif.fr/~gc/topics.en.html

[0]: https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi...

[1]: https://www.irif.fr/~gc/papers/elixir-type-design.pdf

[2]: https://www.youtube.com/watch?v=gJJH7a2J9O8

[3]: https://www.youtube.com/watch?v=VYmo867YF6g

[4]: https://www.youtube.com/watch?v=giYbq4HmfGA

Re: Elixir v1.20: Now a gradually typed language

#324

Post by ch4s3 »

sa1 wrote: post #319

What do set-theoretic types mean? Aren’t types an alternative approach meant to avoid the paradoxes with sets? Is it just being used as a marketing term?

It means that the types are built on unions, intersections, and negations[1]. It's a polymorphic type system with inference at the function level. It also does some type narrowing with pattern matching.

[1] https://www.irif.fr/_media/users/gduboc/elixir-types.pdf

Re: Elixir v1.20: Now a gradually typed language

#325

Post by nesarkvechnep »

neya wrote: post #307
nesarkvechnep wrote: post #301

Earlier quoted context omitted.

Yeah, one of the worst practices. I've been working with Elixir professionally for 6 years now and I still see this sh*t everywhere. Bad APIs, bad UIs because someone coupled themselves to the database structure and can't escape. List of memberships? Keep them as a list with the same fields as the junction table. Top-level APIs taking maps with string keys as "params" so they can very easily be cast for a changeset.

This was the only out of box solution when Elixir didn't support types. So, if you really did Elixir professionally for 6 years, you'd know that by now. > Bad APIs, bad UIs because someone coupled themselves to the database structure and can't escape. If you don't commit yourself to the database structures you defined at the time of application creation, then it just reflects poor planning and architecture overall as…

The disagreement is on Ecto schemas used to represent databases tables from the persistence layer to the UI. Of course, use changesets to normalise user input but using the same schemas everywhere is a sign of immaturity as a developer. You really sound like someone who only does CRUD services. Real world is often more complex.

Re: Elixir v1.20: Now a gradually typed language

#326

Post by sa1 »

ch4s3 wrote: post #324
sa1 wrote: post #319

What do set-theoretic types mean? Aren’t types an alternative approach meant to avoid the paradoxes with sets? Is it just being used as a marketing term?

It means that the types are built on unions, intersections, and negations[1]. It's a polymorphic type system with inference at the function level. It also does some type narrowing with pattern matching. [1] https://www.irif.fr/_media/users/gduboc/elixir-types.pdf

Unions, intersections and negations are available in types as well and are by no means exclusive to sets. The distinguishing feature of a set vs type is that a value belongs to just one type while it can belong to several sets.

Re: Elixir v1.20: Now a gradually typed language

#327

Post by felix_starman »

simoncion wrote: post #267
xlii wrote: post #249

Earlier quoted context omitted.

Dialyzer fails to successfully report errors when there are circular dependencies. Circular dependencies are nigh unavoidable in Elixir (IIRC bootstrapped Phoenix has 3 or 4) and outside of interfering with Dialyzer it impacts on compilation performance and stability (compilation races causing non deterministic compilation)

> ... circular dependencies ... compilation races ... Does Dialyzer understand Elixir? Last I knew, it could only process Erlang source code and BEAM files. Looking around, it seems like folks running Dialyzer against Elixir code are using some "dialyxer" thing. You talk about circular dependencies causing minor compilation troubles, so it doesn't sound like you're talking about types defined in terms of each other.…

Dialyzer (and Dialyxir) were written prior to compiler tracing, and also are based on Erlang's "Typespec" syntax which is a bit lacking.

I still use the Typespec syntax for its documentation benefits, and for catching "dumb" bugs, but as the Elixir compiler has improved I have found Dialyzer to be less relevant as the compiler usually catches things before Dialyzer would as it's not built into the compiler and isn't able to be.

Re: Elixir v1.20: Now a gradually typed language

#328

Post by felix_starman »

losvedir wrote: post #88

Oooh, here we go! As a professional Elixir developer for... 10-ish years now, I've been super excited about types coming. I'm very excited that the beginnings have started to land here. That said, I would love to know how the state of what's in v1.20 compares to un-spec'ed dialyzer. I was under the impression that dyalizer's "success typing" approach (not flagging a function if there are some combination of parameter…

I think the 300th episode of Thinking Elixir w/ José as the guest included a discussion on that point exactly, and if I remember correctly it was a "it depends", but I took away "probably not worth adding more labor into putting it in if you haven't already".

I haven't had it catch something before the compiler in a while. I still use typespecs for their documentation benefit, though I've been using `defguard` w/ `is_struct/2` and complex guards a lot more in recent years.

Re: Elixir v1.20: Now a gradually typed language

#329

Post by giraffe_lady »

josevalim wrote: post #271
teleforce wrote: post #163

Honest question, in the era of vibe and AI assisted coding is there any advantages of using untyped programming languages, apart from the fact that non-typed languages has more traning data for the LLM? This probably controversial, but personally I consider untyped languages as technical debts that need to be fixed sooner or later, and the OP article is partly addressing this very issue. Rewriting critical software i…

> Honest question, in the era of vibe and AI assisted coding is there any advantages of using untyped programming languages, apart from the fact that non-typed languages has more traning data for the LLM? Author here. Type systems restrict which programs can be expressed and increasing expressiveness often requires increasing type-system complexity (which, speaking from experience, both humans and agents will struggl…

> 2. Do we actually have any data or evaluations that show which typing discipline is better for agents? The only benchmark I am aware of [AutoCodeBenchmark] has Elixir come first (dynamic) and C# as second (static), so it doesn't answer the question. There are other benchmarks that show dynamic languages require fewer tokens to solve problems (but that's not a metric I particularly care about)

I am actually writing a paper on this right now so nothing I can point you to yet but yes. LLMs are better (produce working code in fewer attempts controlling for the relative size of training corpus) when using type systems with inference and global unification. It is largely about the quality of the error feedback channel so languages with very good compiler errors (accurate, localized, include the correction with the failure) can close a lot of ground.

But inference + sound type system gives you a constraint propagation that genuinely restricts the ability of the LLM to get into trouble. Type systems that require annotation give up most of the benefit, since the annotations are themselves surface area for LLM mistakes. Unification also puts heavy limits on the expressiveness of the language which is a confounder and may actually be a big part of the benefit too.

Everyone has been on the "the training data is better" thing but I actually don't think so. All of the languages that people report as being better because of good training data actually have fairly restrictive type systems. Elixir is an exception, but it has exceptionally good error messages! And also, along with erlang, pretty unique runtime semantics that may contribute but that's outside my domain I'm on type systems. Debunking the training quality thing is not what I'm working on but I have deep suspicions about that common wisdom.

Re: Elixir v1.20: Now a gradually typed language

#330

Post by sa1 »

mechanicum wrote: post #323
sa1 wrote: post #319

What do set-theoretic types mean? Aren’t types an alternative approach meant to avoid the paradoxes with sets? Is it just being used as a marketing term?

Short answer: “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”. Long answer, well, there are blog posts[0], the Design Principles of the Elixir Type System paper[1] and related presentations[2, 3, 4] that talk about it at length. Giuseppe Castagna’s site has many more…

Sets and types are foundational mathematical concepts so I’m looking for how elixir’s types fit in that context. Union and intersection are not something that belongs only to sets.
Post reply on HN