Scala 中单例类型的 GADT 类型细化

Posted 2023-02-19

【中文标题】Scala 中单例类型的 GADT 类型细化

【英文标题】：GADT type refinement for singleton types in Scala

【发布时间】：2021-02-02 18:03:58

【问题描述】：

我有一个简单的 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
  

【参考方案1】：

通过模式匹配，您尝试在运行时 (ta.name == tb.name) 检查“两个 T 对象的单例类型参数是否相同”，但希望在编译时说服编译器。我会尝试一个类型类

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 是一个类型类，将其用作隐式约束很自然，但将其用作返回类型有点奇怪。）

【讨论】：

这是 GADT 的魔力：您在运行时进行检查，但它在编译时让编译器相信两种类型是相同的。我添加了一个示例来演示它如何与更简单的 GADT 一起使用，但我想知道它如何与上面的 T 类型一起使用（如果可能的话）。基于类型类的方法没有帮助，因为隐式解析纯粹发生在编译时。

@MatthiasBerndt 好吧​​，Scala 对 GADT 类型推断的支持肯定是有限的。但是ta.name == tb.name 太运行时了。而且你不能连接类型变量a，b。 “基于类型类的方法没有帮助，因为隐式解析纯粹发生在编译时。” 为什么这样不好？如果您对编译时解决方案不感兴趣，则应将此限制添加到您的问题中。

这是一件坏事，因为如果 T 使用仅在运行时才知道的字符串进行参数化，则它将不起作用，例如。 G。从标准输入读取。我没有明确要求，因为它有点明显——这就是 GADT 的用途：根据运行时检查得出关于编译时类型的结论。

@MatthiasBerndt 好吧​​，如果name 可以是运行时字符串，那么恐怕您想要的通常是不可能的。 A <: String with Singleton 并不意味着A 是一个单例类型，它是ConstantType 类似类型1、"ab"。它也可以是SingleType 的单例类型，例如someVal.type、SomeObject.type。 （A <: String with Singleton 表示编译器应该尽量不扩大ConstantType/SingleType）。可以看到val s: String = "abc",T.MkT(s)编译...

@MatthiasBerndt ... 这里A 被推断为s.type。但是implicitly[s.type =:= "abc"] 无法编译，SingleType s.type 对ConstantType "abc" 一无所知。因此，如果在编译时我们不能知道两个运行时字符串的类型"abc"、"def"，那么在编译时我们不能断定这些类型是=:=，因此我们无法说服编译器。 GADT SI 的示例不同。在编译时我们知道模式SI.I 有A =:= Int。