Skip to content

Instantly share code, notes, and snippets.

@jbgi
Last active September 25, 2023 00:45
Show Gist options
  • Save jbgi/208a1733f15cdcf78eb5 to your computer and use it in GitHub Desktop.
Save jbgi/208a1733f15cdcf78eb5 to your computer and use it in GitHub Desktop.
Generalized Algebraic Data Types (GADT) in 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);
}
};
}
}
@sir-wabbit
Copy link

This kind of ADT encoding doesn't play nicely with the lack of tailcall elimination in Java. Each match is 3 function calls (match, Cases.X, and BiFunction.apply).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment