haskell - 如何在编译时而不是在运行时使用 GHC.TypeLits.TypeError 获取类型错误？

Question

到目前为止，我假设 GHC 在编译时执行类型级函数(类型系列)。因此，应该在编译时发出由 TypeError 类型族触发的错误消息。

在下面的示例中，我在运行时遇到了类型错误。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits

type family If c t e where
    If 'True  t e = t
    If 'False t e = e

type family EqSymbol (a :: Symbol) (b :: Symbol) where
    EqSymbol a a = 'True
    EqSymbol a b = 'False

type family Lookup (x :: Symbol) (l :: [(Symbol,t)]) :: t where
    Lookup k '[]             = TypeError (Text "Key not found: "  :<>: Text k)
    Lookup k  ('(x,a) ': ls) = If (EqSymbol k x)  a  (Lookup k ls)

type TList =  '[ '("foo", Int), '("bar", String)]

test1 :: Lookup "foo" TList
test1 = undefined

test2 :: Lookup "bar" TList
test2 = undefined

test3 :: Lookup "baz" TList
test3 = undefined

对于函数 test3 类型级函数 Lookup 的评估应该给出类型错误，因为 baz 不是TList.

GHCi 加载代码时没有类型错误:

GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Prelude> :l SO.hs
[1 of 1] Compiling Main             ( SO.hs, interpreted )
Ok, modules loaded: Main.

查询test1、test2函数的类型得到预期结果:

*Main> :t test1
test1 :: Int
*Main> :t test2
test2 :: [Char]

查询函数 test3 的类型给出了类型错误，只有当我尝试评估 test3 函数时才会执行 TypeError 函数:

*Main> :t test3
test3 :: (TypeError ...)
*Main> test3

<interactive>:5:1: error:
    • Key not found: baz
    • When checking the inferred type
        it :: (TypeError ...)

我必须做什么才能得到编译时错误？

Answer 1

编译模块时这不会导致错误的原因是懒惰。这与 print (if True then 1 else error "Mearg") 不会导致任何问题的原因基本相同:因为 else 分支实际上从未使用过，(可证明!)引发错误的表达式不可能影响结果。如果你愿意，错误只会发生在另一个宇宙中。

同样，您永远不会使用 test3 可以(嗯，不是!)提供的类型信息。 IE。您永远不会评估 Lookup "baz"TList 结果，无论是在编译时还是在运行时。所以没有错误!

在任何使用此类类型族的真实程序中，您都会对具体的类型信息感兴趣，并做类似的事情

show0 :: (Show q, Num q) => q -> String
show0 q = show $ 0`asTypeOf`q

main :: IO ()
main = putStrLn $ show0 test3

这确实会导致编译时错误(实际上是两次，出于某种原因):

sagemuej@sagemuej-X302LA:~$ ghc /tmp/wtmpf-file2798.hs 
[1 of 1] Compiling Main             ( /tmp/wtmpf-file2798.hs, /tmp/wtmpf-file2798.o )

/tmp/wtmpf-file2798.hs:35:19: error:
    • Key not found: baz
    • In the second argument of ‘($)’, namely ‘show0 test3’
      In the expression: putStrLn $ show0 test3
      In an equation for ‘main’: main = putStrLn $ show0 test3
   |
35 | main = putStrLn $ show0 test3
   |                   ^^^^^^^^^^^

/tmp/wtmpf-file2798.hs:35:19: error:
    • Key not found: baz
    • In the second argument of ‘($)’, namely ‘show0 test3’
      In the expression: putStrLn $ show0 test3
      In an equation for ‘main’: main = putStrLn $ show0 test3
   |
35 | main = putStrLn $ show0 test3
   |                   ^^^^^^^^^^^