Jak wyzwolić błąd dopasowania wzorca rodziny typów w programie Haskell?

Question

Czy Haskell jest w stanie wskazać błąd dopasowania rodziny typów? Na przykład za pomocą zamkniętego rodzinę typ:

type family Testf a where 
    Testf Char = IO() 
    Testf String = IO() 

Rodzaj Testf Int tylko Testf Int. Kompilator nie generuje żadnego błędu. Czy jest możliwe, aby go wygenerować, jeśli nie ma odpowiedników?

Answer 1

Niemożliwe. Dobrze dobrane aplikacje rodzinne typu nigdy same nie powodują błędów. Zamiast tego otrzymujemy tylko błędy typu, gdy próbujemy użyć czegoś nieskredytowanego w wyrażeniach rodziny.

Możemy użyć typy niestandardowe trzyma komunikaty o błędach, w celu uczynienia błędy nieco jaśniejsze:

import GHC.TypeLits 

data Error (msg :: Symbol) -- a type-level error message 

type family Testf a where 
    Testf Char = IO() 
    Testf String = IO() 
    Testf x  = Error "No match for Testf" 

Teraz GHC zgłasza błąd iw konsekwencji drukuje naszą wiadomość, gdy staramy się wykorzystywać Error msg wpisać non -ograniczona wartość.

Od GHC 8.0, możemy użyć TypeError wydrukować naszą wiadomość w ładniejszy sposób:

{-# language DataKinds #-} 
import GHC.TypeLits 

type family Testf a where 
    Testf Char = IO() 
    Testf String = IO() 
    Testf x  = TypeError (Text "No matching case for Testf") 

Byłoby to wydrukować:

Notes.hs:18:5: error: … 
    • No matching case for Testf 
    • In the expression: ... 

to jednak nadal tylko rzuca błąd na użyciu:

type T = Testf Int -- this typechecks 

x :: T 
x =() -- we throw error only here 

Answer 2

Jest to niemożliwe w GHC przed 8.0, ale the (as of this writing) just-released GHC 8.0.1 dodać s wsparcie dla custom type errors.

Chodzi o to, że, podobnie jak funkcja error :: String -> a zamieszkuje wszelkiego rodzaju z błędem na poziomie termin, mamy teraz, in GHC.TypeLits, rodzinę typu

type family TypeError (msg :: ErrorMessage) :: k 

zamieszkującą dowolny typ z błąd typu. Typ ErrorMessage jest bardzo prosta:

data ErrorMessage = Text  Symbol 
        | ShowType t 
        | ErrorMessage :<>: ErrorMessage 
        | ErrorMessage :$$: ErrorMessage 

Konstruktor (:<>:) łączy dwa komunikaty o błędach poziomo; konstruktor (:$$:) łączy je w pionie. Pozostali dwaj konstruktorzy robią to, co mówią.

Tak więc w twoim przykładzie możesz wypełnić ostatni przypadek przy pomocy TypeError; na przykład

type family Testf a where 
    Testf Char = IO() 
    Testf String = IO() 
    Testf a  = TypeError ( Text "‘Testf’ didn't match" 
          :$$: Text "when applied to the type ‘" 
           :<>: ShowType a :<>: Text "’") 

Następnie próbuje użyć pure() w rodzaju Testf Int zakończy się niepowodzeniem z błędem

....hs:19:12: error: … 
    • ‘Testf’ didn't match 
     when applied to the type ‘Int’ 
    • In the expression: pure() 
     In an equation for ‘testfInt’: testfInt = pure() 
Compilation failed. 

Należy pamiętać, że przy definiowaniu

testfInt :: Testf Int 
testfInt = pure() 

poprawnie złamał, definiując

testfInt :: Testf Int 
testfInt = undefined 

(lub podobnie z testfInt = testfInt) działało bez zarzutu.

---

Oto pełna przykładowy plik źródłowy:

{-# LANGUAGE UndecidableInstances, TypeFamilies, DataKinds, TypeOperators #-} 

import GHC.TypeLits 

type family Testf a where 
    Testf Char = IO() 
    Testf String = IO() 
    Testf a  = TypeError ( Text "‘Testf’ didn't match" 
          :$$: Text "when applied to the type ‘" 
           :<>: ShowType a :<>: Text "’") 

testfChar :: Testf Char 
testfChar = putStrLn "Testf Char" 

testfString :: Testf Char 
testfString = putStrLn "Testf String" 

-- Error here! 
testfInt :: Testf Int 
testfInt = putStrLn "Int"