Algebra With Types

David Sanders via Digitalmars-d-learn digitalmars-d-learn at puremagic.com
Mon Apr 24 14:27:53 PDT 2017


On Friday, 21 April 2017 at 20:49:27 UTC, Meta wrote:
> On Friday, 21 April 2017 at 18:54:38 UTC, David Sanders wrote:
>> [...]
>
> As an aside, there's a less convoluted way to do type-level 
> arithmetic which is IMO also more concise and looks nicer. You 
> don't have to mess around with Algebraic at all:
>
> struct Zero;
>
> struct Succ(N);
>
> alias One = Succ!Zero;
>
> alias Pred(N: Zero)        = Zero;
> alias Pred(N: Succ!Np, Np) = Np;
>
> alias Add(N1: Zero, N2: Zero) = Zero;
> alias Add(N1,       N2: Zero) = N1;
> alias Add(N1: Zero, N2)       = N2;
> alias Add(N1,       N2)       = Add!(Succ!N1, Pred!N2);
>
> void main()
> {
>     static assert(is(Pred!One == Zero));
>     static assert(is(Succ!One == Succ!(Succ!Zero)));
>
>     static assert(is(Add!(Zero, Zero) == Zero));
>     static assert(is(Add!(Zero, One) == One));
>     static assert(is(Add!(One, Zero) == One));
>     static assert(is(Add!(One, One) == Succ!(Succ!(Zero))));
>
>     alias Two = Succ!One;
>     static assert(is(Add!(One, One) == Two));
>     static assert(is(Add!(One, Two) == 
> Succ!(Succ!(Succ!Zero))));
>
>     static assert(is(Sub!(Zero, Zero) == Zero));
>     static assert(is(Sub!(One, Zero) == One));
>     static assert(is(Sub!(Zero, One) == Zero));
>     static assert(is(Sub!(Two, One) == One));
>     static assert(is(Sub!(One, Two) == Zero));
> }
>
> Implementing Mul, Div and the integer set is an exercise left 
> to the reader.

What you've implemented is similar to the Church encoding for 
natural numbers. I'm not trying to encode natural numbers.

I'm trying to investigate the algebra of "adding", "multiplying", 
and "raising to a power" various data types. Adding the int type 
with the char type corresponds to Algebraic!(int, char). 
Multiplying the int type by the char type corresponds to 
Tuple!(int, char). Raising the int type to the char type 
corresponds to a function that accepts a char and returns an int. 
See the blog post in my original forum post for examples.

Thanks,
Dave


More information about the Digitalmars-d-learn mailing list