Почему GADT/экзистенциальные конструкторы данных не могут использоваться в ленивых шаблонах?

Сегодня я получил ошибку компилятора при попытке использовать ленивый шаблон при сопоставлении с экзистенциальным конструктором GADT:

Почему это ограничение? Какие "плохие" вещи могут произойти, если бы это было разрешено?

Ответы

Ответ 1

Рассмотрим

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 угрожают безопасности типов. Нужно быть строгим с ними, чтобы подтвердить эти доказательства: вы не можете доверять неоцененным вычислениям в присутствии дна.

Ответ 2

С "нормальными" данными вы можете пропустить проверку конструктора во время сопоставления с образцом при том понимании, что при попытке использовать данные из шаблона может оказаться, что он не существует, тем самым бросая на вас исключение.

С помощью GADT подпись типа потенциально изменяется в зависимости от того, какой конструктор присутствует. Нам нужно знать о типах во время компиляции; это нехорошо не проверять конструктор, пока вам не понадобятся значения. Если вы это сделаете, у вас может быть ошибка несоответствия типа. И это, возможно, означает, что ваша программа рушится с ошибкой сегментации (или, что еще хуже). Программы Haskell никогда не должны выполняться.