Na programação funcional, como alcançar a modularidade através de leis matemáticas?

Li nesta pergunta que programadores funcionais tendem a usar provas matemáticas para garantir que seu programa esteja funcionando corretamente. Isso parece muito mais fácil e rápido do que o teste de unidade, mas vindo de uma experiência em OOP / Unit Testing, nunca vi isso acontecer.

Você pode me explicar e me dar um exemplo?

Uma prova é muito mais difícil no mundo da OOP por causa de efeitos colaterais, herança irrestrita e nullser membro de todos os tipos. A maioria das provas se baseia em um princípio de indução para mostrar que você cobriu todas as possibilidades, e todas essas três coisas tornam isso mais difícil de provar.

Digamos que estamos implementando árvores binárias que contêm valores inteiros (para manter a sintaxe mais simples, não trarei programação genérica para isso, embora isso não mude nada.) No ML padrão, eu definiria isso como esta:

datatype tree = Empty | Node of (tree * int * tree)

Isso introduz um novo tipo chamado treecujos valores podem vir exatamente em duas variedades (ou classes, que não devem ser confundidas com o conceito OOP de uma classe) - um Emptyvalor que não carrega informações e Nodevalores que carregam uma tripla cuja primeira e última elementos são se treecujo elemento do meio é um int. A aproximação mais próxima a esta declaração no OOP seria assim:

public class Tree {
    private Tree() {} // Prevent external subclassing

    public static final class Empty extends Tree {}

    public static final class Node extends Tree {
        public final Tree leftChild;
        public final int value;
        public final Tree rightChild;

        public Node(Tree leftChild, int value, Tree rightChild) {
            this.leftChild = leftChild;
            this.value = value;
            this.rightChild = rightChild;
        }
    }
}

Com a ressalva de que variáveis ​​do tipo Árvore nunca podem ser null.

Agora vamos escrever uma função para calcular a altura (ou profundidade) da árvore e supor que temos acesso a uma maxfunção que retorna o maior de dois números:

fun height(Empty) =
        0
 |  height(Node (leftChild, value, rightChild)) =
        1 + max( height(leftChild), height(rightChild) )

Nós definimos a heightfunção de casos - não há uma definição para Emptyárvores e uma definição para Nodeárvores. O compilador sabe quantas classes de árvores existem e emitirá um aviso se você não definir os dois casos. A expressão Node (leftChild, value, rightChild)na assinatura da função liga os valores da 3-tupla às variáveis leftChild, valuee, rightChildrespectivamente, para que possa consultá-las na definição da função. É semelhante a ter declarado variáveis locais como este em uma linguagem OOP:

Tree leftChild = tuple.getFirst();
int value = tuple.getSecond();
Tree rightChild = tuple.getThird();

Como podemos provar que implementamos heightcorretamente? Podemos usar a indução estrutural , que consiste em: 1. Prove que heightestá correto no (s) caso (s) base (s) do nosso treetipo ( Empty) 2. Supondo que as chamadas recursivas heightestejam corretas, prove que está correto no (s) caso (s) heightnão básico (s) ) (quando a árvore é realmente a Node).

Para a etapa 1, podemos ver que a função sempre retorna 0 quando o argumento é uma Emptyárvore. Isso está correto por definição da altura de uma árvore.

Para a etapa 2, a função retorna 1 + max( height(leftChild), height(rightChild) ). Supondo que as chamadas recursivas realmente retornem a altura das crianças, podemos ver que isso também está correto.

E isso completa a prova. Os passos 1 e 2 combinados esgotam todas as possibilidades. Observe, no entanto, que não temos mutação, nulos e existem exatamente duas variedades de árvores. Tire essas três condições e a prova rapidamente se torna mais complicada, se não impraticável.

EDIT: Como essa resposta chegou ao topo, gostaria de adicionar um exemplo menos trivial de uma prova e cobrir a indução estrutural um pouco mais completamente. Acima, provamos que, se heightretorna , seu valor de retorno está correto. Porém, não provamos que ele sempre retorna um valor. Também podemos usar a indução estrutural para provar isso (ou qualquer outra propriedade). Novamente, durante a etapa 2, podemos assumir que a propriedade retém as chamadas recursivas, desde que todas as chamadas recursivas operem em um filho direto do árvore.

Uma função pode falhar ao retornar um valor em duas situações: se lança uma exceção e se faz um loop para sempre. Primeiro, vamos provar que, se nenhuma exceção for lançada, a função será encerrada:

1. Prove que (se nenhuma exceção for lançada) a função será encerrada para os casos base ( Empty). Como retornamos 0 incondicionalmente, ele termina.

2. Prove que a função termina nos casos não básicos ( Node). Há três chamadas de função aqui: +, max, e height. Sabemos disso +e maxterminamos porque fazem parte da biblioteca padrão da linguagem e são definidos dessa maneira. Como mencionado anteriormente, podemos assumir que a propriedade que estamos tentando provar é verdadeira em chamadas recursivas, desde que operem em subárvores imediatas; portanto, as chamadas heighttambém serão encerradas.

