Problem with type checking GADTs

[odersky]

Here's an interpreter for simply typed lambda calculus:

sealed trait Exp[T]
case class Num(n: Int) extends Exp[Int]
case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int]
case class Var[T](name: String) extends Exp[T]
case class Lambda[T, U](x: Var[T], e: Exp[U]) extends Exp[T => U]
case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]

abstract class Env { outer =>
  def apply[T](x: Var[T]): T

  def + [T](xe: (Var[T], T)) = new Env {
    def apply[T](x: Var[T]): T =
      if (x == xe._1) xe._2.asInstanceOf[T]
      else outer(x)
  }
}

object Env {
  val empty = new Env {
    def apply[T](x: Var[T]): T = ???
  }
}

object Test {

  val exp = App(Lambda(Var[Int]("x"), Plus(Var[Int]("x"), Num(1))), Var[Int]("2"))

  def eval[T](e: Exp[T])(env: Env): T = e match {
    case Num(n) => n
    case Plus(e1, e2) => eval(e1)(env) + eval(e2)(env)
    case v: Var[T] => env(v)
    case Lambda(x: Var[s], e) => ((y: s) => eval(e)(env + (x -> y)))
    case App(f, e) => eval(f)(env)(eval(e)(env))
  }

  eval(exp)(Env.empty)
}

When we compile that, we get two mysterious warnings:

-- Warning: STL.scala:32:19 ----------------------------------------------------
32 |        case Lambda(x: Var[s], e) => ((y: s) => eval(e)(env + (x -> y)))
   |             ^^^^^^^^^^^^^^^^^^^^
   |         There is no best instantiation of pattern type Lambda[Any, Any]
   |         that makes it a subtype of selector type Exp[T].
   |         Non-variant type variable U cannot be uniquely instantiated.
   |         (This would be an error under strict mode)
-- Warning: STL.scala:33:16 ----------------------------------------------------
33 |        case App(f, e) => eval(f)(env)(eval(e)(env))
   |             ^^^^^^^^^
   |           There is no best instantiation of pattern type App[Any, T]
   |           that makes it a subtype of selector type Exp[T].
   |           Non-variant type variable T' cannot be uniquely instantiated.
   |           
   |           where:    T  is a type in method eval
   |                     T' is a type variable
   |           
   |           (This would be an error under strict mode)
two warnings found

If we look under the hood we find that these stem from the fact that we somehow miss the right subtype constraints for the Lambda and App cases. I suspect something fundamental is wrong here. I don't have the time to look into it now, but maybe someone who is up-to-speed with GADT matching can?

[odersky]

Just verified that scalac has the same behavior. Specifically, it infers the types of the Lambda arguments to Any, Any, which seems wrong - at least the body argument e should have type T. i.e. the U in the Lambda case should be inferred to be the same as Exp's T.

[allanrenucci]

Related: #2675, #1870. Scalac: scala/bug#6680

[liufengyun]

Maybe I miss something here, it seems to me the compiler is justifiable in both of the two cases above.

In the Lambda case, we only know T = S => U, but we don't know what's the S and U here. Inferring U to T is type-incorrect.

In the App case, we only know the result type of application, but we don't know the argument type.

[ctongfei]

I've been plagued by this for a long time.
Shouldn't we infer an existential type (type member)? For example,

  case f @ Lambda(t, u) =>

should infer t: Var[f.T] and u: Exp[f.U]. (use path-dependent types!)

or if e has type Exp[U],

  case e @ App(f, x) =>

should infer f: Exp[e.T => U] and x: Exp[e.T].

[Blaisorblade]

In the Lambda case, we only know T = S => U, but we don't know what's the S and U here. Inferring U to T is type-incorrect.

In the App case, we only know the result type of application, but we don't know the argument type.

In both cases, GADT pattern matching requires synthesizing fresh type variables (with possible equality or subtyping constraints) and using them to refine the types of members. We don’t need those type variables to be made into type members as @ctongfei proposes, at least not to handle such examples, even though that would be sound. Maybe I can give a hand?

[ctongfei]

@Blaisorblade If I recalled correctly, under Dotty, the encoding of generics for

case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]

