如何在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,但我不想添加太多额外的东西(这在评论中有点讨论).

所有这一切,在许多情况下,Maybe@ DirkyJerky提供的解决方案是要走的路(由于类型级操作的复杂性增加).

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