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

Question

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

Answer 1

Апфельмус сделал Видеоурок для лампа что может быть полезно.

Answer 2

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

• Гадты позволяют использовать систему типа 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/rust.hinze/talks/fop.pdf.

Answer 4

Haskell Wiki's Гадты для манекенов лучшее объяснение, которое я видел.

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

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