Haskell:如何测试代码是不是在编译？

Question

测试声明不是类型正确的最佳方法是什么？使用GADT,弄清楚构造函数应用程序是否正确并非易事.如果正在编写类型安全的构造库,则很自然地确保无法创建非法构造.因此,作为测试套件的一部分,我想确保类型检查器拒绝某些示例非法构造.

例如,请参阅尺寸检查的Vector表示.它比我想要决定的典型问题简单得多,但它是检查测试方法的一个很好的例子.

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)

Answer 1

您可以从Haskell程序调用GHCi并使用它来检查字符串.hint来自hackage为此提供了一个方便的包装:

{-# 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中反映类型检查本身,所以这就是我们所拥有的.

Answer 2

我基于(ab？)使用GHC的-fdefer-type-errors选项得到了一个不同的想法,这可能比嵌入一个完整的Haskell解释器更便宜hint.它的输出有点乱,因为在编译期间仍会打印警告,但是如果您愿意在文件和命令行-w中都使用GHC 选项关闭警告,则可以清除它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.