Na área da lógica matemática e da ciência da computação conhecida como teoria dos tipos, um construtor de tipos (do inglês type constructor) é um recurso de uma linguagem formal tipada que constrói novos tipos a partir de antigos. Considera-se que os tipos básicos são construídos usando construtores de tipos nulários. Alguns construtores de tipos recebem outro tipo como argumento, como por exemplo, os construtores para tipos produto, tipos função, tipos potência e tipos lista. Novos tipos podem ser definidos pela composição recursiva de construtores de tipos.
Por exemplo, o cálculo lambda simplesmente tipado pode ser visto como uma linguagem com um único construtor de tipo não-básico — o construtor de tipo função. Tipos produto geralmente podem ser considerados embutidos (built-in) nos cálculos lambda tipados por meio de currying.
De forma abstrata, um construtor de tipos é um operador de tipos n-ário que recebe como argumento zero ou mais tipos e retorna outro tipo. Fazendo uso de currying, os operadores de tipos n-ários podem ser (re)escritos como uma sequência de aplicações de operadores de tipos unários. Portanto, podemos ver os operadores de tipos como um cálculo lambda simplesmente tipado, que possui apenas um tipo básico, geralmente denotado por e pronunciado como "tipo", que é o tipo de todos os tipos na linguagem subjacente, os quais agora são chamados de tipos próprios para distingui-los dos tipos dos operadores de tipo em seu próprio cálculo, que são chamados de kinds.
Os operadores de tipo podem vincular (bind) variáveis de tipo. Por exemplo, fornecer a estrutura do λ-cálculo simplesmente tipado no nível do tipo requer operadores de tipo vinculantes, ou de ordem superior. Esses operadores de tipo vinculantes correspondem ao segundo eixo do cubo lambda (λ-cubo), e a teorias de tipos como o λ-cálculo simplesmente tipado com operadores de tipo, λω. A combinação de operadores de tipo com o λ-cálculo polimórfico (Sistema F) produz o Sistema Fω.
Algumas linguagens de programação funcional fazem uso explícito de construtores de tipos. Um exemplo notável é Haskell, no qual todas as declarações de tipo `data` são consideradas declarações de construtores de tipos, e os tipos básicos (ou construtores de tipos nulários) são chamados de constantes de tipo. Construtores de tipos também podem ser considerados como tipos de dados polimórficos paramétricos.
Bibliografia
, capítulo 29, "Type Operators and Kinding" P. T. Johnstone, Sketches of an Elephant, p. 940
Categoria:Teoria dos tipos