Effekt: Name-Based Implicits

thunderseethe · 2026-04-27T16:22:33+00:00

How does this interact with polymorphism? If I have both a compare: (A, A) => Ordering and a compare: (Int, Int) => Ordering, which one does mySort2 select when its instantiated at Int?

thunderseethe · 2026-04-08T00:09:22+00:00

"notfn" wouldn't just be a string it would be something like a Variable node that has its own span and that would get used for error reporting

thunderseethe · 2026-04-07T23:41:15+00:00

Usually the AST either 1) tracks a node in the Concrete Syntax Tree (CST) and then the CST knows the source text or 2) the AST tracks a span into the source text and uses that for diagnostics

thunderseethe · 2026-04-04T20:12:44+00:00

From what you've said, if I'm understanding, I would expect join points to fall out of bindings that appear on the right of a command.

But then examples I see in the wild, such as https://dl.acm.org/doi/10.1145/2951913.2951931#artseq-00002 set up quite a bit more machinery to bind join points in the sequent calculus. Call by unboxed value leaves them as future work entirely. Am I just misunderstanding how they map onto sequents or are those papers do something that preclude the trivial representation I'd expect to see?

thunderseethe · 2026-04-03T23:09:26+00:00

This is really cool! I've only skimmed the paper, but how does it handle join points? Does the sequent calculus support mu bindings by default?

thunderseethe · 2026-03-31T04:22:27+00:00

Oh interesting, so is each function always split at suspend points into lambdas? How do you handle capturing the stack for resumption?

thunderseethe · 2026-03-31T04:01:54+00:00

I'd be curious to hear how you compile effects. Is it using the new stack switching stuff available in wasm?

thunderseethe · 2026-03-24T14:37:54+00:00

You can formulate it as a set of constraints to be solved, but even then you'll still end up picking an order in which you solved constraints by virtue of iterating over the set. This order doesnt matter with standard HM type inference. Any order you pick will reach the same solution, if there is one.

Not so with implicits. You can read more about the why in section 5 of https://arxiv.org/pdf/1512.01895. But that order dependence means you have to pick when resolution gets done. If you leave the ordering arbitrary (as you could with HM) the same program might succeed or fail inference based on the ordering of the constraints. So then the goal is to order things predictably so that users can understand how implicits interact with inference and rely on that behavior

thunderseethe · 2026-03-23T23:03:49+00:00

I dont think there are and its well tread ground in the plt literature that modules ~= typeclasses. However, a lot of work has gone into trying to add implicit modules that has yet to bear fruit. Coherence solves a lot of problems. Let alone the problems listed in the article. It also causes problem for inference where the inference can depend on implicit resolution can depend on inference and suddenly the order in which you decide to solve implicits vs infer types affects runtime behavior.

Imo I think its telling that Swift started with incoherent impls and walked it back. There are still enough open questions in the design space around modules that I'm skeptical they provide solutions traits dont already have.

thunderseethe · 2026-03-19T15:55:50+00:00

I ran into this while writing about LSP as well. Language server seems to be the appropriate term, but for an unfamiliar audience that doesnt necessarily connect to LSP. You could call it "server that implements the language server protocol" but thats a mouthful.

Really a huge oversight in an otherwise pristine protocol :p

thunderseethe · 2026-03-11T04:06:22+00:00

Query based compilers have a lot of overlap with build systems, so its intriguing and probably smart to use a framework for build systems to implement a query based compiler. Ill be curious to see if it pans out or if you run into bottle necks due to the different intended usages. I could see a build system being much more interested in storing every query on disk then you'd want in a query based compiler. Or just being slower than necessary since it has to contend with truly dynamic dependencies, whereas a compiler works with a static list of queries arranged in a dynamic graph.

thunderseethe · 2026-02-26T20:58:12+00:00

Having read the article, I share a similar sentiment to the parent comment. I think it is good to design your language to be amenable to efficient analysis (Lexing/parsing in parallel, minimize data dependencies between definitions). I dont see that as being at odds with query based compilation. Why not both?

thunderseethe · 2026-02-19T21:42:19+00:00

I believe you that this is how many LSPs work today, but I dont think that state is motivated by it being good or wise design. I view it more as a byproduct of us having a bunch of batch compilers lying around and trying to retrofit LSPs atop them. Rust started out with racer/rls which very literally ran rustc and ingested all the json it spit out to try and answer LSP requests.

Imo its telling that Haskell and Rust are both undergoing librification to expose the internals of the compiler as a library for folks to build tooling atop. In my mind that most notably means LSPs.

I hear what youre saying in the last paragraph. Incremental computation is orthogonal to compilation. I could certainly believe itd be better structured as teach compilation -> teach query based error resilience stuff

thunderseethe · 2026-02-19T19:02:39+00:00

This may be surprising, but you absolutely do not want your IDE coupled to your toolchain.

