haskell - 如何在 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这应该是一个即时的编译时错误，而不是一些可以隐藏在我的代码中多年的运行时异常。

我找到了一些关于契约(Contract)的信息，但我不知道如何在这里使用它们，我很好奇在 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 ，但我不想添加太多额外的东西(这在评论中讨论了一点)。

尽管如此，在许多情况下， Maybe @DirkyJerky 提供的解决方案是可行的方法(由于类型级操作的复杂性增加)。

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