Generalized Algebraic Data Types (GADT) in Java

Term.java

import static java.lang.System.*;

import java.util.function.BiFunction;
import java.util.function.Function;

// Implementation of a pseudo-GADT in Java, translating the examples from
// http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf
// The technique presented below is, in fact, just an encoding of a normal Algebraic Data Type
// using a variation of the visitor pattern + the application of the Yoneda lemma to make it
// isomorphic to the targeted 'GADT'.
// Highlights:
// -> no cast and no subtyping.
// -> all of the eval function logic is static and not scattered all around Term subclasses.
public abstract class Term<T> { private Term(){}

    interface Cases<R, T> {
        R Zero(Function<Integer, T> id);
        R Succ(Term<Integer> pred, Function<Integer, T> id);
        R Pred(Term<Integer> succ, Function<Integer, T> id);
        R IsZero(Term<Integer> a, Function<Boolean, T> id);
        R If(Term<Boolean> cond, Term<T> then, Term<T> otherwise);
    }

    public abstract <R> R match(Cases<R, T> cases);

    public static <T> T eval(final Term<T> term) {
        return term.match(
               cases(
                 (id)                    -> id.apply(0),// eval Zero
                 (pred, id)              -> id.apply(eval(pred) + 1),// eval Succ
                 (succ, id)              -> id.apply(eval(succ) - 1),// eval Pred
                 (a, id)                 -> id.apply(eval(a) == 0),// eval IsZero
                 (cond, then, otherwise) -> eval(cond) ? eval(then) : eval(otherwise)// eval If
               ));
    }
    
    public static <T> String prettyPrint(final Term<T> term, final int indentLevel) {
        return term.match(cases(
                (id)                    -> "0",
                (pred, id)              -> "Succ(" + prettyPrint(pred, indentLevel) + ")",
                (succ, id)              -> "Pred(" + prettyPrint(succ, indentLevel) + ")",
                (a, id)                 -> "IsZero(" + prettyPrint(a, indentLevel) + ")",
                (cond, then, otherwise) -> indent(indentLevel) + "if " + prettyPrint(cond, indentLevel + 1)
                                         + indent(indentLevel) + "then " + prettyPrint(then, indentLevel + 1)
                                         + indent(indentLevel) + "else " + prettyPrint(otherwise, indentLevel + 1)
        ));
    }

    static String indent(final int indentLevel) {
        return "\n" + new String(new char[indentLevel * 2]).replace("\0", " ");
    }

    public static void main(final String[] args) {
        Term<Integer> one = Succ(Zero);
        out.println(eval(one)); // "1"
        out.println(eval(IsZero(one))); // "false"
        // IsZero(IsZero(one)); // does not compile:
        // "The method IsZero(Term<Integer>) in the type Term<T> is not
        // applicable for the arguments (Term<Boolean>)"
        out.println(eval(If(IsZero(one), Zero, one))); // "1"
        Term<Boolean> True = IsZero(Zero);
        Term<Boolean> False = IsZero(one);
        out.println(eval(If(True, True, False))); // "true"
        out.println(prettyPrint(If(True, True, False), 0)); // "if IsZero(0)
                                                         //  then IsZero(0)
                                                         //  else IsZero(Succ(0))"
    }

    // All of what follows is boring and can be generated with Derive4J, an JSR-269 annotation processor:
    // https://github.com/derive4j/derive4j

    public interface IfCase<R, T> {
        R apply(Term<Boolean> cond, Term<T> then, Term<T> otherwise);
    }

    public static <R, T> Cases<R, T> cases(
        final Function<Function<Integer, T>, R> Zero,
        final BiFunction<Term<Integer>, Function<Integer, T>, R> Succ,
        final BiFunction<Term<Integer>, Function<Integer, T>, R> Pred,
        final BiFunction<Term<Integer>, Function<Boolean, T>, R> IsZero,
        final IfCase<R, T> If) {
        return new Cases<R, T>() {
            public R Zero(final Function<Integer, T> id) {
                return Zero.apply(id);
            }
            public R Succ(final Term<Integer> pred, final Function<Integer, T> id) {
                return Succ.apply(pred, id);
            }
            public R Pred(final Term<Integer> succ, final Function<Integer, T> id) {
                return Pred.apply(succ, id);
            }
            public R IsZero(final Term<Integer> a, final Function<Boolean, T> id) {
                return IsZero.apply(a, id);
            }
            public R If(final Term<Boolean> cond, final Term<T> then, final Term<T> otherwise) {
                return If.apply(cond, then, otherwise);
            }
        };
    }

    public static final Term<Integer> Zero = new Term<Integer>() {
        public <R> R match(final Cases<R, Integer> cases) {
            return cases.Zero(Function.identity());
        }
    };

    public static Term<Integer> Succ(final Term<Integer> pred) {
        return new Term<Integer>() {
            public <R> R match(final Cases<R, Integer> cases) {
                return cases.Succ(pred, Function.identity());
            }
        };
    }

    public static Term<Integer> Pred(final Term<Integer> succ) {
        return new Term<Integer>() {
            public <R> R match(final Cases<R, Integer> cases) {
                return cases.Pred(succ, Function.identity());
            }
        };
    }

    public static Term<Boolean> IsZero(final Term<Integer> a) {
        return new Term<Boolean>() {
            public <R> R match(final Cases<R, Boolean> cases) {
                return cases.IsZero(a, Function.identity());
            }
        };
    }

    public static <T> Term<T> If(final Term<Boolean> cond, final Term<T> then, final Term<T> otherwise) {
        return new Term<T>() {
            public <R> R match(final Cases<R, T> cases) {
                return cases.If(cond, then, otherwise);
            }
        };
    }
}