Fix a comment

[mgeier]

No description provided.

[mgeier]

BTW, cool article!

I was wondering though, whether you consider const generics part of the Rust type system?

If you only want to do "First Grade Math in Rust's Type System", you could as well use const generics, which already provide that math, right?
And you are actually already using that in your Value impl, so you might as well use it all the way, e.g.:

struct Add<T, U>(PhantomData<T>, PhantomData<U>);
impl<T: Value, U: Value> Value for Add<T, U> {
    const VALUE: usize = T::VALUE + U::VALUE;
}

struct Sub<T, U>(PhantomData<T>, PhantomData<U>);
impl<T: Value, U: Value> Value for Sub<T, U> {
    const VALUE: usize = T::VALUE.saturating_sub(U::VALUE);
}

struct Mul<T, U>(PhantomData<T>, PhantomData<U>);
impl<T: Value, U: Value> Value for Mul<T, U> {
    const VALUE: usize = T::VALUE * U::VALUE;
}

struct Div<T, U>(PhantomData<T>, PhantomData<U>);
impl<T: Value, U: Value> Value for Div<T, U> {
    const VALUE: usize = T::VALUE / U::VALUE;
}

playground

[fprasx]

Thanks!

Yeah, there is an eentsy bit of cheating for convenience (which I know, the rest of this eschews). You could avoid it by writing:

impl Value for Zero {
    const VALUE = 0;
}
impl Value for Succ<Zero> {
    const VALUE = 1;
}
...

but that would be super inconvenient. Could also be a macro 😄

Ultimately, you need some way of converting from Church/Peano encodings back into integers, so there's bound to be some numbers. I think the important part is showing that you can do do arithmetic in the Church/Peano domain, and this can be represented in the type system.

EDIT: I didn't actually answer your question! Yes, I do consider them part of the type system, but it's more interesting to see if we can make use of other areas to do the calculation.

Thanks for reading!

[mgeier]

Yeah, there is an eentsy bit of cheating for convenience (which I know, the rest of this eschews).

Yeah, it kinda undermines the purity of the whole thing.

Ultimately, you need some way of converting from Church/Peano encodings back into integers, so there's bound to be some numbers.

But is that really so?
You are not starting with numeric types, so why would you need to end with them?

I think the important part is showing that you can do do arithmetic in the Church/Peano domain, and this can be represented in the type system.

Yeah, but it would be more convincing if you could also say "no numeric literals", "no numeric types" and "no operators", wouldn't it?

I did some experimenting and came up with a solution that lets me do type-level compile-time checks outside of main() like this, without mentioning any numbers explicitly:

assert_same!(
    Mul<Add<encode!(*), encode!(**)>, encode!(***)>,
    encode!(*********)
);

playground

This also makes the impls arguably a bit simpler (by moving some stuff into macros), e.g.:

define_binary_function!(Div, DivImpl);

impl<U> Value for DivImpl<Zero, Succ<U>> {
    type Evaluate = Zero;
}

impl<T, U> Value for DivImpl<Succ<T>, Succ<U>> {
    // x = Succ<T>
    // y = Succ<U>
    type Evaluate = Mul<
        // if x >= y: ... else: 0
        GreaterOrEqual<Succ<T>, Succ<U>>,
        // 1 + (x - y) / y
        Add<Succ<Zero>, Div<Sub<Succ<T>, Succ<U>>, Succ<U>>>,
    >;
}

What do you think about that approach?

[fprasx]

You are not starting with numeric types, so why would you need to end with them?
&
Yeah, but it would be more convincing if you could also say "no numeric literals", "no numeric types" and "no operators", wouldn't it?

I wanted to extract them into real integers so we can print them, but yeah, never leaving the "type domain" means we don't need any "numbery stuff" at all (and removing the Value trait would fix this).

I like your implementation - the macro definitely clears things up a bit. I wanted to avoid macros in general so you can see the traits at work more, but if I was going to actually use something like this I'd do something like what you have.

[mgeier]

the macro definitely clears things up a bit. I wanted to avoid macros in general

The macro does nothing magical. It just avoids copy-pasting this 4 times (and changing the struct names):

struct Add<T, U>(PhantomData<T>, PhantomData<U>);

struct AddImpl<T, U>(PhantomData<T>, PhantomData<U>);

