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. It was also pretty non-obvious to me how to extend that system with things like co-inductive predicates (needed for auto traits) and a few other peculiarities of Rust.

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. (Nice work, scalexm!)

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). The basic idea is that traits can have type members associated with them. I find the most intuitive example to be the Iterator trait, which has an associated type Item. This type corresponds to kind of elements that are produced by the iterator:

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. When you are doing type-checking or trait-checking, it often happens that you wind up with types that you don’t know yet. For example, the user might write None – you know that this has type Option<T>, but you don’t know what that type T is. To handle this, the compiler will create a type variable. This basically represents an unknown, to-be-determined type. To denote this, I’ll write Option<?T>, where the leading question mark indicates a variable.

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. After a number of false starts, I think I’m finally getting somewhere, so I wanted to start writing about it.

This post is a continuation of my posts discussing the topic of associated type constructors (ATC) and higher-kinded types (HKT):

1. The first post focused on introducing the basic idea of ATC, as well as introducing some background material.
2. The second post showed how we can use ATC to model HKT, via the “family” pattern.
3. 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.
4. This post considers what it might mean if we had both ATC and HKT in the language: in particular, whether those two concepts can be unified, and at what cost.

Unifying HKT and ATC

So far we have seen “associated-type constructors” and “higher-kinded types” as two distinct concepts. The question is, would it make sense to try and unify these two, and what would that even mean?

This post is a continuation of my posts discussing the topic of associated type constructors (ATC) and higher-kinded types (HKT):

1. The first post focused on introducing the basic idea of ATC, as well as introducing some background material.
2. The second post showed how we can use ATC to model HKT, via the “family” pattern.
3. This post dives into what it would mean to support HKT directly in the language, instead of modeling them via the family pattern.

The story thus far (a quick recap)

In the previous posts, we had introduced a basic Collection trait that used ATC to support an iterate() method:

Hello. This post is a continuation of my posts discussing the topic of associated type constructors (ATC) and higher-kinded types (HKT):

1. The first post focused on introducing the basic idea of ATC, as well as introducing some background material.
2. 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.

The limits of associated type constructors

OK, so in the last post we saw how we can use ATC to define a Collection trait, and how to implement that trait for our sample collection List<T>. In particular, ATC let us express the return type of the iterator() method as Self::Iter<'iter>, so that we can incorporate the lifetime 'iter of each particular iterator.

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 particular, they enable us to add blanket impls like impl<T: Copy> Clone for T in a backwards compatible fashion, though only under certain conditions.

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. We’ll see that specialization actually couples together two things: refinement of behavior and reuse of code. This is no accident, and its normally a natural thing to do, but I’ll show that, in order to enable the kinds of blanket impls I want, it’s important to be able to tease those apart somewhat.

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. Hmm. That puts me back where I started from. Oh well, better try it again!” Obviously a less naive algorithm could keep a stack and then fail to execute, but it was precisely the logic of this stack that I was trying to capture in that restriction.

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. The second was that, in any given impl, the value of a ... z may be a type parameter which does not appear in the self type. I think I understated the importance of this second caveat. For example, consider the example I gave for simulating overloading:

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. The Swiss Einzahlungschein truly opened my eyes! Anyhow.)

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. This first one just describes the basics.