Tipo de inferência com sobrecarga

Question

Eu estou trabalhando em um tipo de sistema de suporte a sobrecarga.Eu tenho uma ideia aproximada do tipo de inferência é geralmente implementado em um cenário como esse, mas eu estou querendo saber como - depois de inferência de tipo é concluída - a correcta implementação de um operador sobrecarregado pode ser escolhido.Ou, em outras palavras, como o tipo inferido pode ser passado de volta para baixo da árvore de sintaxe para o operador.

Para um pequeno exemplo, considere a expressão (x + y) + 1 onde x :: N | S, y :: a, + :: (N -> N -> N) | (S -> S -> S), 1 :: N. :: significa tipo de, e a | b representa o tipo de a ou tipo b.

A propósito, eu suponho, tipo de inferência seria agora, é atravessar a sintaxe da árvore, e para cada nó retornar um tipo de restrição:

(x + y) + 1 => ((N & (N[a=N] | S[a=S])), (N & N) -> N) | ((S & (N[a=N] | S[a=S])), (S & N) -> S) => N[a=N]
  1         => N
  +         => (N -> N -> N) | (S -> S -> S)
  x + y     => ((N & (N | S)), (N & a) -> N) | ((S & (N | S)), (S & a) -> S) => N[a=N] | S[a=S]
    x       => N | S
    y       => a
    +       => (N -> N -> N) | (S -> S -> S)

a & b neste exemplo significa unificador os tipos a e b, [a=T, b=U] é um conjunto de restrições de igualdade para as variáveis do tipo.

Como esperado, o tipo de retorno de uma dada expressão é inferido como N[a=N], que é N onde o tipo da variável a é esperado para ser N.

Portanto, das duas implementações para o + operador (N -> N -> N, S -> S -> S), N -> N -> N deve ser usado.No exemplo dado, o tipo resultante é inferida, mas não o tipo de operador sobrecarregado.A minha pergunta é se existe um padrão comum que é usado para informar a + nó na árvore de sintaxe da implementação.

Answer 1

Você pode organizar a inferência de tipo como se segue.

Suponha que a sua sintaxe de entrada tem tipo Input.Definir a saída de sintaxe Output para ser como Input mas com explícita tipo de anotações em todas as variáveis.O tipo de inferência seria tipo

infer : Input -> List (Output * Type)

Isto é, dada uma entrada e, ele retorna uma lista de possíveis respostas.Cada resposta é um par (e', t) onde e' é e com as variáveis anotada por tipos, e t é o tipo inferido de e.

Você pode visualizar este como todos os acontecendo no nondeterminism mônada.Sempre que você precisar para inferir o tipo de uma variável x, você olhar para cima de seus possíveis tipos de S | T | ... e o ramo em cada um deles.Desta forma, você não tem que "passar para trás" qualquer informação de sub-expressões.Em vez disso, cada sub-expressões já vem anotada, de todas as maneiras possíveis.