fundo

Estou projetando uma linguagem, como um projeto paralelo. Eu tenho um montador de trabalho, um analisador estático e uma máquina virtual para isso. Como já posso compilar e executar programas não triviais usando a infraestrutura que construí, pensei em fazer uma apresentação na minha universidade.

Durante minha palestra, mencionei que a VM fornece um sistema de tipos, foi perguntado " Qual é o seu sistema de tipos? ". Depois de responder, fui ridicularizado pela pessoa que fez a pergunta.

Assim, mesmo que eu quase certamente perca a reputação de fazer essa pergunta, eu volto para os Programadores.

Meu entendimento

Pelo que entendi, os sistemas de tipos são usados ​​para fornecer uma camada adicional de informações sobre entidades em um programa, para que o tempo de execução, o compilador ou qualquer outra peça de maquinaria saiba o que fazer com as cadeias de bits nas quais opera. Eles também ajudam a manter contratos - o compilador (ou analisador de código, tempo de execução ou qualquer outro programa) pode verificar se, a qualquer momento, o programa opera com os valores esperados pelos programadores.

Os tipos também podem ser usados ​​para fornecer informações a esses programadores humanos. Por exemplo, encontro esta declaração:

function sqrt(double n) -> double;

mais útil que este

sqrt(n)

O primeiro fornece muitas informações: que o sqrtidentificador é uma função, pega um doublecomo entrada e produz outro doublecomo saída. O último diz que provavelmente é uma função que aceita um único parâmetro.

Minha resposta

Então, depois de ser perguntado "Qual é o seu sistema de tipos?" Eu respondi da seguinte maneira:

O sistema de tipos é dinâmico (os tipos são atribuídos aos valores, e não às variáveis ​​que os mantêm), mas é forte sem regras de coerção surpreendentes (você não pode adicionar uma string ao número inteiro, pois representam tipos incompatíveis, mas você pode adicionar um número inteiro ao número de ponto flutuante) .

O sistema de tipos é usado pela VM para garantir que os operandos para instruções sejam válidos; e pode ser usado por programadores para garantir que os parâmetros passados ​​para suas funções sejam válidos (ou seja, do tipo correto).
O sistema de tipos suporta subtipagem e herança múltipla (ambos os recursos estão disponíveis para programadores) e os tipos são considerados quando o envio dinâmico de métodos em objetos é usado - a VM usa tipos para verificar por qual função é uma determinada mensagem implementada para um determinado tipo.

A pergunta de acompanhamento foi "E como o tipo é atribuído a um valor?". Então, expliquei que todos os valores estão na caixa e têm um ponteiro apontando para uma estrutura de definição de tipo que fornece informações sobre o nome do tipo, a quais mensagens ele responde e de que tipos é herdado.

Depois disso, fui ridicularizado e minha resposta foi descartada com o comentário "Esse não é um sistema de tipos real".

Então - se o que eu descrevi não se qualifica como um "sistema de tipos real", o que seria? Essa pessoa estava certa de que o que eu forneço não pode ser considerado um sistema de tipos?

Tudo isso parece uma boa descrição do tipo de sistema fornecido. E sua implementação parece bastante razoável para o que está fazendo.

Para alguns idiomas, você não precisará das informações de tempo de execução, pois seu idioma não realiza o despacho de tempo de execução (ou o despacho único via vtables ou outro mecanismo, portanto, não precisa das informações de tipo). Para alguns idiomas, basta ter um símbolo / espaço reservado, pois você se preocupa apenas com a igualdade de tipos, não com seu nome ou herança.

Dependendo do seu ambiente, a pessoa pode ter desejado mais formalismo no seu sistema de tipos. Eles querem saber o que você pode provar com ele, não o que os programadores podem fazer com ele. Infelizmente, isso é bastante comum na academia. Embora os acadêmicos façam essas coisas, é muito fácil ter falhas no sistema de tipos que permitem que as coisas escapem à correção. É possível que tenham visto um deles.

Se você tiver outras dúvidas, Tipos e linguagens de programação é o livro canônico sobre o assunto e pode ajudá-lo a aprender um pouco do rigor necessário aos acadêmicos, bem como algumas terminologias para ajudar a descrever as coisas.

