Variants/case classes/algebraic data types/sums/oh my!
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<ADD>
> typedef Value=Expr<VALUE>
> typedef Expr=Expr<?>
>
> // and for the VM:
> sealed enum ExprKind {
> VALUE,
> ADD
> }
>
> public class Expr<ExprKind K> {
> __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<ExprKind K> {
__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