In this episode, András Kovács is being interviewed by Andres Löh and Matthias Pall Gissurarson. We learn how to go from economics to functional programming, how GHC’s runtime system is superior to Rust’s, the importance of looking at GHC’s Core for spotting stray closures, and why staging might be the answer to all your optimisation problems.
7 Likes
This was a very interesting episode!
@AndrasKovacs you say that using the delimited continuation primops imposes overhead even for operations like get, but I think @lexi.lambda is using them in the eff library in such a way that they only add overhead for those operations that actually need to treat the continuation in a special way. Many of the handlers in that library, like those for Reader/State/Writer, do not actually use the delimited continuation primops (or at least not for implementing their operations).
Also, if people are looking for relatively mature recent effect libraries that implement capabilities on top of the ReaderT pattern then I’d recommend effectful: An easy to use, performant extensible effects library.
4 Likes
I have two questions:
-
András said typechecking dependently typed languages doesn’t really work with static memory allocation and that GC is needed to make it tractable. How does it work in Lean, which is implemented in C++ afaik? Do they use a GC library? If so, then presumably the same can be done with Rust?
-
Is Zig’s comptime (two) staged programming, or are there limitations in expressivity? Or is comptime not built on a solid theoretical foundation? Syntax-wise they seem to be able to get away without splices etc, so I’m wondering if they are cutting corners somehow?
1 Like
- Lean mostly uses reference counting. Sure, the same can be done in Rust, but native precise GC-s are significantly faster.
- I’m not an expert on Zig, but looking at the reference, it appears that there’s no guarantee of well-typing of staging output, and the comptime type system is also fairly weak. These two points are probably related; if we don’t have strong enough types at comptime, many useful metaprograms (like printf in the Zig docs) are not typeable, and we have to rely on post-staging “duck typing”. I prefer the ergonomics of strongly typed staging.
Btw, quotes and splices are not strictly necessary. There’s a quote/splice flavor and also a “HOAS” flavor of two-stage languages, and the two are usually equivalent (exactly the same metaprograms are expressible with them). Quotes and splices are a bit more convenient in the compiler IR-s. But even if we use the quote/splice flavor, they should be almost always inferable in the surface language and programmers should be able to just omit them.
I think that Rust monomorphization and Zig comptime can be both viewed as quote/splice-style, but with enough obvious syntactic stratification in the surface language that there is no need for actual quotes and splices. But the notion of quote and splice must appear at least implicitly in the staging implementation (we have to know where exactly to switch between expression generation and metaprogram execution).
3 Likes