Как получить с помощью GHC.TypeLits.TypeError ошибку типа во время компиляции, а не во время выполнения?

До сих пор я предполагал, что 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 дает ошибку типа, и функция TypeError выполняется только тогда, когда я пытаюсь вычислить функцию test3:

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

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

Что мне нужно сделать, чтобы получить ошибку времени компиляции?


haskell type-level-computation ghc type-families
person Jogger    schedule 13.07.2017    source источник
comment
Обратите внимание, что это не ошибка времени выполнения, а ошибка времени компиляции при компиляции вызова test3. При проверке предполагаемого типа подразумевается время компиляции. Однако я не знаю, почему исходный файл компилируется. Возможно, вам нужно использовать test3 вместо того, чтобы просто определить его?   -  person chi    schedule 13.07.2017
comment
@Chi: Да, добавление новой функции test4 = test3 дает ошибку при перезагрузке файла в GHCi. Спасибо!   -  person Jogger    schedule 13.07.2017

Ответы (1)


arrow_upward
3
arrow_downward

Причина, по которой это не вызывает ошибки при компиляции вашего модуля, заключается в лени. По сути, это та же самая причина, по которой print (if True then 1 else error "Mearg") не вызывает никаких проблем: поскольку ветвь else на самом деле никогда не используется, то (доказуемо!) выражение, вызывающее ошибку, никак не может повлиять на результат. Если хотите, ошибка происходит только в альтернативной вселенной.

Точно так же вы никогда не используете информацию о типе, которую test3 может (ну, не-!) предоставить. т.е. вы никогда не оцениваете результат 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
   |                   ^^^^^^^^^^^
person leftaroundabout    schedule 13.07.2017