如何在 Haskell 中触发类型错误？

Question

假设我有一个类型

data F a = A a | B

我这样实现函数f :: F a -> F a -> F a：

f (A x) B = A x
f B (A _) = B
f (A _) (A x) = A x

但是没有 f B B 这样的东西在逻辑上是不可能的，所以我想要：

f B B = GENERATE_HASKELL_COMPILE_ERROR

这当然是行不通的。省略定义或使用f B B = undefined 不是解决方案，因为它会生成运行时异常。我想得到一个编译时类型错误。

编译器有所有的信息，它应该能够推断出我犯了一个逻辑错误。如果说我声明了let z = f (f B (A 1)) B，那应该是一个立即的编译时错误，而不是一些可以隐藏在我的代码中多年的运行时异常。

我找到了一些关于合约的信息，但我不知道如何在这里使用它们，我很好奇 Haskell 中是否有任何标准方法可以做到这一点。

---

编辑：事实证明，我试图做的被称为依赖类型，它在 Haskell 中还没有完全支持。然而，使用索引类型和几个扩展可能会产生类型错误。 David Young 的解决方案似乎更直接，而 Jon Purdy 创造性地使用类型运算符。我接受第一个，但我都喜欢。

Answer 1

这可以通过一些类型技巧来实现，但它是否值得取决于你在做什么（顺便说一下，你应该提供更多的上下文，这样我们就可以帮助确定多少类型机器看起来值得使用） .

{-# LANGUAGE GADTs           #-}
{-# LANGUAGE TypeFamilies    #-}
{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE ConstraintKinds #-}

import Data.Constraint

data AType
data BType

data F x y where
  A :: a -> F AType a
  B ::      F BType a

type family ValidCombo x y :: Constraint where
  ValidCombo BType ty2 = ty2 ~ AType
  ValidCombo ty1   ty2 = ()

f :: ValidCombo ty1 ty2 => F ty1 a -> F ty2 a -> F ty1 a
f (A x) B     = A x
f B     (A _) = B
f (A _) (A x) = A x

在编译时，既不可能定义f B B = ...，也不可能尝试像f B B 那样调用它。您的示例 let z = f (f B (A 1)) B 不会进行类型检查（尽管更复杂的示例可能会遇到问题）。

做的第一件事是我向F 类型构造函数添加了一个额外的参数。这是一个类型索引（在任何地方都没有该类型的值，它只是一个类型级别标记）。我创建了两种不同的空类型（AType 和 BType）用作F 的幻像类型参数。

类型族ValidCombo 充当类型级别的函数（请注意，该定义与典型的 Haskell 值级别函数的定义非常相似，但使用类型而不是值）。 () 是一个空约束，不会导致类型错误（因为空约束总是很容易满足）。在类型级别，a ~ b 将 a 和 b 约束为相同类型（~ 是类型级别相等），如果它们不是相同类型，则会出错。它大致类似于看起来像这样的值级别代码（使用您原来的 F 类型），但在类型级别：

data Tag = ATag | BTag
  deriving Eq

getTag :: F a -> Tag
getTag (A _) = ATag
getTag B     = BTag

validCombo :: F a -> F a -> Bool
validCombo B tag2 = (getTag tag2) == ATag
validCombo _ _    = True

（这可以减少，但我保留了“标签检查”和明确的相等性以便更清楚地比较。）

您可以使用DataKinds 更进一步要求F 的第一个类型参数为AType 或BType，但我不想添加太多额外的东西（这是在 cmets 中讨论了一下）。

综上所述，在许多情况下，@DirkyJerky 提供的Maybe 解决方案是可行的方法（由于增加了类型级操作的复杂性）。

有时这种类型级别的技术目前在 Haskell 中甚至不完全可行（它可能适用于您提供的示例，但取决于它将如何使用），但您需要提供更多信息供我们确定。

Answer 2

据我所知，执行此操作的“Haskell 方式”不会引发运行时错误，而是返回 Maybe F

将f的签名改为f :: F a -> F a -> Maybe (F a)， 并添加另一种类型的 catch：

f (A x) B = Just $ A x
f B (A _) = Just $ B
f (A _) (A x) = Just $ A x
f B B = Nothing

---

编译器拥有所有信息

不，编译器没有所有信息。

如果您的程序的用户决定了f 函数的输入内容，并且他们选择了两种B 数据类型，该怎么办？那时会发生什么？程序编译后不能抛出编译错误。

Answer 3

这是另一种类型族的解决方案，您可能会发现它更简单，因为它只依赖于布尔逻辑。

{-# LANGUAGE DataKinds, GADTs, TypeFamilies, TypeOperators #-}

data F x a where
  A :: a -> F 'True a
  B :: F 'False a

f
  :: ((x || y) ~ 'True)
  => F x a
  -> F y a
  -> F (x || Not y) a

f (A a) B = A a
f B (A _) = B
f (A _) (A a) = A a

----

type family Not a where
  Not 'True = 'False
  Not 'False = 'True

type family a || b where
  'True || 'True = 'True  -- *
  'True || b = 'True
  a || 'True = 'True
  a || b = 'False

* 这个案例不是必需的，但为了完整起见，我将其包括在内。

现在这是一个类型错误：

• 返回B，其中应为A，反之亦然
• 包括f B B（“无法访问的代码”）的情况
• 拨打f B B，甚至间接拨打f (f B (A 1)) B之类的电话