Ist Peano-Arithmetik mit Java Generics möglich?

Java-Forum Allgemeine Themen
1

Eine triviale Antwort wäre „ja“, denn Java Generics sind turing-komplett: https://arxiv.org/pdf/1605.05274.pdf

Was aber nicht so richtig weiterhilft, wenn man sowas schreiben will:

Vec<S<S<Z>>> v2 = new Vec<>(2, 3);
Vec<S<S<S<S<Z>>>>> v4 = v2.append(v2);

Ich weiß, dass in Scala so etwas möglich ist (https://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/), aber das lässt sich natürlich nicht einfach übersetzen.

Hat sich da schon jemand erfolgreicher als ich dran probiert?

2

Vermutlich ist das eigentlich keine Antwort wert, aber ich hab’ gerade mal ein paar Minuten rumprobiert:

package bytewelt;

public class Klaveer
{
    public static void main(String[] args)
    {
        Vec<Z> v0 = zero();
        Vec<S<Z>> v1 = succ(zero());
        Vec<S<S<Z>>> v2 = succ(v1);        
        Vec<S<S<S<Z>>>> v3 = succ(v2);        
        Vec<S<S<S<S<Z>>>>> v4 = succ(v3);
        Vec<S<S<S<S<S<Z>>>>>> v5 = succ(succ(succ(succ(succ(zero())))));
        Vec<S<S<S<S<S<S<Z>>>>>>> v6 = pred(succ(succ(v5)));
        
        Vec<S<S<S<S<S<Z>>>>>> result = v2.append(v3);
    }
    
    static Vec<Z> zero()
    {
        return new Vec<Z>(0);
    }
    static <T extends S<?>> Vec<S<T>> succ(Vec<T> pred)
    {
        return null;
    }
    static <T extends S<?>> Vec<T> pred(Vec<S<T>> succ)
    {
        return null;
    }
}

class Z extends S<Void>
{
}
class S<P>
{
}
class Vec<N extends S<?>>
{
    private final int n;
    Vec(int n)
    {
        this.n = n;
    }
    boolean isZero()
    {
        return n == 0;
    }
    
    public Vec<N> append0(Vec<Z> v)
    {
        return this;
    }
    public <A extends S<?>, R extends S<?>> Vec<R> append(Vec<A> v)
    {
        // Pseudocode goal:
        //return Klaveer.succ(this.append(Klaveer.pred(v)));
        
        // Hacks that don't work, of course...:
        if (v.isZero())
        {
            return (Vec<R>) this;
        }
        Vec<S<?>> p = Klaveer.pred((Vec<S<S<?>>>) v);
        Vec<S<N>> q = Klaveer.succ(this);
        return (Vec<R>) q;
    }
    
}

Wie in der auskommentierten Zeile steht: Der Grundgedanke war, das append irgendwie auf ein

return succ(append(pred(v)));

runterzubrechen, aber sooo direkt funktioniert das halt nicht: Man müßte irgendwie richtig den „Basisfall“ erkennen können (d.h. den Fall das v den Typ Vec<Z> hat). Ich hatte noch versucht, mich dem anzunähern, mit diesem isZero (was natürlich keinen Sinn ergibt aber ein Experiment war),
und vielleicht könnte man sich dem mit viel Gymnastik noch weiter annähern, aber ich glaube, bei dem eigentlichen Ziel (soweit ich das verstanden zu haben glaube), dem Typsystem die Arbeit zu überlassen (grob gesagt so, dass Eclipse bei

unknown = v2.append(v3);

und einem „Create Local Variable“ wirklich Vec<S<S<S<S<S<Z>>>>>> als Typ inferiert) wird einem die TypeErasure früher oder später einen Strich durch die Rechnung machen…

Edit: Aber mal nebenbei: Mein C++ - Bashing-Argument, dass Templates nicht entscheidbar sind, lass’ ich in Zukunft vielleicht lieber stecken :roll_eyes:

3

Ja, das Problem ist, dass man schon das append nicht vernünftig schreiben kann, noch nicht mal vom Typ her. Man scheint einen „Zwischentyp“ zu brauchen, ähnlich wie das HAppend hier: functionaljava/core/src/main/java/fj/data/hlist/HList.java at series/5.x · functionaljava/functionaljava · GitHub

Lustig, dass du das erwähnst, denn in C++ scheint das Ganze kein großes Problem zu sein: Implement Compile Time Peano Numbers – A Primer in C++ Template Metaprogramming | Yellow River and Blue Mountains

4

In C++ gibt’s die Type-Erasure nicht. Das ist eher ein Textersetzer. (D.h. ich schätze, dass es bei peano<10000000>::type den einen oder anderen Compiler raushauen würde :smiley: ). Wenn Java sowas wie

Vec<S<Z>> succ(Vec<Z> v) { ... }
<T> Vec<S<T>> succ(Vec<T> v) { ... } // für T != Z

auseinander halten könnte, wäre das ja auch kein Problem…