Type inference in type patterns

On 4/4/11 10:03 AM, Kathi Haselhorst wrote:
> Is this the intended behaviour, e.g. are there cases (perhaps due to
> mixin composition) that justify rejecting this program by the type-
> checker? Or might it be the result of the compiler beeing "a little
> buggy" (http://groups.google.com/group/scala-language/msg/
> df4513d2cf59d277) in this area?

One thing we can do to see what's going on is this.

trait TPrime1 extends T {
def inspect[T <: Type](e : Exp[T]) =
e match { case Const(t) => t }

def inspect2[T <: Type](e : Exp[T]) =
e match { case n: Const[_] => n.c }
}

% scalap TPrime1
trait TPrime1 extends java.lang.Object with T with scala.ScalaObject {
def $init$() : scala.Unit = { /* compiled code */ }
def inspect[T <: T.Type](e : T.Exp[T]) : T.Type with T = { /*
compiled code */ }
def inspect2[T <: T.Type](e : T.Exp[T]) : T.Type = { /* compiled code
*/ }
}

I can't think of a good reason for those to have different return types,
so I presume it is a bug. There is some complicated stuff involving
type inference in patterns where method type parameter bounds are
involved, and I'd be lying if I said I entirely understood it, but that
seems like what we have here. But I know for sure that the fully
inferred "pretend there are no type parameters" case works better than
the "throw around some lower case letters" case.

Here's a test case from the "pending" folder illustrating why I say
that. (It doesn't work yet -- it's years old, I found it one of my
periodic test purges.)

/** Cleaned up in october 2010 by paulp.
* Hey, we should get this working.
*/

// Class hierarchy
trait Term[a]

object Var{ def unapply[a](x:Var[a]) = Some(x.name) }
class Var[a] (val name : String) extends Term[a]

object Num{ def unapply(x:Num) = Some(x.value) }
class Num (val value : Int) extends Term[Int]

object Lam{ def unapply[b,c](l: Lam[b,c]) = Some(l.x, l.e) }
class Lam[b, c](val x : Var[b], val e : Term[c]) extends Term[b => c]

object App{ def unapply[b,c](a: App[b,c]) = Some(a.f, a.e) }
class App[b, c] (val f : Term[b => c], val e : Term[b]) extends Term[c]

object Suc { def unapply(a: Suc) = true }
class Suc() extends Term[Int => Int]

// Environments :
abstract class Env {
def apply[a](v: Var[a]): a
def extend[a](v: Var[a], x : a) = new Env {
def apply[b](w: Var[b]): b = w match {
case _ : v.type => x // v eq w, hence a = b
case _ => Env.this.apply(w)
}}
}

object empty extends Env {
def apply[a](x: Var[a]): a = throw new Error("not found : "+x.name)
}

object Test {
val v1 = new Var[util.Random]("random")
val v2 = new Var[Int]("Int")
val v3 = new Var[List[String]]("list")

val anEnv = (empty
.extend(v1, new util.Random)
.extend(v2, 58)
.extend(v3, Nil)
)

def eval[a](t: Term[a], env : Env): a = t match {
// First three work
case v : Var[b] => env(v) // a = b
case n @ Num(value) => value // a = Int
case a @ App(f,e) => eval(f, env)(eval(e, env)) // a = c

// Next one fails like:
//
// found : (Int) => Int
// required: a
case i @ Suc() => { (y: Int) => y + 1 } // a = Int => Int

// Next one fails like:
//
// error: '=>' expected but '[' found.
// case f @ Lam[b,c](x, e) => { (y: b) => eval(e, env.extend(x,
y)) } // a = b=>c
// ^
case f @ Lam[b,c](x, e) => { (y: b) => eval(e, env.extend(x, y)) }
// a = b=>c
}

val f1 = () => eval(v1, anEnv)
val f2 = () => eval(v2, anEnv)
val f3 = () => eval(v3, anEnv)

def main(args: Array[String]): Unit = {
println(f1())
println(f2())
println(f3())
}
}

> One thing we can do to see what's going on is this.
>
> trait TPrime1 extends T {
>    def inspect[T <: Type](e : Exp[T]) =
>      e match { case Const(t) => t }
>
>    def inspect2[T <: Type](e : Exp[T]) =
>      e match { case n: Const[_] => n.c }
>
> }
>
> % scalap TPrime1
> trait TPrime1 extends java.lang.Object with T with scala.ScalaObject {
>    def $init$() : scala.Unit = { /* compiled code */ }
>    def inspect[T <: T.Type](e : T.Exp[T]) : T.Type with T = { /*
> compiled code */ }
>    def inspect2[T <: T.Type](e : T.Exp[T]) : T.Type = { /* compiled code
> */ }
>
> }

Yes, this clearly shows the problem. But to me the inferred return
type "T.Type with T" already looks a bit suspicious. The "T.Type"
seems redundant, because we already know from the type bounds that T
<: T.Type. If I put the same methods directely into trait T, I get the
following (I renamed the type parameter T to X to make the distinction
to trait T clearer):

