Что такое Haskell's Data.Typeable?

Question

Я встречал ссылки на Data.Typeable на Haskell, но мне не ясно, почему я хотел бы использовать его в своем коде.

Какую проблему она решает и как?

Answer 1

Data.Typeable - это кодировка хорошо известного подхода (см., Например, Harper) к реализации отложенной (динамической) проверки типов в статически типизированном языке - с использованием универсального типа.

Такой тип переносит код, для которого проверка типов не будет успешной до более поздней фазы.Вместо того, чтобы отклонять программу как неправильно напечатанную, компилятор передает ее для проверки во время выполнения.

Стиль, созданный в Abadi et al. И разработанный для Haskell Чейни и Хинцем в качестве оболочки для представления всех динамических типов, при этом класс Typeable появился как часть работы SYB SPJ и Lammel.

---

Ссылка

• Мартин Абади, Лука Карделли, Бенджамин Пирс и Гордон Плоткин, " Динамическая печать на языке со статической типизацией", ACM Транзакции на языках программирования и системах (TOPLAS), 1991.
• Джеймс Чейни и Ральф Хинце," Облегченная реализация обобщений и динамики", Haskell '02: Материалы поСеминар ACM SIGPLAN 2002 г. на Хаскелле, 2002 г.
• Ламмель, Ральф и Джонс, Саймон Пейтон, " Соскребите свой шаблон: практический шаблон проектирования для общего программирования , TLDI '03: Материалы по2003 Международный семинар ACM SIGPLAN по типам в проектировании и реализации языков, 2003
• Harper, 2011, Практические основы для языков программирования.

---

Даже в учебниках: динамические типы (с типизируемыми представлениями) являются статически типизированными языками только одного типа, Harper ch 20:

20.4 Unyyped Means UniТипизированный

Нетипизированное λ-исчисление может быть точно встроено в типизированный язык с рекурсивными типами.Это означает, что каждый нетипизированный λ-термин имеет представление в виде типизированного выражения таким образом, что выполнение представления λ-члена соответствует выполнению самого термина.Это вложение является не вопросом написания интерпретатора для λ-исчисления в ℒ {+ × ⇀µ} (что мы наверняка могли бы сделать), а скорее прямым представлением нетипизированных λ-членов в виде типизированных выраженийна языке с рекурсивными типами.

Ключевое наблюдение заключается в том, что нетипизированное λ-исчисление действительно является унифицированным λ-исчислением!Это не отсутствие типов, которые дают ему силу, а скорее то, что он имеет только один тип, а именно рекурсивный тип

D = µt.t →т.

Answer 2

Это библиотека, которая позволяет, среди прочего, именовать типы.Если тип a объявлен Typeable, его имя можно получить с помощью show $ typeOf x, где x - любое значение типа a.Он также имеет ограниченное приведение типов .

(Это похоже на отражение RTTI или динамических языков в C ++.)

Answer 3

Одним из самых ранних описаний библиотеки, подобной Data.Typeable, для Haskell, которую я смог найти, является Джон Питерсон с 1992 года: http://www.cs.yale.edu/publications/techreports/tr1022.pdf

Самая ранняя "официальная" статья, которую я знаю о представлении фактической библиотеки Data.Typeable, - это первая статья Scrap Your Boilerplate с 2003 года: http://research.microsoft.com/en-us/um/people/simonpj/Papers/hmap/index.htm

Я уверен, что есть много промежуточных историй, с которыми кто-то может присоединиться!

Answer 4

Класс Data.Typeable используется главным образом для общего программирования в стиле Scrap Your Boilerplate (SYB). Смотри также Data.Data

Идея состоит в том, что SYB определяет комбинаторы коллекций для выполнения таких операций, как печать, подсчет, поиск, подстановка и т. Д., Единообразным образом для различных типов, созданных пользователем. Класс Typeable обеспечивает необходимую сантехнику.

В современном GHC вы можете просто сказать deriving Data.Typeable при определении своего собственного типа, чтобы обеспечить его необходимыми экземплярами.