Уровень равенства типа Haskell

Haskell имеет синтаксис с ограничениями для определения семейств типов:

(1)   type family Length (xs :: [*]) where
(2)     Length '[] = 0
(3)     Length (x ': xs) = 1 + Length xs

В строках (2) и (3) в левой части знака равенства (=) мы имеем только простую сопоставление образцов. На правой стороне знака равенства мы просто набираем функцию функции уровня и в качестве синтаксического сахара существуют операторы типа ((+) в строке (3)).

Нет никаких охранников, нет выражений case, нет синтаксиса if-then-else, no let и where и нет приложения частичной функции. Это не проблема, так как выражение отсутствующего случая может быть заменено специализированной функцией уровня типа, этот шаблон соответствует в разных случаях, отсутствующий синтаксис if-then-else может быть заменен на If функция Data.Type.Bool пакет.

Посмотрев на некоторые примеры, мы видим, что синтаксис соответствия шаблонов на уровне типа имеет по крайней мере один дополнительная функция, недоступная в обычных функциях уровня Haskell:

(1)   type family Contains (lst :: [a]) (elem :: a) where
(2)     Contains (x ': xs) (x) = 'True
(3)     Contains '[]       (x) = 'False
(4)     Contains (x ': xs) (y) = Contains xs (y)

В строке (2) мы дважды используем переменную x. Строка (2) оценивает значение "True", если глава списка первого параметра равен второму параметру. Если мы будем делать то же самое в функции уровня ценности, GHC отвечает с ошибкой Conflicting definitions for 'x'. В функциях уровня значения мы должны добавить контекст Eq a => для компиляции функции.

Совпадение типов типового уровня похоже похоже на унификацию в старые времена Prolog. Я безуспешно googled для некоторой документации о синтаксисе функций уровня уровня.

  • Почему GHC не требует что-то вроде ограничения равенства типа a ~ b в определении семейства типов Contains?
  • Доступно ли равенство типов?
  • Имеет ли тип семейства синтаксис другие дополнительные функции, недоступные на уровне значений?
  • Где это документировано?

Ответы

Ответ 1

Язык уровня языка Haskell - это чисто язык первого порядка, в котором "приложение" - это просто другой конструктор, а не вещь, которая вычисляет. Существуют конструкторы связывания, такие как forall, но понятие равенства для материала на уровне типа является в основном простой альфа-эквивалентностью: структурной до переименования связанных переменных. Действительно, вся наша машина-конструктор, монады и т.д. Полагаются на возможность однозначно использовать приложение m v.

Функции уровня на самом деле не живут на языке типового уровня как первоклассные граждане: только их полные приложения. В итоге мы получаем эквациональную (для теории тегов ~ понятие равенства), в которой выражения выражаются и решаются, но лежащее в основе понятие ценности, обозначаемое этими выражениями, всегда является первым порядком и, следовательно, всегда равновероятным с равенством.

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