Haskell：如何测试代码是否无法编译？

Question

什么是测试声明不正确类型的最佳方法？使用GADTs时，很难确定构造函数应用程序是否正确。如果有人正在编写一组类型安全构造函数库，则自然要确保无法创建非法构造函数。因此，在测试套件的一部分中，我希望确保一些示例非法构造函数被类型检查器拒绝。

例如，可以看到一个经过大小检查的向量表示。它比我想要解决的典型问题简单得多，但这是一个检查测试方法的好例子。

data Vector n t where
  EmptyVec :: Vector 0 t
  ConsVec  :: t -> Vector n t -> Vector (n+1) t

// TODO: test that it does not typecheck
illegalVec = ConsVec 'c' (ConsVec "b" EmptyVec)

- Boldizsár Németh

---

你可能需要进行“元测试”。编写一个小脚本，尝试编译你的代码并确保编译器不会以0代码退出。 - justkris

我认为你正在尝试实现某种依赖类型，对吧？... 你想在这里使用哪些语言扩展来使第一部分正常工作？ - Random Dev

@CarstenKönig：TypeOperators，GADTs，DataKinds以及GHC.TypeLits的导入。 - András Kovács

Answer 1

您可以从Haskell程序中调用GHCi，并使用它来检查字符串。 hackage的hint提供了一个方便的包装器：

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

import GHC.TypeLits
import Language.Haskell.Interpreter

data Vector n t where
    EmptyVec :: Vector 0 t
    ConsVec  :: t -> Vector n t -> Vector (n + 1) t 

main = do
    print =<< runInterpreter (typeChecks "ConsVec 'c' (ConsVec \"b\" EmptyVec)")
    -- prints "Right False"

当然，这只是检查文本文件的脚本编写的更方便的替代方法，但我相信在Haskell中没有一种方式可以反映类型检查本身，因此我们只能使用这种方法。

- András Kovács

Answer 2

我有一个不同的想法，基于滥用 GHC 的 -fdefer-type-errors 选项，可能比像 hint 这样嵌入完整的 Haskell 解释器更便宜。但是它的输出有点凌乱，因为警告仍然在编译期间打印，但是如果您愿意使用 GHC 的 -w 选项在文件和 ghc 命令行上关闭警告，则可以清理它们。

尽管我在这里包含了所有内容以演示，但我认为这个测试的选项应该只在相关的测试模块中正确启用。

请注意，此方法取决于能够深度评估有问题的值以揭示其延迟的类型错误，在某些用例中可能会很棘手。

{-# OPTIONS_GHC -fdefer-type-errors #-}
{-# LANGUAGE TypeOperators, GADTs, DataKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

import GHC.TypeLits
import Control.Exception
import Data.Typeable

data Vector n t where
  EmptyVec :: Vector 0 t
  ConsVec  :: t -> Vector n t -> Vector (n+1) t

-- Add a Show instance so we can evaluate a Vector deeply to catch any
-- embedded deferred type errors.
deriving instance Show t => Show (Vector n t)

illegalVec = ConsVec 'c' (ConsVec "b" EmptyVec)

test = do
    t <- try . evaluate $ length (show illegalVec)
    case t of
        Right _ -> error "Showing illegalVec gave no error"
        Left e -> putStrLn $ "\nOk: Showing illegalVec returned error:\n"
                    ++ show (e :: ErrorCall)
-- ErrorCall is the exception type returned by the error function and seems
-- also to be used by deferred type errors.

- Ørjan Johansen