Testes ou tipos

Oi Habr. Outro dia, eu estava procurando como fazer algo em Idris, e me deparei com um bom post, cuja tradução gratuita parece bastante apropriada. Liberdades e amordaças, quando necessário, denotarei "aqui por tais rabiscos no começo e no fim".

Quando usar testes e quando - tipos? Quais informações e quais garantias recebemos em troca de nossos esforços para escrevê-las?

Veremos um exemplo simples e um pouco artificial, expresso em Python, C, Haskell e Idris. Também veremos o que pode ser dito sobre a implementação sem nenhum conhecimento adicional sobre ela, em cada caso.

Não levaremos em conta as várias backdoors que nos permitem violar explicitamente as garantias de idioma (por exemplo, extensões C, unsafePerformIO em Haskell, conversões de tipo não seguras); caso contrário, seria impossível tirar conclusões e essa postagem seria bastante curta. ⟦Além disso, o mesmo Haskell possui um subconjunto do Safe Haskell que proíbe explicitamente e transitivamente o uso desses e de vários outros truques que podem violar a integridade do idioma.⟧

Especificação

Deixe uma lista e algum significado ser dado. É necessário retornar o índice desse valor na lista ou indicar que esse valor não está na lista.

A implementação desta especificação é trivial, por isso é natural perguntar, e aqui estão geralmente testes ou tipos. No entanto, essas propriedades e métodos de raciocínio, sobre os quais falaremos hoje, são aplicáveis ​​a um código muito mais complexo. Deixe a implementação levar dez mil linhas de código espaguete ilegível, se isso ajudar a ver sua utilidade.

Python

 def x(y, z): # 10000    

Percebemos imediatamente que não estamos interessados ​​nas propriedades desmarcadas e semânticas - que não afetam as propriedades de um programa como a nomeação de variáveis ​​e a documentação de texto; portanto, intencionalmente não escrevi código que ajude a percepção. Estamos interessados ​​apenas no fato de que, sujeito a aprovação em testes e verificações de tipo, não pode ser falso .

No código acima, praticamente não há informações úteis além do fato de termos uma função que aceita dois argumentos. Essa função pode igualmente encontrar o índice do valor na lista ou pode enviar uma carta ofensiva para sua avó.

Análise

Não apenas obtemos código frágil sem testes e tipos, mas nossa única maneira de entender o que uma função faz é a documentação. E como a documentação é verificada por pessoas, não por máquinas, pode facilmente ficar desatualizada - ou inicialmente incorreta -.

• A documentação
  
  • Know Conhecemos o comportamento esperado
    Não temos nada a nos dizer sobre o comportamento dessa função. Você odeia sua avó. Você é um monstro.
• Garantias
  
  • ✓ Segurança de memória
    Python é uma linguagem de coleta de lixo que remove essa preocupação de nós. No entanto, até onde eu sei, nada impede que você puxe bibliotecas inseguras ou C FFI dentro dessa função.

Python com testes

 def test_happy_path(): assert x([1, 2, 3], 2) == 1 def test_missing(): assert x([1, 2, 3], 4) is None 

Agora sabemos que nossa função funciona e, se o elemento estiver ausente, o resultado será None ?

Bem ... não. Este é apenas um exemplo. Infelizmente, o escopo de nossa função é infinito, e nenhum número de exemplos pode provar o correto funcionamento de nossa função. Mais testes - mais confiança, mas nenhum número de testes resolverá todas as dúvidas.

A possibilidade de que essa função retorne None para 4 , mas não para 5 , parece loucura e, nesse caso em particular, isso provavelmente não faz sentido. Podemos ficar satisfeitos com nosso nível de fé e insistir em um certo número de exemplos. Mas, novamente, a postagem será curta, então vamos imaginar que a implementação não seja tão óbvia.

Como os testes não podem provar algo no caso geral, mas apenas mostram o comportamento com exemplos específicos, os testes não podem mostrar a ausência de erros. Por exemplo, não há teste que mostre que nossa função nunca lança uma exceção ou nunca entra no ciclo eterno ou não contém links inválidos. Isso pode ser apenas uma análise estática.

No entanto, mesmo que os exemplos não sejam muito bons no papel de evidência, eles pelo menos constituem uma boa documentação. A partir desses dois exemplos, podemos derivar a especificação completa sob algumas premissas a priori adicionais - esses dois exemplos também satisfazem, por exemplo, o “counterspec” “encontra o elemento na matriz e retorna o anterior, se houver”, o que levou dez segundos para inventar .

