Конструктор типов - Type constructor
В районе математическая логика и Информатика известный как теория типов, а конструктор типов это особенность типизированного формальный язык который строит новые типы из старых. Основные типы считаются построенными с использованием нулевой конструкторы типов. Некоторые конструкторы типов принимают в качестве аргумента другой тип, например, конструкторы для виды продукции, типы функций, типы мощности и типы списков. Новые типы могут быть определены путем рекурсивного составления конструкторов типов.
Например, просто типизированное лямбда-исчисление можно рассматривать как язык с конструктором одного типа - конструктором типа функции. Типы продуктов обычно можно считать "встроенными" в типизированные лямбда-исчисления через карри.
Абстрактно конструктор типа - это п-ари оператор типа принимая в качестве аргумента ноль или более типов и возвращая другой тип. Используя карри, пОператоры -арного типа могут быть (пере) записаны как последовательность приложений операторов унарного типа. Следовательно, мы можем рассматривать операторы типов как просто типизированное лямбда-исчисление, которое имеет только один базовый тип, обычно обозначаемый , и произносится как «тип» - это тип всех типов основного языка, которые теперь называются правильные типы чтобы отличить их от типов операторов типов в их собственном исчислении, которые называются виды.
Операторы типа могут связывать переменные типа. Например, давая структуру просто типизированное λ-исчисление на уровне типа требует связывания или операторов типа более высокого порядка. Эти операторы типа привязки соответствуют 2nd ось λ-куб, и теории типов, такие как просто типизированное λ-исчисление с операторами типа, λω. Комбинируя операторы типа с полиморфным λ-исчислением (Система F ) дает Система Fω.
Смотрите также
Рекомендации
- Пирс, Бенджамин (2002). Типы и языки программирования. MIT Press. ISBN 0-262-16209-1., глава 29, «Типовые операторы и Kinding»
- P.T. Джонстон, Эскизы слона, п. 940