In my last Chalk post, I talked about an experimental, SLG-based solver that I wrote for Chalk. That particular design was based very closely on the excellent paper “Efficient top-down computation of queries under the well-founded semantics”, by W. Chen, T. Swift, and D. Warren. It followed a traditional Prolog execution model: this has a lot of strengths, but it probably wasn’t really suitable for use in rustc. The single biggest reason for this was that it didn’t really know when to stop: given a query like exists<T> { T: Sized }, it would happily try to enumerate all sized types in the system.

For the last month or so, I’ve gotten kind of obsessed with exploring a new evaluation model for Chalk. Specifically, I’ve been looking at adapting the SLG algorithm, which is used in the XSB Prolog engine. I recently opened a PR that adds this SLG-based solver as an alternative, and this blog post is an effort to describe how that PR works, and explore some of the advantages and disadvantages I see in this approach relative to the current solver that I described in my previous post.

In my last post about chalk queries, I discussed how the query model in chalk. Since that writing, there have been some updates, and I thought it’d be nice to do a new post covering the current model. This post will also cover the tabling technique that scalexm implemented for handling cyclic relations and show how that enables us to implement implied bounds and other long-desired features in an elegant way.

For my next post discussing chalk, I want to take kind of a different turn. I want to talk about the general struct of chalk queries and how chalk handles them right now. (If you’ve never heard of chalk, it’s sort of “reference implementation” for Rust’s trait system, as well as an attempt to describe Rust’s trait system in terms of its logical underpinnings; see this post for an introduction to the big idea.

In my previous post, I talked over the basics of how unification works and showed how that “mathematical version” winds up being expressed in chalk. I want to go a bit further now and extend that base system to cover associated types. These turn out to be a pretty non-trival extension. What is an associated type? If you’re not a Rust programmer, you may not be familiar with the term “associated type” (although many langages have equivalents).

So in my first post on chalk, I mentioned that unification and normalization of associated types were interesting topics. I’m going to write a two-part blog post series covering that. This first part begins with an overview of how ordinary type unification works during compilation. The next post will add in associated types and we can see what kinds of mischief they bring with them. What is unification? Let’s start with a brief overview of what unification is.

Over the last year or two (man, it’s scary how time flies), I’ve been doing quite a lot of thinking about Rust’s trait system. I’ve been looking for a way to correct a number of flaws and shortcomings in the current implementation, not the least of which is that it’s performance is not that great. But also, I’ve been wanting to get a relatively clear, normative definition of how the trait system works, so that we can better judge possible extensions.

This post is a continuation of my posts discussing the topic of associated type constructors (ATC) and higher-kinded types (HKT): The first post focused on introducing the basic idea of ATC, as well as introducing some background material. The second post showed how we can use ATC to model HKT, via the “family” pattern. The third post did some exploration into what it would mean to support HKT directly in the language, instead of modeling them via the family pattern.

This post is a continuation of my posts discussing the topic of associated type constructors (ATC) and higher-kinded types (HKT): The first post focused on introducing the basic idea of ATC, as well as introducing some background material. The second post showed how we can use ATC to model HKT, via the “family” pattern. This post dives into what it would mean to support HKT directly in the language, instead of modeling them via the family pattern.

Hello. This post is a continuation of my posts discussing the topic of associated type constructors (ATC) and higher-kinded types (HKT): The first post focused on introducing the basic idea of ATC, as well as introducing some background material. This post talks about some apparent limitations of associated type constructors, and shows how we can overcome them by making use of a design pattern that I call “family traits”. Along the way, we introduce the term higher-kinded type for the first time, and show (informally) that family traits are equally general.

So for the end of last week, I was at Rust Belt Rust. This was awesome. And not only because the speakers and attendees at Rust Belt Rust were awesome, though they were. But also because it gave aturon, withoutboats, and I a chance to talk over a lot of stuff in person. We covered a lot of territory and so I wanted to do a series of blog posts trying to write down some of the things we were thinking so as to get other people’s input.

In my previous post, I talked about how we can separate out specialization into two distinct concepts: reuse and override. Doing so makes because the conditions that make reuse possible are more stringent than those that make override possible. In this post, I want to extend this idea to talk about a new rule for specialization that allow overriding in more cases. These rules are a big enabler for specialization, allowing it to accommodate many use cases that we couldn’t handle before.

In my previous post, I started discussing the idea of intersection impls, which are a possible extension to specialization. I am specifically looking at the idea of making it possible to add blanket impls to (e.g.) implement Clone for any Copy type. We saw that intersection impls, while useful, do not enable us to do this in a backwards compatible way. Today I want to dive a bit deeper into specialization.

As some of you are probably aware, on the nightly Rust builds, we currently offer a feature called specialization, which was defined in RFC 1210. The idea of specialization is to improve Rust’s existing coherence rules to allow for overlap between impls, so long as one of the overlapping impls can be considered more specific. Specialization is hotly desired because it can enable powerful optimizations, but also because it is an important component for modeling object-oriented designs.

So, the condition that was supposed to ensure termination in my previous post is most certainly wrong. The idea was to prevent tautological impls like the following: impl<A: Foo> A: Foo { ... } Such impls, given a naive algorithm, would loop infinitely trying to decide if a type T implemented Foo. You can imagine: it would ask, “does T implement Foo? Well, if I map A to T then this impl applies, but only if T implements Foo.

I was thinking more about type classes as I walked down the street. In my prior post I wrote that the rules I proposed resulted in a system where traits loosely fit the following Haskell template: class C self a ... z | self -> a ... z where ... However, I gave two caveats. The first was that due to subtyping we cannot say that one type precisely determines another, but only that it puts a bound.

Currently, the Rust compiler accepts all manner of trait, impl, and bound declarations. In fact, it accepts plenty of declarations that later phases of the compiler are not sophisticated enough to handle. In other words, the syntax is writing checks the semantics can’t cash. (An aside: I just love saying that phrase for some perverse reason. I really wish however that checks, like rotary dial telephones, were something that younger people vaguely understood but which no longer had relevance in the modern era.

On the rust-dev mailing list, someone pointed out another “BitC retrospective” post by Jonathon Shapiro concerning typeclasses. The Rust object system provides interesting solutions to some of the problems he raises. We also manage to combine traditional class-oriented OOP with Haskell’s type classes in a way that feels seamless to me. I thought I would describe the object system as I see it in a post. However, it turns out that this will take me far too long to fit into a single blog post, so I’m going to do a series.