HN user

josevalim

4,364 karma
Posts21
Comments446
View on HN
elixir-lang.org 6mo ago

Type inference of all constructs and the next 15 months

josevalim
14pts2
tidewave.ai 7mo ago

Improving web accessibility with trace-augmented generation

josevalim
5pts0
tidewave.ai 11mo ago

Tidewave Web: in-browser coding agent for Rails and Phoenix

josevalim
22pts3
dashbit.co 1y ago

Data evolution with set-theoretic types

josevalim
127pts32
dashbit.co 2y ago

Elixir and Machine Learning: Q3 2023 roundup

josevalim
39pts5
elixir-lang.org 3y ago

Elixir type system updates: moving from research into development

josevalim
19pts1
huggingface.co 3y ago

Deploy Livebook (Elixir) Notebooks as Apps to Hugging Face Spaces

josevalim
17pts0
news.livebook.dev 3y ago

Build and deploy a Whisper chat app to Hugging Face with Livebook in 15 minutes

josevalim
20pts2
news.livebook.dev 3y ago

Distributed Machine Learning Notebooks with Elixir and Livebook

josevalim
299pts31
elixir-lang.org 3y ago

Elixir v1.14 released: improved debugging, partition supervisor, and more

josevalim
59pts5
news.livebook.dev 4y ago

Livebook v0.5: flowcharts, chat apps, custom widgets and more (Elixir notebooks)

josevalim
7pts1
dashbit.co 4y ago

Elixir and Machine Learning: Nx v0.1 released

josevalim
274pts44
dashbit.co 5y ago

Livebook: a collaborative and interactive code notebook for Elixir

josevalim
65pts5
elixir-lang.org 7y ago

Elixir v1.8.0 released: better introspection, faster compilation and speed-ups

josevalim
30pts0
elixir-lang.org 7y ago

Elixir v1.7 released

josevalim
395pts168
elixir-lang.org 8y ago

Elixir v1.6 released: code formatter, dynamic supervisors, and more

josevalim
341pts39
blog.plataformatec.com.br 15y ago

A (successful) git branching model

josevalim
1pts0
blog.plataformatec.com.br 15y ago

Why Rubyists should try Elixir

josevalim
5pts1
blog.plataformatec.com.br 15y ago

[Screencast] Elixir: Object Orientation and charming syntax on top of Erlang

josevalim
34pts11
github.com 15y ago

Elixir: Simple Object Orientation and charming syntax on top of Erlang

josevalim
52pts6
blog.plataformatec.com.br 15y ago

Understanding the latest Rails benchmarks

josevalim
30pts3

It is funny (and perhaps a bit depressing) that LLMs were trained on our content and now, if we generate a similar structure as before, with the usual love and care, we will be criticized by it. Even when it does not "look bad or is a bad result".

Thanks for the kind words and the nice question!

1. The cross module optimizations I mentioned above 2. Have a WASM target for the runtime itself 3. Make it easier to ship single file executables with the whole VM

But they are really “nice-to-have”s. I have been a happy user for 15+ years!

There are multiple people working on the JIT within the last 5-6 years. The WhatsApp folks also contribute meaningfully.

I suspect once the Erlang/OTP team squeezes all performance in the JIT, they will look into optimizing across modules, which will probably open up many new possibilities, but it requires rethinking some runtime primitives.

The Software Mansion folks designed it and we actually iterated on the designs on Figma, having discussions as humans, and exploring alternatives. They were lovely to work with.

I also worked on all of the copy myself, collecting feedback from core maintainers as I went. The new tagline was a suggestion from Theo which we iterated on. I did use LLMs as an assistant, but I did not ask it to generate the content.

Might as well use LLMs for the whole thing next time, since we will be accused of doing so anyway! :D

I don't think these articles fully cover (pun intended) the claims being made.

First of all, we need to separate "types" from "static type checking". Elixir always had types and types by themselves won't eliminate tests. You can combine types with type checkers, as well as tests themselves (as described in the first article), to aid software verification. Plus many of the techniques discussed in the article (property-based testing, static analysis, etc) are available to dynamically typed languages too.

Some notes on the first article:

For example, there is no test we could write that would show that our function never throws an exception or never goes in to an infinite loop, or contains no invalid references. Only static analysis can do this.

Static analysis is doing a lot of heavy lifting here. When applied to type checking, where it can prove absence of exceptions depends entirely on how expressive the type system and checker are.

For example, this Haskell function can fail at runtime even though it type checks:

    maxPosInteger :: (Ord a, Num a) => [a] -> a
    maxPosInteger xs = maximum (filter (> 0) xs)
If `xs` contains no positive elements, maximum fails. The type system does not rule this out.

As the article itself later discusses, proving stronger properties requires more expressive type systems, such as dependent types. Those systems can prove the absence of additional classes of failures, but they come with their own costs in complexity, ergonomics, inference, compile times, and so on. My recent ElixirConf talk touched on these trade-offs: https://www.youtube.com/watch?v=Ay-gnCqDw9o