would create type member T and U for the class App. (http://guillaume.martres.me/publications/dotty-hk.pdf, Section 2.1)
So why not just use <instance>.T and <instance>.U as the inferred type for the pattern-matched type variables? I guess that they are readily available in the compiler.

[Blaisorblade]

In both cases, GADT pattern matching requires synthesizing fresh type variables (with possible equality or subtyping constraints) and using them to refine the types of members.

Forgot to mention: as usual, such constraints would have to be sound even if we extend the case classes. Here all type parameters are invariant, so this should be easier since we can't write class BadVar[T](x: String) extends Var[T] with Exp[Nothing]; but Dotty must be careful.

@ctongfei Using standard existentials (type variables) over type members seems as easy and more standard for GADTs (http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.119.8094&rep=rep1&type=pdf); Dotty already started doing this I think.

What you say makes some sense and I'm familiar with that work, but in fact, Sec. 8 of that paper explains clearly Dotty actually uses the direct representation in Sec. 4, not the simple encoding in Sec. 3. Sec. 2.1 is about the encoding in core DOT; it also mentions dotty in "The problem is solved in DOT and dotty by a radical reduction", but I wouldn't take that too literally given the rest of the paper. And those type members don't seem to be actually available to the user (see below).

Your proposal sounds plausible, and maybe it would be more expressive (I don't see evidence of that); it's also plausible that it's sound, but to know for sure some theorist would need to look at it for more than 5 minutes (there's one tricky question involved). Using type variables has fewer problems.

> console
scala> trait Exp[T] 
// defined trait Exp
scala> case class Var[T](name: String) extends Exp[T] 
// defined case class Var
scala> Var[Int]("a").T 
1 |Var[Int]("a").T
  |^^^^^^^^^^^^^^^
  |value `T` is not a member of Var[Int]
scala> val i : Var[Int]("a").T = 1 
1 |val i : Var[Int]("a").T = 1
  |                 ^^^
  |                 ';' expected, but string literal found
scala> val v = Var[Int]("a") 
val v: Var[Int] = Var(a)
scala> val i : v.T = 1 
1 |val i : v.T = 1
  |        ^^^
  |type T in class Var cannot be accessed as a member of Var[Int](v) from object rs$line$4.

[liufengyun]

Sure @Blaisorblade , I haven't started working on this, I've assigned to you 👍

[Blaisorblade]

@liufengyun Implementing the ideas in dotty will take a while, but yeah I'd like to give it a serious try. (Assigning to me didn't quite work not sure why). Thanks!

[ctongfei]

@Blaisorblade I'm not an expert on compiler design but I think that my proposal does make it more expressive. I'll show with the following example.

I've been working on a typesafe deep learning system and the core part is backward differentiation, which is a traversal over a computation graph.

Nodes in the computation graph, (i.e. symbolic expressions) are defined here as a GADT:
https://github.com/ctongfei/nexus/blob/master/core/src/main/scala/nexus/Expr.scala

To be brief,

sealed trait Expr[X]
case class Input[X]() extends Expr[X]
case class Param[X](var value: X)(implicit val tag: Grad[X]) extends Expr[X]
case class Const[X](value: X)(implicit val tag: Type[X]) extends Expr[X]
case class App1[X, Y](op: Op1[X, Y], x: Expr[X]) extends Expr[Y]
case class App2[X1, X2, Y](op: Op2[X1, X2, Y], x1: Expr[X1], x2: Expr[X2]) extends Expr[Y]
case class App3[X1, X2, X3, Y](op: Op3[X1, X2, X3, Y], x1: Expr[X1], x2: Expr[X2], x3: Expr[X3]) extends Expr[Y]

When doing backpropagation, we do pattern matching on symbolic expressions.
https://github.com/ctongfei/nexus/blob/master/core/src/main/scala/nexus/exec/Backward.scala#L28

// type of e: Expr[Y]
case e @ App2(o, x1, x2) => o match {  
          case o: Op2[e.Input1, e.Input2, _] =>

Naturally, the un-applied variables o, x1 and x2 should have the following type:

o: Op2[e.X1, e.X2, Y]
x1: Expr[e.X1]
x2: Expr[e.X2]

However Scala 2 currently gives existential types (Expr[_]). The type equality constraint o: Op2[e1, e2, Y]; x1: Expr[e3]; e1 =:= e3 is lost.

I have to use another pattern matching on the second line to make it typecheck, without falling back to using the evil asInstanceOf. Patmat GADT with dependent types solves this kind of problem.