Что такое Haskell's Data.Typeable?
Я встречал ссылки на Хаскелла Data.Typeable, но мне не понятно, почему я хотел бы использовать его в своем коде.
Какую проблему это решает и как?
4 ответа
Data.Typeable является кодировкой хорошо известного подхода (см., например, Harper) к реализации отложенной (динамической) проверки типов в статически типизированном языке - с использованием универсального типа.
Такой тип переносит код, для которого проверка типов не будет успешной до более поздней фазы. Вместо того, чтобы отклонять программу как неправильно напечатанную, компилятор передает ее для проверки во время выполнения.
Этот стиль зародился в Abadi et al. И разработан для Haskell Чейни и Хинце как обертка для представления всех динамических типов с Typeable класс, появляющийся как часть работы SYB SPJ и Lammel.
Ссылка
- Мартин Абади, Лука Карделли, Бенджамин Пирс и Гордон Плоткин, " Динамическая типизация в статически типизированном языке", ACM Транзакции на языках программирования и системах (TOPLAS), 1991.
- Джеймс Чейни и Ральф Хинце, " Легкая реализация обобщений и динамики", Haskell '02: Материалы семинара ACM SIGPLAN 2002 года на Хаскеле, 2002.
- Ламмель, Ральф и Джонс, Саймон Пейтон, " Утилизируйте шаблон: практический шаблон проектирования для общего программирования, TLDI '03: Материалы Международного семинара ACM SIGPLAN по типам проектирования и реализации языков, 2003 г., 2003 г.
- Харпер, 2011, Практические основы языков программирования.
Даже в учебниках: динамические типы (с типизируемыми представлениями) являются статически типизированными языками только с одним типом, Harper ch 20:
20.4 Нетипизированные средства
Нетипизированное λ-исчисление может быть точно встроено в типизированный язык с рекурсивными типами. Это означает, что каждый нетипизированный λ-термин имеет представление в виде типизированного выражения таким образом, что выполнение представления λ-члена соответствует выполнению самого термина. Это вложение заключается не в написании интерпретатора для λ-исчисления в ℒ{+×⇀µ} (что мы могли бы наверняка сделать), а скорее в прямом представлении нетипизированных λ-терминов как типизированных выражений в языке с рекурсивными типами,
Ключевое наблюдение заключается в том, что нетипизированное λ-исчисление действительно является однотипным λ-исчислением! Это не отсутствие типов, которое дает ему силу, а скорее то, что он имеет только один тип, а именно рекурсивный тип
D = µt.t → t.
Это библиотека, которая позволяет, среди прочего, именовать типы. Если тип a объявлен Typeable, затем вы можете получить его имя, используя show $ typeOf x где x любое значение типа a, Это также показывает ограниченное приведение типа.
(Это несколько похоже на отражение RTTI или динамических языков в C++.)
Одно из самых ранних описаний, которое я мог найти 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
Я уверен, что есть много промежуточной истории, с которой кто-то здесь может присоединиться!
Класс Data.Typeable используется в основном для общего программирования в стиле Scrap Your Boilerplate (SYB). Смотрите также Data.Data
Идея состоит в том, что SYB определяет комбинаторы коллекций для выполнения операций, таких как печать, подсчет, поиск, подстановка и т. Д., Единообразным образом для различных типов, созданных пользователем. Typeable Typeclass обеспечивает необходимую сантехнику.
В современном GHC можно просто сказать deriving Data.Typeable при определении собственного типа, чтобы обеспечить его необходимыми экземплярами.