不能证明与路径依赖类型等价

Question

为什么最后一个summon编译失败?我怎么做才能使它编译?

import java.time.{LocalDateTime, LocalTime}
trait Circular[T]:
type Parent
given localTimeCircular: Circular[LocalTime] with
type Parent = LocalDateTime
final class CircularMap[K, +V]()(using val circular: Circular[K])
val summoned = summon[Circular[LocalTime]]
val daily = new CircularMap[LocalTime, Int]()
println(summoned == daily.circular) // Prints true
summon[localTimeCircular.Parent =:= LocalDateTime]
summon[summoned.Parent =:= LocalDateTime]
summon[daily.circular.Parent =:= LocalDateTime]

Scastie联系

在Scala 3.0.2和3.1.0-RC1上失败

Answer 1

这个东西不在Scala 3中。在Scala 2.13.6中，类似的代码不编译

import shapeless.the
import java.time.{LocalDateTime, LocalTime}
trait Circular[T] {
type Parent
}
implicit object localTimeCircular extends Circular[LocalTime] {
type Parent = LocalDateTime
}
//  implicit val localTimeCircular: Circular[LocalTime] {type Parent = LocalDateTime} = new Circular[LocalTime] {
//    type Parent = LocalDateTime
//  }
final class CircularMap[K, +V]()(implicit val circular: Circular[K])
val summoned = the[Circular[LocalTime]]
val daily = new CircularMap[LocalTime, Int]()
println(summoned == daily.circular) // Prints true
implicitly[localTimeCircular.Parent =:= LocalDateTime]
implicitly[summoned.Parent =:= LocalDateTime]
//implicitly[daily.circular.Parent =:= LocalDateTime] // doesn't compile

https://scastie.scala-lang.org/DmytroMitin/lsX3fS3ET0ajzChwl2Mctw

(我在一个地方用the代替implicitly，因为implicitly可以打破类型细化，summon更像the)。

让我们简化代码，以便弄清楚发生了什么。让我们删除隐式(让我们显式地解析它们)

import java.time.{LocalDateTime, LocalTime}
trait Circular[T] {
type Parent
}
val localTimeCircular = new Circular[LocalTime] {
type Parent = LocalDateTime
}
final class CircularMap[K, +V](val circular: Circular[K])
val summoned = localTimeCircular
val daily = new CircularMap[LocalTime, Int](localTimeCircular)
println(summoned == daily.circular) // Prints true
implicitly[localTimeCircular.Parent =:= LocalDateTime]
implicitly[summoned.Parent =:= LocalDateTime]
//implicitly[daily.circular.Parent =:= LocalDateTime] // doesn't compile

问题是，路径依赖类型的设计使得即使x == x1也不一定需要x.T =:= x1.T

在最新版本的scala (2.12.x)中，路径依赖类型的实现是否不完整?

强制隐式调用的依赖类型解析

如何使用shapeless

为依赖类型的类型类创建实例的确，summoned == daily.circular和summoned的类型是Circular[LocalTime] { type Parent = LocalDateTime }，而daily.circular的类型是Circular[LocalTime]。您这样指定它:val circular: Circular[K]。因此，您将精炼类型Circular[LocalTime] { type Parent = LocalDateTime }(我们将其表示为Circular.Aux[LocalTime, LocalDateTime])上转换为它的超类型，即没有精炼的类型Circular[LocalTime](又名存在类型Circular.Aux[LocalTime, _])。所以类型localTimeCircular.Parent和summoned.Parent是LocalDateTime，而类型daily.circular.Parent是抽象的。例如，如果要恢复类型细化，可以定义

final class CircularMap[K, +V, P](val circular: Circular[K] {type Parent = P})

另一种方法是使用单例类型

final class CircularMap[K, +V](val circular: localTimeCircular.type)

---

是否有一种方法可以在不引入类型参数P的情况下不丢失细化Circular[LocalTime] { type Parent = LocalDateTime }CircularMap类?类似的final class CircularMap[K, +V](val circular: Circular[K] { type Parent = X })，其中X将在CircularMap体的作用域中引入一个新的类型变量。

你想要的实际上是类上的多个类型参数列表(这样在class CircularMap[K, +V][P]中你可以指定K,V和推断P)

https://github.com/scala/bug/issues/4719

https://contributors.scala-lang.org/t/multiple-type-parameter-lists-in-dotty-si-4719/2399

你可以模仿他们

import java.time.{LocalDateTime, LocalTime}
trait Circular[T] {
type Parent
}
val localTimeCircular = new Circular[LocalTime] {
type Parent = LocalDateTime
}
trait CircularMap[K, +V] {
type P
val circular: Circular[K] {type Parent = P}
}
object CircularMap {
def apply[K, V]: PartiallyApplied[K, V] = new PartiallyApplied[K, V]
class PartiallyApplied[K, V] {
def apply[_P](_circular: Circular[K] {type Parent = _P}): CircularMap[K, V] {type P = _P} = new CircularMap[K, V] {
override type P = _P
override val circular: Circular[K] {type Parent = _P} = _circular
}
}
}
val summoned = localTimeCircular
val daily = CircularMap[LocalTime, Int](localTimeCircular)
println(summoned == daily.circular) // Prints true
implicitly[localTimeCircular.Parent =:= LocalDateTime]
implicitly[summoned.Parent =:= LocalDateTime]
implicitly[daily.circular.Parent =:= LocalDateTime] // compiles