I’m having some problems with path dependent types.
I have some types Foo
with an abstract type member F
. Instances such as Bar
will provide the concrete type.
Then there is a type class Baz
. I have instances of the type class for each concrete type of Foo#F
(but not for Foo
itself).
Here is an example:
sealed trait Foo {
type F
}
object Bar extends Foo {
type F = Array[Byte]
}
trait Baz[B] {
def b(b: B): String
}
object Baz {
implicit val bazByteArray: Baz[Array[Byte]] = (b: Array[Byte]) => new String(b)
}
I can't get this to compile:
def f(a: Foo): Baz[a.F] = {
val baz = a match {
case bar@Bar => g(bar)
}
baz
} // Expression of type Baz[(a.type with Bar.type)#F] doesn't conform to Baz[a.F]
val x2: Foo = Bar
val y2: Baz[x2.F] = f(x2) // Expression of type Baz[Foo#F] doesn't conform to expected type Baz[x2.F]
This does compile:
def g(a: Foo)(implicit baz: Baz[a.F]): Baz[a.F] = {
baz
}
val x1: Bar.type = Bar
val y1: Baz[x1.F] = f(x1)
Why does g
compile but not f
? Aren't the types the same?
How can I get f
to compile? Is there some sort of evidence I need to add?
Seems somewhat similar to this question. Here is a way to make it compile:
sealed trait Foo {
type F
def asSingleton: FooSingleton[F]
}
trait FooSingleton[X] extends Foo {
type F = X
def asSingleton: FooSingleton[X] = this
}
object Bar extends FooSingleton[Array[Byte]]
trait Baz[B] {
def b(b: B): String
}
object Baz {
implicit val bazByteArray: Baz[Array[Byte]] =
(b: Array[Byte]) => new String(b)
}
def g(a: Foo)(implicit baz: Baz[a.F]): Baz[a.F] = {
baz
}
val x1: Bar.type = Bar
val y1: Baz[x1.F] = f(x1)
def f[T](a: Foo { type F = T } ): Baz[T] = {
(a.asSingleton: FooSingleton[T]) match {
case bar @ Bar => g(bar)
}
}
val x2: Foo = Bar
val y2: Baz[x2.F] = f(x2)
Your g
compiles, because the path-dependent argument baz
of type Baz[a.F]
comes from the outside, a concrete implicit instance is inserted by the compiler, and the actual value a
isn't used anywhere inside g
.
Your f
does not compile, because the B[a.F]
appears only in the return type, and it cannot be made more concrete before an actual argument a
is passed to f
.
In a sense, the f
breaks the path between the argument a
and the returned value, because it makes the following "discontinuous jumps":
a: Foo
a
to the Bar
singleton (by pattern-matching)g
to get from the concrete Bar
singleton to the concrete Baz[Array[Byte]]
Baz[Array[Byte]]
, which seems no longer connected to Baz[a.F]
.This path can be repaired by proving that the discontinuous "jump" is indeed just an identity path that stays in the same spot all the time, so it really doesn't move anywhere, so that a.F
and the inferred type are the same, namely T
.