Como ler a notação de sistemas de tipos?

 (langdev.stackexchange.com)
1 pontos por GN⁺ 2023-08-17 | 1 comentários | Compartilhar no WhatsApp
  • Embora a notação de sistemas de tipos varie entre materiais, se você conhecer a estrutura comum de gramática, relação de tipagem e regras de inferência, consegue acompanhar a maioria das variações
  • Um sistema de tipos opera sobre a sintaxe abstrata de uma linguagem, então primeiro é preciso distinguir por gramática os termos (term) que têm tipo e os próprios tipos
  • ⊢ e: τ é um julgamento de tipagem que significa “a expressão e tem o tipo τ”, e deve ser lido como uma regra de inferência em que, se todas as condições acima da linha horizontal forem verdadeiras, a conclusão abaixo também é verdadeira
  • Quando entram variáveis e funções, um contexto é anexado, como em Γ ⊢ e: τ, para rastrear os nomes e tipos das variáveis no escopo atual
  • Muitas regras de tipagem podem ser lidas como uma função recursiva de verificação de tipos, mas nem todo julgamento lógico se torna diretamente um algoritmo de verificação de tipos decidível

Notação de sistemas de tipos a partir da gramática

  • Um sistema de tipos é um sistema sintático de uma linguagem de programação, isto é, um conjunto de regras que opera sobre a sintaxe abstrata da linguagem
  • Uma explicação abrangente de um sistema de tipos normalmente primeiro apresenta a estrutura sintática tratada por meio de uma gramática e a expressa na notação BNF
  • Mesmo na linguagem de tipos mais simples, a sintaxe se divide em duas grandes categorias
    • e: expressões (expression) que têm tipo
    • τ: tipos (type) atribuídos às expressões
  • A linguagem de exemplo tem como expressões literais booleanos, literais inteiros, expressões condicionais, operações aritméticas e operações de comparação, e usa Bool e Int como tipos
  • Dependendo do material, o símbolo de tipo pode aparecer como t, T, σ ou outras letras gregas minúsculas em vez de τ, mas a estrutura geral é parecida
  • Linguagens mais complexas podem incluir mais categorias sintáticas, como comandos e padrões de casamento de padrões

Como ler relações de tipagem e julgamentos

  • Depois de definir a gramática, normalmente se define uma relação de tipagem na forma e : τ
    • 1 + 2 : Int significa “1 + 2 tem tipo Int”
    • 1 + 2 : Bool significaria que a mesma expressão tem tipo Bool, então está errado
    • true + 2 : Int não faz sentido nem como expressão, então não tem tipo algum
  • ⊢ e : τ é um julgamento de tipagem, e ⊢ pode ser lido como “a afirmação a seguir é verdadeira”
  • Uma regra sem nada acima da linha horizontal é um axioma (axiom) sempre verdadeiro
    • ⊢ true : Bool
    • ⊢ false : Bool
    • regras de literais inteiros como ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int
  • Uma regra com parte superior e inferior é uma regra de inferência
    • se todas as condições acima forem verdadeiras, a conclusão abaixo é verdadeira
    • se e₁ e e₂ forem ambos Int, então e₁ + e₂ é Int
    • se e₁ e e₂ forem ambos Int, então e₁ < e₂ é Bool

Expressões condicionais e variáveis de tipo

  • Os dois ramos de if ... then ... else ... podem ter qualquer tipo, mas precisam ter o mesmo tipo entre si
    • if true then 1 else 2 é válido
    • if true then false else true é válido
    • if true then 1 else true é inválido
  • Para expressar isso, a regra usa a variável τ para representar o tipo dos ramos
    • a condição e₁ precisa ser Bool
    • o ramo then e₂ e o ramo else e₃ precisam ter o mesmo tipo τ
    • o tipo da expressão condicional inteira também será τ
  • Ao aplicar a regra, é possível escolher qualquer tipo para τ, mas dentro da mesma regra essa escolha precisa ser mantida de forma consistente