impl<T: Value, U: Value> Value for Add<T, U>
where
    AddImpl<<T as Value>::Evaluate, <U as Value>::Evaluate>: Value,
    <AddImpl<<T as Value>::Evaluate, <U as Value>::Evaluate> as Value>::Evaluate: Value,
{
    // NB: We evaluate the result twice to simplify other impls
    type Evaluate = <<AddImpl<<T as Value>::Evaluate, <U as Value>::Evaluate> as Value>::Evaluate as Value>::Evaluate;
}

If you want to avoid the macro, you can do the copy-pasting instead.

I've also just found out (thanks to rust-lang/rust#38078 (comment)) that this can be dramatically shortened (and IMHO clarified!) with a simple type definition:

type Eval<T> = <T as Value>::Evaluate;

impl<T: Value, U: Value> Value for Add<T, U>
where
    AddImpl<Eval<T>, Eval<U>>: Value,
    Eval<AddImpl<Eval<T>, Eval<U>>>: Value,
{
    // NB: We evaluate the result twice to simplify other impls
    type Evaluate = Eval<Eval<AddImpl<Eval<T>, Eval<U>>>>;
}

I think what really clears things up is the additional level of indirection, which allows to factor out the evaluation of the two inputs and the double-evaluation of the result. This allows me to get rid of the explicit evaluation (Eval<...> or <... as Value>::Evaluate) and all where clauses in the following impls, where the really interesting things happen:

impl<T, U> Value for DivImpl<Succ<T>, Succ<U>> {
    type Evaluate = Mul<
        // if x >= y: ... else: 0
        GreaterOrEqual<Succ<T>, Succ<U>>,
        // 1 + (x - y) / y
        Add<Succ<Zero>, Div<Sub<Succ<T>, Succ<U>>, Succ<U>>>,
    >;
}

Compare this to the monstrosity (your word) from your blog post (which doesn't even include the expansion of RawQuotient):

impl<T, U> Div for (Succ<T>, Succ<Succ<U>>)
where
    (T, Succ<U>): Sub,
    (<(T, Succ<U>) as Sub>::Diff, Succ<Succ<U>>): Div,
    (
        Succ<Zero>,
        <(<(T, Succ<U>) as Sub>::Diff, Succ<Succ<U>>) as Div>::Quotient,
    ): Add,
    (
        <(Succ<T>, Succ<Succ<U>>) as GreaterThanEq>::Greater,
        <(
            Succ<Zero>,
            <(<(T, Succ<U>) as Sub>::Diff, Succ<Succ<U>>) as Div>::Quotient,
        ) as Add>::Sum,
    ): Mul,
    (Succ<T>, Succ<Succ<U>>): GreaterThanEq,
{
    // Hi I'm the important part
    type Quotient = <(
        <(Succ<T>, Succ<Succ<U>>) as GreaterThanEq>::Greater,
        RawQuotient<T, U>,
    ) as Mul>::Product;
}

BTW, I'm not sure if you need the Succ<Succ<U>> here. I'm only using Succ<U> and it seems to work fine. But I might have missed something.

Here is an updated version of my code, where I have also renamed a few things to make it hopefully easier to read: playground

[mgeier]

I found a way to implement it without the macro: playground

I'm not sure if that's easier to understand, though.

[fprasx]

The macro does nothing magical. It just avoids copy-pasting this 4 times (and changing the
struct names):

Agreed, I just mean it's a big win for code clarity!

type Eval<T> = <T as Value>::Evaluate;

This is . . . very nice.

impl<T, U> Value for DivImpl<Succ<T>, Succ<U>> {
    type Evaluate = Mul<
        // if x >= y: ... else: 0
        GreaterOrEqual<Succ<T>, Succ<U>>,
        // 1 + (x - y) / y
        Add<Succ<Zero>, Div<Sub<Succ<T>, Succ<U>>, Succ<U>>>,
    >;
}

This too!

You should consider writing something of your own; if you do, let me know and I'll link to it at the bottom of my post :)

[mgeier]

You should consider writing something of your own

I don't really feel like writing about this stuff ... but I do like tinkering with it.

[fprasx]

Me too :)

[mgeier]

Just for the record: Here is a version of my approach incorporating the impl simplifications from fprasx/arts#5: playground