-
-
Save danieldietrich/6861f6d0ee71eb5cacd6 to your computer and use it in GitHub Desktop.
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(){} | |
public interface F<A, B> {// Could be java.util.function.Function, | |
//used only for the visualy lighter apply method. | |
B __(A a); | |
} | |
interface Cases<R, T> { | |
R Zero(F<Integer, T> id); | |
R Succ(Term<Integer> pred, F<Integer, T> id); | |
R Pred(Term<Integer> succ, F<Integer, T> id); | |
R IsZero(Term<Integer> a, F<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( | |
(__) -> __.__(0),// eval Zero | |
(pred, __) -> __.__(eval(pred) + 1),// eval Succ | |
(succ, __) -> __.__(eval(succ) - 1),// eval Pred | |
(a, __) -> __.__(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( | |
(__) -> "0", | |
(pred, __) -> "Succ(" + prettyPrint(pred, indentLevel) + ")", | |
(succ, __) -> "Pred(" + prettyPrint(succ, indentLevel) + ")", | |
(a, __) -> "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", " "); | |
} | |
// Or if you prefer plain old visitor: | |
public static <T> T eval2(final Term<T> term) { | |
return term.match(new Cases<T, T>() { | |
public T Zero(final F<Integer, T> __) { | |
return __.__(0); | |
} | |
public T Succ(final Term<Integer> pred, final F<Integer, T> __) { | |
return __.__(eval(pred) + 1); | |
} | |
public T Pred(final Term<Integer> succ, final F<Integer, T> __) { | |
return __.__(eval(succ) - 1); | |
} | |
public T IsZero(final Term<Integer> a, final F<Boolean, T> __) { | |
return __.__(eval(a) == 0); | |
} | |
public T If(final Term<Boolean> cond, final Term<T> then, final Term<T> otherwise) { | |
return eval(cond) ? eval(then) : eval(otherwise); | |
} | |
}); | |
} | |
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 could be generated with a JSR-269 annotation processor | |
// (see eg. https://github.com/sviperll/adt4j) | |
static <A> F<A, A> id() { | |
return a -> a; | |
} | |
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<F<Integer, T>, R> Zero, | |
final BiFunction<Term<Integer>, F<Integer, T>, R> Succ, | |
final BiFunction<Term<Integer>, F<Integer, T>, R> Pred, | |
final BiFunction<Term<Integer>, F<Boolean, T>, R> IsZero, | |
final IfCase<R, T> If) { | |
return new Cases<R, T>() { | |
public R Zero(final F<Integer, T> id) { | |
return Zero.apply(id); | |
} | |
public R Succ(final Term<Integer> pred, final F<Integer, T> id) { | |
return Succ.apply(pred, id); | |
} | |
public R Pred(final Term<Integer> succ, final F<Integer, T> id) { | |
return Pred.apply(succ, id); | |
} | |
public R IsZero(final Term<Integer> a, final F<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(id()); | |
} | |
}; | |
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, id()); | |
} | |
}; | |
} | |
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, id()); | |
} | |
}; | |
} | |
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, id()); | |
} | |
}; | |
} | |
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