Variants/case classes/algebraic data types/sums/oh my!

[John Rose]

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