Материал для изучения ГАДТ
Я начал читать о GADT в Haskell Wiki, но не совсем понял, что понимаю. Вы рекомендуете отдельную главу книги или сообщение в блоге, объясняющее GADT для начинающего на Haskell?
4 ответа
Apfelmus сделал видеоурок для GADT, который может быть полезным.
Мне нравится пример в руководстве GHC. Это просто и иллюстрирует некоторые ключевые моменты:
GADT позволяют использовать систему типов Haskell для моделирования системы типов языка, который вы реализуете ("объектный язык")
Это позволяет статической проверке Haskell утверждать, что ваш "компилятор проходит" или что-то не сохраняет тип. Функции, принимающие термины объектного языка, могут предполагать, что эти термины хорошо напечатаны. Функции, возвращающие термины объектного языка, необходимы для создания хорошо типизированных терминов.
Шаблон, соответствующий конструктору GADT, вызывает уточнение типа.
eval
имеет типTerm a -> a
в целом, но правая частьeval (Lit i)
имеет типInt
, потому что левый конструктор имел типTerm Int
,Системе Haskell не важно, какие типы вы предоставляете своим конструкторам GADT. Мы могли бы так же легко сделать каждый конструктор в
data Term a
дать результат типаTerm a
, или жеTerm Bool
иdata
определение все равно будет проходить. Но мы не сможем написатьeval :: Term a -> a
, Вы выбираете GADT "типы тегов" для моделирования вашей проблемы, чтобы полезные функции, которые вы хотите написать, были хорошо напечатаны.
GADT для чайников в викинге Haskell - лучшее объяснение, которое я видел.
Проблема, с которой я (и я подозреваю других) в большинстве представлений, состоит в том, что они показывают примеры GADT с точки зрения синтаксиса, который неочевиден, пока вы не понимаете GADT. Это делает простейшие примеры, на которых все построено, особенно сложным для полного понимания - вы можете догадаться о том, что делают многие шаблоны, но понять точную роль каждого утверждения сложно.
Пост "для чайников" анализирует и наращивает смысл синтаксиса на пути объяснения собственных базовых примеров, что делает его гораздо более полезной отправной точкой. Я очень рекомендую это.
Другие ссылки: