Сегодня я получил ошибку компилятора при попытке использовать ленивый шаблон при сопоставлении с экзистенциальным конструктором GADT:
Конструктор данных экзистенциального или GADT не может использоваться внутри ленивого (~) шаблона
Почему это ограничение? Какие "плохие" вещи могут произойти, если бы это было разрешено?
Рассмотрим
data EQ a b where
Refl :: EQ a a
Если бы мы могли определить
transport :: Eq a b -> a -> b
transport ~Refl a = a
то мы могли бы иметь
transport undefined :: a -> b
и, таким образом, получить
transport undefined True = True :: Int -> Int
а затем сбой, а не более изящный сбой, который вы получаете при попытке нормализовать undefined.
Данные GADT представляют собой данные о типах, поэтому фиктивные данные GADT угрожают безопасности типов. Нужно быть строгим с ними, чтобы подтвердить эти доказательства: вы не можете доверять неоцененным вычислениям в присутствии дна.
С "нормальными" данными вы можете пропустить проверку конструктора во время сопоставления с образцом при том понимании, что при попытке использовать данные из шаблона может оказаться, что он не существует, тем самым бросая на вас исключение.
С помощью GADT подпись типа потенциально изменяется в зависимости от того, какой конструктор присутствует. Нам нужно знать о типах во время компиляции; это нехорошо не проверять конструктор, пока вам не понадобятся значения. Если вы это сделаете, у вас может быть ошибка несоответствия типа. И это, возможно, означает, что ваша программа рушится с ошибкой сегментации (или, что еще хуже). Программы Haskell никогда не должны выполняться.