Que tipo de objeto teórico corresponde a um conceito de C ++?

Não tenho formação em ciência da computação teórica, mas gostaria de entender a que tipo de objetos teóricos os conceitos C ++ correspondem. Basicamente, os conceitos de C ++ permitem definir um conjunto de tipos que satisfazem uma lista de restrições. Portanto, do ponto de vista teórico, a que conceitos C ++ correspondem ou aproximadamente (e nesse caso, quais são as diferenças)?

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

Programas em C ++ são como máquinas de Turing. Funções são como oráculos, elas levam mais tempo. C ++, como muitas linguagens de programação, é como o cálculo lambda. A criação de funções em tempo de execução é aparentemente nova a partir do C ++ 11.

Philip White

@PhilipWhite Acho que você perdeu o ponto da pergunta. O OP não está pedindo uma explicação teórica de vários conceitos de C ++, mas uma explicação teórica de uma construção de C ++ chamada conceito. Não tenho conhecimento suficiente em PL para responder à pergunta, mas pelo que entendi, conceitos são algum tipo de mecanismo para restringir o polimorfismo. Não sei se esses mecanismos já foram estudados formalmente, mas parece um mecanismo razoável para adicionar a um sistema de tipos.

Holf

Meu erro ... Eu segui o link, mas não o li muito de perto. (Eu nunca tinha encontrado uma necessidade de aprender / conceitos de uso em C ++ mim mesmo.)

Philip White

Respostas:

De uma perspectiva da teoria da linguagem de programação, em oposição à perspectiva da computabilidade oferecida por outras respostas e comentários, os modelos C ++ combinados com os conceitos correspondem ao polimorfismo limitado ou à genicidade restrita . Os próprios conceitos correspondem às restrições ou limites colocados em um tipo.

Um modelo é uma função em nível de tipo, parametrizada por tipo que é restringida por um conceito para implementar uma interface específica. Quando o modelo é aplicado a um tipo que satisfaz esse conceito, um novo tipo resulta.

Modelos + conceitos são análogos aos genéricos em Java, Scala ou Eiffel. Eles diferem dos modelos no C ++ anterior porque permitem que restrições nos parâmetros de tipo sejam especificadas e verificadas, enquanto os modelos C ++ não permitem isso. O benefício é uma melhor verificação estática de que o programa após a aplicação do modelo será bem digitado.

Uma boa referência é Pierce, Benjamin C. (2002). Tipos e linguagens de programação . MIT Press, Capítulo 26: Quantificação limitada.

Dave Clarke
fonte

Os modelos C ++ possuem restrições de tipo incorporadas a eles, criando uma forma de tipagem estrutural, porque um tipo deve ter apenas algum conjunto de operações definidas (implícitas na definição de modelo) para satisfazer o verificador de tipos. Os conceitos parecem fazer a mesma coisa, mas permitem que os nomes sejam associados a esses conjuntos de comportamento (uma forma de digitação nominal) e, portanto, fornecem uma maneira de produzir mensagens de erro anteriores e melhores. Também não acho que os conceitos sejam do tipo para digitar funções. A descrição vinculada os descreve como predicados de tipo - ou digite para funções booleanas.

oconnor0

@ oconnor0: Você está certo. Conceitos + modelos fornecem polimorfismo limitado. Vou atualizar minha resposta.

9788 Dave McLaren

Não sei se concordo com isso. Mesmo sem conceitos, modelos C ++ e polimorfismo paramétrico parecem estar apenas muito vagamente relacionados a mim. Um termo polipedido é marcado para garantir que funcione em todas as instâncias possíveis. Os genéricos Java têm isso (apesar de o Java interromper a parametridade). Os modelos C ++ empregam "SFINAE", onde os tipos não são verificados até o momento da instanciação, o que os torna distantes dos tipos universais para mim.

chi

-3

Os conceitos de C ++ são mapeados para linguagens recursivamente enumeráveis. Como o sistema de tipos C ++ é Turing completo, qualquer propriedade de tipos que possa ser interrogada durante a instanciação do modelo (tamanho, parâmetros etc.) pode ser executada através de um programa arbitrário simulado no sistema de tipos.

Geoffrey Irving
fonte

Eu li um pouco mais sobre conceitos. (Aparentemente, os conceitos são novos em C ++.) É claro que qualquer função C ++ aceitará uma linguagem recursivamente enumerável; isso é trivial. Você está afirmando que o mapeamento de conceitos para re linguagens é uma bijeção? Isso parece obviamente falso; se você der uma olhada na seção de conceitos, ela diz que os conceitos de função "devem consistir apenas em uma declaração de retorno, cujo argumento deve ser uma expressão de restrição", enquanto que, quando se trata de conceitos de variáveis, "o inicializador deve ser uma expressão de restrição". Portanto, esses conceitos não me parecem completos de Turing.

Philip White

Expressões constantes são Turing completas, então sim: é uma bijeção. Formalizar isso exige ser explícito sobre codificações de tipos; uma afirmação que não é essa: o conjunto de conceitos que representam subconjuntos dos tipos void, C <void>, C <C <void>>, ... representando os números inteiros em unário são exatamente os idiomas RE.

Geoffrey Irving

Obviamente, compiladores práticos têm limites de computação ao avaliar expressões constantes, mas se essas considerações forem levadas em consideração, a resposta é que existe um conjunto finito de conceitos. Presumivelmente, essa não é a resposta solicitada.

Geoffrey Irving

Você quer dizer expressões de restrição. De acordo com o recurso, existem 9 tipos de expressões de restrição e cada conceito pode usar apenas uma expressão de restrição. Além disso, representar os números inteiros em unário não é uma bijeção significativa entre linguagens re e conceitos C ++. Em particular, ele não preserva a equivalência semântica.

Philip White

Não, eu quis dizer expressões constantes. De acordo com o link na pergunta, esta é a entrada 4 na lista de 9 tipos de restrições. No entanto, a maioria dos outros 9 também é Turing complete: por exemplo, é Turing complete para decidir se um tipo é conversível em outro em C ++.

Geoffrey Irving