Género (teoría de tipos)

Género en la teoría de tipos ( inglés  kind [1] ) es el tipo de un constructor de tipos , o más formalmente, el tipo de un operador de tipo de orden superior . El sistema de género se representa naturalmente como un cálculo lambda principal (superior) simplemente tipificado , equipado con un tipo primitivo, denotado por " *" (léase " tipo "), formando una especie de tipos de datos monomórficos .

Más claramente, un género es un tipo de tipos , o un metatipo; así  como un conjunto de valores forma un tipo , un conjunto de tipos forma un género [2] . Al mismo tiempo, la aparición de tipos en tipos más generales (como subtipos) difiere de la pertenencia de tipos a un género: la división de varios tipos en géneros se produce en un nivel más abstracto. Por ejemplo, los tipos " natural ", " entero " y " real " son subtipos del tipo más general " número "; los cuatro tipos representan valores inmediatos y, por lo tanto, pertenecen al género " *". Otros géneros se forman a partir de varias operaciones sobre tipos  , así como la aritmética distingue entre números y operaciones sobre números .

Sería sintácticamente natural pensar en todos los tipos polimórficos como constructores de tipos ; y, en consecuencia, todos los monomórficos son constructores de tipo nulo . Sin embargo, todos los constructores nulos, es decir, todos los tipos monomórficos, en realidad pertenecen al mismo género, es decir, " *".

Debido a que los operadores de tipos de orden superior son poco comunes en la mayoría de los lenguajes de programación , en la práctica de la programación, los géneros se usan para distinguir los tipos de datos de los tipos de constructores que se usan para implementar el polimorfismo paramétrico . Los géneros aparecen explícita o implícitamente en lenguajes con sistemas de tipos completos , como Haskell y Scala [3] .

Ejemplos

• (léase “ tipo ” ) es un género de todos los tipos monomórficos, considerados como constructores de tipos nulos , también llamados tipos propios .  Los tipos de función en lenguajes funcionales también pertenecen a este género .
•  es el género de todos los constructores de tipos unarios . Por ejemplo, el constructor de tipo de lista  es .list
•  - una especie de constructores de tipos curry binarios . Por ejemplo, un constructor de tipo par , o un constructor de tipo funcional (no confundir con el resultado de aplicar este constructor, es decir, con el propio tipo funcional, que pertenece al género " ").*
•  - un tipo de operadores de tipos de orden superior , es decir, operadores que reciben constructores de tipos unarios en la entrada y generan tipos ellos mismos en la salida [4] .

Inferencia genérica en Haskell

Haskell proporciona tipos polimórficos, pero no permite géneros polimórficos [5] . Por ejemplo, en esta definición de un tipo algebraico polimórfico