如何在Haskell中觸發類型族模式匹配錯誤？

Question

Haskell能夠指示類型家族匹配錯誤嗎？例如，使用一個封閉的家庭類型：

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

類型的Testf Int只是Testf Int。編譯器不會產生任何類型的錯誤。如果沒有匹配，是否有可能生成一個？

Answer 1

不可能。良好的類型家庭應用程序決不會自行觸發錯誤。相反，當我們嘗試使用未減少的類型族表達式進行某些操作時，我們只會遇到類型錯誤。

我們可以使用自定義類型控股的錯誤消息，爲了使錯誤更清楚一點：

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" 

現在，GHC拋出一個錯誤，每當我們試圖用Error msg鍵入非從而打印出我們的信息未定義的值。

從GHC 8.0，我們可以使用TypeError在一個更好的方法來打印我們的信息：

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

這將打印：

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

然而，這仍然只是引發錯誤的使用方法：

type T = Testf Int -- this typechecks 

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

Answer 2

這是不可能的GHCs 8.0之前，但the (as of this writing) just-released GHC 8.0.1加支持custom type errors。

的想法是，就像函數error :: String -> a棲息任何類型並且在任期級別的錯誤，我們現在有，in GHC.TypeLits，類型家庭

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

棲息任何類型有輸入錯誤。該ErrorMessage類型是非常簡單的：

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

的(:<>:)構造水平連接兩個錯誤消息; (:$$:)構造函數將它們垂直連接。另外兩個構造函數按照他們的說法做。

因此，在您的示例中，您可以使用TypeError來填寫最後一個案例;例如，

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 "’") 

然後，嘗試使用pure()在Testf Int類型將與錯誤失敗

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

請注意，雖然定義

testfInt :: Testf Int 
testfInt = pure() 

正確爆發，定義

testfInt :: Testf Int 
testfInt = undefined 

（或與testfInt = testfInt類似）工作正常。

---

這裏有一個完整的示例源文件：

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