scala - Scala 中单例类型的 GADT 类型细化
问题描述
我有一个简单的 GADT 声明如下:
sealed trait T[A]
object T {
case class MkT[A <: String with Singleton](name: A) extends T[A]
}
现在我想编写一个方法来检查两个对象的单例类型参数是否相同,如果是这种情况,则以对象T
的形式返回该事实的证据。cats.evidence.Is
我尝试了以下方法,但它不起作用:
import cats.evidence.Is
def checkIs[A, B](ta: T[A], tb: T[B]): Option[Is[A, B]] =
(ta, tb) match {
case (ta: T.MkT[a], tb: T.MkT[b]) if ta.name == tb.name =>
Some(Is.refl[A])
case _ => None
}
// [error] Main.scala:36:75: type mismatch;
// [error] found : cats.evidence.Is[A,A]
// [error] required: cats.evidence.Is[A,B]
我怎样才能让编译器相信这是合理的?
// 编辑:正如@Dmytro Mitin 指出的那样,进行运行时检查并在编译时说服编译器类型相同似乎是自相矛盾的。但这实际上是可能的,并且可以用更简单的 GADT 来证明:
sealed trait SI[A]
object SI {
case object S extends SI[String]
case object I extends SI[Int]
}
def checkInt[A](si: SI[A]): Option[Is[A, Int]] =
si match {
case SI.I => Some(Is.refl[Int])
case _ => None
}
解决方案
通过模式匹配,您尝试T
在运行时(ta.name == tb.name
)检查“两个对象的单例类型参数是否相同”,但希望在编译时说服编译器。我会尝试一个类型类
trait CheckIs[A, B] {
def checkIs(ta: T[A], tb: T[B]): Option[Is[A, B]]
}
object CheckIs {
implicit def same[A]: CheckIs[A, A] = (_, _) => Some(Is.refl[A])
implicit def diff[A, B]: CheckIs[A, B] = (_, _) => None
}
def checkIs[A, B](ta: T[A], tb: T[B])(implicit ci: CheckIs[A, B]): Option[Is[A, B]] = ci.checkIs(ta, tb)
checkIs(T.MkT("a"), T.MkT("a")) //Some(cats.evidence.Is$$anon$2@28f67ac7)
checkIs(T.MkT("a"), T.MkT("b")) //None
(顺便说一句,Is
是一个类型类,将其用作隐式约束很自然,但将其用作返回类型有点奇怪。)
推荐阅读
- python - 为 Python 分类不同的文本
- sql - 使用动态数据获取 Qrter 明智的数据
- sql - 如何在 vb.net 的 select 语句中使用 group by
- android - Vivo v11 Pro 中未隐藏状态栏
- android - java.lang.NoClassDefFoundError:解析失败:Lkotlinx/coroutines/experimental/CompletableDeferredKt
- bixby - 如何在bixby中触发onclick选择
- ios - 如何从字符串数组创建枚举值数组
- c# - 根据视图上的两个下拉选择显示来自控制器的值(当同时选择它们时)。MVC asp.net
- javascript - 如何让我的浏览器显示服务器向我发送的带有下载提示的文件(图像)?
- javascript - 如何将完整日历日点击日期发送到Angular5中的其他组件