하스켈 : 코드를 컴파일하는 방법을 테스트하는 방법은 무엇입니까?

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

Haskell 프로그램에서 GHCi를 호출하여 문자열을 검사 할 수 있습니다.

물론

{-# 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" 

, 이것은 단지 텍스트 파일을 확인하기위한 스크립트를 작성하는 더 편리한 대안입니다,하지만 난 그 자체를 확인 유형을 반영 할 수있는 방법이없는 생각 : hackage에서 hint이있는 편리한 래퍼를 제공 하스켈, 그래서 우리가 가진거야.

Answer 2

대신 GHC의 -fdefer-type-errors 옵션을 사용하여 (ab?)를 기반으로 다른 아이디어를 얻었습니다. 이는 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.