Por que os programas funcionais têm uma correlação entre o sucesso e a correção da compilação?

Eu tenho tendência para a programação funcional há 4 anos, desde que comecei a trabalhar com o LINQ. Recentemente, escrevi um código C # funcional puro e notei, em primeira mão, o que tenho lido sobre programas funcionais - que, uma vez compilados, tendem a estar corretos.

Tentei explicar por que esse é o caso, mas não consegui.

Um palpite é que, ao aplicar princípios de OO, você tem uma "camada de abstração" que não está presente em programas funcionais e essa camada de abstração possibilita que os contratos entre os objetos estejam corretos enquanto a implementação estiver incorreta.

Alguém já pensou nisso e apresentou a razão abstrata subjacente para a correlação entre o sucesso da compilação e a correção do programa na programação funcional?

Posso escrever essa resposta como alguém que prova muito as coisas, portanto, para mim, a correção não é apenas o que funciona, mas o que funciona e é fácil de provar.

Em muitos sentidos, a programação funcional é mais restritiva do que a programação imperativa. Afinal, nada impede que você nunca mude uma variável em C! De fato, a maioria dos recursos nas linguagens FP é simples de falar em termos de apenas alguns recursos principais. Tudo se resume a lambdas, aplicativo de função e correspondência de padrões!

No entanto, como pagamos antecipadamente ao flautista, temos muito menos com o que lidar e temos muito menos opções de como as coisas podem dar errado. Se você é um fã de 1984, a liberdade é realmente escravidão! Usando 101 truques diferentes para um programa, temos que raciocinar sobre as coisas como se qualquer uma dessas 101 coisas pudesse acontecer! Isso é realmente difícil de fazer, como se vê :)

Se você começar com uma tesoura de segurança em vez de uma espada, correr é moderadamente menos perigoso.

Agora, examinamos sua pergunta: como tudo isso se encaixa no "compila e funciona!" fenômenos. Acho que grande parte disso é o mesmo motivo pelo qual é fácil provar o código! Afinal, quando você escreve um software, está construindo alguma prova informal de que está correto. Por causa disso, o que é coberto pelas suas provas onduladas naturais e os próprios compiladores têm noção de correção (verificação tipográfica) é bastante.

À medida que você adiciona recursos e interações complicadas entre eles, o que não é verificado pelo sistema de tipos aumenta. No entanto, sua capacidade de construir provas informais não parece melhorar! Isso significa que há mais coisas que podem passar pela sua inspeção inicial e devem ser capturadas mais tarde.

a razão abstrata subjacente para a correlação entre o sucesso da compilação e a correção do programa na programação funcional?

Estado mutável.

Compiladores verificam as coisas estaticamente. Eles garantem que seu programa seja bem formado e o sistema de tipos fornece um mecanismo para tentar garantir que o tipo certo de valores seja permitido no tipo certo de local. O sistema de tipos também tenta garantir que o tipo certo de semântica seja permitido no tipo certo de lugares.

Assim que seu programa introduz o estado, essa última restrição se torna menos útil. Você não apenas precisa se preocupar com os valores certos nos pontos certos, mas também deve levar em consideração essa alteração de valor em pontos arbitrários do seu programa. Você precisa levar em consideração a semântica do seu código mudando ao lado desse estado.

Se você estiver executando bem a programação funcional, não há (ou muito pouco) estado mutável.

Há algum debate sobre a causa aqui - se programas sem estado funcionam após a compilação com mais freqüência porque o compilador pode pegar mais bugs ou se programas sem estado funcionam após a compilação com mais freqüência porque esse estilo de programação produz menos bugs.

Provavelmente é uma mistura de ambos na minha experiência.

Simplificando, as restrições significam que há menos maneiras corretas de organizar as coisas, e as funções de primeira classe facilitam o fatoramento de coisas como estruturas de loop. Pegue o loop desta resposta , por exemplo:

for (Iterator<String> iterator = list.iterator(); iterator.hasNext();) {
    String string = iterator.next();
    if (string.isEmpty()) {
        iterator.remove();
    }
}

Essa é a única maneira imperativa e segura em Java para remover um elemento de uma coleção enquanto você está iterando. Há muitas maneiras que parecem muito próximas, mas estão erradas. As pessoas que desconhecem esse método às vezes passam por maneiras complicadas para evitar o problema, como iterando uma cópia.

Não é terrivelmente difícil tornar esse genérico, portanto ele funcionará mais do que apenas coleções Strings, mas sem funções de primeira classe, você não pode substituir o predicado (a condição dentro do if), portanto esse código tende a ser copiado e colado e modificado ligeiramente.

