Digitação gradual - Gradual typing

A tipagem gradual é um sistema de tipos em que algumas variáveis e expressões podem receber tipos e a correção da digitação é verificada em tempo de compilação (que é a tipagem estática ) e algumas expressões podem ser deixadas sem tipo e eventuais erros de tipo são relatados em tempo de execução (que é a digitação dinâmica ). A digitação gradual permite que os desenvolvedores de software escolham qualquer paradigma de tipo conforme apropriado, em um único idioma. Em muitos casos, a digitação gradual é adicionada a uma linguagem dinâmica existente, criando uma linguagem derivada que permite, mas não exige, o uso da digitação estática. Em alguns casos, um idioma usa digitação gradual desde o início.

História

O termo foi cunhado por Jeremy Siek. Jeremy Siek e Walid Taha começaram a pesquisar a digitação gradual em 2006.

Implementação

Em particular, a tipagem gradual usa um tipo especial denominado dinâmico para representar tipos estaticamente desconhecidos, e a tipagem gradual substitui a noção de igualdade de tipo por uma nova relação chamada consistência que relaciona o tipo dinâmico a todos os outros tipos. A relação de consistência é simétrica, mas não transitiva.

Tentativas anteriores de integrar tipagem estática e dinâmica tentaram fazer com que o tipo dinâmico ocupasse o topo e a base da hierarquia de subtipos. No entanto, como a subtipagem é transitiva, isso resulta em cada tipo tornando-se relacionado a todos os outros tipos e, portanto, a subtipagem não excluiria mais quaisquer erros de tipo estático. A adição de uma segunda fase de verificação de plausibilidade ao sistema de tipos não resolveu completamente este problema.

A digitação gradual pode ser facilmente integrada ao sistema de tipos de uma linguagem orientada a objetos que já usa a regra de subsunção para permitir upcasts implícitos com relação à subtipagem. A ideia principal é que consistência e subtipagem são ideias ortogonais que compõem bem. Para adicionar subtipagem a uma linguagem digitada gradualmente, basta adicionar a regra de subsunção e adicionar uma regra de subtipagem que torna o tipo dinâmico um subtipo de si mesmo, porque a subtipagem deve ser reflexiva. (Mas não torne o topo da ordem de subtipagem dinâmico!)

Exemplos

Exemplos de linguagens digitadas gradualmente derivadas de linguagens digitadas dinamicamente existentes incluem Closure Compiler , TypeScript (para JavaScript ), Hack (para PHP), PHP (desde 7.0), Typed Racket (para Racket ), Typed Clojure (para Clojure ), Cython ( um compilador Python ), mypy (um verificador de tipo estático para Python ), pyre (verificador de tipo estático alternativo para Python) ou cperl (um Perl 5 digitado ). O ActionScript é uma linguagem digitada gradualmente que agora é uma implementação do ECMAScript , embora originalmente tenha surgido separadamente como um irmão, ambos influenciados pelo HyperTalk da Apple .

Um sistema para a linguagem de programação J foi desenvolvido, adicionando coerção, propagação de erro e filtragem às propriedades normais de validação do sistema de tipo, bem como aplicando funções de tipo fora das definições de função, aumentando assim a flexibilidade crescente das definições de tipo.

Por outro lado, C # começou como uma linguagem de tipagem estática, mas a partir da versão 4.0 é gradativamente digitada, permitindo que as variáveis ​​sejam explicitamente marcadas como dinâmicas usando o dynamictipo. As linguagens digitadas gradualmente não derivadas de uma linguagem digitada dinamicamente incluem Dart , Dylan e Raku .

Raku (anteriormente Perl6) implementou a tipagem gradual desde o início. As verificações de tipo ocorrem em todos os locais onde os valores são atribuídos ou vinculados. Uma variável ou parâmetro "sem tipo" é digitado como Any, que corresponderá a (quase) todos os valores. O compilador sinaliza conflitos de verificação de tipo em tempo de compilação se puder determinar em tempo de compilação que eles nunca terão êxito.

Objective-C tem digitação gradual para ponteiros de objeto com respeito a chamadas de método. A tipagem estática é usada quando uma variável é digitada como um ponteiro para uma certa classe de objeto: quando uma chamada de método é feita para a variável, o compilador verifica estaticamente se a classe está declarada para suportar tal método ou gera um aviso ou erro . No entanto, se uma variável do tipo idfor usada, o compilador permitirá que qualquer método seja chamado nela.

A JS ++ linguagem de programação, lançado em 2011, é um super conjunto de JavaScript (tipagem dinâmica) com um sistema do tipo gradual que é som para ECMAScript e DOM casos de canto API.

Referências

Leitura adicional

• Siek, Jeremy G .; Vitousek, Michael M .; Cimini, Matteo; Boyland, John Tang (2015). Ball, Thomas; Bodik, Rastislav; Krishnamurthi, Shriram; Lerner, Benjamin S .; Morrisett, Greg (eds.). Critérios refinados para digitação gradual . 1ª Cúpula sobre Avanços em Linguagens de Programação (SNAPL 2015) . Leibniz International Proceedings in Informatics (LIPIcs). 32 . Dagstuhl, Alemanha: Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik. pp. 274–293. doi : 10.4230 / lipics.snapl.2015.274 . ISBN 9783939897804.