Haskell: come testare che il codice non si sta compilando?

Question

Qual è il modo migliore per verificare che una dichiarazione non sia corretta per il tipo? Con GADT, non è banale capire che un'applicazione di costruzione è corretta o meno. Se si sta scrivendo una libreria di costrutti sicuri per tipo è naturale assicurarsi che non sia possibile creare costrutti illegali. Quindi, come parte di una suite di test, voglio assicurarmi che alcuni esempi di costrutti illegali vengano rifiutati dal controllo del tipo.

Ad esempio, vedere una rappresentazione vettoriale a dimensione controllata. È molto più semplice dei tipici problemi che voglio decidere, ma è un buon esempio per verificare il metodo di test.

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

È possibile chiamare GHCi da un programma Haskell e utilizzarlo per verificare le stringhe. hint da hackage offre una vantaggiosa wrapper per questo:

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

Naturalmente, questo è solo un più conveniente alternativa alla scrittura di script per controllare i file di testo, ma credo che non ci sia un modo per riflettere tipo stesso check-in Haskell, quindi questo è quello che abbiamo.

Answer 2

Ho un'idea diversa basata su (ab?) Utilizzando l'opzione di GHC -fdefer-type-errors, che potrebbe essere più economica di un intero interprete Haskell come con hint. La sua uscita è un po 'caotica, perché gli avvertimenti sono ancora stampati durante la compilazione, ma può essere ripulito se sei disposto a disattivare gli avvisi in generale con l'opzione GHC -w in sia il file e sul comando ghc linea.

Sebbene includo tutto per dimostrarlo in un modulo qui, presumo che le opzioni per questo test debbano essere correttamente abilitate nel modulo di test pertinente.

Si noti che questo metodo dipende dalla capacità di valutare il valore offensivo in modo sufficientemente profondo da rivelare i suoi errori di tipo posticipato, il che potrebbe risultare complicato in alcuni casi d'uso.

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