GADT and type variable specialization during inference
Remi Forax
forax at univ-mlv.fr
Wed Nov 24 11:22:35 UTC 2021
Moved to amber-spec-experts,
I've got a very similar issue, if we support patter matching on Class.
public Stream<T> createPrimitiveStrem(Class<T> type) {
return switch(type) {
case int.class -> new SpecializedStream<Integer>();
case double.class -> new SpecializedStream<Double>();
...
};
}
A cast and a pinky swear @SuppressWarnings("unchecked") solve the issue but we may do better.
Rémi
----- Original Message -----
> From: "Brian Goetz" <brian.goetz at oracle.com>
> To: "Jan Lahoda" <jlahoda at openjdk.java.net>, "amber-dev" <amber-dev at openjdk.java.net>
> Sent: Lundi 8 Novembre 2021 21:37:24
> Subject: Re: RFR: 8273328: Compiler implementation for Pattern Matching for switch (Second Preview)
> This is more of a spec issue than a compiler issue. I finally got
> around to running some of my favorite GADT examples on this.
>
> I started with this Haskell type:
>
> data Term t where
> Lit :: t -> Term t
> Succ :: Term Int -> Term Int
> IsZero :: Term Int -> Term Bool
> If :: Term Bool -> Term a -> Term a -> Term a
>
> I can map it to this Java hierarchy:
>
> sealed interface Term<T> { }
>
> record Lit<T>(T val) implements Term<T> { }
> record Succ(Term<Integer> a) implements Term<Integer> { }
> record IsZero(Term<Integer> a) implements Term<Boolean> { }
> record If<T>(Term<Boolean> cond, Term<T> a, Term<T> b) implements
> Term<T> { }
>
> We correctly eliminate the impossible cases in:
>
> String foo(Term<String> t) {
> return switch (t) {
> case Lit<String> -> "Lit";
> case If<String> -> "If";
> }
> }
>
> And the compiler correctly tells me that the switch is exhaustive. But
> if I try to write an evaluator:
>
> static<T> T eval(Term<T> term) {
> return switch (term) {
> case Lit<T> t -> t.val;
> case Succ t -> eval(t.a) + 1;
> case IsZero t -> eval(t.a) == 0;
> case If<T> t -> eval(t.cond) ? eval(t.a) : eval(t.b);
> };
> }
>
>
> I get errors on the Succ and IsZero cases. In Haskell, the equivalent:
>
> eval :: Term t -> t
> eval (Lit t) = t
> eval (Succ i) = (eval i) + 1
> ...
>
> works correctly because when we match on `eval (Succ i)`, we unify t
> with Int, since that's the only instantiation for t that would work in
> this case. That's what allows us to return an Int when we're expecting
> a t, because we've already figured out they are the same.
>
> So in order to make our eval work, we would have to know to _refine_ the
> bounds of T on the RHS of
>
> case Succ t -> eval(t.a) + 1;
>
> where we would say "Succ is Term<T>, and Succ extends Term<Integer>, so
> T=Integer here".
>
> In the absence of this, I have to do an explicit boxing plus an
> unchecked cast:
>
> static<T> T eval(Term<T> term) {
> return switch (term) {
> case Lit<T> t -> t.val;
> case Succ t -> (T) (Integer) (eval(t.a) + 1);
> case IsZero t -> (T) (Boolean) (eval(t.a) == 0);
> case If<T> t -> eval(t.cond) ? eval(t.a) : eval(t.b);
> };
> }
>
> That we need both the boxing and the T cast is probably a bug.
>
More information about the amber-spec-experts
mailing list