Last active
September 25, 2023 00:45
-
-
Save jbgi/208a1733f15cdcf78eb5 to your computer and use it in GitHub Desktop.
Generalized Algebraic Data Types (GADT) in Java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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); | |
} | |
}; | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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
, andBiFunction.apply
).