Um quebra-cabeça de verificação bidirecional de tipos

• A implementação de verificação bidirecional de tipos do Grace usava o tipo do primeiro elemento da lista como se fosse o tipo de todos os elementos, o que fez o campo port: 8080 ser removido e gerou um resultado de avaliação incorreto
• O exemplo do problema percorria uma lista com { domain: "google.com" } e { domain: "localhost", port: 8080 }, usando a porta padrão 443, e retornava [ "google.com:443", "localhost:443" ] em vez do esperado [ "google.com:443", "localhost:8080" ]
• A inferência anterior de listas inferia List { domain: Text } a partir do primeiro elemento e então verificava os demais contra esse tipo; no processo de elaboração (elaboration), o campo port que não existia no supertipo era removido
• A implementação corrigida infere primeiro o tipo de cada elemento, depois calcula o supertipo mais específico e volta a verificar cada elemento contra esse tipo, preenchendo valores Optional ausentes com null ou some
• Após a correção, a lista original passa a ser inferida como List { domain: Text, port: Optional Natural }, preservando port como null no primeiro registro e some 8080 no segundo, o que produz o resultado esperado

---

Bug de inferência de tipo em listas no Grace

• O Grace usa um sistema de verificação bidirecional de tipos baseado em Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, e várias implementações que tentavam contornar limitações dessa abordagem acabaram levando a um bug estranho
• O programa problemático percorria a lista authorities, vinculando domain e port de cada registro, e usava 443 como valor padrão quando port não existia, em uma forma de list comprehension

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"

• O resultado esperado era [ "google.com:443", "localhost:8080" ], mas a versão com bug retornava [ "google.com:443", "localhost:443" ], ignorando completamente o campo port: 8080 do segundo registro
• O problema não estava no avaliador, mas no verificador de tipos, afetando ao mesmo tempo a inferência do tipo da lista e a elaboração feita durante a verificação de tipos

Verificação bidirecional de tipos e os limites da inferência anterior de listas

• O tipo esperado pelo Grace para a lista authorities era o seguinte

List { domain: Text, port: Optional Natural }

• Esse tipo significa que cada registro tem o campo obrigatório domain: Text, enquanto port: Optional Natural pode existir ou não
• Na prática, a implementação anterior inferia um tipo mais estreito

>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }

• A verificação bidirecional de tipos se divide basicamente em duas tarefas
  • inferir o tipo de uma expressão
  • verificar se uma expressão corresponde a um tipo esperado
• Só com essas duas operações, não é fácil combinar os tipos de vários elementos de uma lista para construir um supertipo dos elementos da lista inteira
• A implementação anterior do Grace inferia o tipo da lista da seguinte forma
  • inferia o tipo do primeiro elemento da lista
  • verificava se todos os demais elementos correspondiam ao tipo inferido a partir do primeiro
• Como o tipo do primeiro elemento { domain: "google.com" } era { domain: Text }, o tipo de todos os elementos da lista também passava a ser { domain: Text }
• Se quisesse outro tipo, era preciso adicionar uma anotação de tipo explícita, mas o JSON do mundo real que o Grace quer lidar pode ter esquemas grandes e complexos, então a ideia não era obrigar o usuário a escrever o esquema inteiro como uma enorme anotação de tipo

Por que a elaboração mudou até o resultado da avaliação

• O verificador de tipos do Grace não apenas detecta erros de tipo, mas também realiza elaboração (elaboration), ajustando expressões durante a verificação
• Ao verificar um subtipo contra um supertipo, se os dois tipos forem diferentes, o verificador insere uma coerção explícita
• Internamente, o avaliador do Grace representa todos os valores Optional como valores marcados com null ou some x
• Se um valor sem marcação aparece em uma posição onde se espera Optional, o Grace insere automaticamente a marca some

>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]

• Se o tipo do primeiro elemento é inferido como Optional Natural e o segundo elemento é um Natural sem marcação, o verificador de tipos insere a marca some em vez de gerar um erro de incompatibilidade de tipos
• O mesmo acontece com registros, e o Grace oferece suporte a subtipagem de registros, coercionando registros para que se ajustem ao supertipo

>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }

• Se um registro for anotado com um tipo de registro menor, o verificador aceita isso, mas remove os campos que não existem no supertipo
• Mesmo ao avaliar apenas a lista authorities, a implementação anterior removia o campo port desta forma

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]

• O resultado surgia pelo fluxo a seguir
  • o tipo do primeiro elemento era inferido como { domain: Text }
  • o segundo elemento era verificado contra esse tipo esperado
  • o segundo elemento correspondia ao tipo, mas tinha o campo extra port
  • o verificador removia o campo port para adequá-lo ao tipo esperado