Análise

Embora os testes possam mostrar como usar nossa função e também dar um pouco de confiança de que essa função funcione corretamente com pelo menos alguns exemplos, eles não podem provar nada sobre o nosso código no caso geral. Infelizmente, isso significa que os testes ajudam apenas parcialmente a evitar erros.

• A documentação
  
  • ✓ Temos um exemplo de uso
  • ✓ Conhecemos algumas classes de valores que serão processados ​​corretamente
  • ✗ Conhecemos todos os tipos de valores que serão processados ​​corretamente
    Não temos restrições quanto aos tipos de argumentos; portanto, apesar da existência de exemplos do que a função pode manipular, não sabemos quais tipos não foram testados.
  • Know Conhecemos o comportamento esperado
    "O autor do artigo original assinalado aqui, vou me permitir colocar uma cruz, dado o comentário acima"
• Especificação
  
  • ✓ Funciona em pelo menos um caso
  • Index O índice retornado é sempre um índice válido
  • Index O índice retornado sempre indica um valor adequado
  • Item O item ausente sempre retorna None / Nothing
• Erros comuns
  
  • ✗ Sem erros de digitação ou nomes incorretos
    A análise estática pode ajudar, mas como o Python é uma linguagem dinâmica com a capacidade de substituir várias coisas no tempo de execução, nunca podemos provar que não há erros.
    Em particular, pode ser muito difícil ou impossível determinar se o nome do método está correto, pois a validade da chamada do método depende do tipo de tempo de execução do objeto no qual a chamada é feita.
  • Null Nenhum null inesperado
  • Case Caso de erro é sempre tratado
    Na minha experiência, esta é uma das fontes mais comuns de erros: em nosso exemplo, a função retorna None no caso de um elemento ausente, mas o código que usa essa função pode assumir, por exemplo, que sempre retornará um número. Além disso, isso também pode levar a uma exceção não tratada.
• Garantias
  
  • ✓ Segurança de memória
  • ✗ A função não pode ser chamada com o tipo errado
  • ✗ Sem efeitos colaterais
  • ✗ Sem exceções
  • ✗ Sem erros
  • ✗ Sem ciclos perpétuos

Haskell

 xyz = -- 10000   

Se você não estiver familiarizado com a sintaxe: esta é a definição de uma função x com os parâmetros y e z . No Haskell, você pode omitir tipos, pois eles serão deduzidos da implementação - a menos que, é claro, você use diferentes recursos avançados de extensões modernas do sistema de tipos -.

Pode parecer que isso não é muito diferente da versão do Python, mas apenas porque escrevemos nossa função no Haskell e ela é lado a lado, já podemos falar sobre algumas propriedades interessantes.

Análise

Obviamente, não podemos tirar muitas conclusões aqui, mas aqui estão alguns pontos a serem observados:

• A documentação
  
  • Know Conhecemos o comportamento esperado
• Erros comuns
  
  • ✓ Sem erros de digitação ou nomes incorretos
    Como Haskell é uma linguagem compilada, todos os nomes devem ser resolvidos no momento da compilação. O programa simplesmente não será compilado se houver esse erro.
  • ✓ Nenhum null inesperado
    Haskell simplesmente não possui null . O problema está resolvido!
• Garantias
  
  • ✓ Segurança de memória
  • ✓ A função não pode ser chamada com o tipo errado
  • ✓ Sem efeitos colaterais inesperados
    ⟦O autor do artigo original não indicou esse item, mas permitirei observar que, se houver efeitos colaterais, o tipo deduzido dessa função indicará sua presença, para que o código de chamada saiba sobre seus recursos.⟧

Especificação do tipo Haskell

 x :: Eq a => [a] -> a -> Maybe Int xyz = -- ... 

Anteriormente, conversamos sobre uma atitude bastante conivente com a segurança das avós: ficou claro pelos testes que a função não iria prejudicar ninguém, mas a avó estava realmente segura? Essa função não envia com precisão palavrões?

Haskell é conhecido por ser uma linguagem funcional pura. Isso não significa que o código não pode ter efeitos colaterais, mas todos os efeitos colaterais devem estar presentes no tipo. Conhecemos o tipo dessa função, vemos que ela está limpa e, portanto, temos certeza de que essa função não modifica nenhum estado externo.

