Llogiq on stuff

Type-Level Shenanigans

(This is an extended treatment of the topic of my recent talk at the Rhein-Main Rust Meetup). The code presented should work with Rust 1.3 and following)

If you have programmed anything of interest in Rust, you probably know that it has an awesome type system (that enables the propagation of lifetime constraints, among other things). What you may not know is that the type system is also Turing-complete. Also for some strange reason, seeing cool things encoded in type system gives me warm fuzzy feelings. So it’s hopefully understandable why I look into this topic.

WARNING: EVIL HACK AHEAD!

You can think of Rust’s type system as a Prolog with very weird syntax. To make the type system do calculations, we need to keep it apart from runtime, yet encode our calculations as a series of types. Here’s a simple set of types to implement Kleene logic:

struct True;
struct Unknown;
struct False;

Note that all of those structs are zero-sized, so they will be compiled to nothnig.

Update: Redditor james-darkfox points out that using an empty enum, e.g. enum True {} instead of struct True; will ensure that the type can never be instantiated. This is a good idea, as we want to stay in compile time.

Why not?

Operations are then implemented by traits and (multiple) trait impls:

use std::ops::Not; // why build our own trait when we can have std::ops?

impl Not for True {
    type Output = False; // associated type
    fn not(self) -> Self::Output { unreachable!() } // guard against accidents
}

impl Not for Unknown {
    type Output = Unknown;
    fn not(self) -> Self::Output { unreachable!() }
}

impl Not for False {
    type Output = True;
    fn not(self) -> Self::Output { unreachable!() }
}

Using this operation is as simple as writing <X as Not>::Output. Yes, that’s ugly. Yes, it becomes even more ugly with nesting. Still, with the right incantation, we now have a calculation that is done entirely within the type system.

Sake of the Argument

In our example above, the only input to our “function” was the Self type. Which is ok if we only use functions of a single value, which can be proven to be workable anyway, but we have a better solution to get multiple arguments: Generics. For example, let’s implement std::ops::BitAnd, which has a generic Rhs parameter:

use std::ops::BitAnd;

impl<X> BitAnd<X> for True {
    type Output = X;
    fn bitand(self, _: X) -> Self::Output { unreachable!() }
}

impl<X> BitAnd<X> for False {
    type Output = False;
    fn bitand(self, _: X) -> Self::Output { unreachable!() }
}

impl BitAnd<True> for Unknown { // generic fixed to True here
    type Output = Unknown;
    fn bitand(self, _: True) -> Self::Output { unreachable!() }
}

impl BitAnd for Unknown { // works because `Rhs = Self`
    type Output = Unknown
    fn bitand(self, _: Unknown) -> Self::Output { unreachable!() }
}

impl BitAnd<False> for Unknown {
    type Output = False;
    fn bitand(self, _: False) -> Self::Output { unreachable!() }
}

What’s it does?

Now to have this actually be useful, we need to either output or somehow compare the types. To assert that two types are actually the same, we can implement a Same trait:

pub trait Same<Rhs = Self> {
    /// Should always be `Self`
    type Output;
}

impl<T> Same<T> for T {
    type Output = T; // this is occasionally useful
}

Now if we write <<True as Not>::Output as Same<False>>::Output in our code, we will get a False type and a compile time assertion that ¬⊤ is indeed the same as ⊥. On the other hand, <True as Same<Unknown>>::Output will result in a compiler error. So we can coax the type system into proving assertions for us.

While this alone is highly useful, we also may want to take the information out of our types and transform it into some value that is usable at runtime. For example, we could use an enum and add a trait to convert to that:

pub enum Ternary { T, U, F }

pub trait ToTernary {
    fn to_ternary() -> Ternary;
}

impl ToTernary for True {
    #[inline] fn to_ternary() -> Ternary { Ternary::T }
}

impl ToTernary for Unknown {
    #[inline] fn to_ternary() -> Ternary { Ternary::U }
}

impl ToTernary for False {
    #[inline] fn to_ternary() -> Ternary { Ternary::F }
}

Now <True as Not>::Output::to_ternary() will be a (constant) Ternary::F (be sure to inline as in the above code!).

We also may want to introduce a X: ToTernary bound for our BitAnd impls, e.g.

impl<X: ToTernary> BitAnd<X> for True {
    type Output = X;
    fn bitand(self, _: X) -> Self::Output { unreachable!() }
}

