Instantly share code, notes, and snippets.
Save jbgi/208a1733f15cdcf78eb5 to your computer and use it in GitHub Desktop.
Generalized Algebraic Data Types (GADT) in Java
This file contains hidden or 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
| importstaticjava.lang.System.*; | |
| importjava.util.function.BiFunction; | |
| importjava.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. | |
| publicabstractclassTerm<T> {privateTerm(){} | |
| interfaceCases<R,T> { | |
| RZero(Function<Integer,T>id); | |
| RSucc(Term<Integer>pred,Function<Integer,T>id); | |
| RPred(Term<Integer>succ,Function<Integer,T>id); | |
| RIsZero(Term<Integer>a,Function<Boolean,T>id); | |
| RIf(Term<Boolean>cond,Term<T>then,Term<T>otherwise); | |
| } | |
| publicabstract <R>Rmatch(Cases<R,T>cases); | |
| publicstatic <T>Teval(finalTerm<T>term) { | |
| returnterm.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 | |
| )); | |
| } | |
| publicstatic <T>StringprettyPrint(finalTerm<T>term,finalintindentLevel) { | |
| returnterm.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) | |
| )); | |
| } | |
| staticStringindent(finalintindentLevel) { | |
| return"\n" +newString(newchar[indentLevel *2]).replace("\0"," "); | |
| } | |
| publicstaticvoidmain(finalString[]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 | |
| publicinterfaceIfCase<R,T> { | |
| Rapply(Term<Boolean>cond,Term<T>then,Term<T>otherwise); | |
| } | |
| publicstatic <R,T>Cases<R,T>cases( | |
| finalFunction<Function<Integer,T>,R>Zero, | |
| finalBiFunction<Term<Integer>,Function<Integer,T>,R>Succ, | |
| finalBiFunction<Term<Integer>,Function<Integer,T>,R>Pred, | |
| finalBiFunction<Term<Integer>,Function<Boolean,T>,R>IsZero, | |
| finalIfCase<R,T>If) { | |
| returnnewCases<R,T>() { | |
| publicRZero(finalFunction<Integer,T>id) { | |
| returnZero.apply(id); | |
| } | |
| publicRSucc(finalTerm<Integer>pred,finalFunction<Integer,T>id) { | |
| returnSucc.apply(pred,id); | |
| } | |
| publicRPred(finalTerm<Integer>succ,finalFunction<Integer,T>id) { | |
| returnPred.apply(succ,id); | |
| } | |
| publicRIsZero(finalTerm<Integer>a,finalFunction<Boolean,T>id) { | |
| returnIsZero.apply(a,id); | |
| } | |
| publicRIf(finalTerm<Boolean>cond,finalTerm<T>then,finalTerm<T>otherwise) { | |
| returnIf.apply(cond,then,otherwise); | |
| } | |
| }; | |
| } | |
| publicstaticfinalTerm<Integer>Zero =newTerm<Integer>() { | |
| public <R>Rmatch(finalCases<R,Integer>cases) { | |
| returncases.Zero(Function.identity()); | |
| } | |
| }; | |
| publicstaticTerm<Integer>Succ(finalTerm<Integer>pred) { | |
| returnnewTerm<Integer>() { | |
| public <R>Rmatch(finalCases<R,Integer>cases) { | |
| returncases.Succ(pred,Function.identity()); | |
| } | |
| }; | |
| } | |
| publicstaticTerm<Integer>Pred(finalTerm<Integer>succ) { | |
| returnnewTerm<Integer>() { | |
| public <R>Rmatch(finalCases<R,Integer>cases) { | |
| returncases.Pred(succ,Function.identity()); | |
| } | |
| }; | |
| } | |
| publicstaticTerm<Boolean>IsZero(finalTerm<Integer>a) { | |
| returnnewTerm<Boolean>() { | |
| public <R>Rmatch(finalCases<R,Boolean>cases) { | |
| returncases.IsZero(a,Function.identity()); | |
| } | |
| }; | |
| } | |
| publicstatic <T>Term<T>If(finalTerm<Boolean>cond,finalTerm<T>then,finalTerm<T>otherwise) { | |
| returnnewTerm<T>() { | |
| public <R>Rmatch(finalCases<R,T>cases) { | |
| returncases.If(cond,then,otherwise); | |
| } | |
| }; | |
| } | |
| } |
sir-wabbit commentedSep 27, 2016
This kind of ADT encoding doesn't play nicely with the lack of tailcall elimination in Java. Eachmatch is 3 function calls (match,Cases.X, andBiFunction.apply).
Sign up for freeto join this conversation on GitHub. Already have an account?Sign in to comment