• A coerção de registros em si não era a causa fundamental; a verdadeira origem do problema era tratar o tipo do primeiro elemento como se fosse o tipo de toda a lista durante a inferência

A solução: calcular o supertipo mais específico

• O Grace adicionou uma nova operação para inferir corretamente o tipo da lista inteira
• A nova operação calcula o supertipo mais específico (most-specific supertype) entre dois tipos, ou seja, o menor limite superior (least upper bound)
• Dizer que C é um supertipo de A e B significa que C é supertipo de A e também de B
• Dizer que C é o supertipo mais específico de A e B significa que C é subtipo de qualquer outro supertipo de A e B
• Com essa nova operação, a inferência do tipo de listas passa a seguir esta ordem
  • inferir o tipo de cada elemento da lista
  • calcular o supertipo mais específico de todos os tipos dos elementos
  • verificar cada elemento contra esse supertipo mais específico
  • retornar esse supertipo mais específico como o tipo dos elementos da lista inteira
• Dessa forma, a lista a seguir passa a ter o tipo correto inferido

>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }

• O fluxo interno é o seguinte
  • { x: 1 } é inferido com o tipo { x: Natural }
  • { y: true } é inferido com o tipo { y: Bool }
  • o supertipo mais específico desses dois tipos se torna { x: Optional Natural, y: Optional Bool }
  • cada elemento é então verificado contra esse supertipo
• O motivo para verificar cada elemento novamente contra o supertipo é aplicar a elaboração correta, preenchendo some e null ausentes, entre outros ajustes

>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

O tipo e o resultado de avaliação de authorities após a correção

• Depois da correção no verificador de tipos, a lista original authorities passa a inferir o tipo esperado

>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }

• O resultado avaliado após a elaboração também preserva port como um campo opcional

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]

• O port ausente do primeiro registro é preenchido com null, e o port: 8080 do segundo é preservado como some 8080
• O exemplo original da list comprehension também retorna o resultado esperado

[ "google.com:443", "localhost:8080" ]

Suporte a JSON e a escolha pela complexidade de implementação

• O motivo de o Grace apostar fortemente em verificação bidirecional de tipos é considerar que esse framework, embora mais complexo, é poderoso o suficiente para inferir tipos de JSON do mundo real
• Inferência Hindley-Milner ou frameworks de verificação de tipos mais simples e parecidos com ela têm dificuldade para lidar com formatos que aparecem em dados JSON reais
• O Grace não foi criado apenas como uma linguagem ergonômica para trabalhar com JSON, mas também não ignorou o suporte a JSON
• Com base na experiência com Dhall, o Grace levou em conta a sensibilidade dos usuários à ergonomia da interoperabilidade com JSON, e sua sintaxe e sistema de tipos foram projetados para considerar compatibilidade com JSON, mesmo com maior complexidade de implementação

Materiais relacionados que valem a leitura

• Datatype unification using Monoids: aborda um algoritmo de inferência de tipos para dados simples que é essencialmente o mesmo usado pelo Grace para calcular o supertipo mais específico
• The appeal of bidirectional typechecking: explica por que vale a pena aprender verificação bidirecional de tipos ao implementar linguagens que usam subtipagem de alguma forma
• Local Type Inference: um dos artigos pioneiros sobre verificação bidirecional de tipos, citado como origem de técnicas como menor limite superior e elaboração de expressões para uma linguagem interna

Apêndice: por que a coerção de registros é necessária

• A expressão a seguir em Grace mostra por que a coerção de registros é necessária

let f (input: { }) = input.x

in  f { x: 1 }

• Se essa expressão passasse na verificação de tipos, a pergunta seria: qual deveria ser o tipo de retorno de f?
• O tipo de retorno não pode ser Natural

let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }

• Como f recebe input do tipo de registro vazio { }, ela não pode extrair um valor Natural desse registro
• Mesmo que, na chamada, por acaso seja passado um registro com campo x, a função f precisa funcionar para qualquer entrada do tipo { }
• Fazer o verificador rejeitar acessos a campos que não existem no tipo de entrada declarado também seria uma escolha sólida, mas isso faria a linguagem perder recursos necessários para lidar com dados JSON reais
• O exemplo original de authorities é essencialmente um açúcar sintático para a expressão abaixo

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for authority of authorities

let default = fold{ some port: port, null: 443 }

in  "${authority.domain}:${show (default authority.port)}"