Gosto da resposta de @ Telastyn, especialmente por causa da referência ao interesse acadêmico no formalismo.

Permita-me adicionar à discussão.

O que é um sistema de tipos?

Um sistema de tipos é um mecanismo para definir, detectar e impedir estados ilegais de programas. Ele funciona definindo e aplicando restrições. As definições de restrição são tipos e, os aplicativos de restrição são usos de tipos , por exemplo, na declaração de variáveis.

As definições de tipo normalmente suportam operadores de composição (por exemplo, várias formas de conjunção, como em estruturas, subclasses e disjunção, como enumerações, uniões).

As restrições, usos de tipos, às vezes também permitem operadores de composição (por exemplo, pelo menos isso, exatamente isso, isso ou aquilo, isso, desde que algo mais seja válido).

Se o sistema de tipos estiver disponível no idioma e aplicado em tempo de compilação com o objetivo de poder emitir erros em tempo de compilação, é um sistema de tipos estático; isso evita a compilação de muitos programas ilegais e muito menos a execução; portanto, está impedindo estados ilegais de programas.

(Um sistema de tipo estático interrompe a execução de um programa, sabendo-se (ou não é indecidível) que o programa alcançará aquele código incorreto do qual está reclamando. Um sistema de tipo estático detecta certos tipos de bobagens (violações das restrições declaradas) e julga o programa com erro antes que ele seja executado.)

Se um sistema de tipos for aplicado em tempo de execução, é um sistema de tipos dinâmicos que impede estados ilegais de programas: mas interrompendo o programa no meio da execução, em vez de impedir que seja executado em primeiro lugar.

Uma oferta de sistema do tipo bastante comum é fornecer recursos estáticos e dinâmicos.

Oh cara, estou animado para tentar responder a essa pergunta da melhor maneira possível. Espero conseguir colocar meus pensamentos em ordem.

Como o @Doval mencionou e o questionador apontou (ainda que de forma grosseira), você realmente não possui um sistema de tipos. Você tem um sistema de verificações dinâmicas usando tags, que geralmente são muito mais fracas e também muito menos interessantes.

A questão do "o que é um sistema de tipos" pode ser bastante filosófica, e poderíamos encher um livro com diferentes pontos de vista sobre o assunto. No entanto, como este é um site para programadores, tentarei manter minha resposta o mais prática possível (e realmente, os tipos são extremamente práticos em programação, apesar do que alguns possam pensar).

visão global

Vamos começar com um entendimento básico do que é um sistema de tipos, antes de mergulhar nos fundamentos mais formais. Um sistema de tipos impõe estrutura aos nossos programas . Eles nos dizem como podemos conectar várias funções e expressões. Sem estrutura, os programas são insustentáveis ​​e extremamente complexos, prontos para causar danos ao menor erro do programador.

Escrever programas com um sistema de tipos é como conduzir um cuidado em boas condições - os freios funcionam, as portas fecham com segurança, o motor é lubrificado etc. Programas de escrita sem um sistema de tipos são como andar de moto sem capacete e com rodas feitas sem espaguete. Você não tem absolutamente nenhum controle sobre o seu.

Para fundamentar a discussão, digamos que temos uma linguagem com expressão literal num[n]e str[s]que representa o número n e a sequência s, respectivamente, e funções primitivas pluse concat, com o significado pretendido. Claramente, você não deseja escrever algo como plus "hello" "world"ou concat 2 4. Mas como podemos evitar isso? A priori , não há método para distinguir o numeral 2 da string literal "world". O que gostaríamos de dizer é que essas expressões devem ser usadas em diferentes contextos; eles têm tipos diferentes.

Idiomas e tipos

Vamos recuar um pouco: o que é uma linguagem de programação? Em geral, podemos dividir uma linguagem de programação em duas camadas: a sintaxe e a semântica. Estes também são chamados de estática e dinâmica , respectivamente. Acontece que o sistema de tipos é necessário para mediar a interação entre essas duas partes.

Sintaxe

Um programa é uma árvore. Não se deixe enganar pelas linhas de texto que você escreve em um computador; estas são apenas as representações legíveis por humanos de um programa. O programa em si é uma árvore de sintaxe abstrata . Por exemplo, em C, podemos escrever:

int square(int x) { 
    return x * x;
 }

Essa é a sintaxe concreta do programa (fragmento). A representação em árvore é:

     function square
     /     |       \
   int   int x    return
                     |
                   times
                  /    \
                 x      x

Uma linguagem de programação fornece uma gramática que define as árvores válidas dessa linguagem (sintaxe concreta ou abstrata pode ser usada). Isso geralmente é feito usando algo como notação BNF. Eu diria que você fez isso para o idioma que criou.

Semântica

OK, sabemos o que é um programa, mas é apenas uma estrutura de árvore estática. Presumivelmente, queremos que nosso programa realmente calcule algo. Precisamos de semântica.

A semântica das linguagens de programação é um rico campo de estudo. De um modo geral, existem duas abordagens: semântica denotacional e semântica operacional . A semântica denotacional descreve um programa mapeando-o em alguma estrutura matemática subjacente (por exemplo, números naturais, funções contínuas etc.). que fornece significado ao nosso programa. A semântica operacional, pelo contrário, define um programa detalhando como ele é executado. Na minha opinião, a semântica operacional é mais intuitiva para os programadores (inclusive eu), então vamos manter isso.

Não vou explicar como definir uma semântica operacional formal (os detalhes estão um pouco envolvidos), mas basicamente queremos regras como as seguintes:

1. num[n] é um valor
2. str[s] é um valor
3. Se num[n1]e num[n2]avaliar para os números inteiros n_1$ and $n_2$, thenmais (num [n1], num [n2]) `é avaliado para o número inteiro $ n_1 + n_2 $.
4. Se str[s1]e str[s2]avaliar para as cadeias s1 e s2, será concat(str[s1], str[s2])avaliada para a cadeia s1s2.

Etc. As regras são na prática muito mais formais, mas você entende. No entanto, logo encontramos um problema. O que acontece quando escrevemos o seguinte:

concat(num[5], str[hello])

Hum. Este é um enigma. Não definimos uma regra em nenhum lugar para saber como concatenar um número com uma string. Poderíamos tentar criar essa regra, mas sabemos intuitivamente que essa operação não faz sentido. Não queremos que este programa seja válido. E assim somos levados inexoravelmente a tipos.

Tipos

Um programa é uma árvore, conforme definido pela gramática de um idioma. Os programas recebem significado pelas regras de execução. Mas alguns programas não podem ser executados; isto é, alguns programas não têm sentido . Esses programas estão incorretos. Assim, a digitação caracteriza programas significativos em um idioma. Se um programa for bem digitado, podemos executá-lo.

Vamos dar alguns exemplos. Novamente, como nas regras de avaliação, apresentarei as regras de digitação informalmente, mas elas podem ser rigorosas. Aqui estão algumas regras:

1. Um token do formulário num[n]tem tipo nat.
2. Um token do formulário str[s]tem tipo str.
3. Se expressão e1tiver tipo nate expressão e2tiver tipo nat, a expressão plus(e1, e2)terá tipo nat.
4. Se expressão e1tem tipo stre expressão e2tem tipo str, expressão concat(e1, e2)tem tipo str.

Assim, de acordo com essas regras, existe o plus(num[5], num[2])tipo has nat, mas não podemos atribuir um tipo ao plus(num[5], str["hello"]). Dizemos que um programa (ou expressão) é bem digitado se pudermos atribuir qualquer tipo e, caso contrário, é digitado incorretamente. Um sistema de tipos é válido se todos os programas bem digitados puderem ser executados. Haskell é som; C não é.

Conclusão

Existem outras visualizações sobre tipos. Os tipos, em certo sentido, correspondem à lógica intuicionista e também podem ser vistos como objetos na teoria das categorias. Entender essas conexões é fascinante, mas não é essencial se alguém apenas quer escrever ou mesmo criar uma linguagem de programação. No entanto, entender os tipos como uma ferramenta para controlar formações de programas é essencial para o design e desenvolvimento da linguagem de programação. Eu apenas arranhei a superfície do que os tipos podem expressar. Espero que você pense que vale a pena incorporar ao seu idioma.