Proof's by induction using Rust's type-system

[AnthonyMikh]

fn test_is_nat<T: Nat>() -> () {}

fn main() {
   test_is_nat::<_0>();
   test_is_nat::<_1>();
   test_is_nat::<_2>();
   // ...
}

Вызывать эти функции несколько избыточно, для проверки типов достаточно их инстанцировать:

fn test_is_nat<T: Nat>() -> () {}

fn main() {
   test_is_nat::<_0>;
   test_is_nat::<_1>;
   test_is_nat::<_2>;
   // ...
}

Now to check whether < is holding holds 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.

Это и несколько избыточно, и ненадёжно: перед каждым реальным использованием нужно вызывать ничего не делающий метод для того, чтобы зафорсить проверку типов. Проще это требование поместить непосредственно на определение ProofLt, благо Rust это позволяет:

struct ProofLt<A: Nat, B: Nat>(A, B)
where
    Self: Lt<A, B>;

С таким определением создать невалидное значение доказательства попросту невозможно.

trait Lt<A: Nat, B: Nat> {
   fn check() -> () {}
}

Стрелка после списка параметров избыточна, если тип возвращаемого значения функции не указан, то он считается ().

<shameless_plug> Более продвинутую демонстрацию type-level программирования на Rust можно посмотреть в моей статье: https://habr.com/ru/post/578198 </shameless_plug>