Isso conclui a prova. Observe que você não poderá provar a rescisão com um teste de unidade. Agora tudo o que resta é mostrar que heightnão gera exceções.

1. Prove que heightnão lança exceções no caso base ( Empty). Retornar 0 não pode gerar uma exceção, por isso terminamos.
2. Prove que heightnão gera exceção no caso não básico ( Node). Suponha mais uma vez que sabemos +e maxnão lançamos exceções. E a indução estrutural nos permite assumir que as chamadas recursivas também não serão lançadas (porque operam nos filhos imediatos da árvore). Mas espere! Esta função é recursiva, mas não recursiva de cauda . Nós poderíamos explodir a pilha! Nossa tentativa de prova descobriu um bug. Podemos corrigi-lo mudando heightpara ser recursivo da cauda .

Espero que isso mostre que as provas não precisam ser assustadoras ou complicadas. De fato, sempre que você escreve código, constrói informalmente uma prova em sua mente (caso contrário, não se convenceria de que acabou de implementar a função.) Ao evitar mutações nulas, desnecessárias e herança irrestrita, você pode provar que sua intuição é corrija com bastante facilidade. Essas restrições não são tão severas quanto você imagina:

• null é uma falha de linguagem e acabar com ela é incondicionalmente boa.
• Às vezes, a mutação é inevitável e necessária, mas é necessária com muito menos frequência do que você imagina - especialmente quando você tem estruturas de dados persistentes.
• Quanto a ter um número finito de classes (no sentido funcional) / subclasses (no sentido OOP) versus um número ilimitado delas, esse é um assunto grande demais para uma única resposta . Basta dizer que existe uma troca de design por aí - probabilidade de correção versus flexibilidade de extensão.

1. É muito mais fácil argumentar sobre código quando tudo é imutável . Como resultado, os loops são mais frequentemente gravados como recursão. Em geral, é mais fácil verificar a exatidão de uma solução recursiva. Freqüentemente, essa solução também será lida de maneira muito semelhante a uma definição matemática do problema.

   No entanto, há muito pouca motivação para realizar uma prova formal real de correção na maioria dos casos. As provas são difíceis, demoram muito tempo (humanas) e têm um ROI baixo.

2. Algumas linguagens funcionais (especialmente da família ML) têm sistemas de tipos extremamente expressivos que podem oferecer garantias muito mais completas que um sistema do tipo C (mas algumas idéias como genéricas também se tornaram comuns nas linguagens comuns). Quando um programa passa em uma verificação de tipo, esse é um tipo de prova automatizada. Em alguns casos, este será capaz de detectar alguns erros (por exemplo, esquecer o caso base em uma recursão, ou esquecendo-se de lidar com certos casos em um jogo padrão).

   Por outro lado, estes sistemas do tipo tem que ser mantido muito limitado, a fim de mantê-los decidable . Assim, em certo sentido, nós ganhamos garantias estáticos, dando-se flexibilidade - e estas restrições são uma razão pela qual complicado trabalhos acadêmicos ao longo das linhas de “ A solução monádico a um problema resolvido, em Haskell ” existir.

   Gosto de línguas muito liberais e muito restritas, e ambas têm suas respectivas dificuldades. Mas não é o caso de um ser "melhor", cada um é apenas mais conveniente para um tipo diferente de tarefa.

Depois, é preciso salientar que provas e testes de unidade não são intercambiáveis. Ambos nos permitem colocar limites à exatidão do programa:

• O teste coloca um limite superior na correção: se um teste falhar, o programa está incorreto, se nenhum teste falhar, estamos certos de que o programa tratará dos casos testados, mas ainda poderá haver erros não descobertos.

  int factorial(int n) {
    if (n <= 1) return 1;
    if (n == 2) return 2;
    if (n == 3) return 6;
    return -1;
  }
  
  assert(factorial(0) == 1);
  assert(factorial(1) == 1);
  assert(factorial(3) == 6);
  // oops, we forgot to test that it handles n > 3…
  

• As provas colocam um limite mais baixo na correção: pode ser impossível provar certas propriedades. Por exemplo, pode ser fácil provar que uma função sempre retorna um número (é o que os sistemas de tipos fazem). Mas pode ser impossível provar que o número sempre será < 10.

  int factorial(int n) {
    return n;  // FIXME this is just a placeholder to make it compile
  }
  
  // type system says this will be OK…
  

Uma palavra de aviso pode estar em ordem aqui:

Embora seja geralmente verdade o que os outros escrevem aqui - em resumo, que sistemas de tipo avançado, imutabilidade e transparência referencial contribuem muito para a correção - não é o caso de que o teste não seja realizado no mundo funcional. Pelo contrário !

