Roman Kotelnikov
27 Sep 2021
•
5 min read
Rust's type system is quite powerful as it allows to encode complex relationships between user-defined types using recursive rules that are automatically applied by the compiler. Idea behind this post is to use some of those rules to encode properties of our domain. Here we take a look at Peano axioms defined for natural numbers and try to derive some of them using traits, trait bounds and recursive impl blocks. We want to make the compiler work for us by verifying facts about our domain, so that we could invoke the compiler to check whether a particular statement holds or not. Our end goal is to encode natural numbers as types and their relationships as traits such that only valid relationships would compile. (e.g. in case we define types for 1 and 3 and relationship of less than, 1 < 3 should compile but 3 < 1 shouldn't, that all would be encoded using Rust's language syntax of course)
Let's define some natural numbers on the type level first.
struct _0;
struct Succ<T>(T);
Here we use structs to define elements of the natural set. We can start with _0
and use the type constructor Succ
to create types for each natural number. Succ
here is short for successor and we encode Succ<N>
as successor of N
, the natural number that goes straight after N
.
Important note is that each element is represented by the type itself, not a value of that type, we don't plan to instantiate any values here.
We have to manually construct 1, 2, 3, ... at this point. It should be possible to workaround that but we won't get into those details just yet.
type _1 = Succ<_0>;
type _2 = Succ<_1>;
type _3 = Succ<_2>;
type _4 = Succ<_3>;
type _5 = Succ<_4>;
Now we have types for 1, 2, 3, 4 and 5 but they are hardly useful on their own as they are just labels without any meaning attached.
Let's now define the first property that must hold, which is that all of those numbers are natural numbers. We will use the trait Nat
for this task.
trait Nat {}
Then we implement this trait for types we have just defined using impl
blocks.
impl Nat for _0 {}
impl<T: Nat> Nat for Succ<T> {}
Notice here the second impl
block is taking parameter T
and is implementing Nat
for the successor of that type. This is essentially encoding the property that natural numbers are closed with respect to addition, if you keep adding one to the natural number you still get a natural number.
We've encoded some rules but how do we actually check them? Let's use type bounds and helper functions for that.
First define a function to test whether all number types we have defined are indeed natural (implement Nat
)
fn test_is_nat<T: Nat>() -> () {}
fn main() {
test_is_nat::<_0>();
test_is_nat::<_1>();
test_is_nat::<_2>();
// ...
}
Notice that the function is empty as we are only interested in types of our program.
Now this compiles, which means our property holds. That's great but hardly that interesting.
Let's define a trait Lt
that would take two type parameters A
and B
. The meaning of this trait would be the relationship between types A
and B
, that is A < B
in terms of natural numbers.
In this post we will only consider less than (<
) but deriving various other laws should be similar.
trait Lt<A: Nat, B: Nat> {}
Let's try to derive laws for Lt
using what we have defined so far. To formalize it using induction we can take following approach:
0
is less than any natural number, this is going to be base case of inductionA
and B
, such that A
is less than B
we can state that Succ<A>
is less than Succ<B>
(if we add one to both sides of valid inequality, the inequality should still hold)However before we define those rules using impl
blocks as we did for Nat
traits we need to define another additional type. When describing whether type is a natural number we used that particular type as a target to implement trait Nat
(what goes after for
in impl
definition). In case of Lt
relationship however we need to capture both types into that target type so let's create another struct and call it ProofLt
, naming choice would make more sense later.
struct ProofLt<A: Nat, B: Nat>(A, B);
Another auxiliary bit we need here is the NonZero
trait that would represent any natural number except for zero, we will need it to encode a base case for our induction.
// we also need to amend our `Succ` definition to make it work
struct Succ<T: Nat>(T);
trait NonZero: Nat {}
impl<N: Nat> NonZero for Succ<N> {}
We include only natural numbers that are produced by applying Succ
type constructor, thus excluding _0
.
Now let's use ProofLt
as a target type to define less than relationship.
Encoding the base case is straightforward: we literally translate the rule, for any N
that is not a zero, _0
is less than that N
.
impl<N: NonZero> Lt<_0, N> for ProofLt<_0, N> {}
The key to encoding the induction step is to restrict recursive rule by adding where
clause with constraint.
impl<A: Nat, B: Nat> Lt<Succ<A>, Succ<B>> for ProofLt<Succ<A>, Succ<B>>
where ProofLt<A, B>: Lt<A, B> {}
Here we only implement Lt
for successors of A
and B
if property is less than held for A
and B
themselves.
As this rule is applied recursively, this is just enough for us to encode Lt
for any two natural numbers. Compiler will do the heavy lifting for us here by recursively unwinding type definitions of types in questions until it hits the base case.
Now to check whether <
is holding for some types A
and B
we could use our ProofLt
struct to summon Lt
trait implementations, but in order to do this we need to define some method on the Lt
trait we could call. In case a method is found and compilation succeeds we can conclude that Lt
is implemented for that pair for types, thus <
property holds, otherwise it doesn't.
Let's amend our Lt
definition with this extra function.
trait Lt<A: Nat, B: Nat> {
fn check() -> () {}
}
Semantically this function would mean that Lt
property is holding and we should only be able to call this function on our target type ProofLt
in case Lt
indeed holds. Otherwise the compiler should yell at us failing to find function definition. Again we are not really interested in calling this function (thus empty body and argument list), but whether it is there or not.
fn main() {
// this is actually only using our base case of induction
ProofLt::<_0, _1>::check();
// now the real test
ProofLt::<_1, _3>::check();
}
Yay, it works! Now let's try to check whether it indeed rejects invalid examples.
fn main() {
ProofLt::<_3, _2>::check();
}
If we try to compile above code, the compiler would yell at us with something like
// | struct ProofLt<A: Nat, B: Nat>(A, B);
// | -------------------------------------
// | |
// | function or associated item `check` not found for this
// | doesn't satisfy `_: Lt<Succ<Succ<Succ<_0>>>, Succ<Succ<_0>>>`
// | doesn't satisfy `_: Lt<Succ<Succ<_0>>, Succ<_0>>`
It failed to find the associated function check
because trait Lt
is not implemented for this variant of ProofLt
.
And this is exactly what we wanted to encode!
You can play around more with ProofLt
and interactive examples at https://wg-romank.github.io/peano/
There's also a link to Rust Playground to get a feel for it.
Now this is all obscure and abstract, but it is actually very powerful concept that can help us define properties from our domain in software and ensure that those properties hold using the compiler itself for verification.
This work was very much inspired by similar feature set of Scala that is using implicits as facts that can be derived on other types, if you are curious to learn more check out this video by Rock The Jvm touching on a subject
Roman Kotelnikov
See other articles by Roman
Ground Floor, Verse Building, 18 Brunswick Place, London, N1 6DZ
108 E 16th Street, New York, NY 10003
Join over 111,000 others and get access to exclusive content, job opportunities and more!