to ensure we can convert the results of a BitAnd operation to a Ternary.

The Phantom Tenace

Ok, let’s say we want to use more than one value. For example when representing numbers, needing one type per representable number will severely restrict usefulness of our types; and we’d also need a lot of trait impls, too. Those things tend to explode exponentially unless we tame them with generics (which has its own problem as we will see later).

So why not use a generic tuple of zero-sized types?

// somehow we must restrict U and V to be zero-sized?
struct<U, V> Pair<U, V> (U, V);

This has a problem: The compiler cannot assure that our Pair is zero-sized. In fact, it isn’t – we can construct a Pair<u32, u32>, which has a size of 8 bytes. We need to somehow make the types invisible to the part of the compiler that calculates sizes. Invisible like.. a phantom. Turns out Rust has PhantomData<_> to let us do this:

/// now we can have a zero-sized `Pair<True, False>`.
struct<U, V> Pair<U, V>(PhantomData<(U, V)>);

In fact, this is how typenum stores unsigned integers (and integers). Imagine a pair as a pair of boxes which can take two generic types. Also have a terminator (which is basically an empty box). Then, for example the unsigned number 9 becomes (the first type is displayed as arrow to make the graphic easier to understand; there is no reference actually):

 1  0  0  1 

Or in Rust:UInt<UInt<UInt<UInt<UTerm, B1>, B0>, B0>, B1>. Yes, it’s ugly. No, it won’t get better than that until we get actual type numerals in Rust.

No-where, man.

When using generic types, we often want to restrict the type space to types implementing certain traits (for example, in typenum, UInt operations must result in types bound by Unsigned which allows to convert to various unsigned integer types). This can be done by specifying type bounds in the Generic definition (see the end of the previous section) or by where clauses.

The nice thing when doing this is that we can simply write the code without the clauses and the compiler will tell us the missing definitions.

For example, in typenum, src/int.rs the following definition (here without where):

impl<Ul: Unsigned + NonZero, Ur: Unsigned + NonZero>
        Add<PInt<Ur>> for PInt<Ul> {
    type Output = PInt<<Ul as Add<Ur>>::Output>; // …
}

will lead to the following error:

src/uint.rs:241:1: 247:2 error: the trait `core::ops::Add<Ur>` is
                         not implemented for the type `Ul` [E0277]
src/uint.rs:241 impl<Ul: Unsigned, Ur: Unsigned> Add<Ul, Ur>…

So we can simply add this:

impl<Ul: Unsigned + NonZero, Ur: Unsigned + NonZero>
        Add<PInt<Ur>> for PInt<Ul>
    where Ul: Add<Ur>, // to appease the compiler
          <Ul as Add<Ur>>::Output: Unsigned + NonZero { // for subsequent use
    type Output = PInt<<Ul as Add<Ur>>::Output>;
    fn add(self, _: PInt<Ur>) -> Self::Output { unreachable!() }
}

Shiny!

The not so nice thing is rust issue #26325 which says that the compiler will sometimes do a brute force search through the type space on certain combinations of generics and where clauses (remember when I told you of exponentially exploding clauses? Here they are).

There are two ways of dealing with this:

  • reducing generics and re-coding all the variants (which is a workable solution wherever we only have a few of them)
  • introducing private traits to bind intermediate results

Both can help or not. I don’t have any useful intuition on when it works, so my only recourse is to benchmark and find out – I try to keep my algorithms in O(log n), which means they will devolve to linear runtime, which is easy enough to check. Currently, integer division / remainder in typenum has this problem, and we haven’t yet found a way of doing any of the above that would help.

Lies, Damn Lies and Benchmarks

Speaking of which, we should be able to test and benchmark this stuff. A nice way to do this is to use rustc from within the test code. See typenum for a nice usage example which includes a build script and some macros to make those tests very readable, yet effective.

At the moment, I don’t think low-level performance (as far as you can call it that) is too interesting, If the algorithms are in the right O(..) bracket and one doesn’t trigger the aforementioned bug, it should be plenty fast (That said, I once managed to crash rustc with peano trying to multiply 8 × 3).

Wrapping up

The code for the ternary logic is on my github. I may also experiment a bit more with type data structures in the future, e.g. I have an idea on how to represent something b-tree like within types, which could pave the way for other funny things.

In the meantime, discuss this on /r/rust or rust-users.