Olá pessoal!
Apesar da estranheza e de alguma abstração do tópico considerado hoje - esperamos que ele possa diversificar seu fim de semana. No final do post, colocamos três links do autor, permitindo que você se familiarize com a digitação dependente de Idris, F * e JavaScript
Às vezes, parece que as linguagens de programação não mudaram muito desde os anos 60. Quando eles me falam sobre isso, lembro-me com frequência de quantas ferramentas e recursos interessantes temos agora à nossa disposição e como eles simplificam nossas vidas. Prontamente: trata-se de depuradores integrados, testes de unidade e analisadores estáticos e IDEs legais, bem como matrizes digitadas e muito mais. O desenvolvimento de idiomas é um processo longo e progressivo, e não existem “balas de prata” com as quais o desenvolvimento de idiomas mudaria de uma vez por todas.
Hoje, quero falar sobre uma das últimas etapas deste processo em andamento. A tecnologia de que estamos falando ainda está sendo explorada ativamente, mas tudo indica que em breve se enraizará nos principais idiomas. E nossa história começa com um dos conceitos mais fundamentais em ciência da computação: com
tipos .
Mundo dos tipos
Digitar é uma daquelas coisas tão inseparáveis do nosso pensamento que quase nem pensamos no conceito de tipos como tal? Por que 1 é um
int , mas se você apenas colocar esse valor entre aspas - e ele se transformar em uma
string ? O que é um "tipo" em essência? Como costuma acontecer na programação, a resposta depende da redação da pergunta.
Os tipos são diversos. Em alguns sistemas de tipos, existem limites muito claros entre tipos e valores. Portanto, 3, 2 e 1 são valores
integer , mas
integer não é um valor. Esse construto é "incorporado" na linguagem e fundamentalmente diferente do significado. Mas, de fato, essa diferença não é necessária e pode apenas nos limitar.
Se você liberar os tipos e transformá-los em outra categoria de valores, várias possibilidades surpreendentes se abrirão. Os valores podem ser armazenados, convertidos e passados para funções. Assim, seria possível criar uma função que toma um tipo como parâmetro, criando funções generalizadas: aquelas que podem trabalhar com muitos tipos sem sobrecargas. Você pode ter uma matriz de valores de um determinado tipo, em vez de fazer aritmética e tipografia de ponteiros estranhos, como é necessário em C. Você também pode coletar novos tipos à medida que o programa é executado e fornecer recursos como desserialização automática de JSON. Mas, mesmo se você tratar os tipos como valores, ainda não poderá fazer tudo o que os tipos podem fazer com valores. Portanto, operando com instâncias de usuário, você pode, por exemplo, comparar seus nomes, verificar sua idade ou identificador etc.
if user.name == "Marin" && user.age < 65 { print("You can't retire yet!") }
No entanto, quando você tenta fazer o mesmo com o tipo de
User , você pode comparar apenas nomes de tipos e possivelmente nomes de propriedades. Como esse é um tipo, não uma instância, você não pode verificar os valores de suas propriedades.
if typeof(user) == User { print("Well, it's a user. That's all I know") }
Quão legal seria se tivéssemos uma função capaz de receber apenas uma lista não vazia de usuários? Ou uma função que aceitaria um endereço de email apenas se ele estivesse gravado no formato correto? Para esses fins, você precisaria dos tipos "matriz não vazia" ou "endereço de email". Nesse caso, é um tipo dependente de valor, ou seja, sobre o
tipo dependente . Nos idiomas comuns, isso não é possível.
Para que tipos possam ser usados, o compilador deve verificá-los. Se você afirmar que a variável contém um número inteiro, seria melhor se não houvesse uma
string , caso contrário, o compilador jurará. Em princípio, isso é bom, porque não nos permite cortejar. A verificação de tipos é bastante simples: se uma função retorna um
integer e tentamos retornar
"Marin" nela, isso é um erro.
No entanto, com tipos dependentes, as coisas ficam mais complicadas. O problema é quando exatamente o compilador verifica os tipos. Como ele pode ter certeza de que existem exatamente três valores na matriz, se o programa ainda nem está em execução? Como garantir que um número inteiro seja maior que 3, se ainda nem foi atribuído? Há
mágica nisso ... ou, em outras palavras,
matemática . Se for possível provar matematicamente que o conjunto de números é sempre maior que 3, o compilador pode verificar isso.
Matemática no estúdio!
A indução matemática é usada para formular evidências. A indução permite confirmar incondicionalmente a verdade de uma afirmação. Por exemplo, queremos provar que a seguinte fórmula matemática vale para qualquer número positivo:
1 + 2 + 3 + ... + x = x * (x + 1) / 2
Há um número infinito de possíveis x, por isso levaria muito tempo para verificar todos os números manualmente. Felizmente, isso não é necessário. Só precisamos provar duas coisas:
- Esta afirmação é observada no primeiro dia. (Geralmente é 0 ou 1)
- Se esta afirmação for verdadeira para o número
n , será verdadeira para o próximo número n + 1
Como a instrução é observada para o primeiro número e para todos os números a seguir, sabemos que é verdadeira para todos os números possíveis.
Para provar isso não é difícil:
1 = 1 * (1 + 1) / 2 1 = 1
Agora também temos que provar que a afirmação vale para todos os outros números. Para fazer isso, suponha que funcione para algum número n e verifique se também funciona para n + 1.
Supondo que a seguinte expressão seja verdadeira:
1 + 2 + 3 + ... + n = n * (n + 1) / 2
Confira
n + 1 :
(1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2
Assim, podemos substituir
"(1 + 2 + 3 + ... + n)" igualdade acima:
(n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2)
e simplifique para
(n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1)
Como as duas partes da expressão são iguais, garantimos que essa afirmação seja verdadeira. Essa é uma das maneiras pelas quais você pode verificar a verdade das declarações sem calcular manualmente cada caso, e é com base nesse princípio que os tipos dependentes funcionam. Você escreve uma declaração matemática para garantir que a tese do tipo seja verdadeira.
A beleza dessa abordagem reside no fato de que qualquer prova matemática pode ser emitida na forma de um programa de computador - e é disso que precisamos!
Voltar à programação
Então, descobrimos que algumas coisas podem ser provadas primeiro e depois passar para valores específicos. Para fazer isso em uma linguagem de programação, você precisa de uma maneira de expressar essas instruções no código que será gravado no próprio sistema de tipos, ou seja, o sistema de tipos precisa ser aprimorado.
Considere um exemplo. Aqui temos uma função de acréscimo que pega duas matrizes e as combina. Como regra, a assinatura de uma função será semelhante a esta:
append: (arr1: Array, arr2: Array) -> Array
No entanto, apenas olhando a assinatura, não podemos ter certeza da implementação correta. O fato de a função retornar uma matriz não significa que ela fez alguma coisa. Uma maneira de verificar o resultado é garantir que o comprimento da matriz resultante seja igual à soma dos comprimentos das matrizes de parâmetros.
newArray = append([1], [2, 3]) assert(length(newArray) == 3)
Mas por que verificar isso em tempo de execução, se você pode criar uma restrição que será verificada em tempo de compilação:
append: (arr1: Array, arr2: Array) -> newArray: Array where length(newArray) == length(arr1) + length(arr2)
Declaramos que
append é uma função que recebe dois argumentos de
Array e retorna um novo argumento de
Array , que chamamos de
newArray . Só que desta vez adicionamos uma ressalva de que o comprimento da nova matriz deve ser igual à soma dos comprimentos de todos os argumentos da função. A declaração que tínhamos acima no tempo de execução é convertida para o tipo em tempo de compilação.
O código acima refere-se ao mundo dos tipos, não dos valores, ou seja, o sinal
== indica uma comparação do
length tipo retornado, e não do seu valor. Para que esse mecanismo funcione, o comprimento do tipo retornado deve nos fornecer algumas informações sobre o número real.
Para garantir a operação de um mecanismo desse tipo, você precisa garantir que cada número seja de um tipo separado. Um tipo pode conter apenas um valor: 1. O mesmo se aplica a Dois, Três e todos os outros números. Naturalmente, esse trabalho é muito cansativo, mas é para esse trabalho que temos programação. Você pode escrever um compilador que fará isso por nós.
Feito isso, é possível criar tipos separados para matrizes contendo 1, 2, 3 e um número diferente de elementos.
ArrayOfOne ,
ArrayOfTwo , etc.
Assim, é possível definir um comprimento de função que terá um dos tipos de matriz acima e tenha um tipo de retorno dependente de
One for
ArrayOfOne ,
Two for
ArrayOfTwo , etc. para cada número.
Agora que temos um tipo separado para qualquer comprimento específico da matriz, podemos verificar (em tempo de compilação) que ambas as matrizes têm o mesmo comprimento. Para fazer isso, compare seus tipos. E como os tipos têm os mesmos valores que qualquer outro, você pode atribuir operações a eles. Você pode determinar a adição de dois tipos específicos, especificando que a soma de
ArrayOfOne e
ArrayOfTwo é igual a
ArrayOfThree .
Essas são todas as informações que o compilador precisa para garantir que o código que você escreveu esteja correto.
Suponha que desejemos criar uma variável do tipo
ArrayOfThree :
result: ArrayOfThree = append([1], [2, 3])
O compilador pode determinar que [1] possui apenas um valor, para que você possa atribuir o tipo
ArrayOfOne . Também pode atribuir
ArrayOfTwo a [2, 3].
O compilador sabe que o tipo de resultado deve ser igual à soma dos tipos do primeiro e do segundo argumento. Ele também sabe que ArrayOfOne + ArrayOfTwo é igual a ArrayOfThree, ou seja, ele sabe que toda a expressão no lado direito da identidade é do tipo ArrayOfThree. Corresponde à expressão à esquerda e o compilador está satisfeito.
Se escrevemos o seguinte:
result: ArrayOfTwo = append([1], [2, 3])
o compilador ficaria completamente insatisfeito, pois saberia que o tipo está incorreto.
Digitar dependente é muito legal
Nesse caso, é impossível permitir um grande número de erros. Com a digitação dependente, erros por unidade, acessos a índices de matriz inexistentes, exceções de ponteiro nulo, loops infinitos e código quebrado podem ser evitados.
Usando tipos dependentes, você pode expressar quase tudo. A função fatorial aceita apenas números naturais, a função de
login não aceita linhas vazias, a função
removeLast aceita apenas matrizes não vazias. Além disso, tudo isso é verificado antes de você iniciar o programa.
O problema com as verificações de tempo de execução é que elas falham se o programa já estiver em execução. Isso é normal se o programa for executado apenas por você, mas não pelo usuário. Os tipos dependentes permitem que você leve essas verificações ao nível dos tipos, portanto, falhas desse tipo durante a execução do programa se tornam impossíveis.
Acho que a digitação dependente é o futuro das linguagens de programação convencionais, e mal posso esperar para esperar por isso!
→
Idris→
F *→
Adicionando tipos dependentes ao JavaScript