Haskell: Как проверить, что код не компилируется?

Question

Каков наилучший способ проверить, что декларация не соответствует правильному типу? С помощью GADT нет ничего тривиального в том, что приложение-конструктор является правильным или нет. Если вы пишете библиотеку типа безопасных конструкций, естественно, что нельзя создать незаконную конструкцию. Итак, как часть тестового набора, я хочу, чтобы некоторые примеры незаконных конструкций были отклонены с помощью проверки типа.

В качестве примера см. Векторное представление с размером объекта. Это намного проще, чем типичные проблемы, которые я хочу решить, но это хороший пример для проверки метода тестирования.

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

Вы можете вызвать GHCi из программы Haskell и использовать его для проверки строк. 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" 

Конечно, это просто более удобной альтернативой написанию сценариев для проверки текстовых файлов, но я считаю, что это не способ, чтобы отразить тип проверки себя в Хаскелл, так это то, что у нас есть.

Answer 2

У меня есть другая идея, основанная на (ab?) С использованием опции GHC -fdefer-type-errors, которая может быть дешевле, чем внедрение полного интерпретатора Haskell, например, с помощью hint. Его вывод немного беспорядочен, потому что предупреждения все еще печатаются во время компиляции, но его можно очистить, если вы готовы отключить предупреждения вообще с опцией 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.