使用 curry howard 能够静态地确保两种类型在 scala 中不相等

Posted 2023-05-08

【中文标题】使用 curry howard 能够静态地确保两种类型在 scala 中不相等

【英文标题】：Using curry howard to be able to statically ensure two types aren't equal in scala

【发布时间】：2014-09-01 17:24:21

【问题描述】：

所以我最近阅读了以下爆款：http://www.chuusai.com/2011/06/09/scala-union-types-curry-howard/

我真的很欣赏这种方法！我正在尝试制作一个功能

def neq[A,B] = ...

neq[String, String] 不会编译，但 neq[String, Int] 会。看起来这应该是可能的，但我认为我对我们可以使用 curry-howard 对类型中的逻辑进行编码的方式了解不够深入。

我的失败尝试如下：

我认为我们想要的本质上是一个异或。所以我们想要

A and ~B or ~A and B

由于我们在 scala 中进行隐式解析时所拥有的只是 <:>

~(A and ~B) => (~A and B)

但如果我尝试执行以下操作，这将不起作用：

implicitly[((String with (Int => Nothing)) => Nothing) <:< ((String => Nothing) with Int)]

这是有道理的，因为类型根本不匹配。所以我真的不知道该去哪里！希望得到任何指导。

【问题讨论】：

编程问题在Computer Science上是题外话。

【参考方案1】：

据我了解，您需要保证 A 和 B 的不等式（如果我错了，请纠正我）

Shapeless 库中的好解决方案（来自 Miles Sabin）：

// Type inequalities
trait =:!=[A, B] 
def unexpected : Nothing = sys.error("Unexpected invocation")

implicit def neq[A, B] : A =:!= B = new =:!=[A, B] 
implicit def neqAmbig1[A] : A =:!= A = unexpected
implicit def neqAmbig2[A] : A =:!= A = unexpected

您的 neq 方法将如下所示：

def neq[A,B](implicit ev : A =:!= B) = ...

更新：

异或：

A and ~B or ~A and B

通过隐式解析不是：

~(A and ~B) <:< (~A and B)

正确的变换是：

(A and ~B) <:!< (~A and B)
or:
(A and ~B) =:!= (~A and B)

比scala代码：

type xor[A, B] = (A with ![B]) =:!= (![A] with B)

def neq[A,B](implicit ev : A xor B) = ...

和测试：

neq[Int, String]          // - ok
neq[String, Int]          // - ok
//neq[String, String]     // - compilation error
//neq[Int, Int]           // - compilation error

而且毕竟可以简化为：

A =:!= B

【讨论】：

尤里 -- 谢谢你的建议！我见过这样的事情......这绝对可以完成工作，但是，它比任何数学关系更滥用scala编译器的事实。因此，虽然它肯定回答了这个问题（谢谢！），但我很好奇在类型级别上是否可以证明不平等（或者可能证明是不可能的？）？