GADT : total getters for specific types

[gneuvill]

Hi Jean-Baptiste,

Let's say we have the following GADT :

@data
interface Seminar<T> {
  interface Cases<R, T> {
    R Init(SData.Core core, TypeEq<Init, T> __);
    R Temp(SData.Core core, SData.Add1 add1, TypeEq<Temp, T> __);
  }
  <R> R match(Cases<R, T> cases);

  enum Init {}
  enum Temp {}
}

then the following function

// getter not returning an Option<SData.Add1>
public static SData.Add1 getAdd1(Seminar<Temp> temp) {
  return Seminars.getAdd1(temp).some(); // cannot fail since we have a specific Seminar<Temp>
}

has to be written by hand, as you can see.

Would it be possible, in the case of GADTs, to generate total getters for specific cases ?

[jbgi]

indeed!
@gneuvill Do you think

static SData.Add1 getAdd1(Seminar<Temp> temp) {}

should replace

static <T> Option<SData.Add1> getAdd1(Seminar<T> temp) {}

or should we have both? (I think haskell only generate the former getter)
If we keep both how should we name each method to avoid an ambiguous overload?

[gneuvill]

The return type would prevent ambiguity, wouldn't it ?

In any case, I think we should generate them both.

[jbgi]

@gneuvill the return type is unfortunately not taken into account by javac when checking for erased method clash. What do you think of

static SData.Add1 getAdd1(Seminar<Temp> temp) {}

and

static <T> Option<SData.Add1> getAdd1Option(Seminar<T> temp) {}

for naming ?

[gneuvill]

maybeGetAdd1 ?

[gneuvill]

Would a proper solution to this amount to generate the following ?

// 'Void' here is fj.Void
private static final Void contradiction(TypeEq<Temp, Init> contradiction) {
  return null; // what else could/should it be ?
}

public static SData.Add1 getAdd1(Seminar<Temp> temp) {
  return caseOf(temp)
    .Init((core, eq) -> contradiction(eq).absurd())
    .Temp((core, add1, eq) -> add1);
}

But then since null is involved, how is it better than using the some partial function as above ?