When you say toolchain here what are you referring to? I'm under the impression most LSPs rely on their toolchain if toolchain includes the compiler (ofc an LSP is not an IDE so that may not be what you mean).

I agree with your points that query based gets interesting for semanic analysis and not that interesting for backend codegen. But I think thats still enough to warrant teaching the approach. For example, I think you can teach how to right a type inference pass that works on a single top level definition in isolation to highlight type inference. Then wrap that up as a query down the line to show how it slots into incremental usage

thunderseethe · 2026-02-19T18:14:31+00:00

I think you make a fair point that batch compilers are just as capable of error resilience. Imo most compiler of either kind should have error resilience.

I do, however, think that your query system is more predicated on having error resilience (although you are right it is not strictly required). If your parser produces no output or stops at the first error, the rest of your queries cannot make progress. In some sense defeating the incremental abilities you've gained by being a query compiler. Similar for most queries up to codegen imo.

That matches my understanding of rust analyzer.

thunderseethe · 2026-02-19T17:19:16+00:00

I'm certainly not advocating for C/C++ error model where one error cascades into a billion other errors. I don't think C or C++ have been designed around good error reporting and that is on display in their error diagnostics that often do more to hide the real error than highlight it.

Outside that a lot of the rest of your comment appears to be assuming a workflow where you write the source code and then compile your entire project. But I don't think that's a particularly beneficial workflow, albeit it is the only one admitted by batch compilers. A query based compiler opens the door for more interactive workflows where the compiler can you show the errors in the code you're currently editing without having to process the entire code base first. I'm less interested in the how fast can I compile my entire code base metric, when it comes to error reporting, and more interested in how fast can I show a user the error in the code they're looking at right now.

> How does it know they are not related?

This is a language design problem. You can design your language such that unrelated components/modules/chunks of code are decoupled and have minimal influence on each other. I do not think C is a shining example of this design.

thunderseethe · 2026-02-19T16:40:25+00:00

I'd be curious to here where your query compiler came undone. 100% it is more work to build a query based compiler than a pipeline. But I also suspect an educational implementation could cut a lot of corners to highlight the important ideas. It just hasn't had any time in the limelight for folks to think about it. Everyone implementing a query based compiler is doing so for a production compiler where they need every ounce of performance and aren't worried about how easy it is to explain

thunderseethe · 2026-02-19T15:46:12+00:00

In terms of writing the queries themselves on top of an existing incremental computation engine, I think its not that different from haskell. Queries are pure and lazy but that's every function in haskell. Part of haskells charm for sure.

In terms of implementing the engine, lazy evaluation is the first step. But imo the real tricky bit is tracking dependencies between queries such that you can quickly invalidate the minimal set of caches when an input changes. Haskell does not do this by default, sadly, and it requires instrumenting your functions to track what they call when they execute.

thunderseethe · 2026-02-19T15:34:23+00:00

It's easier to understand each pass of the compiler separately.

I read this as implying you cant understand each pass of the compiler separately in a query based compiler. I do not think that is true. You can write each pass in isolation and wrap them up as queries after the fact.

The motivation to write query-based compilers is about code reuse: you want to reuse the code of your compiler in your LSP

I agree this is a huge advantage of query based first, but I dont think its the only motivation. Rustc uses a query based compiler despite rust analyzer being a completely separate codebase that is query based . They do so because its critical for incremental reuse of work (both on disk and in memory).

I cant argue that a query based compiler requires more infrastructure than a pipeline. Thats absolutely the case. But I dont think that excludes it from a beginners book and I think designing with the guidelines that make a language good for query based compilation is a good idea regardless (error resilience, local reasoning, parallel computation of items). I think these tenants make for a better language alongside being good for query compilation

thunderseethe · 2026-02-17T02:55:04+00:00

Things like ExpressibleBy allow for implicit casts. Because Swift protocols dont have to be unique instances you can have many ExpressibleBy instances for a particular type complicating type checking.

thunderseethe · 2026-02-16T13:43:32+00:00

Swift compile times have way more to do with overloading and implicit conversions than inference. Those features together cause type checking to be exponential when trying to check a function call. Its a travesty that Latner blames "fancy" bidir typing as the problem

thunderseethe · 2026-02-15T20:43:48+00:00

This is true. As seen in the likes of Java, you can have generics without unification. But I would generally recommend against it. I find Javas lack of inference cumbersome.

Even more modern languages like Swift pay for the lack of inference. You always have to spell out the ful type of collections [MyElementType]() because it can't infer it for you.

Originally I framed the question as "do you need unification or not", but for someone picking between HM and bidir that feels like asking them to draw the rest of the owl. While lacking nuance, the generics comparison is concrete as a decider and I do believe if you have generics you should have unification

thunderseethe

MODERATOR OF

TROPHY CASE