如何在Haskell中触发类型族模式匹配错误？

Question

Haskell是否能指示类型系列匹配错误？例如，使用闭合类型系列：

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()

Testf Int的类型仅为Testf Int，编译器不会生成任何错误。如果没有匹配项，是否可能让它生成一种错误？

- rityzmon

Answer 1

不可能的。良好分类的类型族应用程序本身永远不会触发错误。相反，只有在尝试将未简化的类型族表达式用于某些内容时才会出现类型错误。

我们可以使用自定义类型来保存错误消息，以使错误更加清晰：

import GHC.TypeLits

data Error (msg :: Symbol) -- a type-level error message

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()
  Testf x      = Error "No match for Testf"

现在，当我们使用 Error msg 来为非 undefined 的值定义类型时，GHC 会抛出错误并打印我们的消息。

从 GHC 8.0 开始，我们可以使用 TypeError 更好地打印我们的消息。

{-# language DataKinds #-}
import GHC.TypeLits

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()
  Testf x      = TypeError (Text "No matching case for Testf")

这会打印出以下内容：

Notes.hs:18:5: error: …
    • No matching case for Testf
    • In the expression: ...

然而，这仍然只是在使用时抛出错误：

type T = Testf Int -- this typechecks

x :: T
x = () -- we throw error only here

- András Kovács

---

GHC 8.0 在 TypeLits 中提供了类似的功能，通过特殊的类型检查器支持使错误信息更加易读。 - dfeuer

很好的发现，已经添加了参考。 - András Kovács

Answer 2

这在 GHC 8.0 之前是不可能的，但截至本文发布时最新的GHC 8.0.1添加了对自定义类型错误的支持。

这个想法就像函数error :: String -> a在项级别上存在任何具有错误的类型一样，我们现在有了GHC.TypeLits中的类型族。

type family TypeError (msg :: ErrorMessage) :: k

任何具有类型错误的类型都可以使用ErrorMessage类型。这个类型非常简单：

data ErrorMessage = Text     Symbol
                  | ShowType t
                  | ErrorMessage :<>: ErrorMessage
                  | ErrorMessage :$$: ErrorMessage

(:<>:) 构造器将两个错误消息水平连接在一起；(:$$:) 构造器将它们垂直连接。另外两个构造器则按其名称所示执行操作。

因此，在您的示例中，您可以使用 TypeError 填充最后一个情况；例如，

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()
  Testf a      = TypeError (    Text "‘Testf’ didn't match"
                           :$$: Text "when applied to the type ‘"
                                :<>: ShowType a :<>: Text "’")

然后，尝试在类型为 Testf Int 的情况下使用 pure () 将会失败，并显示错误信息。

....hs:19:12: error: …
    • ‘Testf’ didn't match
      when applied to the type ‘Int’
    • In the expression: pure ()
      In an equation for ‘testfInt’: testfInt = pure ()
Compilation failed.

请注意，在定义时。

testfInt :: Testf Int
testfInt = pure ()

正确地打破，定义

testfInt :: Testf Int
testfInt = undefined

使用类似于 testfInt = testfInt 的方式也可以正常工作。

---

这是一个完整的示例源文件：

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

import GHC.TypeLits

type family Testf a where
  Testf Char   = IO ()
  Testf String = IO ()
  Testf a      = TypeError (    Text "‘Testf’ didn't match"
                           :$$: Text "when applied to the type ‘"
                                :<>: ShowType a :<>: Text "’")

testfChar :: Testf Char
testfChar = putStrLn "Testf Char"

testfString :: Testf Char
testfString = putStrLn "Testf String"

-- Error here!
testfInt :: Testf Int
testfInt = putStrLn "Int"

- Antal Spector-Zabusky