Конструктор типу

У галузі математичної логіки і інформатики відомій як теорія типів, конструктор типу — це властивість характерна типізованим формальним мовам, за допомогою якої нові типи створюються з уже наявних. Вважається, що примітивні типи конструюються за допомогою конструкторів нульової арності. Деякі конструктори типів приймають інші типи як аргументи, наприклад, типи-добутки, функціональні типи, списки. Нові типи можна визначити через рекурсивну композицію конструкторів типів.

Наприклад, просто типізоване лямбда числення можна розглядати як мову із єдиним конструктором типів—конструктором функціонального типу. Каррування дозволяє розглядати типи-добутки як вбудовані у типізованому лямбда численні.

Абстрактно, конструктор типів є n-арним оператор над типами, що приймає нуль або більше типів і повертає інший тип. Через використання каррування, n-арний оператор над типами можна записати як послідовність застосувань унарного оператора над типами. Отже, ми можемо розглядати оператор над типами як просто типізоване лямбда числення, яке має лише один примітивний тип, зазвичай позначуваний як «*» (читається «тип»), що є типом усіх типів у нижчий мові, які називають властивими типами, щоб відрізняти їх від типів операторів над типами у їх власному численні — родів типів.

Використання простого лямбда числення над операторами над типами, призводить до більш ніж просто формалізації конструкторів типів. Це уможливлює оператори типами вищого порядку. Оператори над типами відповідають другій осі лямбда-куба, приводячи до просто типізованого лямбда числення з операторами над типами, λ_ω; поєднання операторів над типами із поліморфним лямбда численням породжує систему Fω.