Chamadas de função de verificação de tipo com subtipagem funcional

Question

Sou relativamente novo no assunto. Suponha que você queira verificar o tipo de uma expressão do formulário f(a), ou seja, uma chamada de função. Supondo que todas as declarações sejam tipos explícitos, acredito que um verificador de tipo simples se comportaria da seguinte maneira:

1. Dado o ambiente, calcule os tipos de ae f;
2. Verifique se o tipo de fé do formulário$T\to U$;
3. Verifique se o tipo de aé um subtipo de$T$;
4. Retornar $U$ se necessário.

Mas agora suponha que, para todos $U$, a seguinte relação de subtipagem é válida:

$$ [U]<:\text{Int}\to U $$

Onde $[\thinspace\cdot\thinspace]$denota o tipo de matriz, e esse cálculo (1) encontra os tipos de ae fa serem resp.$T$ e $[U]$ para alguns $T$, $U$. Agora,$[U]$não é um tipo de função, portanto, a verificação (2) falha. Estou assumindo que a definição de$<:$é completamente independente do verificador de tipo, portanto, não podemos apenas codificar uma verificação (2.1) para tipos de array também. Em vez disso, poderíamos verificar se$[U]$ ser um subtipo de um tipo de função menos aceitável $T\to\top$, Onde $\top$ denota o tipo de universo, mas e se os tipos de função forem invariantes de acordo com $<:$?

Suspeito que o que realmente preciso é de uma forma de inferência de tipos, em vez de verificação de tipos, embora os tipos de fe asejam completamente determinados, o que não faz sentido para mim. Qual seria a abordagem correta, aqui?

Answer 1

Presumivelmente, o que Scala faz (já que você mencionou) é relaxar seu passo 2. É incorreto verificar se o tipo de $f$ é meramente 'da forma' $T → U$porque é aplicado. Em vez disso, deve-se verificar se o tipo de$f$ é conhecido por ser um subtipo de alguns $T → U$.

No Scala, esses subtipos de 'fatos' podem ser adicionados por declaração ao definir um tipo. Portanto, os arrays são declarados como subtipos de tipos de função. Você deu isso como:

$$[U] <: \mathsf{Int} → U$$

Este é apenas um axioma que precisa fazer parte da verificação de subtipagem. Scala é na verdade ainda mais complexo do que isso, mas pelo menos cobre a parte da subtipagem.

Como Andrej mencionou nos comentários, esses tipos de axiomas de subtipagem 'declarados' arbitrários não levam necessariamente ao melhor comportamento (tipos principais, decidibilidade etc.). Pode haver várias estratégias específicas pelas quais você pode substituir suas etapas para incorporar a mudança para a etapa 2, e elas podem ter diferentes limitações sobre os tipos que podem verificar / inferir para vários exemplos.