Tipo de inferência com sobrecarga
-
29-09-2020 - |
Pergunta
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.
Solução
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.