Lendo regras de inferência como algoritmos

  • Essa notação vem da lógica formal, e a forma de especificar sistemas de tipos se parece especialmente com a dedução natural
  • Essas regras são usadas para construir provas formais sobre propriedades do sistema e são importantes para demonstrar propriedades como segurança de tipos
  • Um julgamento lógico nem sempre corresponde de imediato a um algoritmo de verificação de tipos decidível
  • Em muitos casos, ⊢ e : τ pode ser lido como uma função que obtém o tipo τ a partir da expressão e
    • normalmente há uma regra para cada forma de expressão da gramática
    • cada regra de tipagem pode ser vista como um ramo de uma função recursiva de verificação de tipos
  • A função infer do exemplo corresponde ao seguinte fluxo
    • true ou false resultam em Bool
    • literais inteiros resultam em Int
    • e₁ + e₂ verifica se os resultados de inferência dos dois lados são Int e então retorna Int
    • e₁ < e₂ verifica se ambos os lados são Int e então retorna Bool
    • if e₁ then e₂ else e₃ verifica se a condição é Bool, depois se os tipos dos dois ramos são iguais, e então retorna esse tipo
  • Mesmo quando não dá para traduzir diretamente em algoritmo, pensar em e como entrada e τ como saída ajuda a entender o fluxo de informação no julgamento

Variáveis e contexto

  • Para lidar com linguagens de programação úteis, são necessárias variáveis, e o exemplo é estendido com funções para tomar a forma do simply typed lambda calculus
  • A gramática estendida inclui
    • variável x
    • abstração de função λx:τ. e
    • aplicação de função e e
    • tipo de função τ → τ
  • λx:τ. e corresponde a (x:τ) => e em TypeScript, e f x corresponde a f(x)
  • Como o tipo de uma variável depende do contexto em que ela aparece, não dá para escrever a regra apenas na forma ⊢ x : ???
  • Por isso, o julgamento de tipagem é estendido para Γ ⊢ e : τ
    • Γ é o contexto ou ambiente de tipos
    • ⊢ separa as suposições contextuais à esquerda da afirmação a ser provada à direita
    • isso é lido como “sob o contexto Γ, a expressão e tem tipo τ”
  • Do ponto de vista algorítmico, Γ pode ser visto como uma entrada adicional no formato Map<Variable, Type>
  • Formalmente, o contexto também é especificado como uma estrutura sintática
    • ∅: contexto vazio
    • Γ, x:τ: contexto com uma nova associação de variável
    • às vezes • é usado como contexto vazio no lugar de ∅
  • Nessa representação, o contexto é mais próximo de uma association list que mapeia nomes de variáveis para tipos

O papel do contexto dentro das regras

  • Muitas regras de tipagem não alteram o contexto e apenas o propagam
    • Γ ⊢ true : Bool
    • se Γ ⊢ e₁ : Int e Γ ⊢ e₂ : Int, então Γ ⊢ e₁ + e₂ : Int
  • Nas regras de uso de variável e de expressão lambda, o contexto tem papel central
    • se x:τ ∈ Γ, então Γ ⊢ x : τ
    • se Γ, x:τ₁ ⊢ e : τ₂, então Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • Ao verificar o tipo do corpo e de uma expressão lambda, o contexto é estendido com a nova associação x:τ₁
  • A regra de variável julga que, se houver uma associação da variável no contexto atual, então a variável tem aquele tipo
  • O contexto é usado como um mecanismo de comunicação que transmite informação entre a regra da expressão lambda e a regra da variável
  • Para simplificar, especificações desse tipo geralmente assumem que todas as variáveis já foram resolvidas e tornadas únicas, sem tratar sombreamento de variáveis
  • A regra de aplicação de função verifica em conjunto o tipo da expressão função e o da expressão argumento
    • e₁ precisa ter tipo τ₁ → τ₂
    • e₂ precisa ter tipo τ₁
    • o tipo da aplicação inteira e₁ e₂ passa a ser τ₂

Outras notações frequentes

  • Regras de inferência nem sempre são escritas apenas na vertical
    • várias condições podem aparecer lado a lado na horizontal
    • arranjos verticais e horizontais podem se misturar dentro da mesma regra
  • As condições acima da linha horizontal normalmente são outros julgamentos, mas também podem ser condições laterais (side condition) booleanas arbitrárias
    • x:τ ∈ Γ na regra de variável é um exemplo
    • em sistemas de tipos algorítmicos, pode aparecer α fresh, significando que α deve ser uma nova variável de tipo distinta das demais

Subtipagem

  • Subtipagem é uma relação que trata a compatibilidade entre tipos de forma mais fraca do que igualdade estrita, e precisa ser definida explicitamente
  • Em geral se escreve τ₁ <: τ₂ e se lê “τ₁ é subtipo de τ₂”
  • Uma relação simples de subtipagem pode introduzir o tipo topo ⊤ e o tipo fundo ⊥
    • τ <: τ: todo tipo é subtipo de si mesmo
    • τ <: ⊤: todo tipo é subtipo de ⊤
    • ⊥ <: τ: ⊥ é subtipo de todo tipo
  • A primeira regra é a regra de reflexividade, frequentemente abreviada como refl
  • Para permitir subtipagem, cada regra de tipagem que a aceita precisa usar explicitamente essa relação
    • na regra de aplicação de função, pode-se permitir a aplicação se o tipo do argumento τ₁ for subtipo do tipo de parâmetro τ₂

