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

John Rose john.r.rose at oracle.com
Fri Jun 17 20:28:01 UTC 2016

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.

— John

More information about the valhalla-dev mailing list