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

[forax at univ-mlv.fr]

----- 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<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.
> 

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