Múltiplos contextos e verificação de tipos bidirecional

  • Alguns sistemas de tipos definem julgamentos de tipagem que incluem mais de um contexto
    • o segundo contexto costuma ser chamado de Δ
    • Γ;Δ ⊢ e : τ é comum quando ambos os contextos funcionam como entrada
    • Γ ⊢ e : τ ⊣ Δ é comum quando Δ funciona como saída
  • O segundo contexto pode ter usos diferentes conforme o caso
    • pode limitar certas variáveis para que só possam ser referenciadas dentro de determinadas expressões
    • em linguagens de programação sensíveis a recursos, pode servir como contexto de saída para rastrear quais variáveis foram consumidas
  • A verificação de tipos bidirecional é uma abordagem para fazer inferência de tipos não local limitada sem resolvedor de restrições
  • Um sistema bidirecional divide o julgamento geral Γ ⊢ e : τ em dois julgamentos especializados
    • Γ ⊢ e ⇐ τ: julgamento de checagem (checking), que verifica se a expressão e tem o tipo esperado τ; do ponto de vista algorítmico, τ é entrada
    • Γ ⊢ e ⇒ τ: julgamento de inferência (inference), usado quando não há informação de tipo esperada; do ponto de vista algorítmico, τ é saída
  • Os dois julgamentos são definidos de forma mutuamente recursiva, transmitindo informação de tipo nos dois sentidos
  • Com essa abordagem, algumas anotações de tipo podem ser omitidas, e a regra de checagem para abstração lambda pode obter o tipo do parâmetro a partir do tipo de função esperado, permitindo omitir a anotação no vinculador da variável

Leituras relacionadas

