Skip to content

Instantly share code, notes, and snippets.

@jbgi jbgi/Term.java
Last active Nov 3, 2018

Embed
What would you like to do?
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);
}
};
}
}
@alexknvl

This comment has been minimized.

Copy link

commented Sep 27, 2016

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
You can’t perform that action at this time.