scala - 证明嵌套路径依赖类型成员的等效性

标签 scala dependent-type

这是一个简化的案例,我完全愿意采用不同/更好的方式来实现这一目标

trait Container {
  type T
  def data: List[T]
}

trait Transform {
  val from: Container
  val to: Container
  def xform: from.T => to.T
}

case class Identity(c: Container) extends Transform {
  val from = c
  val to = c
  def xform = { t: from.T => t }
}

这产生了可预测的误差:
<console>:12: error: type mismatch;
 found   : t.type (with underlying type Identity.this.from.T)
 required: Identity.this.to.T
         def xform = { t: from.T => t }

目标基本上是有一个转换容器下面的对象的转换,但能够说服类型检查器(没有可怕的可怕的强制转换)类型是相同的。

能够以这种方式显示类型的等价性和关系的最佳方式是什么?

就像我说的,对重构代码完全开放,我在实际示例中保证它是出于真正的目的:)

最佳答案

我认为通用参数可能是描述这种模式的一种更简单的方法。

但是,您可以通过明确标识类型 T 来避免使用泛型参数。在 Container 上实例:

case class Identity(c: Container) extends Transform {
  val from: Container { type T = c.T } = c
  val to: Container { type T = c.T } = c
  def xform = { t: from.T => t }
}

或者更简单:
case class Identity(c: Container) extends Transform {
  val from: c.type = c
  val to: c.type = c
  def xform = { t: from.T => t }
}

如果您只需要避免使用 Container 上的通用参数就可以了和 Transform ,您可以通过执行以下操作使编译器相信这些类型有效:
case class Identity[U](c: Container { type T = U }) extends Transform {
  val from = c
  val to = c
  def xform = { t: c.T => t }
}

泛型参数 U除了给 T 取另一个名字外,别无他法。在 Container 上键入参数,但这足以解决问题!

对我来说,所有这些解决方案实际上只是强调了类型检查器在处理这些类型时的威力是多么的随意。我无法真正解释为什么它们是必要的或足够的。根据我的经验,使用通用参数更容易预测(当然它可能会更困惑)。

关于scala - 证明嵌套路径依赖类型成员的等效性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/31151111/

相关文章:

scala - Spark 工作节点超时

java - 将 scala.Function1 写成 lambda 的正确方法是什么?

pattern-matching - 什么是公理K?

javascript - 如何保证传递的对象键可以使用 Typescript 进行调用?

scala - 有没有办法删除 Slick GetResult 中的样板文件?

Scala 集合元组而不是元组集合

scala - 方法和领域有什么区别?

agda - 如何在 Agda 中将安全的 `length` 函数写入 `Vec`?

list - 编译时强制有限列表

haskell - 在从属 Haskell 中证明 m + (1 + n) == 1+ (m + n)