¿Qué tipo de objeto teórico corresponde a un concepto de C ++?

Me falta una formación en informática teórica, pero me hubiera gustado entender a qué tipo de objetos teóricos corresponden los conceptos de C ++ . Básicamente, los conceptos de C ++ permiten definir un conjunto de tipos que satisfacen una lista de restricciones. Entonces, desde un punto de vista teórico, ¿a qué conceptos de C ++ corresponden, o corresponden aproximadamente (y en ese caso, cuáles son las diferencias)?

pl.programming-languages type-theory algebra ct.category-theory Vincent
fuente

Los programas de C ++ son como las máquinas de Turing. Las funciones son como oráculos, solo toman más tiempo. C ++, como muchos lenguajes de programación, es como el cálculo lambda. La creación de funciones en tiempo de ejecución es aparentemente nueva a partir de C ++ 11.

Philip White

@PhilipWhite Creo que te pierdes el punto de la pregunta. El OP no está pidiendo una explicación teórica de varios conceptos de C ++ sino una explicación teórica de una construcción de C ++ llamada concepto. No tengo suficiente conocimiento en PL para responder la pregunta, pero por lo que entiendo, los conceptos son algún tipo de mecanismo para restringir el polimorfismo. No sé si tales mecanismos ya se han estudiado formalmente, pero parece un mecanismo razonable para agregar a un sistema de tipos.

holf

Mi error ... Seguí el enlace pero no lo leí demasiado de cerca. (Nunca había encontrado la necesidad de aprender / usar conceptos en C ++.)

Philip White

Respuestas:

Desde la perspectiva de la teoría del lenguaje de programación, a diferencia de la perspectiva de computabilidad que han ofrecido otras respuestas y comentarios, las plantillas de C ++ combinadas con conceptos corresponden a polimorfismo limitado o genérico limitado . Los conceptos mismos corresponden a las restricciones o límites colocados en un tipo.

Una plantilla es una función de nivel de tipo, parametrizada por tipo que está limitada por un concepto para implementar una interfaz particular. Cuando la plantilla se aplica a un tipo que satisface ese concepto, se genera un nuevo tipo.

Las plantillas + conceptos son análogos a los genéricos en Java, Scala o Eiffel. Se diferencian de las plantillas en C ++ anterior porque permiten que se especifiquen y verifiquen restricciones en los parámetros de tipo, mientras que las plantillas de C ++ no lo permitieron. El beneficio es una mejor comprobación estática de que el programa después de aplicar la plantilla estará bien escrito.

Una buena referencia es Pierce, Benjamin C. (2002). Tipos y lenguajes de programación . MIT Press, Capítulo 26: Cuantificación limitada.

Dave Clarke
fuente

Las plantillas C ++ tienen restricciones de tipo incorporadas, creando una forma de escritura estructural, porque un tipo solo debe tener un conjunto de operaciones definidas (implícitas en la definición de plantilla) para satisfacer el verificador de tipo. Los conceptos parecen hacer lo mismo, pero permiten que los nombres se asocien con esos conjuntos de comportamiento (una forma de escritura nominal) y, por lo tanto, proporcionan una forma de producir mensajes de error mejores y más tempranos. Tampoco creo que los conceptos sean funciones de tipo a tipo. La descripción vinculada los describe como predicados de tipo, o de tipo a funciones booleanas.

oconnor0

@ oconnor0: Tienes razón. Conceptos + plantillas dan polimorfismo acotado. Actualizaré mi respuesta.

Dave Clarke

No estoy seguro de estar de acuerdo con esto. Incluso sin conceptos, las plantillas de C ++ y el polimorfismo paramétrico parecen estar muy vagamente relacionados conmigo. Un término politipo se verifica de tipo para garantizar que funcione en todas sus instancias posibles. Los genéricos de Java tienen eso (a pesar de que Java rompe la parametricidad). En cambio, las plantillas de C ++ emplean "SFINAE", donde los tipos no se comprueban hasta el momento de la creación de instancias, lo que los aleja de los tipos universales para mí.

chi

-3

Los conceptos de C ++ se asignan a lenguajes recursivamente enumerables. Dado que el sistema de tipos C ++ está Turing completo, cualquier propiedad de los tipos que se puede interrogar durante la creación de instancias de plantilla (tamaño, parámetros, etc.) se puede ejecutar a través de un programa arbitrario simulado en el sistema de tipos.

Geoffrey Irving
fuente

He leído un poco más sobre conceptos. (Aparentemente, los conceptos son nuevos en C ++.) Por supuesto, cualquier función de C ++ aceptará un lenguaje recursivamente enumerable; Eso es trivial. ¿Está afirmando que el mapeo de conceptos a re idiomas es una biyección? Esto parece obviamente falso; si observa la sección de conceptos, dice que los conceptos de función "deben consistir solo en una declaración de retorno, cuyo argumento debe ser una expresión de restricción", mientras que cuando se trata de conceptos variables, "el inicializador debe ser una expresión de restricción". Entonces, estos conceptos no me suenan completos a Turing.

Philip White

Las expresiones constantes son completas de Turing, entonces sí: es una biyección. Formalizar eso requiere ser explícito sobre las codificaciones de tipos; Una afirmación que no es así es que el conjunto de conceptos que representan subconjuntos de los tipos void, C <void>, C <C <void>>, ... que representan los enteros en unario son exactamente los idiomas RE.

Geoffrey Irving

Por supuesto, los compiladores prácticos tienen límites de cálculo al evaluar expresiones constantes, pero si se tienen en cuenta esas consideraciones, la respuesta es que hay un conjunto finito de conceptos. Presumiblemente esa no es la respuesta solicitada.

Geoffrey Irving

Te refieres a expresiones de restricción. Según el recurso, hay 9 tipos de expresiones de restricción, y cada concepto puede usar solo una expresión de restricción. Además, representar los enteros en unario no es una biyección significativa entre los lenguajes re y los conceptos de C ++. En particular, no conserva la equivalencia semántica.

Philip White

No, quise decir expresiones constantes. Según el enlace en la pregunta, esta es la entrada 4 en la lista de 9 tipos de restricciones. Sin embargo, la mayoría de los otros 9 también están completos en Turing: por ejemplo, es completo para decidir si un tipo es convertible a otro en C ++.

Geoffrey Irving