Arithmetic with the type system

[Alan Karp]

https://gist.github.com/gretingz/bc194c20a2de2c7bcc0f457282ba2662

It looks to me like Church numerals in Rust.  Is it?

--------------
Alan Karp

[Kevin Reid]

On Sat, Oct 17, 2020 at 6:24 PM Alan Karp <alan...@gmail.com> wrote:

https://gist.github.com/gretingz/bc194c20a2de2c7bcc0f457282ba2662

It looks to me like Church numerals in Rust.  Is it?

I'd say they aren't Church numerals, but they are Peano numbers, of which Church numerals could be considered a special case. Peano numbers are representing natural numbers as "a number is either zero or the successor of a number".

(Note: The precise term "Peano number" seems to be a Haskellism; I didn't find a clearly standard academic term.)

Church numerals are functions, and in this system zero is not a function even at the type level. Here, we are working within a system that has equality of structures, and writing "zero" and "successor" directly in that system. It's the type-level analogue of the straightforward algebraic data type:

#[derive(Copy, Clone, Eq, PartialEq)]

pub enum Number {

    Zero,

    Successor(Box<Number>),

}

 

You can give this an "apply" method to get Church numeral behavior, but it doesn't naturally have one.

[Tony Arcieri]

Note that the "typenum" crate provides an implementation of this concept which is actually leveraged in production Rust code:

https://docs.rs/typenum/

It's somewhat painful to use due to the type signatures it generates though, and will ideally be obsoleted by const generics at some point in the future.

--

Tony Arcieri