O futuro dos sistemas de tipos das linguagens de programação

Discussões infindáveis sobre qual a melhor linguagem de programação sempre existiram e sempre existirão. Um dos pontos sempre muito discutidos é a questão do melhor estilo de tipagem: seria melhor uma tipagem dinâmica a la Ruby, com muita concisão, ou seria mais interessante uma linguagem estaticamente tipada a la Java, que consegue detectar vários erros em tempo de compilação, mas bastante verbosa e menos flexível?

É engraçado que quando programo em Ruby e tenho que usar um método fico muitas vezes desconfortável por não saber exatamente que tipo posso passar nos parâmetros sem olhar a documentação, ou ainda fico gastando um tempão em um jeito de fazer a assinatura dos meus métodos deixar bem claro o tipo de objeto esperado, ao passo que voltando pra Java chegava a ser ridículo o número de linhas necessários para fazer coisas simples, ou ainda acaba acontecendo muita dificuldade em refatorações que deveriam ser simples.

Sempre foi bem claro que ambas as abordagens tem vantagens e desvantagens, e sentia que a linguagem que conseguisse juntar isso estaria a frente das demais em questão de design e expressividade.

E assistindo a essa palestra mais acadêmica do Strangeloop, fica ainda mais claro que essa noção intuitiva é verdadeira. 

Nela, os palestrantes começam pelo objetivo de um bom sistema de tipos: fazer representações de estados ilegais não serem possíveis de representar pela sintaxe de um programa bem formado (ou seja, que compila sem erros). Se extrapolarmos, em um sistema de tipos perfeito (tipo um verificador formal), você tem segurança total que seu programa vai funcionar para todas as entradas antes mesmo de ele executar. 

Os sistemas de tipos atuais como os de Java e C++ estão tão longe desse ideal (nullpointer exceptions, pra citar um exemplo comum de problema de runtime), ficando muitas vezes tão no caminho do programador, que muitos designers de linguagens de programação tais como Ruby preferiram simplesmente sequer ter um sistema de tipos, e deixar que todos esses erros sejam capturados em runtime mesmo. E provavelmente esse foi um dos grandes motivadores para a comunidade Ruby ter desenvolvido tantos frameworks de teste bons, já que com testes você pode em runtime (pelo menos não em produção) se certificar que tudo funciona como esperado.

Uma frase que eu gostei da Amanda Laucher nessa mesma palestra é que não precisamos de mais linguagens dinâmicas, precisamos de linguagens com sistemas de tipos melhores. E é por esse caminho que as linguagems tem andado. Scala é um caso de linguagem estaticamente tipada que faz tantas inferências em tempo de compilação que chega a enganar os mais desavisados num primeiro momento olhando pro código de que é dinâmica (ainda que com o custo de uma compilação muito lenta). Golang também segue por ai também, com bastante inferência de tipos.

Além de estarmos presenciando essa evolução nos sistemas de tipos das linguagens mais recentes, as tradicionais dinamicamente tipadas Ruby e Python também começaram a perceber que certas verificações antes do tempo de runtime podem ser bastante benéficas. Matz, o criador de Ruby, anunciou suas propostas de verificações de tipo na Rubyconf 2014, na esperança de já ver elas em Ruby 3.0 (que eu espero que realmente aconteçam). Python também teve propostas nessa linha feitas por seu criador Guido van Rossum.

Se você pensava que já tinhamos linguagens demais, o futuro parece indicar que teremos muitas outras, além de grandes modificações nas já existentes, há muito ainda por onde evoluir.

PS: Pra quem acha o assunto fascinante, dê uma olhada em linguagens acadêmicas com dependent types como o Idrys, é meio complicado, mas as ideias pro trás parecem bem imteressantes.

Outro PS: Post inspirado por esse excelente post do Yevgeniy Brikman.