Existem alternativas para tipos para análise estática?

A digitação estática em uma linguagem de programação pode ser útil para impor certas garantias no momento da compilação - mas os tipos são a única ferramenta para este trabalho? Existem outras maneiras de especificar invariantes?

Por exemplo, um idioma ou ambiente pode ajudar a impor uma garantia com relação ao comprimento da matriz ou com relação aos relacionamentos entre as entradas de uma função. Eu simplesmente não ouvi nada assim fora de um sistema de tipos.

Uma coisa relacionada sobre a qual eu estava pensando é se existem maneiras não declarativas de fazer análise estática (os tipos são declarativos, na maior parte ).

Sistemas de tipo estático são um tipo de análise estática, mas existem muitas análises estáticas que geralmente não são codificadas em sistemas de tipo. Por exemplo:

• A verificação de modelo é uma técnica de análise e verificação para sistemas concorrentes que permite provar que seu programa é bem-comportado em todas as intercalações de encadeamentos possíveis.

• A análise do fluxo de dados reúne informações sobre os possíveis valores das variáveis, que podem determinar se algum cálculo é redundante ou se algum erro não é contabilizado.

• A interpretação abstrata modela de maneira conservadora os efeitos de um programa, geralmente de maneira que a análise termine - os verificadores do tipo podem ser implementados de maneira semelhante aos intérpretes abstratos.

• A lógica de separação é uma lógica de programa (usada, por exemplo, no analisador Infer ), que pode ser usada para raciocinar sobre os estados do programa e identificar problemas como desreferências de ponteiros nulos, estados inválidos e vazamentos de recursos.

• A programação baseada em contrato é um meio de especificar pré-condições, pós-condições, efeitos colaterais e invariantes. Ada tem suporte nativo para contratos e pode verificar alguns deles estaticamente.

Os compiladores de otimização fazem muitas análises pequenas para criar estruturas de dados intermediárias para uso durante a otimização - como SSA, estimativas de custos inline, informações de emparelhamento de instruções e assim por diante.

Outro exemplo de análise estática não declarativa é encontrado no typechecker Hack , em que construções normais de fluxo de controle podem refinar o tipo de uma variável:

$x = get_value();
if ($x !== null) {
    $x->method();    // Typechecks because $x is known to be non-null.
} else {
    $x->method();    // Does not typecheck.
}

E por falar em “refinar”, de volta à terra dos sistemas de tipos , os tipos de refinamento (como usados ​​no LiquidHaskell ) emparelham tipos com predicados que são garantidos para as instâncias do tipo “refinado”. E os tipos dependentes levam isso adiante, permitindo que os tipos dependam dos valores. O "olá mundo" da digitação dependente geralmente é a função de concatenação da matriz:

(++) : (a : Type) -> (m n : Nat) -> Vec a m -> Vec a n -> Vec a (m + n)

Aqui, ++toma dois operandos do tipo Vec a me Vec a n, sendo vetores com tipo ae comprimento de elemento me n, respectivamente, que são números naturais ( Nat). Retorna um vetor com o mesmo tipo de elemento cujo comprimento é m + n. E essa função comprova essa restrição abstratamente, sem conhecer os valores específicos de me n, portanto, os comprimentos dos vetores podem ser dinâmicos.

A resposta de @ JonPurdy é melhor, mas eu gostaria de adicionar mais alguns exemplos:

Óbvio:

• verificação de sintaxe

• fiapos

Não óbvio:

• A ferrugem permite que o programador especifique se "ligações" são mutáveis e aplica essas restrições.

• Isso está relacionado a algo: algumas linguagens permitem que algum código seja executado no tempo de compilação, o que significa que muitas coisas que seriam erros de tempo de execução podem ser capturadas no tempo de compilação. Alguns exemplos são macros e procedimentos de linguagem Nim marcados com o compileTimepragma .

• A programação lógica é basicamente a construção de um programa, fornecendo asserções.

Digitação semi-estática:

• O Flow do Facebook permite um híbrido entre digitação dinâmica e estática. A idéia é que mesmo o código dinâmico é digitado implicitamente. O Flow permite que você execute um servidor que observe seu código enquanto ele executa para detectar possíveis erros de tipo, mesmo que você não anote suas funções.

A análise de tipo não significa muito.

A Agda é conhecida por ter um sistema do tipo Turing completo, muito diferente (e muito mais difícil de calcular) do que as linguagens ML (por exemplo, Ocaml ).