Esta é uma propriedade muito interessante por outros motivos: como sabemos que não há efeitos colaterais, podemos entender o que essa função faz, com base apenas em sua assinatura! Basta pesquisar nesta assinatura do Hoogle e ver o primeiro resultado. Obviamente, essa não é a única função possível que teria esse tipo, mas o tipo nos dá confiança suficiente para os fins da documentação.

Análise

• A documentação
  
  • ✓ Conhecemos o comportamento esperado
  • ✗ Temos um exemplo de uso
  • ✓ Conhecemos algumas classes de valores que serão processados ​​corretamente
  • ✓ Conhecemos todos os tipos de valores que serão processados ​​corretamente
• Especificação
  
  • ✗ Funciona em pelo menos um caso.
    Com testes ou evidências ausentes, não sabemos se nossa função funciona como esperado!
  • Index O índice retornado é sempre um índice válido.
  • Index O índice retornado sempre indica um valor adequado.
  • Item Um item ausente sempre retorna None / Nothing .
• Erros comuns
  
  • ✓ Sem erros de digitação ou nomes incorretos
  • ✓ Nenhum null inesperado
  • ✓ Caso de erro é sempre tratado
    Se nossa função retornar Nothing , o sistema de tipos garantirá que este caso seja tratado corretamente pelo código de chamada. Obviamente, esse caso pode ser ignorado, mas isso deve ser feito explicitamente.
• Garantias
  
  • ✓ Segurança de memória
  • ✓ A função não pode ser chamada com o tipo errado
  • ✓ Sem efeitos colaterais
  • ✗ Sem exceções
    Compartilho exceções e erros, acreditando que após as exceções é possível recuperar e após erros (por exemplo, funções parcialmente definidas) - não.
    Na maioria das vezes, as exceções são descritas em tipos (por exemplo, na mônada de E / S). De uma maneira boa, devemos saber que uma função não gera uma exceção, apenas com base em seu tipo. No entanto, Haskell quebra essa expectativa ao permitir que exceções sejam lançadas do código puro .
    Addition Além disso, vale a pena notar que, em Haskell, erros como chamar incorretamente funções parcialmente definidas também são apresentados como exceções que podem ser capturadas e processadas; portanto, a diferença entre as duas categorias é um pouco menos óbvia.
  • ✗ Sem erros
    Ainda podemos usar funções parcialmente definidas, por exemplo, divisão por zero.
  • ✗ Sem ciclos perpétuos

Haskell com testes

Lembre-se, eu disse anteriormente que testes não podem provar a ausência de erros? Eu menti. Quando as estrelas convergem corretamente e se os testes são combinados com tipos, isso se torna possível! A primeira estrela é a finitude do domínio de nossa função. O segundo - o domínio da definição deve ser não apenas finito, mas também não muito grande; caso contrário, esse teste será difícil de colocar em prática.

Por exemplo:

 not :: Bool -> Bool not x = ... 

A entrada pode ser True ou False . Basta testar essas duas opções e aqui está o Santo Graal! Sem exceções, ciclos perpétuos, resultados incorretos, sem erros. No entanto, para uma função um pouco mais complexa, pode não estar claro quanto tempo é dedicado aos testes: se eles levam muito tempo para serem concluídos, terminamos em um ciclo eterno, ou é apenas pesado? O problema de impedi-la.

De fato, isso também não é inteiramente verdade no caso de Haskell: em cada tipo de Haskell também há um valor ⊥ (que pode ser obtido como undefined , error ou error em certo sentido, como recursão infinita), mas os haskellistas tradicionalmente fecham os olhos e acreditam que isso não existe.

Leitura extracurricular: Existem apenas quatro bilhões de carros alegóricos - então teste todos!

De qualquer forma, em nosso exemplo original, o escopo é infinito; portanto, os testes podem mostrar apenas que nosso código funciona para um conjunto finito de exemplos.

Análise
Nesse caso, os testes complementam os tipos e tamponam alguns orifícios no sistema do tipo Haskell. Temos muito mais confiança em nosso código em comparação ao uso apenas de testes ou tipos.

C

 /* C    ,    int */ int x(int *y, size_t n, int z) { /* 10000    */ } 

Consideramos C fora de interesse em sistemas do tipo mais antigo. Em C, em particular, os tipos provavelmente não são necessários pelo programador, mas pelo compilador para ajudá-lo a gerar código mais rápido.

Em nosso exemplo, não sabemos o que a função retornará se o elemento não for encontrado. Teremos que confiar na tradição ou na documentação (por exemplo, neste caso, pode ser -1 ).