1 comentários

 
GN⁺ 2023-08-17
Opiniões no Hacker News

  • Guy Steele já fez uma apresentação sobre esse tema no passado. Ele até deu nomes pesquisáveis a algumas notações, como diagramas bidimensionais de regras de inferência
    Ele chama isso de metanotação da ciência da computação, mas, pessoalmente, parece mais próximo de teoria de linguagens de programação. https://m.youtube.com/watch?v=dCuZkaaou0Q

  • Essa notação remonta a Frege. É difícil pesquisar se você não sabe o que procurar, mas este artigo parece ser um resumo bem bom: https://plato.stanford.edu/entries/frege-logic
    O símbolo de catraca |- já era usado, e a linha horizontal que nas aulas era chamada de “Fregescher Schlussstrich”, isto é, o traço de conclusão de Frege, parece ter sido originalmente parte da própria catraca e depois virou um elemento separado na notação moderna

    • “Schlussstrich” provavelmente seria mais bem traduzido como traço dedutivo ou traço de inferência

  • Types and Programming Languages, de Benjamin C. Pierce, é um bom livro-texto que aborda esse conteúdo

    • É irônico que o TAPL seja bastante pouco claro ao explicar o significado básico da sintaxe que ele próprio usa. Esta resposta é várias ordens de grandeza mais clara que o TAPL

  • Mesmo sendo formado em ciência da computação, ainda me confundo com a diferença de significado entre |– e |=, e também com em qual nível de metassintaxe estão as variáveis usadas
    Ironicamente, um dos motivos é que a própria notação não tem tipos explícitos

  • Para quem está em dúvida se deve ler: este texto explica a notação de sistemas de tipos que aparece em artigos de ciência da computação e, na prática, é uma introdução à notação BNF, regras de inferência etc. para sistemas de tipos
    Parece um bom resumo

    • Sinceramente, eu só precisava de uma cola dizendo como ler os símbolos em palavras em inglês
      Entendo o conceito lógico de aplicação de tipos, mas, como não leio artigos de ciência da computação com frequência, a correspondência entre símbolos e significado não fixa bem na minha cabeça
    • O fato de esse tipo de coisa ter sido abstraído rigorosamente ao longo de anos mostra bem o lado ciência da computação da área

  • Em um dos exemplos, 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 significa “𝗍𝗋𝗎𝖾+2 é do tipo 𝖨𝗇𝗍”, mas o texto diz que isso é ainda mais estranho porque a própria expressão 𝗍𝗋𝗎𝖾+2 não faz sentido e não tem tipo
    Só que, em Python, True + 2 de fato é um inteiro e o valor é 3. Independentemente de se deveria ser assim, é assim que funciona

    • Se você acha que True + 2 faz sentido, basta definir diretamente uma regra de julgamento que permita isso
      Lógica e teoria de sistemas de tipos não se importam em si com quais axiomas e regras de inferência você usa; elas apenas permitem raciocinar sobre essas regras e suas interações. Por exemplo, você pode ter algo como |- True : Bool, |- True : Int, ou, se quiser permitir apenas em certas expressões, pode construir uma regra que derive |- True + x: Int a partir de |- x : Int
    • Isso não varia de linguagem para linguagem? Por exemplo, em C, true é mapeado para 1, então true+1=2
    • Mesmo que True + 2 não gere erro em Python ou C, isso continua sendo tolice, porque torna a semântica da linguagem mais difícil de inferir só para dar ao programador um pouco de açúcar sintático

  • Ótimo. Eu tinha curiosidade sobre isso havia anos, mas não sabia quais termos pesquisar para aprender mais

  • Às vezes dá uma raiva quando alguém libera de graça um conhecimento esotérico que você aprendeu a duras penas ;) Eu realmente gostaria que um texto assim existisse quando aprendi isso. Espero que, com mais acessibilidade, haja menos linguagens bagunçadas

  • Ao ler o Ada Reference Manual, reconheci imediatamente esse tipo de sintaxe. Eu não sabia o nome, mas achei interessante vê-la em um caso de uso real, e a linguagem inteira é definida com essa notação
    Ex.: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • Parece um bom lugar para evangelizar uma causa que decidi defender até o fim. Em formatos de anotação de tipo que usam dois-pontos, os espaços dos dois lados dos dois-pontos devem ser iguais
    Para mim, há dois símbolos diferentes que por acaso têm a mesma forma, isto é, dois pontos. Um é o dois-pontos de rótulo, em que a parte da frente introduz a parte de trás, como em inglês, ou a esquerda é o rótulo da direita; entram aqui o início de bloco em Python, pares chave-valor e pares nome-valor de structs em C ou Rust
    O outro é a anotação de tipo emprestada da matemática. Trata-se de uma relação binária, e relações binárias usam espaçamento igual à esquerda e à direita. Assim como não escrevemos x= 1, x> y, x+ z, o natural seria escrever x : X, não x: X
    Quando vejo a: b, leio imediatamente como dois-pontos de rótulo; quando é anotação de tipo, sempre exige uma conversão mental extra, ainda que minúscula. Estou falando de sintaxe de linguagens de programação e, pessoalmente, prefiro muito mais x : X a X x
    [1] “Evangelion” é uma palavra bacana que vem de εὐαγγέλιον, ou seja, “boa notícia”. [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • Pode haver alguns mal-entendidos. Mesmo na escrita matemática, aparece de fato a notação f: X->Y, com mais espaço à direita dos dois-pontos; de 3 livros que verifiquei, 1 usava apenas essa notação
      Além disso, isso ainda se aproxima de rotulagem: é rotular uma aplicação de um tipo específico. O caso em que os dois-pontos são usados com um significado realmente diferente em matemática é quando servem como abreviação de such that; por exemplo, em definições de conjunto como { x : x \in IN and x | 2}, ou frequentemente junto com quantificadores
    • É uma perspectiva interessante. O que você diz sobre uma etapa mental extra é o mesmo que sinto ao ler a notação comum X x. x: X é muito mais natural para mim, e também parece mais próximo do modo como os dois-pontos são usados na linguagem natural
      Há uma proposição, e o que vem depois dos dois-pontos a explica em mais detalhes; como um tipo também é informação adicional sobre o que está à esquerda, encaixa perfeitamente
    • Em teoria dos tipos, considero prática padrão normalmente colocar o mesmo espaço dos dois lados dos dois-pontos, como em t[espaço]:[espaço]T
      A teoria dos tipos como um todo tem aspectos de uma bagunça inconsistente, mas este é um dos raros casos em que todo mundo é bastante consistente. Fiquei curioso para ver como eu escrevia na graduação, e vi que eu também deixava bonitinho e simétrico: https://dvt.name/logic/horse2.pdf
    • x: X corresponde ao uso em que “a explicação vem depois dos dois-pontos”
      Ou seja, algo como variable x: It’s an X.
    • age: int pode ser facilmente lido em inglês como “person’s age: an integer”
      Por isso, os dois-pontos nunca me incomodaram muito