Материал для обучения GADT

Question

Я начал читать о GADT в Haskell Wiki, но не чувствовал себя вполне комфортно, понимая это. Вы рекомендуете конкретную книгу или статью в блоге, объясняющую GADT для новичков Haskell?

Answer 1

Apfelmus изготовлен video tutorial for GADTs который может быть полезен.

Answer 2

Мне нравится пример в GHC manual. Это просто, и это иллюстрирует некоторые ключевые моменты:

• GADTs позволяют использовать систему типов 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 для модели вашей проблемы, так что полезные функции, которые вы хотите написать, хорошо типизированы.

Answer 3

Другие ссылки:

• http://www.haskell.org/haskellwiki/Generalised_algebraic_datatype
• http://www.comlab.ox.ac.uk/people/ralf.hinze/talks/FOP.pdf

Answer 4

Haskell вики GADTs for dummies лучшее объяснение, которое я видел.

Проблема, с которой я (и подозреваю других) в том, что они показывают примеры GADT в терминах синтаксиса, который неочевиден , пока вы не поймете GADTs. Это делает простейшие примеры, на которые все построено особенно сложно, чтобы полностью понять - вы можете догадаться о том, что делают многие из шаблонов, но понимание точной роли каждого утверждения является сложной задачей.

Сообщение «для манекенов» раскрывает и вырабатывает значение синтаксиса на пути к объяснению его собственных основных примеров, что делает его гораздо более полезной отправной точкой. Я очень рекомендую.