scala - Scala 中的依赖打字风格相等证明

Question

是否可以在 Scala 中实现等式证明？

在 Type Driven Development with Idris 一书中，它给出了一个如何定义等式证明类型的例子。

data (=): a -> b -> Type where
    Refl : x = x

我将其转换为 Scala 的第一直觉是这样的。

sealed trait EqualityProof[A, B]
final case class EqualityProofToken[T](value: T) extends EqualityProof[value.type, value.type]

但是，这需要我向编译器证明我要比较的两个对象是完全相同的实例。理想情况下，这适用于不同实例的相同对象，尽管这可能要求太多。这是否只是由于 Scala 允许可变数据而无法避免的限制？有什么方法可以正确实现吗？如果不是，除了使用 asInstanceOf 欺骗编译器(或限制使用 asInstanceOf 的方法)之外，还有其他解决方法吗？

更新:似乎对问题的定义有些混淆，所以我添加了一个更完整的 Idris 示例。

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
 Same : (num : Nat) -> EqNat num num

sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS k k (Same k) = Same (S k)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just (Same 0)
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just eq => Just (sameS _ _ eq)

此时，EqNat 实例可用于执行需要相等值的操作，例如压缩到已证明相等的长度列表。

Answer 1

来自 Idris 的简单翻译非常简单，您只需使用隐式来提供编译时证明:

sealed trait Equality[A, B]

case class Refl[A]() extends Equality[A, A]

case object Equality {

  implicit def refl[B]: Equality[B, B] = Refl[B]()
}

它被放置在伴随对象中，因此当您需要隐含的 Equality 时，它将始终在范围内。类型。

您可以在 ohnosequences/cosas 中找到此类相等类型的更复杂的定义。图书馆和一些 tests/examples . (免责声明:我是维护者之一)