dependent types

[Paul Phillips]

Is it expected that f1 works and f2 doesn't? Is there a way to
structure f2 so it does work?

trait Foo {
type Arg
type Prod
def makeProd(a: Arg): Prod
}

object Test {
def f1(x: Foo)(y: x.Arg) = x.makeProd(y)

case class f2(x: Foo) {
def apply(y: x.Arg) = x.makeProd(y)
}

val myFoo = new Foo {
type Arg = Int
type Prod = (Int, Int)
def makeProd(i: Int) = (i, i)
}

def main(args: Array[String]): Unit = {
println(f1(myFoo)(5)) // works
println(f2(myFoo)(10)) // nope
// test/files/run/t102.scala:22: error: type mismatch;
// found : Int(10)
// required: _1.x.Arg where val _1: Test.f2
// println(f2(myFoo)(10))
// ^
// one error found
}
}

[Miles Sabin]

How about,

case class f2[T <: Foo](x: T) {

def apply(y: x.Arg) = x.makeProd(y)
}

Cheers,

Miles

--
Miles Sabin
tel: +44 7813 944 528
gtalk: mi...@milessabin.com
skype: milessabin
http://www.chuusai.com/
http://twitter.com/milessabin

[Adriaan Moors]

that's probably tricky to fix, although the violation uniformity is quite the incentive to do just that

if we zoom in on the culprit, f2(myFoo)(10):

(f2.apply(myFoo))(10) // redundant parentheses are not that redundant

where the apply method has been synthesized as:

def apply(x: Foo): Test.f2 = new Test.this.f2(x)

breaking it down further

(f2.apply(myFoo)): f2

the type of this expression conveniently forgets about x == myFoo,

so by the time we get to the apply that supplies the 10, we don't know we're looking for a myFoo.Arg,

not a f2#Arg

Miles solution fixes exactly that problem. We could probably generate some kind of refinement type for the synthesized def,

def apply(_x: Foo): Test.f2{val x = _x} = new Test.this.f2(x)

so that the value can be propagated, but that seems pretty, errr, unlikely to happen (right?)

obviously, f1 is a totally different beast, where we get a shot at propagating actual arguments to the types in later argument lists

(it's the following line in doTypedApply:

val restpe = mt.resultType(args1 map (arg => gen.stableTypeFor(arg) getOrElse arg.tpe))

)