Também podemos usar argumentos: dessa forma, podemos retornar um erro e armazenar o valor de retorno nesse argumento de saída. Essa é uma opção um pouco mais expressiva, mas ainda precisamos confiar na documentação para entender quais parâmetros são lidos e quais são escritos. Nos dois casos, é difícil entender o comportamento observando os tipos.

 /*   ,   out- */ error_t x(int *y, size_t n, int z, size_t *w) { /* 10000    */ } 

Análise
O sistema de tipos em si não nos oferece tantas garantias. Obviamente, obtemos algumas informações desses tipos, mas basta compará-las com o caso Haskell.

Idris

 x : Eq x => List x -> x -> Maybe Int xyz = ... 

Esta função é do mesmo tipo que no caso de Haskell. No entanto, com um sistema de tipo mais expressivo, podemos obter mais. A escolha dos tipos pode falar sobre a implementação.

 %default total x : Eq x => Vect nx -> x -> Maybe (Fin n) xyz = ... 

Esse tipo pode ser lido como "me dê uma lista de tamanho n e algum valor, e retornarei um número menor que n ou Nothing ". Isso garante que a função retorne um índice que obviamente não excede os limites.

Além disso, esta função é total, ou seja, o temporizador verificou se sempre termina. Isso elimina ciclos e erros perpétuos.

Análise

• Especificação
  
  • ✗ Funciona em pelo menos um caso.
  • ✓ O índice retornado é sempre o índice correto
  • Index O índice retornado sempre indica um valor adequado
  • Item O item ausente sempre retorna None / Nothing
• Garantias
  
  • ✓ Segurança de memória
  • ✓ A função não pode ser chamada com o tipo errado
  • ✓ Sem efeitos colaterais
  • ✗ Sem exceções
  • ✓ Sem erros
  • ✓ Sem ciclos perpétuos

Idris com testes

Como a linguagem de tipo de Idris é tão expressiva quanto a linguagem de seus termos ⟦(ou melhor, sua parte comprovadamente total)⟧, a distinção entre teste e tipo fica embaçada:

 ex : x [1, 2, 3] 2 = Just 1 ex = Refl 

Essa função possui um tipo bastante estranho x [1, 2, 3] 2 = Just 1 . Esse tipo significa que, para uma verificação bem-sucedida do tipo, o typer deve provar que x [1, 2, 3] 2 estruturalmente igual a Just 1 . ⟦Neste caso, a prova é trivial, pois basta o basculante normalizar os termos nos dois lados do sinal de igual, o que será feito em tempo finito devido à totalidade de todas as funções utilizadas e que levará a um resultado único devido a Church-Rosser. Depois disso, pode-se usar a reflexividade da igualdade, que é o que Refl .

De fato, escrevemos um teste de nível de tipo.

Idris com evidência

Para uma análise completa, podemos usar todo o poder dos tipos dependentes e provar nossa implementação (já que os tipos dependentes no Idris são equivalentes a um sistema lógico que inclui lógica construtiva de primeira ordem).

Em particular, podemos provar propriedades que antes eram inatingíveis para nós:

 --      Eq  DecEq x : DecEq a => Vect na -> (y : a) -> Maybe (Fin n) xyz = ... --    ,       `x` findIndexOk : DecEq a => (y : Vect na) -> (z : a) -> case xyz of Just i => index iy = z Nothing => Not (Elem zy) findIndexOk yz = ... 

O tipo findIndexOk pode ser lido como “para qualquer tipo a que tenha uma comparação algoritmicamente decidível ( DecEq ), para qualquer vetor y elementos do tipo a qualquer comprimento n e qualquer valor z tipo a : se xyz retornar o índice i , esse índice está z , mas se xyz retorna Nothing , então não existe esse elemento no vetor. ”

Is É interessante que o autor do artigo original ofereça um tipo um pouco mais fraco que o indicado acima.⟧

Agora temos tudo capturado! Quais são as desvantagens? Bem, escrever todas essas evidências pode ser bastante difícil.

Comparação

Parecer

Na minha opinião, o uso de um sistema de tipo moderno em si é mais eficaz em termos de relacionamento das informações recebidas e garantias aos esforços despendidos. Se você deseja escrever um código razoavelmente confiável, os tipos podem ser temperados com testes. Idealmente - no estilo do QuickCheck.

Com tipos dependentes, a linha entre testes e tipos se torna menos óbvia. Se você estiver escrevendo um software para a Boeing ou para marca-passos, pode ser útil escrever evidências.