Isso ocorre porque temos ferramentas como o Quickcheck, que geram casos de teste automática e aleatoriamente. Você apenas declara as leis que uma função deve obedecer e, em seguida, a verificação rápida verifica essas leis em centenas de casos de teste aleatórios.

Veja bem, esse é um nível um pouco mais alto do que as verificações triviais de igualdade em alguns casos de teste.

Aqui está um exemplo de uma implementação de uma árvore AVL:

--- A generator for arbitrary Trees with integer keys and string values
aTree = arbitrary :: Gen (Tree Int String)


--- After insertion, a lookup with the same key yields the inserted value        
p_insert = forAll aTree (\t -> 
             forAll arbitrary (\k ->
               forAll arbitrary (\v ->
                lookup (insert t k v) k == Just v)))

--- After deletion of a key, lookup results in Nothing
p_delete = forAll aTree (\t ->
            not (null t) ==> forAll (elements (keys t)) (\k ->
                lookup (delete t k) k == Nothing))

A segunda lei (ou propriedade) que podemos ler da seguinte maneira: Para todas as árvores arbitrárias t, o seguinte vale: se tnão estiver vazio, para todas as chaves kdessa árvore, ela manterá a procura kna árvore resultante da exclusão kde t, o resultado será Nothing(o que indica: não encontrado).

Isso verifica a funcionalidade adequada para exclusão de uma chave existente. Quais leis devem governar a exclusão de uma chave inexistente? Certamente queremos que a árvore resultante seja igual à que excluímos. Podemos expressar isso facilmente:

p_delete_nonexistant = forAll aTree (\t ->
                          forAll arbitrary (\k -> 
                              k `notElem` keys t ==> delete t k == t))

Dessa forma, testar é realmente divertido. Além disso, depois de aprender a ler as propriedades de verificação rápida, elas servem como uma especificação testável por máquina .

Não entendo exatamente o que a resposta vinculada significa "alcançar a modularidade por meio de leis matemáticas", mas acho que tenho uma idéia do que se entende.

Confira o Functor :

A classe Functor é definida assim:

 class Functor f where
   fmap :: (a -> b) -> f a -> f b

Não vem com casos de teste, mas com algumas leis que devem ser cumpridas.

Todas as instâncias do Functor devem obedecer:

 fmap id = id
 fmap (p . q) = (fmap p) . (fmap q)

Agora, digamos que você implemente Functor( fonte ):

instance  Functor Maybe  where
    fmap _ Nothing       = Nothing
    fmap f (Just a)      = Just (f a)

O problema é verificar se sua implementação atende às leis. Como você faz isso?

Uma abordagem é escrever casos de teste. A limitação fundamental dessa abordagem é que você está verificando o comportamento em um número finito de casos (boa sorte testando exaustivamente uma função com 8 parâmetros!) E, portanto, passar nos testes não pode garantir nada, exceto que os testes passam.

Outra abordagem é usar o raciocínio matemático, ou seja, uma prova, com base na definição real (em vez de no comportamento em um número limitado de casos). A idéia aqui é que uma prova matemática pode ser mais eficaz; no entanto, isso depende de quão favorável é o seu programa à prova matemática.

Não posso guiá-lo através de uma prova formal real de que a Functorinstância acima satisfaz as leis, mas tentarei fornecer um esboço de como a prova pode parecer:

1. fmap id = id
   • se tiver-mos Nothing
     • fmap id Nothing= Nothingpela parte 1 da implementação
     • id Nothing= Nothingpela definição deid
   • se tiver-mos Just x
     • fmap id (Just x)= Just (id x)= Just xpela parte 2 da implementação, depois pela definição deid
2. fmap (p . q) = (fmap p) . (fmap q)
   • se tiver-mos Nothing
     • fmap (p . q) Nothing= Nothingpela parte 1
     • (fmap p) . (fmap q) $ Nothing= (fmap p) $ Nothing= Nothingpor duas aplicações da parte 1
   • se tiver-mos Just x
     • fmap (p . q) (Just x)= Just ((p . q) x)= Just (p (q x))pela parte 2, depois pela definição de.
     • (fmap p) . (fmap q) $ (Just x)= (fmap p) $ (Just (q x))= Just (p (q x))por duas aplicações da parte dois

"Cuidado com os bugs no código acima; eu apenas provei que está correto, não tentei." - Donald Knuth

Em um mundo perfeito, os programadores são perfeitos e não cometem erros, então não há bugs.

Em um mundo perfeito, cientistas da computação e matemáticos também são perfeitos, e também não cometem erros.

Mas não vivemos em um mundo perfeito. Portanto, não podemos confiar nos programadores para cometer erros. Mas não podemos assumir que qualquer cientista da computação que forneça uma prova matemática de que um programa esteja correto não cometeu nenhum erro nessa prova. Portanto, eu não prestaria atenção a ninguém tentando provar que seu código funciona. Escreva testes de unidade e mostre-me que o código se comporta de acordo com as especificações. Qualquer outra coisa não vai me convencer de nada.