Combine funções de primeira classe que lhe dão a capacidade para passar o predicado como um parâmetro, com a restrição de imutabilidade que o torna muito chato se você não faz, e você vem com blocos de construção simples, como filter, como neste código Scala isso faz a mesma coisa:

list filter (!_.isEmpty)

Agora pense no que o sistema de tipos verifica para você, no momento da compilação, no caso do Scala, mas essas verificações também são feitas por sistemas de tipos dinâmicos na primeira vez em que você o executa:

• listdeve ser algum tipo de tipo que suporte o filtermétodo, ou seja, uma coleção.
• Os elementos de listdevem ter um isEmptymétodo que retorne um booleano.
• A saída será uma coleção (potencialmente) menor com o mesmo tipo de elementos.

Uma vez que essas coisas foram verificadas, que outras maneiras restam para o programador estragar? Esqueci acidentalmente o !que causou uma falha extremamente óbvia no caso de teste. Esse é praticamente o único erro disponível para ser cometido, e eu o cometi apenas porque estava traduzindo diretamente do código que testou a condição inversa.

Esse padrão é repetido repetidamente. As funções de primeira classe permitem refatorar as coisas em pequenos utilitários reutilizáveis ​​com semântica precisa, restrições como a imutabilidade fornecem o ímpeto para fazê-lo e a verificação de tipo dos parâmetros desses utilitários deixa pouco espaço para estragar tudo.

Obviamente, tudo depende do programador saber que a função simplificadora filterjá existe e ser capaz de encontrá-la ou reconhecer o benefício de criar você mesmo. Tente implementar isso sozinho em qualquer lugar usando apenas recursão da cauda, ​​e você estará de volta no mesmo barco de complexidade que a versão imperativa, apenas pior. Só porque você pode escrevê-lo de maneira muito simples, não significa que a versão simples seja óbvia.

Eu não acho que exista uma correlação significativa entre a compilação da programação funcional e a correção do tempo de execução. Pode haver alguma correlação entre a compilação digitada estaticamente e a correção do tempo de execução, pois pelo menos você pode ter os tipos certos, se não estiver transmitindo.

O aspecto da linguagem de programação que pode, de alguma forma, correlacionar a compilação bem-sucedida com a correção do tipo de tempo de execução, como você descreve, é digitação estática e, mesmo assim, apenas se você não estiver enfraquecendo o verificador de tipos com moldes que só podem ser afirmados em tempo de execução (em ambientes com valores ou locais fortemente digitados, por exemplo, Java ou .Net) ou não (em ambientes onde as informações de tipo são perdidas ou com digitação fraca, por exemplo, C e C ++).

No entanto, a programação funcional em si pode ajudar de outras maneiras, como evitar dados compartilhados e estado mutável.

Ambos os aspectos juntos podem ter uma correlação significativa na correção, mas você deve estar ciente de que não ter erros de compilação e tempo de execução não diz nada, estritamente falando, sobre a correção em um sentido mais amplo, como no programa faz o que deve fazer e falha rapidamente sobre entrada inválida ou falha incontrolável do tempo de execução. Para isso, você precisa de regras de negócios, requisitos, casos de uso, asserções, testes de unidade, testes de integração etc. No final, pelo menos na minha opinião, eles fornecem muito mais confiança do que a programação funcional, a digitação estática ou ambas.

Explicação para gerentes:

Um programa funcional é como uma grande máquina onde tudo está conectado, tubos, cabos. [Um carro]

Um programa processual é como um prédio com salas contendo uma pequena máquina, armazenando produtos parciais em caixas, obtendo produtos parciais de outros lugares. [Uma fábrica]

Então, quando a máquina funcional já se encaixa: ela deve produzir alguma coisa. Se um complexo processual for executado, você poderá ter supervisionado efeitos específicos, introduzido o caos, sem garantir o funcionamento. Mesmo se você tiver uma lista de verificação de tudo que está sendo corretamente integrado, existem tantos estados, situações possíveis (produtos parciais por aí, baldes transbordando, falta), que as garantias são difíceis de dar.

Mas, sério, o código processual não especifica a semântica do resultado desejado, tanto quanto o código funcional. Programadores de procedimentos podem mais facilmente se livrar de códigos e dados circunstanciais e introduzir várias maneiras de fazer uma coisa (algumas delas imperfeitas). Normalmente, dados estranhos são criados. Programadores funcionais podem levar mais tempo quando o problema fica mais complexo?

Uma linguagem funcional de tipo forte ainda pode fazer melhores dados e análise de fluxo. Com uma linguagem processual, o objetivo de um programa geralmente precisa ser definido fora do programa, como uma análise formal de correção.