Почему конструкторы GADT/ экзистенциальных данных нельзя использовать в ленивых шаблонах?
Сегодня я получил ошибку компилятора при попытке использовать ленивый шаблон при сопоставлении с экзистенциальным конструктором GADT:
Экзистенциальный или конструктор данных GADT нельзя использовать внутри ленивого (~) шаблона
Почему это ограничение? Какие "плохие" вещи могли бы случиться, если бы это было разрешено?
2 ответа
Рассматривать
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 никогда не должны быть segfault.