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

Ответ 1

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

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

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

Ссылка

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

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

20.4 Untypedified Uni-Typed

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

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

D = μt.t → t.

Ответ 2

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

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

Ответ 3

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

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

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

Ответ 4

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

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

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