如何使用 :~: 来确定 Haskell 中的类型相等性？

Question

我试图使用:~:Data.Type.Equality在编译时确定类型相等。我的期望是它的行为符合 Scala 确定类型相等的标准方法：

case class Equals[A >: B <:B , B]()

Equals[Int, Int]     // compiles fine
Equals[String, Int]  // doesn't compile

所以我尝试了

foo :: Int :~: Bool
foo = undefined

我预计会失败，因为Int :~: Bool它不适合居住。但它编译得很好。

• 应该如何:~:工作？的文档Data.Type.Equality对我来说非常难以理解，而且我无法在任何地方找到简洁的示例。

• 也许我完全偏离了轨道。那么，我怎样才能Equals在 Haskell 中实现示例的语义呢？

Answer 1

就像我们 Haskell 人经常假装的那样，Haskell 中的每一个正常^{1类型都是有人居住的。}这包括data Void，并且它包括a :~: b所有a和b。除了我们通常承认的礼貌价值观外，还有底线价值观。

undefined :: a是产生任何类型的底部值的一种方法a。特别是undefined :: Int :~: Bool，因此您的代码类型完全正确。

如果您想要一个类型相等，但如果在编译时无法证明相等则根本无法编译，那么您需要一个类型相等约束（即运算符~），而不是:~:类型。你可以像这样使用它：

foo :: Int ~ Int => ()   -- compiles fine
foo = ()

bar :: Int ~ Bool => ()  -- does technically compile
bar = ()

bar编译仅是因为在具有约束的函数体内假定了约束。但任何调用尝试都需要 bar编译器能够证明约束才能编译调用。所以这失败了：

baz :: ()
baz = bar

:~:然而，不是一个约束（它不在=>类型中箭头的左侧），而是一个普通类型。a :~: b是值的类型，用作类型等于 type 的运行时证明。如果实际上它们不相等，您的程序不会在表达类型之前编译失败；相反，您将无法实际得出该类型的值（底部除外）。aba :~: b

特别是，a :~: b是具有数据构造函数的类型：Refl。为了有效地使用它，您通常需要 aa :~: b作为参数。然后对其进行模式匹配。在模式匹配的范围内（即语句主体case），编译器将使用两种类型相等的假设。由于底部值的模式匹配永远不会成功（它可能会抛出异常，或者可能会永远计算），因此您始终可以提供底部作为“证明”，这a :~: b实际上不会导致巨大的问题；你可以对编译器撒谎，但它永远不会执行依赖于你的谎言的代码。

与 OP 中的示例相对应的示例是：

foo :: Int :~: Int -> ()
foo proof
  = case proof of
      Refl  -> ()

bar :: Int :~: Bool -> ()
bar proof
  = case proof of
      Refl  -> ()

bar即使需要不可能的证明，它仍然可以存在。我们甚至可以使用类型中的底部值来调用 。这不会在编译时被检测为错误，但会抛出运行时异常（如果实际计算它；延迟计算可能会避免该错误）。而可以简单地用 来调用。barbar undefinedInt :~: Boolfoofoo Refl

:~:当两种类型是（或包含）变量时， (and ~) 当然更有用，而不是像Intand那样的简单具体类型Bool。它也经常与类似的东西结合起来，这样当类型没有被证明是相等Maybe时，你就有了一种表达方式。一个稍微不那么简单的例子是：

strange :: Maybe (a :~: b) -> a -> b -> [a]
strange Nothing x _ = [x]
strange (Just Refl) x y
  = [x, y]

strange接受一个可能的证明，证明类型a和b是相等的，以及每个的值。如果 Maybe 是Nothing，那么类型可能不相等，所以我们只能放入x的列表中a。然而，如果我们得到Just Refl，那么a和b实际上是相同的类型（仅在模式匹配内！x ），因此将和放在y同一个列表中是有效的。

但这确实显示了:~:无法实现的功能~。strange即使我们想传递两个不同类型的值，我们仍然可以调用；在这种情况下，我们被迫Nothing作为第一个值传递（或Just undefined，但这不会给我们带来任何有用的东西）。它允许我们编写考虑到a和b 可能相等的代码，而不会在实际上不相等时强制编译失败。而a ~ b（在约束中）只允许我们要求它们绝对相等，并且在编译时可以证明如此。

¹Type其中“正常类型”是指AKA类型的成员*。