• Se acessos a campos ausentes fossem rejeitados, não seria possível vincular campos potencialmente ausentes nem tratá-los com valores padrão
• A escolha de projeto para lidar bem com dados JSON reais foi a seguinte
  • retornar null quando o campo não existir
  • atribuir ao acesso o tipo forall (a: Type) . Optional a
• Esse tipo é um tipo que só pode conter null
• Ao seguir essa abordagem, torna-se necessário remover dos registros os campos que não existem no supertipo
• Sem remover os campos extras, o exemplo abaixo acabaria retornando 1 : forall (a: Type) . Optional a

let f (input: { }) = input.x

in  f { x: 1 }

• Isso produziria uma expressão mal tipada, com 1 ocupando um tipo que deveria conter apenas null
• Uma expressão incorreta assim poderia até quebrar o avaliador

let f (input: { }) = input.x  # Inferred type: forall (a: Type). Optional a

let default (input: Optional Text) = fold{ some text: text, "" }

in  "${default (f { x: 1 })}!"  # Runtime error if `f` returns `1`

• No Grace, que lida com dados JSON reais, coercionar explicitamente registros para o supertipo faz sentido; o bug real não estava na coerção, mas sim na solução temporária anterior para a inferência do tipo List

[GN⁺]

Opiniões no Lobste.rs

• É algo a se comemorar terem pego o artigo Complete And Easy e transformado em algo que realmente funciona. Também é um bom exemplo de como a natureza gananciosa da checagem de tipos bidirecional pode criar problemas sutis
  Não é uma crítica; inferência sempre traz problemas, e no fim das contas é mais uma questão de escolher quais problemas aceitar. Por isso, pessoalmente vejo subtipagem e coerção de tipos em geral como algo próximo de um antipadrão
  Se você trata os dados como fonte da verdade para o tipo, fica mais difícil verificar se os dados estão errados, e você acaba obtendo o tipo errado em vez de um erro útil, como no exemplo. Dito isso, como a pessoa criou o Dhall, provavelmente entende muito mais disso do que eu. A ideia em si de gerar um esquema a partir de vários dados parece digna de pesquisa, mas não sei se eu chamaria isso de “checagem de tipos”, já que normalmente se pensa em tipos como algo prescritivo, e não descritivo

• Não entendo muito bem por que simplesmente não rejeitar f. Você está acessando um campo em um registro de um tipo que nunca poderia ter esse campo, então quase certamente isso é um bug no programa e parece exatamente o tipo de situação sobre a qual um checador de tipos deveria avisar
  A diferença para o exemplo de authority é que o tipo de port não está ausente, e sim é Optional. Rejeitar campos ausentes não significa que você precise rejeitar também campos opcionais. Se você já está fazendo coerção de valores com base no tipo, então { domain: "google.com" } também pode ser convertido por coerção em um valor { domain: "google.com", port: null }

  • Em resumo, não há necessidade de rejeitar f; isso é uma restrição desnecessária. Eu diria que fazer um acesso de campo inválido retornar null : forall (a : Type) . Optional a é estritamente melhor do que rejeitar esse acesso inválido
    Isso permite mais programas válidos, e programas com tipos incorretos ainda continuam falhando. Por exemplo, um programa que tente usar o valor acessado sem tratar o null ainda continuará com erro de tipo

• O pensamento imediato que me vem é que tipos de linha (row types) resolvem isso. Imagino que isso já tenha sido considerado. Aqui os tipos de linha quebram ao interagir com subtipagem?

  • Grace tem tipos de linha e polimorfismo de linha. Em Grace, as linhas são chamadas de “fields”, mas fora isso é exatamente a mesma coisa
    De fato, o algoritmo de supertipo mais específico também leva tipos de linha em conta
    Por exemplo, se você escrever algo assim:

    \\record0 record1 ->
    
    let _ = record0.x
    
    let _ = record1.y
    
    in  [ record0, record1 ]  
    

    Grace infere o seguinte tipo para essa expressão:

    forall (a : Type) .  
    forall (b : Type) .  
    forall (c : Fields) .  
      { x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c }  
    

• Isso não é um exemplo do problema de instanciação gananciosa mencionado na seção 5.1.1 do artigo Bidirectional Typing?
  “Foi bem infeliz que, na configuração original, essa abordagem gananciosa fosse sensível à ordem dos argumentos. Mas ela pode funcionar bem em um cenário predicativo de polimorfismo de alta ordem sem outras formas de subtipagem. O ‘problema tabby-first’ não pode ocorrer, porque a única forma de um tipo ficar estritamente menor é se tornar estritamente mais polimórfico, e se o primeiro argumento fosse polimórfico então teríamos que instanciar 𝛼 com um tipo polimórfico, o que violaria a predicatividade”