But overall the article does not discuss coverage. Under some of the scenarios it presents, such as finite domains, exhaustive testing guided by coverage can prove the absence of bugs too. Additionally, some of the concerns the article has about Python, such as runtime redefinition and excessive polymorphism, do not really apply to dynamic languages like Elixir and Clojure.

Correctness oracles abound. We have test suites, fuzzers and property-based testers, runtime sanitizers, static analyzers, linters, strong type systems, and formal verifiers. Any time such a tool can be made available to the LLM, we’ll reap the benefits in terms of not dealing with bugs the hard way, later on.

I completely agree with that framing. Static type systems are valuable tools, but they're one tool among many. My overall point is that I wouldn't draw the line at static typing as the "must have" mechanism for software quality, especially in the context of AI-assisted development where multiple correctness oracles can be composed together.

Thanks for sharing, those were great reads!

That’s very exciting! Is there anywhere I could follow you for updates? If you don’t want to share it publicly, and is ok with sharing it privately, my email is my username on gmail. Thank you!!

Agreed on the guardrails bit. My point is that we still don't have much evidence that static types are an effective way to constrain the search space for coding agents, or how much value they add on top of other mechanisms. Redundancy can certainly be beneficial, but how much and at what cost?

On expressiveness, people often frame it as a dynamic-language goal, but a large portion of type system research is precisely about making type systems more expressive so they can describe a wider range of programs and invariants. This is clearly something both camps value. I suppose another interesting benchmark could be: how do coding agents perform across languages with different degrees of type-system expressiveness?

We may directionally agree, but it is hard to draw conclusions without measurements. Overall, I'd say this is much more of an open question than people give it credit for.

No, this comes from interacting with the community, companies, and large projects throughout the years, followed by research, publishing of papers, and careful analysis on the costs and benefits of introducing said feature! Only then we added it.

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 struggle with). Plus they are not the only mechanism to assert correctness (they only validate a subset of your program correctness and do not replace tests) and you are still on your own when it comes to actually recovering from unexpected errors (something Erlang/Elixir were designed for).

I'd say there are two flip sides to your question:

1. Given types do not replace tests, if you can use AI to automate full test coverage, are there actual benefits in static typing for coding agents? The downside of tests for humans is that we suck at writing them (but guided agents can do better) and they can take time to run (which agents do not care)

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)

My gut feeling is that local structure, documentation, quality and quantity in the training data, etc are likely to play a more important role than typing for coding agents. I'd also love to measure how agents perform on specific domains. If you are writing concurrent software, how does Elixir/Java/Rust/Go compare? But without data, it's hard to say.

[AutoCodeBenchmark]: https://github.com/Tencent-Hunyuan/AutoCodeBenchmark

You are mixing runtime and compile-time dependencies. Runtime dependencies (circular or not) have no impact on compilation performance and stability. Phoenix does include one circular dependency (the layout is rendered by your endpoint and it references your endpoint) but it is a runtime one.

That can be a concern indeed but it is worth noting that strong arrows compose/propagate. So if you have a function without guards that calls a function that guards on said types, the caller is also strong! We will likely have mechanisms to measure "strength" when we introduce type annotations.

some stuff being sold as "all these libs/packages that haven't had any updates for over a year is fine because Elixir" I just don't buy it

I maintain more than 20 packages and, except for the major ones, like Phoenix and Ecto, they haven't been updated in more than a year and yes, they are all fine.

The language has been extremely stable. There has been almost no breaking changes in over a decade. Case in point: we introduced a whole gradual type system without making any changes to the language surface! The language is still on v1.x!

The syntax you are commenting on has always existed in Elixir, before v1.0, as part of patterns and guards.

You are commenting as if we added this now but we have made no changes to the language surface. The difference is that we now leverage these same language constructs to extract precise type information.

The team that built Erlang (Joe, Robert, Mike, and Bjorn) didn't know the actor model was actually a thing. They wanted to build reliable distributed systems and came up with the isolated processes model you find in Erlang today. Eventually (probably when Erlang was open sourced?), folks connected the dots that the actor model was the most accurate description of what was going on!

You are right, poor phrasing on my side. Instead of focusing on C appearing twice, I should rather focus on how complex the expansion is, meaning that everytime we have to expand the BDD (which we need to do during subtyping or emptiness for example), we end-up doing a lot of repeated operations. I will push an update, thank you for commenting.

Elixir 1.19 9 months ago

LiveView was still before v1.0, hence the churn, but Phoenix itself did not introduce breaking changes since v1.0, released more than a decade ago. Our skeleton for new applications change, as best practices around web apps are still evolving, but it is completely up to you to migrate. As a reference point, most other web frameworks have gone through several major versions in the same time, changing how new apps are built but also breaking old ones.

The idea that Phoenix is also mostly macros does not hold in practice. Last time this came up, I believe less than 5% of Phoenix' public API turned out to be macros. You get this impression because the initial skeleton it generates has the endpoint and the router, which are macro heavy, but once you start writing the actual application logic, your context, your controllers, and templates are all regular functions.

I hear you. I'd love to integrate with whatever model subscription is available but it seems using Max outside of Claude products is against their terms. I suggest reaching out to Anthropic and letting them know you would like to use your Max subscription with other coding agents.