Variants/case classes/algebraic data types/sums/oh my! (original) (raw)

forax at univ-mlv.fr forax at univ-mlv.fr
Sat Jun 18 22:09:59 UTC 2016

----- Mail original -----

De: "John Rose" <john.r.rose at oracle.com> À: "Rémi Forax" <forax at univ-mlv.fr> Cc: "org openjdk" <org.openjdk at io7m.com>, valhalla-dev at openjdk.java.net Envoyé: Vendredi 17 Juin 2016 22:28:01 Objet: Re: Variants/case classes/algebraic data types/sums/oh my!

On Jun 17, 2016, at 6:43 AM, Remi Forax <forax at univ-mlv.fr> wrote: > > Thinking a little bit more about that ... > I we want to represent something like this, > Expr = Value(int value) | Add(Expr left, Expr right) > instead of using an interface wich is wrong because we want Value and Add > to be Exprs and not subtypes of Expr, _> we can use the Where clause to disambiguate between the Add and the > Value. > > > // for the compiler, Value and Add are seen as specialization (species) of > Expr: > typedef Add=Expr > typedef Value=Expr > typedef Expr=Expr<?> > > // and for the VM: > sealed enum ExprKind { > VALUE, > ADD > } > > public class Expr { _> Where(K == VALUE) final int value; _> Where(K == ADD) final Expr left, Expr right; > _> Where(K == VALUE) public Expr(int value) { this.value = value; } _> Where(K == ADD) public Expr(Expr left, Expr right) { this.left = > left; this.right = right; } > _> Where(K == VALUE) public int eval() { return value; } _> Where(K == ADD) public int eval() { return left.eval() + right.eval(); } > } > > left.eval() which is typed as Expr<?>.eval() is sound because ExprKind is > sealed and eval() is defined on both specialization (both species). There's lots of scary here, but probably no show-stoppers. I see two hard parts: 1. allow speciation to be parameterized by the enum (as we see here) 2. put intra-species type checking on a better footing The way it looks here (at least on the surface) is you can't type-check (say) Expr(int) unless you can collect all members (switched by where-clauses) that are guaranteed to be present in all species that contain Expr(int). Given the language of where-clauses, that seems to require something like a theorem prover with access to equality predicates (maybe more). I think (and I am independently going to suggest this for the JVM's sake in the class file format) that the problem of theorem-proving be reduced to logic checking, by nominalizing the predicates as named (or numbered) conditions. (In the class file format, there should be a "Conditions" attribute, containing evaluable expressions, and where-clause attributes simply have indexes into the Conditions array.) Something like this at a pseudo-code level: public class Expr { _WhereConditions { V = (K == VALUE), A = (K == ADD) }; _Where(V) final int value; _Where(A) final Expr left, Expr right; _Where(V) public Expr(int value) { this.value = value; } _Where(A) public Expr(Expr left, Expr right) { this.left = left; this.right = right; } _Where(V) public int eval() { return value; } _Where(A) public int eval() { return left.eval() + right.eval(); } } This turns the theorem proving (at load time, at least) into bitmask checking.

I wonder if it's not better to de-correlate the type argument and the condition, i.e. where conditions are just numbered and when a specialization is instantiated, the code has to provide type argument and a condition, so the VM doesn't have to run arbitrary code at runtime.

— John

Rémi

More information about the valhalla-dev mailing list