def inspect[X <: Type](e : scratch.T.Exp[X]) : X = { /* compiled code
*/ }
def inspect2[X <: Type](e : scratch.T.Exp[X]) : X = { /* compiled code
*/ }

which looks more reasonable.

> I can't think of a good reason for those to have different return types,
> so I presume it is a bug.
I agree. The language specification §8.3 states the following about
type parameter inference for constructor patterns:

"Assume a constructor pattern C (p 1 , . . . , p n ) where class C has
type type parameters a 1 , . . . , a n . These type parameters are
inferred in the same way as for the typed pattern (_: C [a 1 , . . . ,
a n ])."

so exactely the same algorithm should be used in both cases for type
parameter inference...

> There is some complicated stuff involving
> type inference in patterns where method type parameter bounds are
> involved, and I'd be lying if I said I entirely understood it, but that
> seems like what we have here.  But I know for sure that the fully
> inferred "pretend there are no type parameters" case works better than
> the "throw around some lower case letters" case.

Yeah - but in some cases you need the type variables to write the code
(see for example the Lam[b, c] case in eval's match expression below:
you need to annotate the type of the parameter y).

> Here's a test case from the "pending" folder illustrating why I say
> that.  (It doesn't work yet -- it's years old, I found it one of my
> periodic test purges.)

I don't see why this example illustrates your claim that "pretend
there are no type parameters" works better than using type variables.
The errors below seem to be caused by the unapply methods in the
corresponding companion objects. If you remove these objects entirely
and instead only use type patterns in eval's match expression the code
compiles just fine. But I really don't understand this strange
interaction between unapply methods and type checking... Any ideas?
The error concerning the Lam case is merely a syntax error: scala does
not allow you to both bind term variables and type variables in the
same pattern (would be interesting to know why there is this
limitation... it seems the bahaviour could be easily encoded by first
using a type pattern and then use a nested constructor pattern for
binding the corresponding term variables - so why not allow it in the
first place? The type checker itself annotates the intermediate
representation in this way (can be seen when compiling with -
Xprint:typer), but still it is no valid scala syntax)).

> /** Cleaned up in october 2010 by paulp.
>   *  Hey, we should get this working.
>   */
>
> // Class hierarchy
> trait Term[a]
>
> object Var{ def unapply[a](x:Var[a]) = Some(x.name) }
> class Var[a] (val name : String) extends Term[a]
>
> object Num{ def unapply(x:Num) = Some(x.value) }
> class Num (val value : Int) extends Term[Int]
>
> object Lam{ def unapply[b,c](l: Lam[b,c]) = Some(l.x, l.e) }
> class Lam[b, c](val x : Var[b], val e : Term[c]) extends Term[b => c]
>
> object App{ def unapply[b,c](a: App[b,c]) = Some(a.f, a.e) }
> class App[b, c] (val f : Term[b => c], val e : Term[b]) extends Term[c]
>
> object Suc { def unapply(a: Suc) = true }
> class Suc() extends Term[Int => Int]
>
> // Environments :
> abstract class Env {
>    def apply[a](v: Var[a]): a
>    def extend[a](v: Var[a], x : a) = new Env {
>      def apply[b](w: Var[b]): b = w match {
>        case _ : v.type => x // v eq w, hence a = b
>        case _ => Env.this.apply(w)
>      }}
>
> }
>
> object empty extends Env {
>    def apply[a](x: Var[a]): a = throw new Error("not found : "+x.name)
>
> }
>
> object Test {
>    val v1 = new Var[util.Random]("random")
>    val v2 = new Var[Int]("Int")
>    val v3 = new Var[List[String]]("list")
>
>    val anEnv = (empty
>      .extend(v1, new util.Random)
>      .extend(v2, 58)
>      .extend(v3, Nil)
>    )
>
>    def eval[a](t: Term[a], env : Env): a = t match {
>      // First three work
>      case v : Var[b]         => env(v)                     // a = b
>      case n @ Num(value)     => value                      // a = Int
>      case a @ App(f,e)       => eval(f, env)(eval(e, env)) // a = c
>
>      // Next one fails like:
>      //
>      // found   : (Int) => Int
>      // required: a
>      case i @ Suc()          => { (y: Int) => y + 1 }      // a = Int => Int
>
>      // Next one fails like:
>      //
>      // error: '=>' expected but '[' found.
>      //     case f @ Lam[b,c](x, e) => { (y: b) => eval(e, env.extend(x,
> y)) }  // a = b=>c
>      //                 ^
>      case f @ Lam[b,c](x, e) => { (y: b) => eval(e, env.extend(x, y)) }
>   // a = b=>c
>    }
>
>    val f1 = () => eval(v1, anEnv)
>    val f2 = () => eval(v2, anEnv)
>    val f3 = () => eval(v3, anEnv)
>
>    def main(args: Array[String]): Unit = {
>      println(f1())
>      println(f2())
>      println(f3())
>    }
> }

kathi